Theorem rpne0 12155

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

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2107   ≠ wne 2969   class class class wbr 4886  ℝcr 10271  0cc0 10272   < clt 10411  ℝ⁺crp 12137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-resscn 10329  ax-1cn 10330  ax-addrcl 10333  ax-rnegex 10343  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-po 5274  df-so 5275  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-pnf 10413  df-mnf 10414  df-ltxr 10416  df-rp 12138

This theorem is referenced by:  rprene0  12156  rpcnne0  12157  rpne0d  12186  divge1  12207  xlemul1  12432  ltdifltdiv  12954  mulmod0  12995  negmod0  12996  moddiffl  13000  modid0  13015  modmuladd  13031  modmuladdnn0  13033  2txmodxeq0  13049  rpexpcl  13197  expnlbnd  13313  rennim  14386  sqrtdiv  14413  o1fsum  14949  divrcnv  14988  rpmsubg  20206  itg2const2  23945  reeff1o  24638  reefgim  24641  logne0  24763  advlog  24837  advlogexp  24838  logcxp  24852  cxprec  24869  cxpmul  24871  abscxp  24875  cxple2  24880  dvcxp1  24921  dvcxp2  24922  dvsqrt  24923  relogbreexp  24953  relogbzexp  24954  relogbmul  24955  relogbdiv  24957  relogbexp  24958  relogbcxp  24963  relogbcxpb  24965  relogbf  24969  logblog  24970  logbgt0b  24971  rlimcnp  25144  efrlim  25148  cxplim  25150  cxp2limlem  25154  cxploglim  25156  logdifbnd  25172  logdiflbnd  25173  logfacrlim2  25403  bposlem8  25468  vmadivsum  25623  mudivsum  25671  mulogsumlem  25672  logdivsum  25674  log2sumbnd  25685  selberg2lem  25691  selberg2  25692  pntrmax  25705  selbergr  25709  pntrlog2bndlem4  25721  pntrlog2bndlem5  25722  pntlem3  25750  padicabvcxp  25773  blocnilem  28231  nmcexi  29457  probfinmeasbOLD  31089  probfinmeasb  31090  signsplypnf  31227  logdivsqrle  31330  poimirlem29  34064  areacirclem1  34125  areacirclem4  34128  areacirc  34130  heiborlem6  34239  heiborlem7  34240  xralrple2  40478  recnnltrp  40501  rpgtrecnn  40505  ioodvbdlimc1lem2  41075  ioodvbdlimc2lem  41077  fldivmod  43328  relogbmulbexp  43370  relogbdivb  43371  blenre  43383