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

Theorem nnrpd 10540
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 10514 . 2  |-  ( A  e.  NN  ->  A  e.  RR+ )
31, 2syl 15 1  |-  ( ph  ->  A  e.  RR+ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1715   NNcn 9893   RR+crp 10505
This theorem is referenced by:  modmulnn  11152  nnesq  11390  digit1  11400  bcpasc  11499  iseralt  12365  mertenslem1  12548  mertenslem2  12549  ege2le3  12579  eftlub  12597  effsumlt  12599  eirrlem  12690  sqr2irrlem  12734  dvdsmod  12793  bitsfzo  12834  bitsmod  12835  bitscmp  12837  bitsinv1lem  12840  sadaddlem  12865  sadasslem  12869  bitsres  12872  smumul  12892  bezoutlem3  12927  eucalglt  12963  prmind2  12977  crt  13054  eulerthlem2  13058  fermltl  13060  prmdiv  13061  prmdiveq  13062  odzdvds  13068  prmreclem3  13173  prmreclem5  13175  prmreclem6  13176  4sqlem5  13197  4sqlem6  13198  4sqlem7  13199  4sqlem10  13202  4sqlem12  13211  vdwlem1  13236  mndodcong  15067  odmod  15071  oddvds  15072  dfod2  15087  gexexlem  15354  zlpirlem3  16660  met1stc  18280  met2ndci  18281  lebnumlem3  18676  lebnumii  18679  ovollb2lem  19062  ovoliunlem1  19076  ovoliunlem3  19078  uniioombllem6  19158  itg2cnlem2  19332  elqaalem2  19915  aalioulem2  19928  aalioulem4  19930  aalioulem5  19931  aaliou2b  19936  aaliou3lem9  19945  logfac  20173  cxpeq  20319  leibpi  20460  amgmlem  20506  emcllem1  20512  emcllem2  20513  emcllem3  20514  emcllem5  20516  harmoniclbnd  20525  harmonicubnd  20526  harmonicbnd4  20527  fsumharmonic  20528  wilthlem1  20529  wilthlem2  20530  basellem1  20541  basellem6  20546  basellem8  20548  chtf  20569  efchtcl  20572  chtge0  20573  vmacl  20579  efvmacl  20581  sgmnncl  20608  chtprm  20614  chtdif  20619  efchtdvds  20620  prmorcht  20639  sgmppw  20659  vmalelog  20667  chtleppi  20672  chtublem  20673  fsumvma2  20676  pclogsum  20677  vmasum  20678  chpchtsum  20681  chpub  20682  logfacubnd  20683  logfaclbnd  20684  logfacbnd3  20685  logfacrlim  20686  logexprlim  20687  logfacrlim2  20688  perfectlem2  20692  bclbnd  20742  bposlem1  20746  bposlem2  20747  bposlem4  20749  bposlem5  20750  bposlem6  20751  bposlem7  20752  bposlem9  20754  lgslem1  20758  lgslem4  20761  lgsvalmod  20777  lgsmod  20783  lgsdirprm  20791  lgsne0  20795  lgsqrlem2  20804  lgseisenlem1  20811  lgseisenlem2  20812  lgseisenlem3  20813  lgseisenlem4  20814  lgseisen  20815  lgsquadlem2  20817  lgsquadlem3  20818  m1lgs  20824  2sqlem8  20834  chebbnd1lem1  20841  chebbnd1lem2  20842  chebbnd1lem3  20843  chebbnd1  20844  chtppilimlem1  20845  chtppilimlem2  20846  chtppilim  20847  chebbnd2  20849  chto1lb  20850  vmadivsum  20854  vmadivsumb  20855  rplogsumlem1  20856  rplogsumlem2  20857  dchrisum0lem1a  20858  rpvmasumlem  20859  dchrisumlema  20860  dchrisumlem1  20861  dchrisumlem2  20862  dchrmusum2  20866  dchrvmasumlem1  20867  dchrvmasum2lem  20868  dchrvmasum2if  20869  dchrvmasumlem2  20870  dchrvmasumlem3  20871  dchrvmasumiflem1  20873  dchrvmasumiflem2  20874  dchrisum0flblem2  20881  dchrisum0fno1  20883  dchrisum0lema  20886  dchrisum0lem1b  20887  dchrisum0lem1  20888  dchrisum0lem2a  20889  dchrisum0lem2  20890  dchrisum0lem3  20891  dchrisum0  20892  dirith2  20900  mudivsum  20902  mulogsumlem  20903  mulogsum  20904  mulog2sumlem1  20906  mulog2sumlem2  20907  mulog2sumlem3  20908  vmalogdivsum2  20910  vmalogdivsum  20911  2vmadivsumlem  20912  logsqvma  20914  log2sumbnd  20916  selberglem1  20917  selberglem2  20918  selberglem3  20919  selberg  20920  selbergb  20921  selberg2lem  20922  selberg2  20923  selberg2b  20924  chpdifbndlem1  20925  logdivbnd  20928  selberg3lem1  20929  selberg3lem2  20930  selberg3  20931  selberg4lem1  20932  selberg4  20933  pntrsumo1  20937  pntrsumbnd2  20939  selbergr  20940  selberg3r  20941  selberg4r  20942  selberg34r  20943  pntsf  20945  pntsval2  20948  pntrlog2bndlem1  20949  pntrlog2bndlem2  20950  pntrlog2bndlem3  20951  pntrlog2bndlem4  20952  pntrlog2bndlem5  20953  pntrlog2bndlem6  20955  pntrlog2bnd  20956  pntpbnd1a  20957  pntpbnd1  20958  pntpbnd2  20959  pntibndlem2  20963  pntlemn  20972  pntlemj  20975  pntlemf  20977  pntlemk  20978  pntlemo  20979  pnt  20986  padicabvcxp  21004  ostth2lem2  21006  ostth2lem3  21007  ostth2lem4  21008  ostth2  21009  ostth3  21010  ubthlem2  21884  minvecolem3  21889  lnconi  23047  ltesubnnd  23686  rnlogblem  23985  zetacvg  24368  lgamgulmlem2  24383  lgamgulmlem3  24384  lgamgulmlem4  24385  lgamgulmlem5  24386  lgamgulmlem6  24387  lgamgulm2  24389  lgambdd  24390  lgamucov  24391  lgamcvg2  24408  gamcvg  24409  gamcvg2lem  24412  regamcl  24414  relgamcl  24415  lgam1  24417  gammacvglem1  24919  gammacvglem2  24920  gammacvglem3  24921  faclimlem1  24922  faclimlem3  24924  faclim  24925  iprodfac  24926  heiborlem3  26128  heiborlem5  26130  heiborlem6  26131  heiborlem7  26132  heiborlem8  26133  heibor  26136  rrndstprj2  26146  rrncmslem  26147  rrnequiv  26150  irrapxlem5  26502  pell14qrgapw  26552  pellqrexplicit  26553  pellqrex  26555  pellfundge  26558  pellfundgt1  26559  jm3.1lem1  26701  jm3.1lem2  26702  stoweidlem59  27399  wallispilem3  27407  wallispi  27410  stirlinglem12  27425  stirlinglem15  27428
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-13 1717  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-sep 4243  ax-nul 4251  ax-pow 4290  ax-pr 4316  ax-un 4615  ax-resscn 8941  ax-1cn 8942  ax-icn 8943  ax-addcl 8944  ax-addrcl 8945  ax-mulcl 8946  ax-mulrcl 8947  ax-mulcom 8948  ax-addass 8949  ax-mulass 8950  ax-distr 8951  ax-i2m1 8952  ax-1ne0 8953  ax-1rid 8954  ax-rnegex 8955  ax-rrecex 8956  ax-cnre 8957  ax-pre-lttri 8958  ax-pre-lttrn 8959  ax-pre-ltadd 8960  ax-pre-mulgt0 8961
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 936  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-mo 2222  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-nel 2532  df-ral 2633  df-rex 2634  df-reu 2635  df-rab 2637  df-v 2875  df-sbc 3078  df-csb 3168  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-pss 3254  df-nul 3544  df-if 3655  df-pw 3716  df-sn 3735  df-pr 3736  df-tp 3737  df-op 3738  df-uni 3930  df-iun 4009  df-br 4126  df-opab 4180  df-mpt 4181  df-tr 4216  df-eprel 4408  df-id 4412  df-po 4417  df-so 4418  df-fr 4455  df-we 4457  df-ord 4498  df-on 4499  df-lim 4500  df-suc 4501  df-om 4760  df-xp 4798  df-rel 4799  df-cnv 4800  df-co 4801  df-dm 4802  df-rn 4803  df-res 4804  df-ima 4805  df-iota 5322  df-fun 5360  df-fn 5361  df-f 5362  df-f1 5363  df-fo 5364  df-f1o 5365  df-fv 5366  df-ov 5984  df-oprab 5985  df-mpt2 5986  df-riota 6446  df-recs 6530  df-rdg 6565  df-er 6802  df-en 7007  df-dom 7008  df-sdom 7009  df-pnf 9016  df-mnf 9017  df-xr 9018  df-ltxr 9019  df-le 9020  df-sub 9186  df-neg 9187  df-nn 9894  df-rp 10506
  Copyright terms: Public domain W3C validator