Theorem rpne0 12954

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2121   ≠ wne 2936   class class class wbr 5075  ℝcr 11032  0cc0 11033   < clt 11174  ℝ⁺crp 12937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-resscn 11090  ax-1cn 11091  ax-addrcl 11094  ax-rnegex 11104  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11176  df-mnf 11177  df-ltxr 11179  df-rp 12938

This theorem is referenced by:  rprene0  12955  rpcnne0  12956  rpne0d  12986  divge1  13007  xlemul1  13237  ltdifltdiv  13788  mulmod0  13831  negmod0  13832  moddiffl  13836  modid0  13851  modmuladd  13870  modmuladdnn0  13872  2txmodxeq0  13888  rpexpcl  14037  expnlbnd  14190  rennim  15196  sqrtdiv  15222  o1fsum  15771  divrcnv  15812  rpmsubg  21410  itg2const2  25730  reeff1o  26434  logne0  26565  advlog  26640  advlogexp  26641  logcxp  26655  cxprec  26672  cxpmul  26674  abscxp  26678  cxple2  26683  dvcxp1  26726  dvcxp2  26727  dvsqrt  26728  relogbreexp  26761  relogbzexp  26762  relogbmul  26763  relogbdiv  26765  relogbexp  26766  relogbcxp  26771  relogbcxpb  26773  relogbf  26777  logbgt0b  26779  rlimcnp  26951  efrlim  26955  cxplim  26957  cxp2limlem  26961  cxploglim  26963  logdifbnd  26979  logdiflbnd  26980  logfacrlim2  27211  bposlem8  27276  vmadivsum  27467  mudivsum  27515  mulogsumlem  27516  logdivsum  27518  log2sumbnd  27529  selberg2lem  27535  selberg2  27536  pntrmax  27549  selbergr  27553  pntrlog2bndlem4  27565  pntrlog2bndlem5  27566  pntlem3  27594  padicabvcxp  27617  blocnilem  30897  nmcexi  32119  probfinmeasb  34624  probfinmeasbALTV  34625  signsplypnf  34746  logdivsqrle  34846  poimirlem29  38031  areacirclem1  38090  areacirclem4  38093  areacirc  38095  heiborlem6  38198  heiborlem7  38199  dvrelog2  42564  dvrelog3  42565  aks4d1p1p6  42573  xralrple2  45813  recnnltrp  45835  rpgtrecnn  45838  ioodvbdlimc1lem2  46389  ioodvbdlimc2lem  46391  fldivmod  47821  ceildivmod  47822  relogbmulbexp  49066  relogbdivb  49067  blenre  49079