Theorem nnrpd 12978

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℕcn 12168  ℝ⁺crp 12936

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 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7812  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-nn 12169  df-rp 12937

This theorem is referenced by:  zgt1rpn0n1  12979  modmulnn  13842  modaddid  13863  mulp1mod1  13867  modsumfzodifsn  13900  addmodlteq  13902  nnesq  14183  digit1  14193  bcpasc  14277  cshwn  14753  iseralt  15641  climcndslem2  15809  mertenslem1  15843  mertenslem2  15844  fprodmodd  15956  efcllem  16036  ege2le3  16049  eftlub  16070  effsumlt  16072  eirrlem  16165  sqrt2irrlem  16209  p1modz1  16222  dvdsmod  16292  bitsfzo  16398  bitsmod  16399  bitscmp  16401  bitsinv1lem  16404  sadaddlem  16429  sadasslem  16433  bitsres  16436  smumul  16456  bezoutlem3  16504  eucalglt  16548  prmind2  16648  prmdvdsbc  16690  crth  16742  eulerthlem2  16746  fermltl  16748  prmdiv  16749  prmdiveq  16750  odzdvds  16760  vfermltlALT  16767  powm2modprm  16768  modprm0  16770  modprmn0modprm0  16772  prmreclem3  16883  prmreclem5  16885  prmreclem6  16886  4sqlem5  16907  4sqlem6  16908  4sqlem7  16909  4sqlem10  16912  4sqlem12  16921  vdwlem1  16946  mndodcong  19511  odmod  19515  oddvds  19516  dfod2  19533  gexexlem  19821  zringlpirlem3  21457  fermltlchr  21522  met1stc  24499  met2ndci  24500  lebnumlem3  24943  lebnumii  24946  ovollb2lem  25468  ovoliunlem1  25482  ovoliunlem3  25484  uniioombllem6  25568  itg2cnlem2  25742  elqaalem2  26300  aalioulem2  26313  aalioulem4  26315  aalioulem5  26316  aaliou2b  26321  aaliou3lem9  26330  logfac  26581  cxpeq  26737  zrtelqelz  26738  rtprmirr  26740  logbgcd1irr  26774  leibpi  26922  birthdaylem2  26932  amgmlem  26970  emcllem1  26976  emcllem2  26977  emcllem3  26978  emcllem5  26980  harmoniclbnd  26989  harmonicubnd  26990  harmonicbnd4  26991  fsumharmonic  26992  zetacvg  26995  lgamgulmlem2  27010  lgamgulmlem3  27011  lgamgulmlem4  27012  lgamgulmlem5  27013  lgamgulmlem6  27014  lgamgulm2  27016  lgambdd  27017  lgamucov  27018  lgamcvg2  27035  gamcvg  27036  gamcvg2lem  27039  regamcl  27041  relgamcl  27042  lgam1  27044  wilthlem1  27048  wilthlem2  27049  basellem1  27061  basellem6  27066  basellem8  27068  chtf  27088  efchtcl  27091  chtge0  27092  vmacl  27098  efvmacl  27100  sgmnncl  27127  chtprm  27133  chtdif  27138  efchtdvds  27139  prmorcht  27158  sgmppw  27177  vmalelog  27185  chtleppi  27190  chtublem  27191  fsumvma2  27194  pclogsum  27195  vmasum  27196  chpchtsum  27199  chpub  27200  logfacubnd  27201  logfaclbnd  27202  logfacbnd3  27203  logfacrlim  27204  logexprlim  27205  logfacrlim2  27206  perfectlem2  27210  bclbnd  27260  bposlem1  27264  bposlem2  27265  bposlem4  27267  bposlem5  27268  bposlem6  27269  bposlem7  27270  bposlem9  27272  lgslem1  27277  lgsvalmod  27296  lgsmod  27303  lgsdirprm  27311  lgsne0  27315  lgsqrlem2  27327  gausslemma2dlem0i  27344  gausslemma2dlem5a  27350  gausslemma2d  27354  lgseisenlem1  27355  lgseisenlem2  27356  lgseisenlem3  27357  lgseisenlem4  27358  lgseisen  27359  lgsquadlem2  27361  lgsquadlem3  27362  m1lgs  27368  2sqlem8  27406  2sqmod  27416  chebbnd1lem1  27449  chebbnd1lem2  27450  chebbnd1lem3  27451  chebbnd1  27452  chtppilimlem1  27453  chtppilimlem2  27454  chtppilim  27455  chebbnd2  27457  chto1lb  27458  vmadivsum  27462  vmadivsumb  27463  rplogsumlem1  27464  rplogsumlem2  27465  dchrisum0lem1a  27466  rpvmasumlem  27467  dchrisumlema  27468  dchrisumlem1  27469  dchrisumlem2  27470  dchrmusum2  27474  dchrvmasumlem1  27475  dchrvmasum2lem  27476  dchrvmasum2if  27477  dchrvmasumlem2  27478  dchrvmasumlem3  27479  dchrvmasumiflem1  27481  dchrvmasumiflem2  27482  dchrisum0flblem2  27489  dchrisum0fno1  27491  dchrisum0lema  27494  dchrisum0lem1b  27495  dchrisum0lem1  27496  dchrisum0lem2a  27497  dchrisum0lem2  27498  dchrisum0lem3  27499  dchrisum0  27500  dirith2  27508  mudivsum  27510  mulogsumlem  27511  mulogsum  27512  mulog2sumlem1  27514  mulog2sumlem2  27515  mulog2sumlem3  27516  vmalogdivsum2  27518  vmalogdivsum  27519  2vmadivsumlem  27520  logsqvma  27522  log2sumbnd  27524  selberglem1  27525  selberglem2  27526  selberglem3  27527  selberg  27528  selbergb  27529  selberg2lem  27530  selberg2  27531  selberg2b  27532  chpdifbndlem1  27533  logdivbnd  27536  selberg3lem1  27537  selberg3lem2  27538  selberg3  27539  selberg4lem1  27540  selberg4  27541  pntrsumo1  27545  pntrsumbnd2  27547  selbergr  27548  selberg3r  27549  selberg4r  27550  selberg34r  27551  pntsf  27553  pntsval2  27556  pntrlog2bndlem1  27557  pntrlog2bndlem2  27558  pntrlog2bndlem3  27559  pntrlog2bndlem4  27560  pntrlog2bndlem5  27561  pntrlog2bndlem6  27563  pntrlog2bnd  27564  pntpbnd1a  27565  pntpbnd1  27566  pntpbnd2  27567  pntibndlem2  27571  pntlemn  27580  pntlemj  27583  pntlemf  27585  pntlemk  27586  pntlemo  27587  pnt  27594  padicabvcxp  27612  ostth2lem2  27614  ostth2lem3  27615  ostth2lem4  27616  ostth2  27617  ostth3  27618  clwwisshclwwslemlem  30101  numclwwlk5  30476  numclwwlk7  30479  nrt2irr  30561  ubthlem2  30960  minvecolem3  30965  lnconi  32122  ltesubnnd  32914  2exple2exp  32936  cshwrnid  33039  cycpmfv2  33193  znfermltl  33444  madjusmdetlem2  33991  eulerpartlemgc  34525  reprle  34777  hgt750lemc  34810  hgt750lemd  34811  hgt750lemb  34819  hgt750leme  34821  tgoldbachgtde  34823  iprodgam  35943  faclimlem1  35944  faclimlem3  35946  faclim  35947  iprodfac  35948  knoppndvlem17  36807  poimirlem29  37987  heiborlem3  38151  heiborlem5  38153  heiborlem6  38154  heiborlem7  38155  heiborlem8  38156  heibor  38159  rrndstprj2  38169  rrncmslem  38170  rrnequiv  38173  lcmineqlem20  42504  lcmineqlem23  42507  3lexlogpow5ineq2  42511  3lexlogpow2ineq2  42515  aks4d1p5  42536  aks4d1p6  42537  aks4d1p8d2  42541  aks4d1p8  42543  remexz  42560  hashscontpow1  42577  aks6d1c2lem4  42583  aks6d1c2  42586  bcled  42634  bcle2d  42635  aks6d1c7lem1  42636  dvdsexpnn  42782  fltne  43094  flt4lem7  43109  fltltc  43111  fltnltalem  43112  fltnlta  43113  irrapxlem5  43275  pell14qrgapw  43325  pellqrexplicit  43326  pellqrex  43328  pellfundge  43331  pellfundgt1  43332  jm3.1lem1  43466  jm3.1lem2  43467  hashnzfz2  44769  xralrple4  45823  recnnltrp  45827  rpgtrecnn  45830  fsumnncl  46023  limsup10exlem  46221  stoweidlem31  46480  stoweidlem59  46508  wallispilem3  46516  wallispi  46519  stirlinglem12  46534  stirlinglem15  46537  fourierdlem73  46628  etransclem23  46706  nnfoctbdjlem  46904  ovnsubaddlem1  47019  ovolval5lem1  47101  ovolval5lem2  47102  vonioolem1  47129  vonioolem2  47130  vonicclem2  47133  2timesltsqm1  47842  fmtnoprmfac1lem  48042  sfprmdvdsmersenne  48081  lighneallem2  48084  proththd  48092  perfectALTVlem2  48213  fppr2odd  48222  fpprwppr  48230  fpprel2  48232  gpgedgvtx1  48553  gpg5nbgrvtx03starlem2  48560  gpg5nbgrvtx13starlem2  48563  gpg3nbgrvtx0  48567  pw2m1lepw2m1  49011  logbge0b  49054  logblt1b  49055  logbpw2m1  49058  nnpw2pmod  49074  nnolog2flm1  49081  blennngt2o2  49083  dignnld  49094  digexp  49098  amgmlemALT  50293