Theorem rpne0 12743

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2110   ≠ wne 2945   class class class wbr 5079  ℝcr 10869  0cc0 10870   < clt 11008  ℝ⁺crp 12727

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7580  ax-resscn 10927  ax-1cn 10928  ax-addrcl 10931  ax-rnegex 10941  ax-cnre 10943  ax-pre-lttri 10944  ax-pre-lttrn 10945

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5489  df-po 5503  df-so 5504  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6389  df-fun 6433  df-fn 6434  df-f 6435  df-f1 6436  df-fo 6437  df-f1o 6438  df-fv 6439  df-er 8479  df-en 8715  df-dom 8716  df-sdom 8717  df-pnf 11010  df-mnf 11011  df-ltxr 11013  df-rp 12728

This theorem is referenced by:  rprene0  12744  rpcnne0  12745  rpne0d  12774  divge1  12795  xlemul1  13021  ltdifltdiv  13550  mulmod0  13593  negmod0  13594  moddiffl  13598  modid0  13613  modmuladd  13629  modmuladdnn0  13631  2txmodxeq0  13647  rpexpcl  13797  expnlbnd  13944  rennim  14946  sqrtdiv  14973  o1fsum  15521  divrcnv  15560  rpmsubg  20658  itg2const2  24902  reeff1o  25602  logne0  25731  advlog  25805  advlogexp  25806  logcxp  25820  cxprec  25837  cxpmul  25839  abscxp  25843  cxple2  25848  dvcxp1  25889  dvcxp2  25890  dvsqrt  25891  relogbreexp  25921  relogbzexp  25922  relogbmul  25923  relogbdiv  25925  relogbexp  25926  relogbcxp  25931  relogbcxpb  25933  relogbf  25937  logbgt0b  25939  rlimcnp  26111  efrlim  26115  cxplim  26117  cxp2limlem  26121  cxploglim  26123  logdifbnd  26139  logdiflbnd  26140  logfacrlim2  26370  bposlem8  26435  vmadivsum  26626  mudivsum  26674  mulogsumlem  26675  logdivsum  26677  log2sumbnd  26688  selberg2lem  26694  selberg2  26695  pntrmax  26708  selbergr  26712  pntrlog2bndlem4  26724  pntrlog2bndlem5  26725  pntlem3  26753  padicabvcxp  26776  blocnilem  29160  nmcexi  30382  probfinmeasb  32389  probfinmeasbALTV  32390  signsplypnf  32523  logdivsqrle  32624  poimirlem29  35800  areacirclem1  35859  areacirclem4  35862  areacirc  35864  heiborlem6  35968  heiborlem7  35969  dvrelog2  40067  dvrelog3  40068  aks4d1p1p6  40076  xralrple2  42862  recnnltrp  42885  rpgtrecnn  42888  ioodvbdlimc1lem2  43442  ioodvbdlimc2lem  43444  fldivmod  45831  relogbmulbexp  45874  relogbdivb  45875  blenre  45887