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 11246 | . 2 ⊢ (0 < 𝐴 → 𝐴 ≠ 0) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ 𝐴 ≠ 0 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2113 ≠ wne 2934 class class class wbr 5027 ℝcr 10607 0cc0 10608 < clt 10746 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-sep 5164 ax-nul 5171 ax-pow 5229 ax-pr 5293 ax-un 7473 ax-resscn 10665 ax-1cn 10666 ax-addrcl 10669 ax-rnegex 10679 ax-cnre 10681 ax-pre-lttri 10682 ax-pre-lttrn 10683 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3399 df-sbc 3680 df-csb 3789 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-nul 4210 df-if 4412 df-pw 4487 df-sn 4514 df-pr 4516 df-op 4520 df-uni 4794 df-br 5028 df-opab 5090 df-mpt 5108 df-id 5425 df-po 5438 df-so 5439 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6291 df-fun 6335 df-fn 6336 df-f 6337 df-f1 6338 df-fo 6339 df-f1o 6340 df-fv 6341 df-er 8313 df-en 8549 df-dom 8550 df-sdom 8551 df-pnf 10748 df-mnf 10749 df-ltxr 10751 |
This theorem is referenced by: eqneg 11431 recgt0ii 11617 nnne0i 11749 2ne0 11813 3ne0 11815 4ne0 11817 8th4div3 11929 halfpm6th 11930 5recm6rec 12316 0.999... 15322 bpoly2 15496 bpoly3 15497 fsumcube 15499 efi4p 15575 resin4p 15576 recos4p 15577 ef01bndlem 15622 cos2bnd 15626 sincos2sgn 15632 ene0 15647 sinhalfpilem 25200 sincos6thpi 25252 sineq0 25260 coseq1 25261 efeq1 25264 cosne0 25265 efif1olem2 25279 efif1olem4 25281 eflogeq 25337 logf1o2 25385 cxpsqrt 25438 root1eq1 25488 sqrt2cxp2logb9e3 25529 ang180lem1 25539 ang180lem2 25540 ang180lem3 25541 2lgsoddprmlem1 26136 2lgsoddprmlem2 26137 chebbnd1lem3 26199 chebbnd1 26200 dp2cl 30721 dp2ltc 30728 dpfrac1 30733 dpmul4 30755 subfaclim 32713 bj-pinftynminfty 35008 taupilem1 35101 acos1half 39746 proot1ex 40582 coseq0 42931 sinaover2ne0 42935 wallispi 43137 stirlinglem3 43143 stirlinglem15 43155 dirkertrigeqlem2 43166 dirkertrigeqlem3 43167 dirkertrigeq 43168 dirkeritg 43169 dirkercncflem1 43170 fourierdlem24 43198 fourierdlem95 43268 fourierswlem 43297 |
Copyright terms: Public domain | W3C validator |