Theorem rpne0 13018

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107   ≠ wne 2931   class class class wbr 5117  ℝcr 11121  0cc0 11122   < clt 11262  ℝ⁺crp 13001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5264  ax-nul 5274  ax-pow 5333  ax-pr 5400  ax-un 7724  ax-resscn 11179  ax-1cn 11180  ax-addrcl 11183  ax-rnegex 11193  ax-cnre 11195  ax-pre-lttri 11196  ax-pre-lttrn 11197

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4882  df-br 5118  df-opab 5180  df-mpt 5200  df-id 5546  df-po 5559  df-so 5560  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-er 8714  df-en 8955  df-dom 8956  df-sdom 8957  df-pnf 11264  df-mnf 11265  df-ltxr 11267  df-rp 13002

This theorem is referenced by:  rprene0  13019  rpcnne0  13020  rpne0d  13049  divge1  13070  xlemul1  13299  ltdifltdiv  13841  mulmod0  13884  negmod0  13885  moddiffl  13889  modid0  13904  modmuladd  13921  modmuladdnn0  13923  2txmodxeq0  13939  rpexpcl  14088  expnlbnd  14241  rennim  15247  sqrtdiv  15273  o1fsum  15818  divrcnv  15857  rpmsubg  21386  itg2const2  25681  reeff1o  26396  logne0  26526  advlog  26601  advlogexp  26602  logcxp  26616  cxprec  26633  cxpmul  26635  abscxp  26639  cxple2  26644  dvcxp1  26687  dvcxp2  26688  dvsqrt  26689  relogbreexp  26723  relogbzexp  26724  relogbmul  26725  relogbdiv  26727  relogbexp  26728  relogbcxp  26733  relogbcxpb  26735  relogbf  26739  logbgt0b  26741  rlimcnp  26913  efrlim  26917  efrlimOLD  26918  cxplim  26920  cxp2limlem  26924  cxploglim  26926  logdifbnd  26942  logdiflbnd  26943  logfacrlim2  27175  bposlem8  27240  vmadivsum  27431  mudivsum  27479  mulogsumlem  27480  logdivsum  27482  log2sumbnd  27493  selberg2lem  27499  selberg2  27500  pntrmax  27513  selbergr  27517  pntrlog2bndlem4  27529  pntrlog2bndlem5  27530  pntlem3  27558  padicabvcxp  27581  blocnilem  30719  nmcexi  31941  probfinmeasb  34389  probfinmeasbALTV  34390  signsplypnf  34511  logdivsqrle  34611  poimirlem29  37602  areacirclem1  37661  areacirclem4  37664  areacirc  37666  heiborlem6  37769  heiborlem7  37770  dvrelog2  42006  dvrelog3  42007  aks4d1p1p6  42015  xralrple2  45315  recnnltrp  45338  rpgtrecnn  45341  ioodvbdlimc1lem2  45897  ioodvbdlimc2lem  45899  fldivmod  47293  ceildivmod  47294  relogbmulbexp  48435  relogbdivb  48436  blenre  48448