Theorem nnrpd 12984

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 12954	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2114  ℕcn 12174  ℝ⁺crp 12942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-nn 12175  df-rp 12943

This theorem is referenced by:  zgt1rpn0n1  12985  modmulnn  13848  modaddid  13869  mulp1mod1  13873  modsumfzodifsn  13906  addmodlteq  13908  nnesq  14189  digit1  14199  bcpasc  14283  cshwn  14759  iseralt  15647  climcndslem2  15815  mertenslem1  15849  mertenslem2  15850  fprodmodd  15962  efcllem  16042  ege2le3  16055  eftlub  16076  effsumlt  16078  eirrlem  16171  sqrt2irrlem  16215  p1modz1  16228  dvdsmod  16298  bitsfzo  16404  bitsmod  16405  bitscmp  16407  bitsinv1lem  16410  sadaddlem  16435  sadasslem  16439  bitsres  16442  smumul  16462  bezoutlem3  16510  eucalglt  16554  prmind2  16654  prmdvdsbc  16696  crth  16748  eulerthlem2  16752  fermltl  16754  prmdiv  16755  prmdiveq  16756  odzdvds  16766  vfermltlALT  16773  powm2modprm  16774  modprm0  16776  modprmn0modprm0  16778  prmreclem3  16889  prmreclem5  16891  prmreclem6  16892  4sqlem5  16913  4sqlem6  16914  4sqlem7  16915  4sqlem10  16918  4sqlem12  16927  vdwlem1  16952  mndodcong  19517  odmod  19521  oddvds  19522  dfod2  19539  gexexlem  19827  zringlpirlem3  21444  fermltlchr  21509  met1stc  24486  met2ndci  24487  lebnumlem3  24930  lebnumii  24933  ovollb2lem  25455  ovoliunlem1  25469  ovoliunlem3  25471  uniioombllem6  25555  itg2cnlem2  25729  elqaalem2  26286  aalioulem2  26299  aalioulem4  26301  aalioulem5  26302  aaliou2b  26307  aaliou3lem9  26316  logfac  26565  cxpeq  26721  zrtelqelz  26722  rtprmirr  26724  logbgcd1irr  26758  leibpi  26906  birthdaylem2  26916  amgmlem  26953  emcllem1  26959  emcllem2  26960  emcllem3  26961  emcllem5  26963  harmoniclbnd  26972  harmonicubnd  26973  harmonicbnd4  26974  fsumharmonic  26975  zetacvg  26978  lgamgulmlem2  26993  lgamgulmlem3  26994  lgamgulmlem4  26995  lgamgulmlem5  26996  lgamgulmlem6  26997  lgamgulm2  26999  lgambdd  27000  lgamucov  27001  lgamcvg2  27018  gamcvg  27019  gamcvg2lem  27022  regamcl  27024  relgamcl  27025  lgam1  27027  wilthlem1  27031  wilthlem2  27032  basellem1  27044  basellem6  27049  basellem8  27051  chtf  27071  efchtcl  27074  chtge0  27075  vmacl  27081  efvmacl  27083  sgmnncl  27110  chtprm  27116  chtdif  27121  efchtdvds  27122  prmorcht  27141  sgmppw  27160  vmalelog  27168  chtleppi  27173  chtublem  27174  fsumvma2  27177  pclogsum  27178  vmasum  27179  chpchtsum  27182  chpub  27183  logfacubnd  27184  logfaclbnd  27185  logfacbnd3  27186  logfacrlim  27187  logexprlim  27188  logfacrlim2  27189  perfectlem2  27193  bclbnd  27243  bposlem1  27247  bposlem2  27248  bposlem4  27250  bposlem5  27251  bposlem6  27252  bposlem7  27253  bposlem9  27255  lgslem1  27260  lgsvalmod  27279  lgsmod  27286  lgsdirprm  27294  lgsne0  27298  lgsqrlem2  27310  gausslemma2dlem0i  27327  gausslemma2dlem5a  27333  gausslemma2d  27337  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem3  27340  lgseisenlem4  27341  lgseisen  27342  lgsquadlem2  27344  lgsquadlem3  27345  m1lgs  27351  2sqlem8  27389  2sqmod  27399  chebbnd1lem1  27432  chebbnd1lem2  27433  chebbnd1lem3  27434  chebbnd1  27435  chtppilimlem1  27436  chtppilimlem2  27437  chtppilim  27438  chebbnd2  27440  chto1lb  27441  vmadivsum  27445  vmadivsumb  27446  rplogsumlem1  27447  rplogsumlem2  27448  dchrisum0lem1a  27449  rpvmasumlem  27450  dchrisumlema  27451  dchrisumlem1  27452  dchrisumlem2  27453  dchrmusum2  27457  dchrvmasumlem1  27458  dchrvmasum2lem  27459  dchrvmasum2if  27460  dchrvmasumlem2  27461  dchrvmasumlem3  27462  dchrvmasumiflem1  27464  dchrvmasumiflem2  27465  dchrisum0flblem2  27472  dchrisum0fno1  27474  dchrisum0lema  27477  dchrisum0lem1b  27478  dchrisum0lem1  27479  dchrisum0lem2a  27480  dchrisum0lem2  27481  dchrisum0lem3  27482  dchrisum0  27483  dirith2  27491  mudivsum  27493  mulogsumlem  27494  mulogsum  27495  mulog2sumlem1  27497  mulog2sumlem2  27498  mulog2sumlem3  27499  vmalogdivsum2  27501  vmalogdivsum  27502  2vmadivsumlem  27503  logsqvma  27505  log2sumbnd  27507  selberglem1  27508  selberglem2  27509  selberglem3  27510  selberg  27511  selbergb  27512  selberg2lem  27513  selberg2  27514  selberg2b  27515  chpdifbndlem1  27516  logdivbnd  27519  selberg3lem1  27520  selberg3lem2  27521  selberg3  27522  selberg4lem1  27523  selberg4  27524  pntrsumo1  27528  pntrsumbnd2  27530  selbergr  27531  selberg3r  27532  selberg4r  27533  selberg34r  27534  pntsf  27536  pntsval2  27539  pntrlog2bndlem1  27540  pntrlog2bndlem2  27541  pntrlog2bndlem3  27542  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntrlog2bndlem6  27546  pntrlog2bnd  27547  pntpbnd1a  27548  pntpbnd1  27549  pntpbnd2  27550  pntibndlem2  27554  pntlemn  27563  pntlemj  27566  pntlemf  27568  pntlemk  27569  pntlemo  27570  pnt  27577  padicabvcxp  27595  ostth2lem2  27597  ostth2lem3  27598  ostth2lem4  27599  ostth2  27600  ostth3  27601  clwwisshclwwslemlem  30083  numclwwlk5  30458  numclwwlk7  30461  nrt2irr  30543  ubthlem2  30942  minvecolem3  30947  lnconi  32104  ltesubnnd  32896  2exple2exp  32918  cshwrnid  33021  cycpmfv2  33175  znfermltl  33426  madjusmdetlem2  33972  eulerpartlemgc  34506  reprle  34758  hgt750lemc  34791  hgt750lemd  34792  hgt750lemb  34800  hgt750leme  34802  tgoldbachgtde  34804  iprodgam  35924  faclimlem1  35925  faclimlem3  35927  faclim  35928  iprodfac  35929  knoppndvlem17  36788  poimirlem29  37970  heiborlem3  38134  heiborlem5  38136  heiborlem6  38137  heiborlem7  38138  heiborlem8  38139  heibor  38142  rrndstprj2  38152  rrncmslem  38153  rrnequiv  38156  lcmineqlem20  42487  lcmineqlem23  42490  3lexlogpow5ineq2  42494  3lexlogpow2ineq2  42498  aks4d1p5  42519  aks4d1p6  42520  aks4d1p8d2  42524  aks4d1p8  42526  remexz  42543  hashscontpow1  42560  aks6d1c2lem4  42566  aks6d1c2  42569  bcled  42617  bcle2d  42618  aks6d1c7lem1  42619  dvdsexpnn  42765  fltne  43077  flt4lem7  43092  fltltc  43094  fltnltalem  43095  fltnlta  43096  irrapxlem5  43254  pell14qrgapw  43304  pellqrexplicit  43305  pellqrex  43307  pellfundge  43310  pellfundgt1  43311  jm3.1lem1  43445  jm3.1lem2  43446  hashnzfz2  44748  xralrple4  45802  recnnltrp  45806  rpgtrecnn  45809  fsumnncl  46002  limsup10exlem  46200  stoweidlem31  46459  stoweidlem59  46487  wallispilem3  46495  wallispi  46498  stirlinglem12  46513  stirlinglem15  46516  fourierdlem73  46607  etransclem23  46685  nnfoctbdjlem  46883  ovnsubaddlem1  46998  ovolval5lem1  47080  ovolval5lem2  47081  vonioolem1  47108  vonioolem2  47109  vonicclem2  47112  2timesltsqm1  47827  fmtnoprmfac1lem  48027  sfprmdvdsmersenne  48066  lighneallem2  48069  proththd  48077  perfectALTVlem2  48198  fppr2odd  48207  fpprwppr  48215  fpprel2  48217  gpgedgvtx1  48538  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx13starlem2  48548  gpg3nbgrvtx0  48552  pw2m1lepw2m1  48996  logbge0b  49039  logblt1b  49040  logbpw2m1  49043  nnpw2pmod  49059  nnolog2flm1  49066  blennngt2o2  49068  dignnld  49079  digexp  49083  amgmlemALT  50278