Theorem rpne0 12907

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 12905	. 2 ⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 < 𝐴))
2		gt0ne0 11582	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 𝐴 ≠ 0)
3	1, 2	syl 17	1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111   ≠ wne 2928   class class class wbr 5089  ℝcr 11005  0cc0 11006   < clt 11146  ℝ⁺crp 12890

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-resscn 11063  ax-1cn 11064  ax-addrcl 11067  ax-rnegex 11077  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-po 5522  df-so 5523  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-ltxr 11151  df-rp 12891

This theorem is referenced by:  rprene0  12908  rpcnne0  12909  rpne0d  12939  divge1  12960  xlemul1  13189  ltdifltdiv  13738  mulmod0  13781  negmod0  13782  moddiffl  13786  modid0  13801  modmuladd  13820  modmuladdnn0  13822  2txmodxeq0  13838  rpexpcl  13987  expnlbnd  14140  rennim  15146  sqrtdiv  15172  o1fsum  15720  divrcnv  15759  rpmsubg  21368  itg2const2  25669  reeff1o  26384  logne0  26515  advlog  26590  advlogexp  26591  logcxp  26605  cxprec  26622  cxpmul  26624  abscxp  26628  cxple2  26633  dvcxp1  26676  dvcxp2  26677  dvsqrt  26678  relogbreexp  26712  relogbzexp  26713  relogbmul  26714  relogbdiv  26716  relogbexp  26717  relogbcxp  26722  relogbcxpb  26724  relogbf  26728  logbgt0b  26730  rlimcnp  26902  efrlim  26906  efrlimOLD  26907  cxplim  26909  cxp2limlem  26913  cxploglim  26915  logdifbnd  26931  logdiflbnd  26932  logfacrlim2  27164  bposlem8  27229  vmadivsum  27420  mudivsum  27468  mulogsumlem  27469  logdivsum  27471  log2sumbnd  27482  selberg2lem  27488  selberg2  27489  pntrmax  27502  selbergr  27506  pntrlog2bndlem4  27518  pntrlog2bndlem5  27519  pntlem3  27547  padicabvcxp  27570  blocnilem  30784  nmcexi  32006  probfinmeasb  34441  probfinmeasbALTV  34442  signsplypnf  34563  logdivsqrle  34663  poimirlem29  37688  areacirclem1  37747  areacirclem4  37750  areacirc  37752  heiborlem6  37855  heiborlem7  37856  dvrelog2  42156  dvrelog3  42157  aks4d1p1p6  42165  xralrple2  45452  recnnltrp  45474  rpgtrecnn  45477  ioodvbdlimc1lem2  46029  ioodvbdlimc2lem  46031  fldivmod  47437  ceildivmod  47438  relogbmulbexp  48661  relogbdivb  48662  blenre  48674