Theorem gt0ne0ii 11664

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 11663	. 2 ⊢ (0 < 𝐴 → 𝐴 ≠ 0)
4	1, 3	ax-mp 5	1 ⊢ 𝐴 ≠ 0

Syntax hints:   ∈ wcel 2113   ≠ wne 2929   class class class wbr 5095  ℝcr 11016  0cc0 11017   < clt 11157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-resscn 11074  ax-1cn 11075  ax-addrcl 11078  ax-rnegex 11088  ax-cnre 11090  ax-pre-lttri 11091  ax-pre-lttrn 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-er 8631  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11159  df-mnf 11160  df-ltxr 11162

This theorem is referenced by:  eqneg  11852  recgt0ii  12039  nnne0i  12176  8th4div3  12352  halfpm6th  12354  5recm6rec  12741  0.999...  15795  bpoly2  15971  bpoly3  15972  fsumcube  15974  efi4p  16053  resin4p  16054  recos4p  16055  ef01bndlem  16100  cos2bnd  16104  sincos2sgn  16110  ene0  16125  pine0  26416  sinhalfpilem  26419  tan4thpi  26470  sincos6thpi  26472  sineq0  26480  coseq1  26481  efeq1  26484  cosne0  26485  efif1olem2  26499  efif1olem4  26501  eflogeq  26558  logf1o2  26606  cxpsqrt  26659  root1eq1  26712  sqrt2cxp2logb9e3  26756  ang180lem1  26766  ang180lem2  26767  ang180lem3  26768  2lgsoddprmlem1  27366  2lgsoddprmlem2  27367  chebbnd1lem3  27429  chebbnd1  27430  dp2cl  32889  dp2ltc  32896  dpfrac1  32901  dpmul4  32923  subfaclim  35304  bj-pinftynminfty  37344  taupilem1  37438  acos1half  42528  proot1ex  43353  coseq0  46024  sinaover2ne0  46028  wallispi  46230  stirlinglem3  46236  stirlinglem15  46248  dirkertrigeqlem2  46259  dirkertrigeqlem3  46260  dirkertrigeq  46261  dirkeritg  46262  dirkercncflem1  46263  fourierdlem24  46291  fourierdlem95  46361  fourierswlem  46390