Theorem nnrpd 13075

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℕcn 12266  ℝ⁺crp 13034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-rp 13035

This theorem is referenced by:  zgt1rpn0n1  13076  modmulnn  13929  mulp1mod1  13952  modsumfzodifsn  13985  addmodlteq  13987  nnesq  14266  digit1  14276  bcpasc  14360  cshwn  14835  iseralt  15721  climcndslem2  15886  mertenslem1  15920  mertenslem2  15921  fprodmodd  16033  efcllem  16113  ege2le3  16126  eftlub  16145  effsumlt  16147  eirrlem  16240  sqrt2irrlem  16284  p1modz1  16297  dvdsmod  16366  bitsfzo  16472  bitsmod  16473  bitscmp  16475  bitsinv1lem  16478  sadaddlem  16503  sadasslem  16507  bitsres  16510  smumul  16530  bezoutlem3  16578  eucalglt  16622  prmind2  16722  prmdvdsbc  16763  crth  16815  eulerthlem2  16819  fermltl  16821  prmdiv  16822  prmdiveq  16823  odzdvds  16833  vfermltlALT  16840  powm2modprm  16841  modprm0  16843  modprmn0modprm0  16845  prmreclem3  16956  prmreclem5  16958  prmreclem6  16959  4sqlem5  16980  4sqlem6  16981  4sqlem7  16982  4sqlem10  16985  4sqlem12  16994  vdwlem1  17019  mndodcong  19560  odmod  19564  oddvds  19565  dfod2  19582  gexexlem  19870  zringlpirlem3  21475  fermltlchr  21544  met1stc  24534  met2ndci  24535  lebnumlem3  24995  lebnumii  24998  ovollb2lem  25523  ovoliunlem1  25537  ovoliunlem3  25539  uniioombllem6  25623  itg2cnlem2  25797  elqaalem2  26362  aalioulem2  26375  aalioulem4  26377  aalioulem5  26378  aaliou2b  26383  aaliou3lem9  26392  logfac  26643  cxpeq  26800  zrtelqelz  26801  rtprmirr  26803  logbgcd1irr  26837  leibpi  26985  birthdaylem2  26995  amgmlem  27033  emcllem1  27039  emcllem2  27040  emcllem3  27041  emcllem5  27043  harmoniclbnd  27052  harmonicubnd  27053  harmonicbnd4  27054  fsumharmonic  27055  zetacvg  27058  lgamgulmlem2  27073  lgamgulmlem3  27074  lgamgulmlem4  27075  lgamgulmlem5  27076  lgamgulmlem6  27077  lgamgulm2  27079  lgambdd  27080  lgamucov  27081  lgamcvg2  27098  gamcvg  27099  gamcvg2lem  27102  regamcl  27104  relgamcl  27105  lgam1  27107  wilthlem1  27111  wilthlem2  27112  basellem1  27124  basellem6  27129  basellem8  27131  chtf  27151  efchtcl  27154  chtge0  27155  vmacl  27161  efvmacl  27163  sgmnncl  27190  chtprm  27196  chtdif  27201  efchtdvds  27202  prmorcht  27221  sgmppw  27241  vmalelog  27249  chtleppi  27254  chtublem  27255  fsumvma2  27258  pclogsum  27259  vmasum  27260  chpchtsum  27263  chpub  27264  logfacubnd  27265  logfaclbnd  27266  logfacbnd3  27267  logfacrlim  27268  logexprlim  27269  logfacrlim2  27270  perfectlem2  27274  bclbnd  27324  bposlem1  27328  bposlem2  27329  bposlem4  27331  bposlem5  27332  bposlem6  27333  bposlem7  27334  bposlem9  27336  lgslem1  27341  lgsvalmod  27360  lgsmod  27367  lgsdirprm  27375  lgsne0  27379  lgsqrlem2  27391  gausslemma2dlem0i  27408  gausslemma2dlem5a  27414  gausslemma2d  27418  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem3  27421  lgseisenlem4  27422  lgseisen  27423  lgsquadlem2  27425  lgsquadlem3  27426  m1lgs  27432  2sqlem8  27470  2sqmod  27480  chebbnd1lem1  27513  chebbnd1lem2  27514  chebbnd1lem3  27515  chebbnd1  27516  chtppilimlem1  27517  chtppilimlem2  27518  chtppilim  27519  chebbnd2  27521  chto1lb  27522  vmadivsum  27526  vmadivsumb  27527  rplogsumlem1  27528  rplogsumlem2  27529  dchrisum0lem1a  27530  rpvmasumlem  27531  dchrisumlema  27532  dchrisumlem1  27533  dchrisumlem2  27534  dchrmusum2  27538  dchrvmasumlem1  27539  dchrvmasum2lem  27540  dchrvmasum2if  27541  dchrvmasumlem2  27542  dchrvmasumlem3  27543  dchrvmasumiflem1  27545  dchrvmasumiflem2  27546  dchrisum0flblem2  27553  dchrisum0fno1  27555  dchrisum0lema  27558  dchrisum0lem1b  27559  dchrisum0lem1  27560  dchrisum0lem2a  27561  dchrisum0lem2  27562  dchrisum0lem3  27563  dchrisum0  27564  dirith2  27572  mudivsum  27574  mulogsumlem  27575  mulogsum  27576  mulog2sumlem1  27578  mulog2sumlem2  27579  mulog2sumlem3  27580  vmalogdivsum2  27582  vmalogdivsum  27583  2vmadivsumlem  27584  logsqvma  27586  log2sumbnd  27588  selberglem1  27589  selberglem2  27590  selberglem3  27591  selberg  27592  selbergb  27593  selberg2lem  27594  selberg2  27595  selberg2b  27596  chpdifbndlem1  27597  logdivbnd  27600  selberg3lem1  27601  selberg3lem2  27602  selberg3  27603  selberg4lem1  27604  selberg4  27605  pntrsumo1  27609  pntrsumbnd2  27611  selbergr  27612  selberg3r  27613  selberg4r  27614  selberg34r  27615  pntsf  27617  pntsval2  27620  pntrlog2bndlem1  27621  pntrlog2bndlem2  27622  pntrlog2bndlem3  27623  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntrlog2bndlem6  27627  pntrlog2bnd  27628  pntpbnd1a  27629  pntpbnd1  27630  pntpbnd2  27631  pntibndlem2  27635  pntlemn  27644  pntlemj  27647  pntlemf  27649  pntlemk  27650  pntlemo  27651  pnt  27658  padicabvcxp  27676  ostth2lem2  27678  ostth2lem3  27679  ostth2lem4  27680  ostth2  27681  ostth3  27682  clwwisshclwwslemlem  30032  numclwwlk5  30407  numclwwlk7  30410  nrt2irr  30492  ubthlem2  30890  minvecolem3  30895  lnconi  32052  ltesubnnd  32824  2exple2exp  32834  cshwrnid  32946  cycpmfv2  33134  znfermltl  33394  madjusmdetlem2  33827  eulerpartlemgc  34364  reprle  34629  hgt750lemc  34662  hgt750lemd  34663  hgt750lemb  34671  hgt750leme  34673  tgoldbachgtde  34675  iprodgam  35742  faclimlem1  35743  faclimlem3  35745  faclim  35746  iprodfac  35747  knoppndvlem17  36529  poimirlem29  37656  heiborlem3  37820  heiborlem5  37822  heiborlem6  37823  heiborlem7  37824  heiborlem8  37825  heibor  37828  rrndstprj2  37838  rrncmslem  37839  rrnequiv  37842  lcmineqlem20  42049  lcmineqlem23  42052  3lexlogpow5ineq2  42056  3lexlogpow2ineq2  42060  aks4d1p5  42081  aks4d1p6  42082  aks4d1p8d2  42086  aks4d1p8  42088  remexz  42105  hashscontpow1  42122  aks6d1c2lem4  42128  aks6d1c2  42131  bcled  42179  bcle2d  42180  aks6d1c7lem1  42181  metakunt18  42223  metakunt30  42235  dvdsexpnn  42368  fltne  42654  flt4lem7  42669  fltltc  42671  fltnltalem  42672  fltnlta  42673  irrapxlem5  42837  pell14qrgapw  42887  pellqrexplicit  42888  pellqrex  42890  pellfundge  42893  pellfundgt1  42894  jm3.1lem1  43029  jm3.1lem2  43030  hashnzfz2  44340  xralrple4  45384  recnnltrp  45388  rpgtrecnn  45391  fsumnncl  45587  limsup10exlem  45787  stoweidlem31  46046  stoweidlem59  46074  wallispilem3  46082  wallispi  46085  stirlinglem12  46100  stirlinglem15  46103  fourierdlem73  46194  etransclem23  46272  nnfoctbdjlem  46470  ovnsubaddlem1  46585  ovolval5lem1  46667  ovolval5lem2  46668  vonioolem1  46695  vonioolem2  46696  vonicclem2  46699  fmtnoprmfac1lem  47551  sfprmdvdsmersenne  47590  lighneallem2  47593  proththd  47601  perfectALTVlem2  47709  fppr2odd  47718  fpprwppr  47726  fpprel2  47728  gpgedgvtx1  48020  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx13starlem2  48028  gpg3nbgrvtx0  48032  pw2m1lepw2m1  48437  logbge0b  48484  logblt1b  48485  logbpw2m1  48488  nnpw2pmod  48504  nnolog2flm1  48511  blennngt2o2  48513  dignnld  48524  digexp  48528  amgmlemALT  49322