![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > gt0ne0 | Structured version Unicode version |
Description: Positive implies nonzero. (Contributed by NM, 3-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
gt0ne0 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0red 9493 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ltne 9577 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylan 471 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1954 ax-ext 2431 ax-sep 4516 ax-nul 4524 ax-pow 4573 ax-pr 4634 ax-un 6477 ax-resscn 9445 ax-1cn 9446 ax-icn 9447 ax-addcl 9448 ax-addrcl 9449 ax-mulcl 9450 ax-mulrcl 9451 ax-i2m1 9456 ax-1ne0 9457 ax-rnegex 9459 ax-rrecex 9460 ax-cnre 9461 ax-pre-lttri 9462 ax-pre-lttrn 9463 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2265 df-mo 2266 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2602 df-ne 2647 df-nel 2648 df-ral 2801 df-rex 2802 df-rab 2805 df-v 3074 df-sbc 3289 df-csb 3391 df-dif 3434 df-un 3436 df-in 3438 df-ss 3445 df-nul 3741 df-if 3895 df-pw 3965 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4195 df-br 4396 df-opab 4454 df-mpt 4455 df-id 4739 df-po 4744 df-so 4745 df-xp 4949 df-rel 4950 df-cnv 4951 df-co 4952 df-dm 4953 df-rn 4954 df-res 4955 df-ima 4956 df-iota 5484 df-fun 5523 df-fn 5524 df-f 5525 df-f1 5526 df-fo 5527 df-f1o 5528 df-fv 5529 df-ov 6198 df-er 7206 df-en 7416 df-dom 7417 df-sdom 7418 df-pnf 9526 df-mnf 9527 df-ltxr 9529 |
This theorem is referenced by: recgt0 10279 lemul1 10287 lediv1 10300 gt0div 10301 ge0div 10302 mulge0b 10305 ltdivmul 10310 ledivmul 10311 ledivmulOLD 10312 lt2mul2div 10314 lemuldiv 10317 ltdiv2 10323 ltrec1 10325 lerec2 10326 ledivdiv 10327 lediv2 10328 ltdiv23 10329 lediv23 10330 lediv12a 10331 recreclt 10337 nnrecl 10683 elnnz 10762 recnz 10823 rpne0 11112 divelunit 11539 resqrex 12853 sqrgt0 12861 argregt0 22187 argimgt0 22189 logneg2 22192 logcnlem3 22217 atanlogsublem 22438 leopmul 25685 cdj1i 25984 lediv2aALT 27461 nndivlub 28443 sineq0ALT 31986 |
Copyright terms: Public domain | W3C validator |