Theorem rpne0 13161

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147   ≠ wne 2959   class class class wbr 5106  ℝcr 11223  0cc0 11224   < clt 11367  ℝ⁺crp 13144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-resscn 11281  ax-1cn 11282  ax-addrcl 11285  ax-rnegex 11295  ax-cnre 11297  ax-pre-lttri 11298  ax-pre-lttrn 11299

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-er 8742  df-en 8999  df-dom 9000  df-sdom 9001  df-pnf 11369  df-mnf 11370  df-ltxr 11372  df-rp 13145

This theorem is used by:  rprene0  13162  rpcnne0  13163  rpne0d  13193  divge1  13214  xlemul1  13444  ltdifltdiv  13998  mulmod0  14041  negmod0  14042  moddiffl  14046  modid0  14061  modmuladd  14080  modmuladdnn0  14082  2txmodxeq0  14098  rpexpcl  14247  expnlbnd  14401  rennim  15432  sqrtdiv  15458  o1fsum  16006  divrcnv  16047  rpmsubg  21764  itg2const2  26089  reeff1o  26801  logne0  26934  advlog  27009  advlogexp  27010  logcxp  27024  cxprec  27041  cxpmul  27043  abscxp  27047  cxple2  27052  dvcxp1  27095  dvcxp2  27096  dvsqrt  27097  relogbreexp  27130  relogbzexp  27131  relogbmul  27132  relogbdiv  27134  relogbexp  27135  relogbcxp  27140  relogbcxpb  27142  relogbf  27146  logbgt0b  27148  rlimcnp  27320  efrlim  27324  cxplim  27326  cxp2limlem  27330  cxploglim  27332  logdifbnd  27348  logdiflbnd  27349  logfacrlim2  27580  bposlem8  27645  vmadivsum  27836  mudivsum  27884  mulogsumlem  27885  logdivsum  27887  log2sumbnd  27898  selberg2lem  27904  selberg2  27905  pntrmax  27918  selbergr  27922  pntrlog2bndlem4  27934  pntrlog2bndlem5  27935  pntlem3  27963  padicabvcxp  27986  blocnilem  31433  nmcexi  32655  probfinmeasb  35127  probfinmeasbALTV  35128  signsplypnf  35246  logdivsqrle  35346  poimirlem29  38758  areacirclem1  38817  areacirclem4  38820  areacirc  38822  heiborlem6  38941  heiborlem7  38942  dvrelog2  43305  dvrelog3  43306  aks4d1p1p6  43314  xralrple2  46569  recnnltrp  46591  rpgtrecnn  46594  ioodvbdlimc1lem2  47145  ioodvbdlimc2lem  47147  fldivmod  48617  ceildivmod  48618  relogbmulbexp  49876  relogbdivb  49877  blenre  49889