Theorem gt0ne0ii 11845

Description: Positive implies nonzero. (Contributed by NM, 15-May-1999.)

Hypotheses

Ref	Expression
lt2.1	⊢ 𝐴 ∈ ℝ
gt0ne0i.2	⊢ 0 < 𝐴

Assertion

Ref	Expression
gt0ne0ii	⊢ 𝐴 ≠ 0

Proof of Theorem gt0ne0ii

Step	Hyp	Ref	Expression
1		gt0ne0i.2	. 2 ⊢ 0 < 𝐴
2		lt2.1	. . 3 ⊢ 𝐴 ∈ ℝ
3	2	gt0ne0i 11844	. 2 ⊢ (0 < 𝐴 → 𝐴 ≠ 0)
4	1, 3	ax-mp 5	1 ⊢ 𝐴 ≠ 0

This proof depends on syntax axioms:   ∈ wcel 2145   ≠ wne 2956   class class class wbr 5103  ℝcr 11192  0cc0 11193   < clt 11336

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-resscn 11250  ax-1cn 11251  ax-addrcl 11254  ax-rnegex 11264  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-ltxr 11341

This theorem is used by:  eqneg  12030  recgt0ii  12216  nnne0i  12371  8th4div3  12559  halfpm6th  12561  5recm6rec  12957  0.999...  16043  bpoly2  16216  bpoly3  16217  fsumcube  16219  efi4p  16298  resin4p  16299  recos4p  16300  ef01bndlem  16345  cos2bnd  16349  sincos2sgn  16355  ene0  16370  pine0  26782  sinhalfpilem  26785  tan4thpi  26836  sincos6thpi  26837  sineq0  26845  coseq1  26846  efeq1  26849  cosne0  26850  efif1olem2  26864  efif1olem4  26866  eflogeq  26923  logf1o2  26971  cxpsqrt  27024  root1eq1  27076  sqrt2cxp2logb9e3  27120  ang180lem1  27130  ang180lem2  27131  ang180lem3  27132  2lgsoddprmlem1  27728  2lgsoddprmlem2  27729  chebbnd1lem3  27791  chebbnd1  27792  dp2cl  33439  dp2ltc  33446  dpfrac1  33451  dpmul4  33473  subfaclim  35932  bj-pinftynminfty  38128  taupilem1  38222  acos1half  43389  proot1ex  44182  coseq0  46843  sinaover2ne0  46847  wallispi  47049  stirlinglem3  47055  stirlinglem15  47067  dirkertrigeqlem2  47078  dirkertrigeqlem3  47079  dirkertrigeq  47080  dirkeritg  47081  dirkercncflem1  47082  fourierdlem24  47110  fourierdlem95  47180  fourierswlem  47209  goldrarr  47897  goldrasin  47898  goldrapos  47899  goldracos5teq  47901  goldratmolem4  47904