Theorem nnrpd 12945

Description: A positive integer is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
nnrpd.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nnrpd	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Proof of Theorem nnrpd

Step	Hyp	Ref	Expression
1		nnrpd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
2		nnrp 12915	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2113  ℕcn 12143  ℝ⁺crp 12903

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100  ax-pre-mulgt0 11101

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 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8882  df-dom 8883  df-sdom 8884  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170  df-sub 11364  df-neg 11365  df-nn 12144  df-rp 12904

This theorem is referenced by:  zgt1rpn0n1  12946  modmulnn  13807  modaddid  13828  mulp1mod1  13832  modsumfzodifsn  13865  addmodlteq  13867  nnesq  14148  digit1  14158  bcpasc  14242  cshwn  14718  iseralt  15606  climcndslem2  15771  mertenslem1  15805  mertenslem2  15806  fprodmodd  15918  efcllem  15998  ege2le3  16011  eftlub  16032  effsumlt  16034  eirrlem  16127  sqrt2irrlem  16171  p1modz1  16184  dvdsmod  16254  bitsfzo  16360  bitsmod  16361  bitscmp  16363  bitsinv1lem  16366  sadaddlem  16391  sadasslem  16395  bitsres  16398  smumul  16418  bezoutlem3  16466  eucalglt  16510  prmind2  16610  prmdvdsbc  16651  crth  16703  eulerthlem2  16707  fermltl  16709  prmdiv  16710  prmdiveq  16711  odzdvds  16721  vfermltlALT  16728  powm2modprm  16729  modprm0  16731  modprmn0modprm0  16733  prmreclem3  16844  prmreclem5  16846  prmreclem6  16847  4sqlem5  16868  4sqlem6  16869  4sqlem7  16870  4sqlem10  16873  4sqlem12  16882  vdwlem1  16907  mndodcong  19469  odmod  19473  oddvds  19474  dfod2  19491  gexexlem  19779  zringlpirlem3  21417  fermltlchr  21482  met1stc  24463  met2ndci  24464  lebnumlem3  24916  lebnumii  24919  ovollb2lem  25443  ovoliunlem1  25457  ovoliunlem3  25459  uniioombllem6  25543  itg2cnlem2  25717  elqaalem2  26282  aalioulem2  26295  aalioulem4  26297  aalioulem5  26298  aaliou2b  26303  aaliou3lem9  26312  logfac  26564  cxpeq  26721  zrtelqelz  26722  rtprmirr  26724  logbgcd1irr  26758  leibpi  26906  birthdaylem2  26916  amgmlem  26954  emcllem1  26960  emcllem2  26961  emcllem3  26962  emcllem5  26964  harmoniclbnd  26973  harmonicubnd  26974  harmonicbnd4  26975  fsumharmonic  26976  zetacvg  26979  lgamgulmlem2  26994  lgamgulmlem3  26995  lgamgulmlem4  26996  lgamgulmlem5  26997  lgamgulmlem6  26998  lgamgulm2  27000  lgambdd  27001  lgamucov  27002  lgamcvg2  27019  gamcvg  27020  gamcvg2lem  27023  regamcl  27025  relgamcl  27026  lgam1  27028  wilthlem1  27032  wilthlem2  27033  basellem1  27045  basellem6  27050  basellem8  27052  chtf  27072  efchtcl  27075  chtge0  27076  vmacl  27082  efvmacl  27084  sgmnncl  27111  chtprm  27117  chtdif  27122  efchtdvds  27123  prmorcht  27142  sgmppw  27162  vmalelog  27170  chtleppi  27175  chtublem  27176  fsumvma2  27179  pclogsum  27180  vmasum  27181  chpchtsum  27184  chpub  27185  logfacubnd  27186  logfaclbnd  27187  logfacbnd3  27188  logfacrlim  27189  logexprlim  27190  logfacrlim2  27191  perfectlem2  27195  bclbnd  27245  bposlem1  27249  bposlem2  27250  bposlem4  27252  bposlem5  27253  bposlem6  27254  bposlem7  27255  bposlem9  27257  lgslem1  27262  lgsvalmod  27281  lgsmod  27288  lgsdirprm  27296  lgsne0  27300  lgsqrlem2  27312  gausslemma2dlem0i  27329  gausslemma2dlem5a  27335  gausslemma2d  27339  lgseisenlem1  27340  lgseisenlem2  27341  lgseisenlem3  27342  lgseisenlem4  27343  lgseisen  27344  lgsquadlem2  27346  lgsquadlem3  27347  m1lgs  27353  2sqlem8  27391  2sqmod  27401  chebbnd1lem1  27434  chebbnd1lem2  27435  chebbnd1lem3  27436  chebbnd1  27437  chtppilimlem1  27438  chtppilimlem2  27439  chtppilim  27440  chebbnd2  27442  chto1lb  27443  vmadivsum  27447  vmadivsumb  27448  rplogsumlem1  27449  rplogsumlem2  27450  dchrisum0lem1a  27451  rpvmasumlem  27452  dchrisumlema  27453  dchrisumlem1  27454  dchrisumlem2  27455  dchrmusum2  27459  dchrvmasumlem1  27460  dchrvmasum2lem  27461  dchrvmasum2if  27462  dchrvmasumlem2  27463  dchrvmasumlem3  27464  dchrvmasumiflem1  27466  dchrvmasumiflem2  27467  dchrisum0flblem2  27474  dchrisum0fno1  27476  dchrisum0lema  27479  dchrisum0lem1b  27480  dchrisum0lem1  27481  dchrisum0lem2a  27482  dchrisum0lem2  27483  dchrisum0lem3  27484  dchrisum0  27485  dirith2  27493  mudivsum  27495  mulogsumlem  27496  mulogsum  27497  mulog2sumlem1  27499  mulog2sumlem2  27500  mulog2sumlem3  27501  vmalogdivsum2  27503  vmalogdivsum  27504  2vmadivsumlem  27505  logsqvma  27507  log2sumbnd  27509  selberglem1  27510  selberglem2  27511  selberglem3  27512  selberg  27513  selbergb  27514  selberg2lem  27515  selberg2  27516  selberg2b  27517  chpdifbndlem1  27518  logdivbnd  27521  selberg3lem1  27522  selberg3lem2  27523  selberg3  27524  selberg4lem1  27525  selberg4  27526  pntrsumo1  27530  pntrsumbnd2  27532  selbergr  27533  selberg3r  27534  selberg4r  27535  selberg34r  27536  pntsf  27538  pntsval2  27541  pntrlog2bndlem1  27542  pntrlog2bndlem2  27543  pntrlog2bndlem3  27544  pntrlog2bndlem4  27545  pntrlog2bndlem5  27546  pntrlog2bndlem6  27548  pntrlog2bnd  27549  pntpbnd1a  27550  pntpbnd1  27551  pntpbnd2  27552  pntibndlem2  27556  pntlemn  27565  pntlemj  27568  pntlemf  27570  pntlemk  27571  pntlemo  27572  pnt  27579  padicabvcxp  27597  ostth2lem2  27599  ostth2lem3  27600  ostth2lem4  27601  ostth2  27602  ostth3  27603  clwwisshclwwslemlem  30037  numclwwlk5  30412  numclwwlk7  30415  nrt2irr  30497  ubthlem2  30895  minvecolem3  30900  lnconi  32057  ltesubnnd  32852  2exple2exp  32875  cshwrnid  32992  cycpmfv2  33145  znfermltl  33396  madjusmdetlem2  33934  eulerpartlemgc  34468  reprle  34720  hgt750lemc  34753  hgt750lemd  34754  hgt750lemb  34762  hgt750leme  34764  tgoldbachgtde  34766  iprodgam  35885  faclimlem1  35886  faclimlem3  35888  faclim  35889  iprodfac  35890  knoppndvlem17  36671  poimirlem29  37789  heiborlem3  37953  heiborlem5  37955  heiborlem6  37956  heiborlem7  37957  heiborlem8  37958  heibor  37961  rrndstprj2  37971  rrncmslem  37972  rrnequiv  37975  lcmineqlem20  42241  lcmineqlem23  42244  3lexlogpow5ineq2  42248  3lexlogpow2ineq2  42252  aks4d1p5  42273  aks4d1p6  42274  aks4d1p8d2  42278  aks4d1p8  42280  remexz  42297  hashscontpow1  42314  aks6d1c2lem4  42320  aks6d1c2  42323  bcled  42371  bcle2d  42372  aks6d1c7lem1  42373  dvdsexpnn  42530  fltne  42829  flt4lem7  42844  fltltc  42846  fltnltalem  42847  fltnlta  42848  irrapxlem5  43010  pell14qrgapw  43060  pellqrexplicit  43061  pellqrex  43063  pellfundge  43066  pellfundgt1  43067  jm3.1lem1  43201  jm3.1lem2  43202  hashnzfz2  44504  xralrple4  45559  recnnltrp  45563  rpgtrecnn  45566  fsumnncl  45760  limsup10exlem  45958  stoweidlem31  46217  stoweidlem59  46245  wallispilem3  46253  wallispi  46256  stirlinglem12  46271  stirlinglem15  46274  fourierdlem73  46365  etransclem23  46443  nnfoctbdjlem  46641  ovnsubaddlem1  46756  ovolval5lem1  46838  ovolval5lem2  46839  vonioolem1  46866  vonioolem2  46867  vonicclem2  46870  fmtnoprmfac1lem  47752  sfprmdvdsmersenne  47791  lighneallem2  47794  proththd  47802  perfectALTVlem2  47910  fppr2odd  47919  fpprwppr  47927  fpprel2  47929  gpgedgvtx1  48250  gpg5nbgrvtx03starlem2  48257  gpg5nbgrvtx13starlem2  48260  gpg3nbgrvtx0  48264  pw2m1lepw2m1  48708  logbge0b  48751  logblt1b  48752  logbpw2m1  48755  nnpw2pmod  48771  nnolog2flm1  48778  blennngt2o2  48780  dignnld  48791  digexp  48795  amgmlemALT  49990