Theorem rpne0d 12939

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

Syntax hints:   → wi 4   ∈ wcel 2111   ≠ wne 2928  0cc0 11006  ℝ⁺crp 12890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-resscn 11063  ax-1cn 11064  ax-addrcl 11067  ax-rnegex 11077  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-po 5522  df-so 5523  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-ltxr 11151  df-rp 12891

This theorem is referenced by:  rprene0d  12942  rpcnne0d  12943  iccf1o  13396  ltexp2r  14080  discr  14147  bcpasc  14228  sqrtdiv  15172  abs00  15196  absdiv  15202  o1rlimmul  15526  geomulcvg  15783  mertenslem1  15791  retanhcl  16068  tanhlt1  16069  tanhbnd  16070  sylow1lem1  19510  nrginvrcnlem  24606  nmoi2  24645  reperflem  24734  icchmeoOLD  24866  icopnfcnv  24867  nmoleub2lem  25041  nmoleub2lem2  25043  nmoleub3  25046  pjthlem1  25364  sca2rab  25440  ovolscalem1  25441  ovolsca  25443  itg2mulclem  25674  itg2mulc  25675  c1liplem1  25928  aalioulem4  26270  aaliou3lem8  26280  itgulm  26344  dvradcnv  26357  abelthlem7  26375  abelthlem8  26376  tanrpcl  26440  tanregt0  26475  efiarg  26543  argregt0  26546  argrege0  26547  argimgt0  26548  tanarg  26555  logdivlti  26556  logno1  26572  logcnlem4  26581  divcxp  26623  cxple2  26633  cxpcn3lem  26684  cxpcn3  26685  cxpaddlelem  26688  cxpaddle  26689  logbrec  26719  asinlem3  26808  rlimcnp  26902  rlimcnp2  26903  rlimcxp  26911  cxp2limlem  26913  cxp2lim  26914  cxploglim2  26916  jensenlem2  26925  amgmlem  26927  logdiflbnd  26932  lgamgulmlem2  26967  lgamucov  26975  basellem3  27020  basellem8  27025  isppw  27051  chpeq0  27146  chteq0  27147  bposlem9  27230  chebbnd1lem2  27408  chebbnd1  27410  chtppilimlem1  27411  chebbnd2  27415  chto1lb  27416  chpchtlim  27417  chpo1ubb  27419  rplogsumlem1  27422  rplogsumlem2  27423  dchrvmasumlem1  27433  dchrvmasum2lem  27434  dchrisum0lema  27452  dchrisum0lem1b  27453  dchrisum0lem1  27454  dchrisum0lem2a  27455  dchrisum0lem2  27456  dchrisum0lem3  27457  dchrisum0  27458  mulog2sumlem1  27472  vmalogdivsum2  27476  vmalogdivsum  27477  2vmadivsumlem  27478  chpdifbndlem1  27491  selberg3lem1  27495  selberg3lem2  27496  selberg3  27497  selberg4lem1  27498  selberg4  27499  selberg3r  27507  selberg4r  27508  selberg34r  27509  pntrlog2bndlem1  27515  pntrlog2bndlem2  27516  pntrlog2bndlem3  27517  pntrlog2bndlem4  27518  pntrlog2bndlem5  27519  pntrlog2bndlem6  27521  pntpbnd2  27525  pntibndlem2  27529  pntlemr  27540  pntlemo  27545  pnt2  27551  pnt  27552  padicabv  27568  padicabvcxp  27570  ostth2lem3  27573  ostth2lem4  27574  ostth3  27576  smcnlem  30677  pjhthlem1  31371  rpxdivcld  32914  xrmulc1cn  33943  esumdivc  34096  probmeasb  34443  signsply0  34564  divsqrtid  34607  hgt750leme  34671  circum  35718  iprodgam  35786  faclimlem1  35787  faclimlem3  35789  knoppndvlem17  36572  knoppndvlem18  36573  itg2addnclem3  37712  geomcau  37798  cntotbnd  37835  bfplem1  37861  rrncmslem  37871  rrnequiv  37874  relogbzexpd  42067  aks4d1p1p1  42155  dvrelogpow2b  42160  aks4d1p1p4  42163  aks4d1p1p6  42165  aks4d1p1p7  42166  aks4d1p5  42172  aks4d1p6  42173  exp11d  42418  rplog11d  42439  irrapxlem5  42918  pellfund14  42990  rmxyneg  43012  rmxyadd  43013  modabsdifz  43078  binomcxplemnotnn0  44448  oddfl  45378  xralrple3  45471  ioodvbdlimc1lem2  46029  ioodvbdlimc2lem  46031  stoweidlem1  46098  stoweidlem14  46111  stoweidlem60  46157  wallispilem4  46165  wallispilem5  46166  wallispi  46167  wallispi2lem1  46168  stirlinglem1  46171  stirlinglem3  46173  stirlinglem4  46174  stirlinglem5  46175  stirlinglem8  46178  stirlinglem12  46182  stirlinglem15  46185  dirkertrigeqlem1  46195  dirkercncflem1  46200  dirkercncflem4  46203  fourierdlem30  46234  fourierdlem39  46243  fourierdlem47  46250  fourierdlem65  46268  fourierdlem73  46276  fourierdlem87  46290  qndenserrnbllem  46391  sge0rpcpnf  46518  hoiqssbllem2  46720  young2d  49905