Theorem rpne0d 13044

Description: A positive real is nonzero. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rpred.1	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Assertion

Ref	Expression
rpne0d	⊢ (𝜑 → 𝐴 ≠ 0)

Proof of Theorem rpne0d

Step	Hyp	Ref	Expression
1		rpred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2		rpne0 13012	. 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ≠ 0)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ∈ wcel 2144   ≠ wne 2959  0cc0 11075  ℝ⁺crp 12995

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-resscn 11132  ax-1cn 11133  ax-addrcl 11136  ax-rnegex 11146  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5544  df-po 5557  df-so 5558  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-er 8680  df-en 8930  df-dom 8931  df-sdom 8932  df-pnf 11220  df-mnf 11221  df-ltxr 11223  df-rp 12996

This theorem is referenced by:  rprene0d  13047  rpcnne0d  13048  iccf1o  13502  ltexp2r  14188  discr  14255  bcpasc  14336  sqrtdiv  15294  abs00  15318  absdiv  15324  o1rlimmul  15648  geomulcvg  15908  mertenslem1  15916  retanhcl  16193  tanhlt1  16194  tanhbnd  16195  sylow1lem1  19640  nrginvrcnlem  24753  nmoi2  24792  reperflem  24881  icopnfcnv  25006  nmoleub2lem  25178  nmoleub2lem2  25180  nmoleub3  25183  pjthlem1  25501  sca2rab  25576  ovolscalem1  25577  ovolsca  25579  itg2mulclem  25810  itg2mulc  25811  c1liplem1  26060  aalioulem4  26401  aaliou3lem8  26411  itgulm  26473  dvradcnv  26486  abelthlem7  26503  abelthlem8  26504  tanrpcl  26571  tanregt0  26606  efiarg  26674  argregt0  26677  argrege0  26678  argimgt0  26679  tanarg  26686  logdivlti  26687  logno1  26703  logcnlem4  26712  divcxp  26754  cxple2  26764  cxpcn3lem  26814  cxpcn3  26815  cxpaddlelem  26818  cxpaddle  26819  logbrec  26849  asinlem3  26938  rlimcnp  27032  rlimcnp2  27033  rlimcxp  27040  cxp2limlem  27042  cxp2lim  27043  cxploglim2  27045  jensenlem2  27054  amgmlem  27056  logdiflbnd  27061  lgamgulmlem2  27096  lgamucov  27104  basellem3  27149  basellem8  27154  isppw  27180  chpeq0  27274  chteq0  27275  bposlem9  27358  chebbnd1lem2  27536  chebbnd1  27538  chtppilimlem1  27539  chebbnd2  27543  chto1lb  27544  chpchtlim  27545  chpo1ubb  27547  rplogsumlem1  27550  rplogsumlem2  27551  dchrvmasumlem1  27561  dchrvmasum2lem  27562  dchrisum0lema  27580  dchrisum0lem1b  27581  dchrisum0lem1  27582  dchrisum0lem2a  27583  dchrisum0lem2  27584  dchrisum0lem3  27585  dchrisum0  27586  mulog2sumlem1  27600  vmalogdivsum2  27604  vmalogdivsum  27605  2vmadivsumlem  27606  chpdifbndlem1  27619  selberg3lem1  27623  selberg3lem2  27624  selberg3  27625  selberg4lem1  27626  selberg4  27627  selberg3r  27635  selberg4r  27636  selberg34r  27637  pntrlog2bndlem1  27643  pntrlog2bndlem2  27644  pntrlog2bndlem3  27645  pntrlog2bndlem4  27646  pntrlog2bndlem5  27647  pntrlog2bndlem6  27649  pntpbnd2  27653  pntibndlem2  27657  pntlemr  27668  pntlemo  27673  pnt2  27679  pnt  27680  padicabv  27696  padicabvcxp  27698  ostth2lem3  27701  ostth2lem4  27702  ostth3  27704  smcnlem  30902  pjhthlem1  31596  rpxdivcld  33113  xrmulc1cn  34229  esumdivc  34382  probmeasb  34729  signsply0  34847  divsqrtid  34890  hgt750leme  34954  circum  36029  iprodgam  36097  faclimlem1  36098  faclimlem3  36100  knoppndvlem17  36971  knoppndvlem18  36972  itg2addnclem3  38177  geomcau  38263  cntotbnd  38300  bfplem1  38326  rrncmslem  38336  rrnequiv  38339  relogbzexpd  42598  aks4d1p1p1  42685  dvrelogpow2b  42690  aks4d1p1p4  42693  aks4d1p1p6  42695  aks4d1p1p7  42696  aks4d1p5  42702  aks4d1p6  42703  exp11d  42940  rplog11d  42961  irrapxlem5  43408  pellfund14  43480  rmxyneg  43502  rmxyadd  43503  modabsdifz  43568  binomcxplemnotnn0  44937  oddfl  45862  xralrple3  45954  ioodvbdlimc1lem2  46511  ioodvbdlimc2lem  46513  stoweidlem1  46580  stoweidlem14  46593  stoweidlem60  46639  wallispilem4  46647  wallispilem5  46648  wallispi  46649  wallispi2lem1  46650  stirlinglem1  46653  stirlinglem3  46655  stirlinglem4  46656  stirlinglem5  46657  stirlinglem8  46660  stirlinglem12  46664  stirlinglem15  46667  dirkertrigeqlem1  46677  dirkercncflem1  46682  dirkercncflem4  46685  fourierdlem30  46716  fourierdlem39  46725  fourierdlem47  46732  fourierdlem65  46750  fourierdlem73  46758  fourierdlem87  46772  qndenserrnbllem  46873  sge0rpcpnf  47000  hoiqssbllem2  47202  young2d  50431