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

Theorem nnrpd 11138
Description: A positive integer 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 11112 . 2  |-  ( A  e.  NN  ->  A  e.  RR+ )
31, 2syl 16 1  |-  ( ph  ->  A  e.  RR+ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   NNcn 10434   RR+crp 11103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4522  ax-nul 4530  ax-pow 4579  ax-pr 4640  ax-un 6483  ax-resscn 9451  ax-1cn 9452  ax-icn 9453  ax-addcl 9454  ax-addrcl 9455  ax-mulcl 9456  ax-mulrcl 9457  ax-mulcom 9458  ax-addass 9459  ax-mulass 9460  ax-distr 9461  ax-i2m1 9462  ax-1ne0 9463  ax-1rid 9464  ax-rnegex 9465  ax-rrecex 9466  ax-cnre 9467  ax-pre-lttri 9468  ax-pre-lttrn 9469  ax-pre-ltadd 9470  ax-pre-mulgt0 9471
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2804  df-rex 2805  df-reu 2806  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3747  df-if 3901  df-pw 3971  df-sn 3987  df-pr 3989  df-tp 3991  df-op 3993  df-uni 4201  df-iun 4282  df-br 4402  df-opab 4460  df-mpt 4461  df-tr 4495  df-eprel 4741  df-id 4745  df-po 4750  df-so 4751  df-fr 4788  df-we 4790  df-ord 4831  df-on 4832  df-lim 4833  df-suc 4834  df-xp 4955  df-rel 4956  df-cnv 4957  df-co 4958  df-dm 4959  df-rn 4960  df-res 4961  df-ima 4962  df-iota 5490  df-fun 5529  df-fn 5530  df-f 5531  df-f1 5532  df-fo 5533  df-f1o 5534  df-fv 5535  df-riota 6162  df-ov 6204  df-oprab 6205  df-mpt2 6206  df-om 6588  df-recs 6943  df-rdg 6977  df-er 7212  df-en 7422  df-dom 7423  df-sdom 7424  df-pnf 9532  df-mnf 9533  df-xr 9534  df-ltxr 9535  df-le 9536  df-sub 9709  df-neg 9710  df-nn 10435  df-rp 11104
This theorem is referenced by:  modmulnn  11843  nnesq  12106  digit1  12116  bcpasc  12215  cshwn  12553  iseralt  13281  mertenslem1  13463  mertenslem2  13464  ege2le3  13494  eftlub  13512  effsumlt  13514  eirrlem  13605  sqr2irrlem  13649  dvdsmod  13709  bitsfzo  13750  bitsmod  13751  bitscmp  13753  bitsinv1lem  13756  sadaddlem  13781  sadasslem  13785  bitsres  13788  smumul  13808  bezoutlem3  13843  eucalglt  13879  prmind2  13893  crt  13972  eulerthlem2  13976  fermltl  13978  prmdiv  13979  prmdiveq  13980  odzdvds  13986  modprm0  13992  modprmn0modprm0  13994  prmreclem3  14098  prmreclem5  14100  prmreclem6  14101  4sqlem5  14122  4sqlem6  14123  4sqlem7  14124  4sqlem10  14127  4sqlem12  14136  vdwlem1  14161  mndodcong  16167  odmod  16171  oddvds  16172  dfod2  16187  gexexlem  16456  zringlpirlem3  18031  zlpirlem3  18036  met1stc  20229  met2ndci  20230  lebnumlem3  20668  lebnumii  20671  ovollb2lem  21104  ovoliunlem1  21118  ovoliunlem3  21120  uniioombllem6  21202  itg2cnlem2  21374  elqaalem2  21920  aalioulem2  21933  aalioulem4  21935  aalioulem5  21936  aaliou2b  21941  aaliou3lem9  21950  logfac  22183  cxpeq  22329  leibpi  22471  amgmlem  22517  emcllem1  22523  emcllem2  22524  emcllem3  22525  emcllem5  22527  harmoniclbnd  22536  harmonicubnd  22537  harmonicbnd4  22538  fsumharmonic  22539  wilthlem1  22540  wilthlem2  22541  basellem1  22552  basellem6  22557  basellem8  22559  chtf  22580  efchtcl  22583  chtge0  22584  vmacl  22590  efvmacl  22592  sgmnncl  22619  chtprm  22625  chtdif  22630  efchtdvds  22631  prmorcht  22650  sgmppw  22670  vmalelog  22678  chtleppi  22683  chtublem  22684  fsumvma2  22687  pclogsum  22688  vmasum  22689  chpchtsum  22692  chpub  22693  logfacubnd  22694  logfaclbnd  22695  logfacbnd3  22696  logfacrlim  22697  logexprlim  22698  logfacrlim2  22699  perfectlem2  22703  bclbnd  22753  bposlem1  22757  bposlem2  22758  bposlem4  22760  bposlem5  22761  bposlem6  22762  bposlem7  22763  bposlem9  22765  lgslem1  22769  lgslem4  22772  lgsvalmod  22788  lgsmod  22794  lgsdirprm  22802  lgsne0  22806  lgsqrlem2  22815  lgseisenlem1  22822  lgseisenlem2  22823  lgseisenlem3  22824  lgseisenlem4  22825  lgseisen  22826  lgsquadlem2  22828  lgsquadlem3  22829  m1lgs  22835  2sqlem8  22845  chebbnd1lem1  22852  chebbnd1lem2  22853  chebbnd1lem3  22854  chebbnd1  22855  chtppilimlem1  22856  chtppilimlem2  22857  chtppilim  22858  chebbnd2  22860  chto1lb  22861  vmadivsum  22865  vmadivsumb  22866  rplogsumlem1  22867  rplogsumlem2  22868  dchrisum0lem1a  22869  rpvmasumlem  22870  dchrisumlema  22871  dchrisumlem1  22872  dchrisumlem2  22873  dchrmusum2  22877  dchrvmasumlem1  22878  dchrvmasum2lem  22879  dchrvmasum2if  22880  dchrvmasumlem2  22881  dchrvmasumlem3  22882  dchrvmasumiflem1  22884  dchrvmasumiflem2  22885  dchrisum0flblem2  22892  dchrisum0fno1  22894  dchrisum0lema  22897  dchrisum0lem1b  22898  dchrisum0lem1  22899  dchrisum0lem2a  22900  dchrisum0lem2  22901  dchrisum0lem3  22902  dchrisum0  22903  dirith2  22911  mudivsum  22913  mulogsumlem  22914  mulogsum  22915  mulog2sumlem1  22917  mulog2sumlem2  22918  mulog2sumlem3  22919  vmalogdivsum2  22921  vmalogdivsum  22922  2vmadivsumlem  22923  logsqvma  22925  log2sumbnd  22927  selberglem1  22928  selberglem2  22929  selberglem3  22930  selberg  22931  selbergb  22932  selberg2lem  22933  selberg2  22934  selberg2b  22935  chpdifbndlem1  22936  logdivbnd  22939  selberg3lem1  22940  selberg3lem2  22941  selberg3  22942  selberg4lem1  22943  selberg4  22944  pntrsumo1  22948  pntrsumbnd2  22950  selbergr  22951  selberg3r  22952  selberg4r  22953  selberg34r  22954  pntsf  22956  pntsval2  22959  pntrlog2bndlem1  22960  pntrlog2bndlem2  22961  pntrlog2bndlem3  22962  pntrlog2bndlem4  22963  pntrlog2bndlem5  22964  pntrlog2bndlem6  22966  pntrlog2bnd  22967  pntpbnd1a  22968  pntpbnd1  22969  pntpbnd2  22970  pntibndlem2  22974  pntlemn  22983  pntlemj  22986  pntlemf  22988  pntlemk  22989  pntlemo  22990  pnt  22997  padicabvcxp  23015  ostth2lem2  23017  ostth2lem3  23018  ostth2lem4  23019  ostth2  23020  ostth3  23021  ubthlem2  24425  minvecolem3  24430  lnconi  25590  ltesubnnd  26237  rnlogblem  26604  eulerpartlemgc  26890  zetacvg  27146  lgamgulmlem2  27161  lgamgulmlem3  27162  lgamgulmlem4  27163  lgamgulmlem5  27164  lgamgulmlem6  27165  lgamgulm2  27167  lgambdd  27168  lgamucov  27169  lgamcvg2  27186  gamcvg  27187  gamcvg2lem  27190  regamcl  27192  relgamcl  27193  lgam1  27195  iprodgam  27651  faclimlem1  27694  faclimlem3  27696  faclim  27697  iprodfac  27698  heiborlem3  28861  heiborlem5  28863  heiborlem6  28864  heiborlem7  28865  heiborlem8  28866  heibor  28869  rrndstprj2  28879  rrncmslem  28880  rrnequiv  28883  irrapxlem5  29316  pell14qrgapw  29366  pellqrexplicit  29367  pellqrex  29369  pellfundge  29372  pellfundgt1  29373  jm3.1lem1  29515  jm3.1lem2  29516  stoweidlem31  29975  stoweidlem59  30003  wallispilem3  30011  wallispi  30014  stirlinglem12  30029  stirlinglem15  30032  powm2modprm  30397  clwwisshclwwlem1  30618  numclwwlk5  30854  numclwwlk7  30856
  Copyright terms: Public domain W3C validator