Theorem rpne0 13030

Description: A positive real is nonzero. (Contributed by NM, 18-Jul-2008.)

Assertion

Ref	Expression
rpne0	⊢ (𝐴 ∈ ℝ+ → 𝐴 ≠ 0)

Proof of Theorem rpne0

Step	Hyp	Ref	Expression
1		rpregt0 13028	. 2 ⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 < 𝐴))
2		gt0ne0 11716	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 𝐴 ≠ 0)
3	1, 2	syl 17	1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2098   ≠ wne 2929   class class class wbr 5149  ℝcr 11144  0cc0 11145   < clt 11285  ℝ⁺crp 13014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-resscn 11202  ax-1cn 11203  ax-addrcl 11206  ax-rnegex 11216  ax-cnre 11218  ax-pre-lttri 11219  ax-pre-lttrn 11220

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-po 5590  df-so 5591  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11287  df-mnf 11288  df-ltxr 11290  df-rp 13015

This theorem is referenced by:  rprene0  13031  rpcnne0  13032  rpne0d  13061  divge1  13082  xlemul1  13309  ltdifltdiv  13840  mulmod0  13883  negmod0  13884  moddiffl  13888  modid0  13903  modmuladd  13919  modmuladdnn0  13921  2txmodxeq0  13937  rpexpcl  14086  expnlbnd  14236  rennim  15230  sqrtdiv  15256  o1fsum  15803  divrcnv  15842  rpmsubg  21398  itg2const2  25732  reeff1o  26446  logne0  26575  advlog  26650  advlogexp  26651  logcxp  26665  cxprec  26682  cxpmul  26684  abscxp  26688  cxple2  26693  dvcxp1  26736  dvcxp2  26737  dvsqrt  26738  relogbreexp  26772  relogbzexp  26773  relogbmul  26774  relogbdiv  26776  relogbexp  26777  relogbcxp  26782  relogbcxpb  26784  relogbf  26788  logbgt0b  26790  rlimcnp  26962  efrlim  26966  efrlimOLD  26967  cxplim  26969  cxp2limlem  26973  cxploglim  26975  logdifbnd  26991  logdiflbnd  26992  logfacrlim2  27224  bposlem8  27289  vmadivsum  27480  mudivsum  27528  mulogsumlem  27529  logdivsum  27531  log2sumbnd  27542  selberg2lem  27548  selberg2  27549  pntrmax  27562  selbergr  27566  pntrlog2bndlem4  27578  pntrlog2bndlem5  27579  pntlem3  27607  padicabvcxp  27630  blocnilem  30706  nmcexi  31928  probfinmeasb  34199  probfinmeasbALTV  34200  signsplypnf  34333  logdivsqrle  34433  poimirlem29  37273  areacirclem1  37332  areacirclem4  37335  areacirc  37337  heiborlem6  37440  heiborlem7  37441  dvrelog2  41687  dvrelog3  41688  aks4d1p1p6  41696  xralrple2  44879  recnnltrp  44902  rpgtrecnn  44905  ioodvbdlimc1lem2  45463  ioodvbdlimc2lem  45465  fldivmod  47782  relogbmulbexp  47825  relogbdivb  47826  blenre  47838