Theorem nnrpd 12959

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℕcn 12157  ℝ⁺crp 12917

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 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  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 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 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-nn 12158  df-rp 12918

This theorem is referenced by:  zgt1rpn0n1  12960  modmulnn  13821  modaddid  13842  mulp1mod1  13846  modsumfzodifsn  13879  addmodlteq  13881  nnesq  14162  digit1  14172  bcpasc  14256  cshwn  14732  iseralt  15620  climcndslem2  15785  mertenslem1  15819  mertenslem2  15820  fprodmodd  15932  efcllem  16012  ege2le3  16025  eftlub  16046  effsumlt  16048  eirrlem  16141  sqrt2irrlem  16185  p1modz1  16198  dvdsmod  16268  bitsfzo  16374  bitsmod  16375  bitscmp  16377  bitsinv1lem  16380  sadaddlem  16405  sadasslem  16409  bitsres  16412  smumul  16432  bezoutlem3  16480  eucalglt  16524  prmind2  16624  prmdvdsbc  16665  crth  16717  eulerthlem2  16721  fermltl  16723  prmdiv  16724  prmdiveq  16725  odzdvds  16735  vfermltlALT  16742  powm2modprm  16743  modprm0  16745  modprmn0modprm0  16747  prmreclem3  16858  prmreclem5  16860  prmreclem6  16861  4sqlem5  16882  4sqlem6  16883  4sqlem7  16884  4sqlem10  16887  4sqlem12  16896  vdwlem1  16921  mndodcong  19483  odmod  19487  oddvds  19488  dfod2  19505  gexexlem  19793  zringlpirlem3  21431  fermltlchr  21496  met1stc  24477  met2ndci  24478  lebnumlem3  24930  lebnumii  24933  ovollb2lem  25457  ovoliunlem1  25471  ovoliunlem3  25473  uniioombllem6  25557  itg2cnlem2  25731  elqaalem2  26296  aalioulem2  26309  aalioulem4  26311  aalioulem5  26312  aaliou2b  26317  aaliou3lem9  26326  logfac  26578  cxpeq  26735  zrtelqelz  26736  rtprmirr  26738  logbgcd1irr  26772  leibpi  26920  birthdaylem2  26930  amgmlem  26968  emcllem1  26974  emcllem2  26975  emcllem3  26976  emcllem5  26978  harmoniclbnd  26987  harmonicubnd  26988  harmonicbnd4  26989  fsumharmonic  26990  zetacvg  26993  lgamgulmlem2  27008  lgamgulmlem3  27009  lgamgulmlem4  27010  lgamgulmlem5  27011  lgamgulmlem6  27012  lgamgulm2  27014  lgambdd  27015  lgamucov  27016  lgamcvg2  27033  gamcvg  27034  gamcvg2lem  27037  regamcl  27039  relgamcl  27040  lgam1  27042  wilthlem1  27046  wilthlem2  27047  basellem1  27059  basellem6  27064  basellem8  27066  chtf  27086  efchtcl  27089  chtge0  27090  vmacl  27096  efvmacl  27098  sgmnncl  27125  chtprm  27131  chtdif  27136  efchtdvds  27137  prmorcht  27156  sgmppw  27176  vmalelog  27184  chtleppi  27189  chtublem  27190  fsumvma2  27193  pclogsum  27194  vmasum  27195  chpchtsum  27198  chpub  27199  logfacubnd  27200  logfaclbnd  27201  logfacbnd3  27202  logfacrlim  27203  logexprlim  27204  logfacrlim2  27205  perfectlem2  27209  bclbnd  27259  bposlem1  27263  bposlem2  27264  bposlem4  27266  bposlem5  27267  bposlem6  27268  bposlem7  27269  bposlem9  27271  lgslem1  27276  lgsvalmod  27295  lgsmod  27302  lgsdirprm  27310  lgsne0  27314  lgsqrlem2  27326  gausslemma2dlem0i  27343  gausslemma2dlem5a  27349  gausslemma2d  27353  lgseisenlem1  27354  lgseisenlem2  27355  lgseisenlem3  27356  lgseisenlem4  27357  lgseisen  27358  lgsquadlem2  27360  lgsquadlem3  27361  m1lgs  27367  2sqlem8  27405  2sqmod  27415  chebbnd1lem1  27448  chebbnd1lem2  27449  chebbnd1lem3  27450  chebbnd1  27451  chtppilimlem1  27452  chtppilimlem2  27453  chtppilim  27454  chebbnd2  27456  chto1lb  27457  vmadivsum  27461  vmadivsumb  27462  rplogsumlem1  27463  rplogsumlem2  27464  dchrisum0lem1a  27465  rpvmasumlem  27466  dchrisumlema  27467  dchrisumlem1  27468  dchrisumlem2  27469  dchrmusum2  27473  dchrvmasumlem1  27474  dchrvmasum2lem  27475  dchrvmasum2if  27476  dchrvmasumlem2  27477  dchrvmasumlem3  27478  dchrvmasumiflem1  27480  dchrvmasumiflem2  27481  dchrisum0flblem2  27488  dchrisum0fno1  27490  dchrisum0lema  27493  dchrisum0lem1b  27494  dchrisum0lem1  27495  dchrisum0lem2a  27496  dchrisum0lem2  27497  dchrisum0lem3  27498  dchrisum0  27499  dirith2  27507  mudivsum  27509  mulogsumlem  27510  mulogsum  27511  mulog2sumlem1  27513  mulog2sumlem2  27514  mulog2sumlem3  27515  vmalogdivsum2  27517  vmalogdivsum  27518  2vmadivsumlem  27519  logsqvma  27521  log2sumbnd  27523  selberglem1  27524  selberglem2  27525  selberglem3  27526  selberg  27527  selbergb  27528  selberg2lem  27529  selberg2  27530  selberg2b  27531  chpdifbndlem1  27532  logdivbnd  27535  selberg3lem1  27536  selberg3lem2  27537  selberg3  27538  selberg4lem1  27539  selberg4  27540  pntrsumo1  27544  pntrsumbnd2  27546  selbergr  27547  selberg3r  27548  selberg4r  27549  selberg34r  27550  pntsf  27552  pntsval2  27555  pntrlog2bndlem1  27556  pntrlog2bndlem2  27557  pntrlog2bndlem3  27558  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntrlog2bndlem6  27562  pntrlog2bnd  27563  pntpbnd1a  27564  pntpbnd1  27565  pntpbnd2  27566  pntibndlem2  27570  pntlemn  27579  pntlemj  27582  pntlemf  27584  pntlemk  27585  pntlemo  27586  pnt  27593  padicabvcxp  27611  ostth2lem2  27613  ostth2lem3  27614  ostth2lem4  27615  ostth2  27616  ostth3  27617  clwwisshclwwslemlem  30100  numclwwlk5  30475  numclwwlk7  30478  nrt2irr  30560  ubthlem2  30959  minvecolem3  30964  lnconi  32121  ltesubnnd  32914  2exple2exp  32937  cshwrnid  33054  cycpmfv2  33208  znfermltl  33459  madjusmdetlem2  34006  eulerpartlemgc  34540  reprle  34792  hgt750lemc  34825  hgt750lemd  34826  hgt750lemb  34834  hgt750leme  34836  tgoldbachgtde  34838  iprodgam  35958  faclimlem1  35959  faclimlem3  35961  faclim  35962  iprodfac  35963  knoppndvlem17  36750  poimirlem29  37900  heiborlem3  38064  heiborlem5  38066  heiborlem6  38067  heiborlem7  38068  heiborlem8  38069  heibor  38072  rrndstprj2  38082  rrncmslem  38083  rrnequiv  38086  lcmineqlem20  42418  lcmineqlem23  42421  3lexlogpow5ineq2  42425  3lexlogpow2ineq2  42429  aks4d1p5  42450  aks4d1p6  42451  aks4d1p8d2  42455  aks4d1p8  42457  remexz  42474  hashscontpow1  42491  aks6d1c2lem4  42497  aks6d1c2  42500  bcled  42548  bcle2d  42549  aks6d1c7lem1  42550  dvdsexpnn  42703  fltne  43002  flt4lem7  43017  fltltc  43019  fltnltalem  43020  fltnlta  43021  irrapxlem5  43183  pell14qrgapw  43233  pellqrexplicit  43234  pellqrex  43236  pellfundge  43239  pellfundgt1  43240  jm3.1lem1  43374  jm3.1lem2  43375  hashnzfz2  44677  xralrple4  45731  recnnltrp  45735  rpgtrecnn  45738  fsumnncl  45932  limsup10exlem  46130  stoweidlem31  46389  stoweidlem59  46417  wallispilem3  46425  wallispi  46428  stirlinglem12  46443  stirlinglem15  46446  fourierdlem73  46537  etransclem23  46615  nnfoctbdjlem  46813  ovnsubaddlem1  46928  ovolval5lem1  47010  ovolval5lem2  47011  vonioolem1  47038  vonioolem2  47039  vonicclem2  47042  fmtnoprmfac1lem  47924  sfprmdvdsmersenne  47963  lighneallem2  47966  proththd  47974  perfectALTVlem2  48082  fppr2odd  48091  fpprwppr  48099  fpprel2  48101  gpgedgvtx1  48422  gpg5nbgrvtx03starlem2  48429  gpg5nbgrvtx13starlem2  48432  gpg3nbgrvtx0  48436  pw2m1lepw2m1  48880  logbge0b  48923  logblt1b  48924  logbpw2m1  48927  nnpw2pmod  48943  nnolog2flm1  48950  blennngt2o2  48952  dignnld  48963  digexp  48967  amgmlemALT  50162