MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnrpd Unicode version

Theorem nnrpd 10611
Description: A natural number is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
nnrpd.1  |-  ( ph  ->  A  e.  NN )
Assertion
Ref Expression
nnrpd  |-  ( ph  ->  A  e.  RR+ )

Proof of Theorem nnrpd
StepHypRef Expression
1 nnrpd.1 . 2  |-  ( ph  ->  A  e.  NN )
2 nnrp 10585 . 2  |-  ( A  e.  NN  ->  A  e.  RR+ )
31, 2syl 16 1  |-  ( ph  ->  A  e.  RR+ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   NNcn 9964   RR+crp 10576
This theorem is referenced by:  modmulnn  11228  nnesq  11466  digit1  11476  bcpasc  11575  iseralt  12441  mertenslem1  12624  mertenslem2  12625  ege2le3  12655  eftlub  12673  effsumlt  12675  eirrlem  12766  sqr2irrlem  12810  dvdsmod  12869  bitsfzo  12910  bitsmod  12911  bitscmp  12913  bitsinv1lem  12916  sadaddlem  12941  sadasslem  12945  bitsres  12948  smumul  12968  bezoutlem3  13003  eucalglt  13039  prmind2  13053  crt  13130  eulerthlem2  13134  fermltl  13136  prmdiv  13137  prmdiveq  13138  odzdvds  13144  prmreclem3  13249  prmreclem5  13251  prmreclem6  13252  4sqlem5  13273  4sqlem6  13274  4sqlem7  13275  4sqlem10  13278  4sqlem12  13287  vdwlem1  13312  mndodcong  15143  odmod  15147  oddvds  15148  dfod2  15163  gexexlem  15430  zlpirlem3  16733  met1stc  18512  met2ndci  18513  lebnumlem3  18949  lebnumii  18952  ovollb2lem  19345  ovoliunlem1  19359  ovoliunlem3  19361  uniioombllem6  19441  itg2cnlem2  19615  elqaalem2  20198  aalioulem2  20211  aalioulem4  20213  aalioulem5  20214  aaliou2b  20219  aaliou3lem9  20228  logfac  20456  cxpeq  20602  leibpi  20743  amgmlem  20789  emcllem1  20795  emcllem2  20796  emcllem3  20797  emcllem5  20799  harmoniclbnd  20808  harmonicubnd  20809  harmonicbnd4  20810  fsumharmonic  20811  wilthlem1  20812  wilthlem2  20813  basellem1  20824  basellem6  20829  basellem8  20831  chtf  20852  efchtcl  20855  chtge0  20856  vmacl  20862  efvmacl  20864  sgmnncl  20891  chtprm  20897  chtdif  20902  efchtdvds  20903  prmorcht  20922  sgmppw  20942  vmalelog  20950  chtleppi  20955  chtublem  20956  fsumvma2  20959  pclogsum  20960  vmasum  20961  chpchtsum  20964  chpub  20965  logfacubnd  20966  logfaclbnd  20967  logfacbnd3  20968  logfacrlim  20969  logexprlim  20970  logfacrlim2  20971  perfectlem2  20975  bclbnd  21025  bposlem1  21029  bposlem2  21030  bposlem4  21032  bposlem5  21033  bposlem6  21034  bposlem7  21035  bposlem9  21037  lgslem1  21041  lgslem4  21044  lgsvalmod  21060  lgsmod  21066  lgsdirprm  21074  lgsne0  21078  lgsqrlem2  21087  lgseisenlem1  21094  lgseisenlem2  21095  lgseisenlem3  21096  lgseisenlem4  21097  lgseisen  21098  lgsquadlem2  21100  lgsquadlem3  21101  m1lgs  21107  2sqlem8  21117  chebbnd1lem1  21124  chebbnd1lem2  21125  chebbnd1lem3  21126  chebbnd1  21127  chtppilimlem1  21128  chtppilimlem2  21129  chtppilim  21130  chebbnd2  21132  chto1lb  21133  vmadivsum  21137  vmadivsumb  21138  rplogsumlem1  21139  rplogsumlem2  21140  dchrisum0lem1a  21141  rpvmasumlem  21142  dchrisumlema  21143  dchrisumlem1  21144  dchrisumlem2  21145  dchrmusum2  21149  dchrvmasumlem1  21150  dchrvmasum2lem  21151  dchrvmasum2if  21152  dchrvmasumlem2  21153  dchrvmasumlem3  21154  dchrvmasumiflem1  21156  dchrvmasumiflem2  21157  dchrisum0flblem2  21164  dchrisum0fno1  21166  dchrisum0lema  21169  dchrisum0lem1b  21170  dchrisum0lem1  21171  dchrisum0lem2a  21172  dchrisum0lem2  21173  dchrisum0lem3  21174  dchrisum0  21175  dirith2  21183  mudivsum  21185  mulogsumlem  21186  mulogsum  21187  mulog2sumlem1  21189  mulog2sumlem2  21190  mulog2sumlem3  21191  vmalogdivsum2  21193  vmalogdivsum  21194  2vmadivsumlem  21195  logsqvma  21197  log2sumbnd  21199  selberglem1  21200  selberglem2  21201  selberglem3  21202  selberg  21203  selbergb  21204  selberg2lem  21205  selberg2  21206  selberg2b  21207  chpdifbndlem1  21208  logdivbnd  21211  selberg3lem1  21212  selberg3lem2  21213  selberg3  21214  selberg4lem1  21215  selberg4  21216  pntrsumo1  21220  pntrsumbnd2  21222  selbergr  21223  selberg3r  21224  selberg4r  21225  selberg34r  21226  pntsf  21228  pntsval2  21231  pntrlog2bndlem1  21232  pntrlog2bndlem2  21233  pntrlog2bndlem3  21234  pntrlog2bndlem4  21235  pntrlog2bndlem5  21236  pntrlog2bndlem6  21238  pntrlog2bnd  21239  pntpbnd1a  21240  pntpbnd1  21241  pntpbnd2  21242  pntibndlem2  21246  pntlemn  21255  pntlemj  21258  pntlemf  21260  pntlemk  21261  pntlemo  21262  pnt  21269  padicabvcxp  21287  ostth2lem2  21289  ostth2lem3  21290  ostth2lem4  21291  ostth2  21292  ostth3  21293  ubthlem2  22334  minvecolem3  22339  lnconi  23497  ltesubnnd  24123  rnlogblem  24360  zetacvg  24760  lgamgulmlem2  24775  lgamgulmlem3  24776  lgamgulmlem4  24777  lgamgulmlem5  24778  lgamgulmlem6  24779  lgamgulm2  24781  lgambdd  24782  lgamucov  24783  lgamcvg2  24800  gamcvg  24801  gamcvg2lem  24804  regamcl  24806  relgamcl  24807  lgam1  24809  iprodgam  25280  faclimlem1  25318  faclimlem3  25320  faclim  25321  iprodfac  25322  mblfinlem  26151  heiborlem3  26420  heiborlem5  26422  heiborlem6  26423  heiborlem7  26424  heiborlem8  26425  heibor  26428  rrndstprj2  26438  rrncmslem  26439  rrnequiv  26442  irrapxlem5  26787  pell14qrgapw  26837  pellqrexplicit  26838  pellqrex  26840  pellfundge  26843  pellfundgt1  26844  jm3.1lem1  26986  jm3.1lem2  26987  stoweidlem31  27655  stoweidlem59  27683  wallispilem3  27691  wallispi  27694  stirlinglem12  27709  stirlinglem15  27712
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668  ax-resscn 9011  ax-1cn 9012  ax-icn 9013  ax-addcl 9014  ax-addrcl 9015  ax-mulcl 9016  ax-mulrcl 9017  ax-mulcom 9018  ax-addass 9019  ax-mulass 9020  ax-distr 9021  ax-i2m1 9022  ax-1ne0 9023  ax-1rid 9024  ax-rnegex 9025  ax-rrecex 9026  ax-cnre 9027  ax-pre-lttri 9028  ax-pre-lttrn 9029  ax-pre-ltadd 9030  ax-pre-mulgt0 9031
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-nel 2578  df-ral 2679  df-rex 2680  df-reu 2681  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-pss 3304  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-tp 3790  df-op 3791  df-uni 3984  df-iun 4063  df-br 4181  df-opab 4235  df-mpt 4236  df-tr 4271  df-eprel 4462  df-id 4466  df-po 4471  df-so 4472  df-fr 4509  df-we 4511  df-ord 4552  df-on 4553  df-lim 4554  df-suc 4555  df-om 4813  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-ov 6051  df-oprab 6052  df-mpt2 6053  df-riota 6516  df-recs 6600  df-rdg 6635  df-er 6872  df-en 7077  df-dom 7078  df-sdom 7079  df-pnf 9086  df-mnf 9087  df-xr 9088  df-ltxr 9089  df-le 9090  df-sub 9257  df-neg 9258  df-nn 9965  df-rp 10577
  Copyright terms: Public domain W3C validator