![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 2ap0 | GIF version |
Description: The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.) |
Ref | Expression |
---|---|
2ap0 | ⊢ 2 # 0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2re 8700 | . 2 ⊢ 2 ∈ ℝ | |
2 | 2pos 8721 | . 2 ⊢ 0 < 2 | |
3 | 1, 2 | gt0ap0ii 8308 | 1 ⊢ 2 # 0 |
Colors of variables: wff set class |
Syntax hints: class class class wbr 3895 0cc0 7547 # cap 8261 2c2 8681 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 586 ax-in2 587 ax-io 681 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-10 1466 ax-11 1467 ax-i12 1468 ax-bndl 1469 ax-4 1470 ax-13 1474 ax-14 1475 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 ax-sep 4006 ax-pow 4058 ax-pr 4091 ax-un 4315 ax-setind 4412 ax-cnex 7636 ax-resscn 7637 ax-1cn 7638 ax-1re 7639 ax-icn 7640 ax-addcl 7641 ax-addrcl 7642 ax-mulcl 7643 ax-mulrcl 7644 ax-addcom 7645 ax-mulcom 7646 ax-addass 7647 ax-mulass 7648 ax-distr 7649 ax-i2m1 7650 ax-0lt1 7651 ax-1rid 7652 ax-0id 7653 ax-rnegex 7654 ax-precex 7655 ax-cnre 7656 ax-pre-ltirr 7657 ax-pre-lttrn 7659 ax-pre-apti 7660 ax-pre-ltadd 7661 ax-pre-mulgt0 7662 |
This theorem depends on definitions: df-bi 116 df-3an 947 df-tru 1317 df-fal 1320 df-nf 1420 df-sb 1719 df-eu 1978 df-mo 1979 df-clab 2102 df-cleq 2108 df-clel 2111 df-nfc 2244 df-ne 2283 df-nel 2378 df-ral 2395 df-rex 2396 df-reu 2397 df-rab 2399 df-v 2659 df-sbc 2879 df-dif 3039 df-un 3041 df-in 3043 df-ss 3050 df-pw 3478 df-sn 3499 df-pr 3500 df-op 3502 df-uni 3703 df-br 3896 df-opab 3950 df-id 4175 df-xp 4505 df-rel 4506 df-cnv 4507 df-co 4508 df-dm 4509 df-iota 5046 df-fun 5083 df-fv 5089 df-riota 5684 df-ov 5731 df-oprab 5732 df-mpo 5733 df-pnf 7726 df-mnf 7727 df-ltxr 7729 df-sub 7858 df-neg 7859 df-reap 8255 df-ap 8262 df-2 8689 |
This theorem is referenced by: 2div2e1 8756 4d2e2 8784 halfre 8837 1mhlfehlf 8842 halfpm6th 8844 2muliap0 8848 halfcl 8850 rehalfcl 8851 half0 8852 2halves 8853 halfaddsub 8858 xp1d2m1eqxm1d2 8876 div4p1lem1div2 8877 zneo 9056 nneoor 9057 nneo 9058 zeo 9060 zeo2 9061 qbtwnrelemcalc 9926 2tnp1ge0ge0 9967 zesq 10303 sqoddm1div8 10337 faclbnd2 10381 crre 10522 addcj 10556 resqrexlemover 10674 resqrexlemcalc1 10678 resqrexlemcvg 10683 maxabslemab 10870 max0addsup 10883 minabs 10899 bdtri 10903 arisum 11159 arisum2 11160 geo2sum 11175 geo2lim 11177 geoihalfsum 11183 ege2le3 11228 efgt0 11241 tanval2ap 11271 tanval3ap 11272 efi4p 11275 efival 11290 cosadd 11295 sinmul 11302 cosmul 11303 sin01bnd 11315 cos01bnd 11316 sin02gt0 11321 odd2np1 11418 mulsucdiv2z 11430 ltoddhalfle 11438 halfleoddlt 11439 nn0enne 11447 nn0o 11452 flodddiv4 11479 flodddiv4t2lthalf 11482 6lcm4e12 11614 sqrt2irrlem 11685 sqrt2irr 11686 oddennn 11750 evenennn 11751 |
Copyright terms: Public domain | W3C validator |