Theorem rpne0 12924

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ≠ wne 2931   class class class wbr 5097  ℝcr 11027  0cc0 11028   < clt 11168  ℝ⁺crp 12907

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 2183  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pow 5309  ax-pr 5376  ax-un 7680  ax-resscn 11085  ax-1cn 11086  ax-addrcl 11089  ax-rnegex 11099  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103

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 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5518  df-po 5531  df-so 5532  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6447  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-fv 6499  df-er 8635  df-en 8886  df-dom 8887  df-sdom 8888  df-pnf 11170  df-mnf 11171  df-ltxr 11173  df-rp 12908

This theorem is referenced by:  rprene0  12925  rpcnne0  12926  rpne0d  12956  divge1  12977  xlemul1  13207  ltdifltdiv  13756  mulmod0  13799  negmod0  13800  moddiffl  13804  modid0  13819  modmuladd  13838  modmuladdnn0  13840  2txmodxeq0  13856  rpexpcl  14005  expnlbnd  14158  rennim  15164  sqrtdiv  15190  o1fsum  15738  divrcnv  15777  rpmsubg  21388  itg2const2  25700  reeff1o  26415  logne0  26546  advlog  26621  advlogexp  26622  logcxp  26636  cxprec  26653  cxpmul  26655  abscxp  26659  cxple2  26664  dvcxp1  26707  dvcxp2  26708  dvsqrt  26709  relogbreexp  26743  relogbzexp  26744  relogbmul  26745  relogbdiv  26747  relogbexp  26748  relogbcxp  26753  relogbcxpb  26755  relogbf  26759  logbgt0b  26761  rlimcnp  26933  efrlim  26937  efrlimOLD  26938  cxplim  26940  cxp2limlem  26944  cxploglim  26946  logdifbnd  26962  logdiflbnd  26963  logfacrlim2  27195  bposlem8  27260  vmadivsum  27451  mudivsum  27499  mulogsumlem  27500  logdivsum  27502  log2sumbnd  27513  selberg2lem  27519  selberg2  27520  pntrmax  27533  selbergr  27537  pntrlog2bndlem4  27549  pntrlog2bndlem5  27550  pntlem3  27578  padicabvcxp  27601  blocnilem  30860  nmcexi  32082  probfinmeasb  34564  probfinmeasbALTV  34565  signsplypnf  34686  logdivsqrle  34786  poimirlem29  37819  areacirclem1  37878  areacirclem4  37881  areacirc  37883  heiborlem6  37986  heiborlem7  37987  dvrelog2  42353  dvrelog3  42354  aks4d1p1p6  42362  xralrple2  45636  recnnltrp  45658  rpgtrecnn  45661  ioodvbdlimc1lem2  46213  ioodvbdlimc2lem  46215  fldivmod  47621  ceildivmod  47622  relogbmulbexp  48844  relogbdivb  48845  blenre  48857