Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > gt0ne0ii | Structured version Visualization version GIF version |
Description: Positive implies nonzero. (Contributed by NM, 15-May-1999.) |
Ref | Expression |
---|---|
lt2.1 | ⊢ 𝐴 ∈ ℝ |
gt0ne0i.2 | ⊢ 0 < 𝐴 |
Ref | Expression |
---|---|
gt0ne0ii | ⊢ 𝐴 ≠ 0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gt0ne0i.2 | . 2 ⊢ 0 < 𝐴 | |
2 | lt2.1 | . . 3 ⊢ 𝐴 ∈ ℝ | |
3 | 2 | gt0ne0i 11510 | . 2 ⊢ (0 < 𝐴 → 𝐴 ≠ 0) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ 𝐴 ≠ 0 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 ≠ wne 2943 class class class wbr 5074 ℝcr 10870 0cc0 10871 < clt 11009 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-resscn 10928 ax-1cn 10929 ax-addrcl 10932 ax-rnegex 10942 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-mpt 5158 df-id 5489 df-po 5503 df-so 5504 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-er 8498 df-en 8734 df-dom 8735 df-sdom 8736 df-pnf 11011 df-mnf 11012 df-ltxr 11014 |
This theorem is referenced by: eqneg 11695 recgt0ii 11881 nnne0i 12013 2ne0 12077 3ne0 12079 4ne0 12081 8th4div3 12193 halfpm6th 12194 5recm6rec 12581 0.999... 15593 bpoly2 15767 bpoly3 15768 fsumcube 15770 efi4p 15846 resin4p 15847 recos4p 15848 ef01bndlem 15893 cos2bnd 15897 sincos2sgn 15903 ene0 15918 sinhalfpilem 25620 sincos6thpi 25672 sineq0 25680 coseq1 25681 efeq1 25684 cosne0 25685 efif1olem2 25699 efif1olem4 25701 eflogeq 25757 logf1o2 25805 cxpsqrt 25858 root1eq1 25908 sqrt2cxp2logb9e3 25949 ang180lem1 25959 ang180lem2 25960 ang180lem3 25961 2lgsoddprmlem1 26556 2lgsoddprmlem2 26557 chebbnd1lem3 26619 chebbnd1 26620 dp2cl 31154 dp2ltc 31161 dpfrac1 31166 dpmul4 31188 subfaclim 33150 bj-pinftynminfty 35398 taupilem1 35492 acos1half 40170 proot1ex 41026 coseq0 43405 sinaover2ne0 43409 wallispi 43611 stirlinglem3 43617 stirlinglem15 43629 dirkertrigeqlem2 43640 dirkertrigeqlem3 43641 dirkertrigeq 43642 dirkeritg 43643 dirkercncflem1 43644 fourierdlem24 43672 fourierdlem95 43742 fourierswlem 43771 |
Copyright terms: Public domain | W3C validator |