Theorem rpne0 12936

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ≠ wne 2933   class class class wbr 5100  ℝcr 11039  0cc0 11040   < clt 11180  ℝ⁺crp 12919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-resscn 11097  ax-1cn 11098  ax-addrcl 11101  ax-rnegex 11111  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-po 5542  df-so 5543  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-er 8647  df-en 8898  df-dom 8899  df-sdom 8900  df-pnf 11182  df-mnf 11183  df-ltxr 11185  df-rp 12920

This theorem is referenced by:  rprene0  12937  rpcnne0  12938  rpne0d  12968  divge1  12989  xlemul1  13219  ltdifltdiv  13768  mulmod0  13811  negmod0  13812  moddiffl  13816  modid0  13831  modmuladd  13850  modmuladdnn0  13852  2txmodxeq0  13868  rpexpcl  14017  expnlbnd  14170  rennim  15176  sqrtdiv  15202  o1fsum  15750  divrcnv  15789  rpmsubg  21403  itg2const2  25715  reeff1o  26430  logne0  26561  advlog  26636  advlogexp  26637  logcxp  26651  cxprec  26668  cxpmul  26670  abscxp  26674  cxple2  26679  dvcxp1  26722  dvcxp2  26723  dvsqrt  26724  relogbreexp  26758  relogbzexp  26759  relogbmul  26760  relogbdiv  26762  relogbexp  26763  relogbcxp  26768  relogbcxpb  26770  relogbf  26774  logbgt0b  26776  rlimcnp  26948  efrlim  26952  efrlimOLD  26953  cxplim  26955  cxp2limlem  26959  cxploglim  26961  logdifbnd  26977  logdiflbnd  26978  logfacrlim2  27210  bposlem8  27275  vmadivsum  27466  mudivsum  27514  mulogsumlem  27515  logdivsum  27517  log2sumbnd  27528  selberg2lem  27534  selberg2  27535  pntrmax  27548  selbergr  27552  pntrlog2bndlem4  27564  pntrlog2bndlem5  27565  pntlem3  27593  padicabvcxp  27616  blocnilem  30898  nmcexi  32120  probfinmeasb  34612  probfinmeasbALTV  34613  signsplypnf  34734  logdivsqrle  34834  poimirlem29  37929  areacirclem1  37988  areacirclem4  37991  areacirc  37993  heiborlem6  38096  heiborlem7  38097  dvrelog2  42463  dvrelog3  42464  aks4d1p1p6  42472  xralrple2  45742  recnnltrp  45764  rpgtrecnn  45767  ioodvbdlimc1lem2  46319  ioodvbdlimc2lem  46321  fldivmod  47727  ceildivmod  47728  relogbmulbexp  48950  relogbdivb  48951  blenre  48963