![]() |
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 10855 | . 2 ⊢ (0 < 𝐴 → 𝐴 ≠ 0) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ 𝐴 ≠ 0 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2157 ≠ wne 2971 class class class wbr 4843 ℝcr 10223 0cc0 10224 < clt 10363 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5097 ax-un 7183 ax-resscn 10281 ax-1cn 10282 ax-addrcl 10285 ax-rnegex 10295 ax-cnre 10297 ax-pre-lttri 10298 ax-pre-lttrn 10299 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ne 2972 df-nel 3075 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3387 df-sbc 3634 df-csb 3729 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-pw 4351 df-sn 4369 df-pr 4371 df-op 4375 df-uni 4629 df-br 4844 df-opab 4906 df-mpt 4923 df-id 5220 df-po 5233 df-so 5234 df-xp 5318 df-rel 5319 df-cnv 5320 df-co 5321 df-dm 5322 df-rn 5323 df-res 5324 df-ima 5325 df-iota 6064 df-fun 6103 df-fn 6104 df-f 6105 df-f1 6106 df-fo 6107 df-f1o 6108 df-fv 6109 df-er 7982 df-en 8196 df-dom 8197 df-sdom 8198 df-pnf 10365 df-mnf 10366 df-ltxr 10368 |
This theorem is referenced by: eqneg 11037 recgt0ii 11221 nnne0i 11353 2ne0 11424 3ne0 11426 4ne0 11428 8th4div3 11540 halfpm6th 11541 5recm6rec 11929 0.999... 14950 bpoly2 15124 bpoly3 15125 fsumcube 15127 efi4p 15203 resin4p 15204 recos4p 15205 ef01bndlem 15250 cos2bnd 15254 sincos2sgn 15260 ene0 15273 sinhalfpilem 24557 sincos6thpi 24609 sineq0 24615 coseq1 24616 efeq1 24617 cosne0 24618 efif1olem2 24631 efif1olem4 24633 eflogeq 24689 logf1o2 24737 ecxp 24760 cxpsqrt 24790 root1eq1 24840 sqrt2cxp2logb9e3 24881 ang180lem1 24891 ang180lem2 24892 ang180lem3 24893 2lgsoddprmlem1 25485 2lgsoddprmlem2 25486 chebbnd1lem3 25512 chebbnd1 25513 dp2cl 30104 dp2ltc 30111 dpfrac1 30116 dpmul4 30138 subfaclim 31687 bj-pinftynminfty 33613 taupilem1 33666 proot1ex 38564 coseq0 40819 sinaover2ne0 40823 wallispi 41030 stirlinglem3 41036 stirlinglem15 41048 dirkertrigeqlem2 41059 dirkertrigeqlem3 41060 dirkertrigeq 41061 dirkeritg 41062 dirkercncflem1 41063 fourierdlem24 41091 fourierdlem95 41161 fourierswlem 41190 |
Copyright terms: Public domain | W3C validator |