MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rpne0d Structured version   Visualization version   GIF version

Theorem rpne0d 12426
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
StepHypRef Expression
1 rpred.1 . 2 (𝜑𝐴 ∈ ℝ+)
2 rpne0 12395 . 2 (𝐴 ∈ ℝ+𝐴 ≠ 0)
31, 2syl 17 1 (𝜑𝐴 ≠ 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  wne 3016  0cc0 10526  +crp 12379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-resscn 10583  ax-1cn 10584  ax-addrcl 10587  ax-rnegex 10597  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-po 5468  df-so 5469  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-ltxr 10669  df-rp 12380
This theorem is referenced by:  rprene0d  12429  rpcnne0d  12430  iccf1o  12872  ltexp2r  13527  discr  13591  bcpasc  13671  sqrtdiv  14615  abs00  14639  absdiv  14645  o1rlimmul  14965  geomulcvg  15222  mertenslem1  15230  retanhcl  15502  tanhlt1  15503  tanhbnd  15504  sylow1lem1  18654  nrginvrcnlem  23229  nmoi2  23268  reperflem  23355  icchmeo  23474  icopnfcnv  23475  nmoleub2lem  23647  nmoleub2lem2  23649  nmoleub3  23652  pjthlem1  23969  sca2rab  24042  ovolscalem1  24043  ovolsca  24045  itg2mulclem  24276  itg2mulc  24277  c1liplem1  24522  aalioulem4  24853  aaliou3lem8  24863  itgulm  24925  dvradcnv  24938  abelthlem7  24955  abelthlem8  24956  tanrpcl  25019  tanregt0  25050  efiarg  25117  argregt0  25120  argrege0  25121  argimgt0  25122  tanarg  25129  logdivlti  25130  logno1  25146  logcnlem4  25155  divcxp  25197  cxple2  25207  cxpcn3lem  25255  cxpcn3  25256  cxpaddlelem  25259  cxpaddle  25260  logbrec  25287  asinlem3  25376  rlimcnp  25471  rlimcnp2  25472  rlimcxp  25479  cxp2limlem  25481  cxp2lim  25482  cxploglim2  25484  jensenlem2  25493  amgmlem  25495  logdiflbnd  25500  lgamgulmlem2  25535  lgamucov  25543  basellem3  25588  basellem8  25593  isppw  25619  chpeq0  25712  chteq0  25713  bposlem9  25796  chebbnd1lem2  25974  chebbnd1  25976  chtppilimlem1  25977  chebbnd2  25981  chto1lb  25982  chpchtlim  25983  chpo1ubb  25985  rplogsumlem1  25988  rplogsumlem2  25989  dchrvmasumlem1  25999  dchrvmasum2lem  26000  dchrisum0lema  26018  dchrisum0lem1b  26019  dchrisum0lem1  26020  dchrisum0lem2a  26021  dchrisum0lem2  26022  dchrisum0lem3  26023  dchrisum0  26024  mulog2sumlem1  26038  vmalogdivsum2  26042  vmalogdivsum  26043  2vmadivsumlem  26044  chpdifbndlem1  26057  selberg3lem1  26061  selberg3lem2  26062  selberg3  26063  selberg4lem1  26064  selberg4  26065  selberg3r  26073  selberg4r  26074  selberg34r  26075  pntrlog2bndlem1  26081  pntrlog2bndlem2  26082  pntrlog2bndlem3  26083  pntrlog2bndlem4  26084  pntrlog2bndlem5  26085  pntrlog2bndlem6  26087  pntpbnd2  26091  pntibndlem2  26095  pntlemr  26106  pntlemo  26111  pnt2  26117  pnt  26118  padicabv  26134  padicabvcxp  26136  ostth2lem3  26139  ostth2lem4  26140  ostth3  26142  smcnlem  28402  pjhthlem1  29096  rpxdivcld  30538  xrmulc1cn  31073  esumdivc  31242  probmeasb  31588  signsply0  31721  divsqrtid  31765  hgt750leme  31829  circum  32815  iprodgam  32872  faclimlem1  32873  faclimlem3  32875  knoppndvlem17  33765  knoppndvlem18  33766  itg2addnclem3  34827  geomcau  34917  cntotbnd  34957  bfplem1  34983  rrncmslem  34993  rrnequiv  34996  cxpgt0d  39060  exp11d  39069  irrapxlem5  39303  pellfund14  39375  rmxyneg  39397  rmxyadd  39398  modabsdifz  39463  binomcxplemnotnn0  40568  oddfl  41423  xralrple3  41522  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  stoweidlem1  42167  stoweidlem14  42180  stoweidlem60  42226  wallispilem4  42234  wallispilem5  42235  wallispi  42236  wallispi2lem1  42237  stirlinglem1  42240  stirlinglem3  42242  stirlinglem4  42243  stirlinglem5  42244  stirlinglem8  42247  stirlinglem12  42251  stirlinglem15  42254  dirkertrigeqlem1  42264  dirkercncflem1  42269  dirkercncflem4  42272  fourierdlem30  42303  fourierdlem39  42312  fourierdlem47  42319  fourierdlem65  42337  fourierdlem73  42345  fourierdlem87  42359  qndenserrnbllem  42460  sge0rpcpnf  42584  hoiqssbllem2  42786  young2d  44804
  Copyright terms: Public domain W3C validator