Theorem rpne0 13012

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2144   ≠ wne 2959   class class class wbr 5102  ℝcr 11074  0cc0 11075   < clt 11218  ℝ⁺crp 12995

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-resscn 11132  ax-1cn 11133  ax-addrcl 11136  ax-rnegex 11146  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5544  df-po 5557  df-so 5558  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-er 8680  df-en 8930  df-dom 8931  df-sdom 8932  df-pnf 11220  df-mnf 11221  df-ltxr 11223  df-rp 12996

This theorem is referenced by:  rprene0  13013  rpcnne0  13014  rpne0d  13044  divge1  13065  xlemul1  13295  ltdifltdiv  13846  mulmod0  13889  negmod0  13890  moddiffl  13894  modid0  13909  modmuladd  13928  modmuladdnn0  13930  2txmodxeq0  13946  rpexpcl  14095  expnlbnd  14248  rennim  15268  sqrtdiv  15294  o1fsum  15843  divrcnv  15884  rpmsubg  21485  itg2const2  25805  reeff1o  26512  logne0  26646  advlog  26721  advlogexp  26722  logcxp  26736  cxprec  26753  cxpmul  26755  abscxp  26759  cxple2  26764  dvcxp1  26807  dvcxp2  26808  dvsqrt  26809  relogbreexp  26842  relogbzexp  26843  relogbmul  26844  relogbdiv  26846  relogbexp  26847  relogbcxp  26852  relogbcxpb  26854  relogbf  26858  logbgt0b  26860  rlimcnp  27032  efrlim  27036  cxplim  27038  cxp2limlem  27042  cxploglim  27044  logdifbnd  27060  logdiflbnd  27061  logfacrlim2  27292  bposlem8  27357  vmadivsum  27548  mudivsum  27596  mulogsumlem  27597  logdivsum  27599  log2sumbnd  27610  selberg2lem  27616  selberg2  27617  pntrmax  27630  selbergr  27634  pntrlog2bndlem4  27646  pntrlog2bndlem5  27647  pntlem3  27675  padicabvcxp  27698  blocnilem  31009  nmcexi  32231  probfinmeasb  34727  probfinmeasbALTV  34728  signsplypnf  34846  logdivsqrle  34946  poimirlem29  38153  areacirclem1  38212  areacirclem4  38215  areacirc  38217  heiborlem6  38320  heiborlem7  38321  dvrelog2  42686  dvrelog3  42687  aks4d1p1p6  42695  xralrple2  45935  recnnltrp  45957  rpgtrecnn  45960  ioodvbdlimc1lem2  46511  ioodvbdlimc2lem  46513  fldivmod  47943  ceildivmod  47944  relogbmulbexp  49188  relogbdivb  49189  blenre  49201