![]() |
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 11745 | . 2 ⊢ (0 < 𝐴 → 𝐴 ≠ 0) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ 𝐴 ≠ 0 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 ≠ wne 2940 class class class wbr 5147 ℝcr 11105 0cc0 11106 < clt 11244 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 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 2703 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-resscn 11163 ax-1cn 11164 ax-addrcl 11167 ax-rnegex 11177 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-po 5587 df-so 5588 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-er 8699 df-en 8936 df-dom 8937 df-sdom 8938 df-pnf 11246 df-mnf 11247 df-ltxr 11249 |
This theorem is referenced by: eqneg 11930 recgt0ii 12116 nnne0i 12248 2ne0 12312 3ne0 12314 4ne0 12316 8th4div3 12428 halfpm6th 12429 5recm6rec 12817 0.999... 15823 bpoly2 15997 bpoly3 15998 fsumcube 16000 efi4p 16076 resin4p 16077 recos4p 16078 ef01bndlem 16123 cos2bnd 16127 sincos2sgn 16133 ene0 16148 sinhalfpilem 25964 sincos6thpi 26016 sineq0 26024 coseq1 26025 efeq1 26028 cosne0 26029 efif1olem2 26043 efif1olem4 26045 eflogeq 26101 logf1o2 26149 cxpsqrt 26202 root1eq1 26252 sqrt2cxp2logb9e3 26293 ang180lem1 26303 ang180lem2 26304 ang180lem3 26305 2lgsoddprmlem1 26900 2lgsoddprmlem2 26901 chebbnd1lem3 26963 chebbnd1 26964 dp2cl 32033 dp2ltc 32040 dpfrac1 32045 dpmul4 32067 subfaclim 34167 bj-pinftynminfty 36096 taupilem1 36190 acos1half 41018 proot1ex 41928 coseq0 44566 sinaover2ne0 44570 wallispi 44772 stirlinglem3 44778 stirlinglem15 44790 dirkertrigeqlem2 44801 dirkertrigeqlem3 44802 dirkertrigeq 44803 dirkeritg 44804 dirkercncflem1 44805 fourierdlem24 44833 fourierdlem95 44903 fourierswlem 44932 |
Copyright terms: Public domain | W3C validator |