Theorem rpne0 13039

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∈ wcel 2142   ≠ wne 2957   class class class wbr 5108  ℝcr 11105  0cc0 11106   < clt 11249  ℝ⁺crp 13022

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734  ax-resscn 11163  ax-1cn 11164  ax-addrcl 11167  ax-rnegex 11177  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5555  df-po 5568  df-so 5569  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-er 8692  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11251  df-mnf 11252  df-ltxr 11254  df-rp 13023

This theorem is used by:  rprene0  13040  rpcnne0  13041  rpne0d  13071  divge1  13092  xlemul1  13322  ltdifltdiv  13874  mulmod0  13917  negmod0  13918  moddiffl  13922  modid0  13937  modmuladd  13956  modmuladdnn0  13958  2txmodxeq0  13974  rpexpcl  14123  expnlbnd  14276  rennim  15297  sqrtdiv  15323  o1fsum  15872  divrcnv  15913  rpmsubg  21592  itg2const2  25911  reeff1o  26621  logne0  26755  advlog  26830  advlogexp  26831  logcxp  26845  cxprec  26862  cxpmul  26864  abscxp  26868  cxple2  26873  dvcxp1  26916  dvcxp2  26917  dvsqrt  26918  relogbreexp  26951  relogbzexp  26952  relogbmul  26953  relogbdiv  26955  relogbexp  26956  relogbcxp  26961  relogbcxpb  26963  relogbf  26967  logbgt0b  26969  rlimcnp  27141  efrlim  27145  cxplim  27147  cxp2limlem  27151  cxploglim  27153  logdifbnd  27169  logdiflbnd  27170  logfacrlim2  27401  bposlem8  27466  vmadivsum  27657  mudivsum  27705  mulogsumlem  27706  logdivsum  27708  log2sumbnd  27719  selberg2lem  27725  selberg2  27726  pntrmax  27739  selbergr  27743  pntrlog2bndlem4  27755  pntrlog2bndlem5  27756  pntlem3  27784  padicabvcxp  27807  blocnilem  31167  nmcexi  32389  probfinmeasb  34827  probfinmeasbALTV  34828  signsplypnf  34946  logdivsqrle  35046  poimirlem29  38328  areacirclem1  38387  areacirclem4  38390  areacirc  38392  heiborlem6  38495  heiborlem7  38496  dvrelog2  42859  dvrelog3  42860  aks4d1p1p6  42868  xralrple2  46098  recnnltrp  46120  rpgtrecnn  46123  ioodvbdlimc1lem2  46674  ioodvbdlimc2lem  46676  fldivmod  48109  ceildivmod  48110  relogbmulbexp  49369  relogbdivb  49370  blenre  49382