![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 2ap0 | Unicode version |
Description: The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.) |
Ref | Expression |
---|---|
2ap0 |
![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2re 8228 |
. 2
![]() ![]() ![]() ![]() | |
2 | 2pos 8249 |
. 2
![]() ![]() ![]() ![]() | |
3 | 1, 2 | gt0ap0ii 7846 |
1
![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: class class
class wbr 3805 ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-13 1445 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-sep 3916 ax-pow 3968 ax-pr 3992 ax-un 4216 ax-setind 4308 ax-cnex 7181 ax-resscn 7182 ax-1cn 7183 ax-1re 7184 ax-icn 7185 ax-addcl 7186 ax-addrcl 7187 ax-mulcl 7188 ax-mulrcl 7189 ax-addcom 7190 ax-mulcom 7191 ax-addass 7192 ax-mulass 7193 ax-distr 7194 ax-i2m1 7195 ax-0lt1 7196 ax-1rid 7197 ax-0id 7198 ax-rnegex 7199 ax-precex 7200 ax-cnre 7201 ax-pre-ltirr 7202 ax-pre-lttrn 7204 ax-pre-apti 7205 ax-pre-ltadd 7206 ax-pre-mulgt0 7207 |
This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-fal 1291 df-nf 1391 df-sb 1688 df-eu 1946 df-mo 1947 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ne 2250 df-nel 2345 df-ral 2358 df-rex 2359 df-reu 2360 df-rab 2362 df-v 2612 df-sbc 2825 df-dif 2984 df-un 2986 df-in 2988 df-ss 2995 df-pw 3402 df-sn 3422 df-pr 3423 df-op 3425 df-uni 3622 df-br 3806 df-opab 3860 df-id 4076 df-xp 4397 df-rel 4398 df-cnv 4399 df-co 4400 df-dm 4401 df-iota 4917 df-fun 4954 df-fv 4960 df-riota 5519 df-ov 5566 df-oprab 5567 df-mpt2 5568 df-pnf 7269 df-mnf 7270 df-ltxr 7272 df-sub 7400 df-neg 7401 df-reap 7794 df-ap 7801 df-2 8217 |
This theorem is referenced by: 2div2e1 8283 4d2e2 8311 halfre 8363 1mhlfehlf 8368 halfpm6th 8370 2muliap0 8374 halfcl 8376 rehalfcl 8377 half0 8378 2halves 8379 halfaddsub 8384 xp1d2m1eqxm1d2 8402 div4p1lem1div2 8403 zneo 8581 nneoor 8582 nneo 8583 zeo 8585 zeo2 8586 qbtwnrelemcalc 9394 2tnp1ge0ge0 9435 zesq 9740 sqoddm1div8 9774 faclbnd2 9818 crre 9945 addcj 9979 resqrexlemover 10097 resqrexlemcalc1 10101 resqrexlemcvg 10106 maxabslemab 10293 max0addsup 10306 odd2np1 10480 mulsucdiv2z 10492 ltoddhalfle 10500 halfleoddlt 10501 nn0enne 10509 nn0o 10514 flodddiv4 10541 flodddiv4t2lthalf 10544 6lcm4e12 10676 sqrt2irrlem 10747 sqrt2irr 10748 oddennn 10812 evenennn 10813 |
Copyright terms: Public domain | W3C validator |