HomeRelated theorems
Unicode version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: The empty set is not a positive fraction. |
| Ref | Expression |
|---|---|
| 0npq |
     |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | enqer 3840 |
. . 3
  | |
| 2 | dmenq 3839 |
. . 3
      | |
| 3 | 1, 2 | 0nelqs 3234 |
. 2
 |
| 4 | df-nq 3832 |
. . 3
| |
| 5 | 4 | eleq2i 1153 |
. 2
 |
| 6 | 3, 5 | mtbir 167 |
1
|
| Colors of variables: wff set class |
| Syntax hints: wn 1
wcel 1092
c0 1707
cxp 2408
cqs 3199
cnpi 3766
ceq 3772
cnq 3773 |
| This theorem is referenced by: dmaddpq 3853 dmmulpq 3855 addasspq 3857 mulasspq 3859 distrpq 3861 recmulpq 3864 recclpq 3866 ltapq 3870 ltmpq 3871 ltexpq 3874 ltexpq2 3875 nsmallpq 3877 ltbtwnpq 3878 ltaddpr 3934 ltexprlem2 3937 ltexprlem3 3938 ltexprlem4 3939 ltexprlem6 3941 ltexprlem7 3942 reclem1pr 3950 reclem2pr 3951 |
| This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 |
| This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-fv 2438 df-rdg 2970 df-opr 3003 df-oprab 3004 df-oadd 3106 df-omul 3107 df-er 3200 df-ec 3202 df-qs 3205 df-ni 3794 df-mi 3796 df-enq 3831 df-nq 3832 |