Theorem nnrpd 13053

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℕcn 12228  ℝ⁺crp 13011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-nn 12229  df-rp 13012

This theorem is referenced by:  zgt1rpn0n1  13054  modmulnn  13918  modaddid  13939  mulp1mod1  13943  modsumfzodifsn  13976  addmodlteq  13978  nnesq  14259  digit1  14269  bcpasc  14353  cshwn  14830  iseralt  15732  climcndslem2  15900  mertenslem1  15934  mertenslem2  15935  fprodmodd  16047  efcllem  16126  ege2le3  16139  eftlub  16160  effsumlt  16162  eirrlem  16255  sqrt2irrlem  16299  p1modz1  16312  dvdsmod  16382  bitsfzo  16488  bitsmod  16489  bitscmp  16491  bitsinv1lem  16494  sadaddlem  16519  sadasslem  16523  bitsres  16526  smumul  16546  bezoutlem3  16594  eucalglt  16638  prmind2  16738  prmdvdsbc  16780  crth  16832  eulerthlem2  16836  fermltl  16838  prmdiv  16839  prmdiveq  16840  odzdvds  16850  vfermltlALT  16857  powm2modprm  16858  modprm0  16860  modprmn0modprm0  16862  prmreclem3  16973  prmreclem5  16975  prmreclem6  16976  4sqlem5  16997  4sqlem6  16998  4sqlem7  16999  4sqlem10  17002  4sqlem12  17011  vdwlem1  17036  mndodcong  19607  odmod  19611  oddvds  19612  dfod2  19629  gexexlem  19917  zringlpirlem3  21614  fermltlchr  21679  met1stc  24678  met2ndci  24679  lebnumlem3  25122  lebnumii  25125  ovollb2lem  25647  ovoliunlem1  25661  ovoliunlem3  25663  uniioombllem6  25747  itg2cnlem2  25921  elqaalem2  26481  aalioulem2  26496  aalioulem4  26498  aalioulem5  26499  aaliou2b  26504  aaliou3lem9  26513  logfac  26766  cxpeq  26922  zrtelqelz  26923  rtprmirr  26925  logbgcd1irr  26959  leibpi  27107  birthdaylem2  27117  amgmlem  27154  emcllem1  27160  emcllem2  27161  emcllem3  27162  emcllem5  27164  harmoniclbnd  27173  harmonicubnd  27174  harmonicbnd4  27175  fsumharmonic  27176  zetacvg  27179  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamgulmlem4  27196  lgamgulmlem5  27197  lgamgulmlem6  27198  lgamgulm2  27200  lgambdd  27201  lgamucov  27202  lgamcvg2  27219  gamcvg  27220  gamcvg2lem  27223  regamcl  27225  relgamcl  27226  lgam1  27228  wilthlem1  27232  wilthlem2  27233  basellem1  27245  basellem6  27250  basellem8  27252  chtf  27272  efchtcl  27275  chtge0  27276  vmacl  27282  efvmacl  27284  sgmnncl  27311  chtprm  27317  chtdif  27322  efchtdvds  27323  prmorcht  27342  sgmppw  27361  vmalelog  27369  chtleppi  27374  chtublem  27375  fsumvma2  27378  pclogsum  27379  vmasum  27380  chpchtsum  27383  chpub  27384  logfacubnd  27385  logfaclbnd  27386  logfacbnd3  27387  logfacrlim  27388  logexprlim  27389  logfacrlim2  27390  perfectlem2  27394  bclbnd  27444  bposlem1  27448  bposlem2  27449  bposlem4  27451  bposlem5  27452  bposlem6  27453  bposlem7  27454  bposlem9  27456  lgslem1  27461  lgsvalmod  27480  lgsmod  27487  lgsdirprm  27495  lgsne0  27499  lgsqrlem2  27511  gausslemma2dlem0i  27528  gausslemma2dlem5a  27534  gausslemma2d  27538  lgseisenlem1  27539  lgseisenlem2  27540  lgseisenlem3  27541  lgseisenlem4  27542  lgseisen  27543  lgsquadlem2  27545  lgsquadlem3  27546  m1lgs  27552  2sqlem8  27590  2sqmod  27600  chebbnd1lem1  27633  chebbnd1lem2  27634  chebbnd1lem3  27635  chebbnd1  27636  chtppilimlem1  27637  chtppilimlem2  27638  chtppilim  27639  chebbnd2  27641  chto1lb  27642  vmadivsum  27646  vmadivsumb  27647  rplogsumlem1  27648  rplogsumlem2  27649  dchrisum0lem1a  27650  rpvmasumlem  27651  dchrisumlema  27652  dchrisumlem1  27653  dchrisumlem2  27654  dchrmusum2  27658  dchrvmasumlem1  27659  dchrvmasum2lem  27660  dchrvmasum2if  27661  dchrvmasumlem2  27662  dchrvmasumlem3  27663  dchrvmasumiflem1  27665  dchrvmasumiflem2  27666  dchrisum0flblem2  27673  dchrisum0fno1  27675  dchrisum0lema  27678  dchrisum0lem1b  27679  dchrisum0lem1  27680  dchrisum0lem2a  27681  dchrisum0lem2  27682  dchrisum0lem3  27683  dchrisum0  27684  dirith2  27692  mudivsum  27694  mulogsumlem  27695  mulogsum  27696  mulog2sumlem1  27698  mulog2sumlem2  27699  mulog2sumlem3  27700  vmalogdivsum2  27702  vmalogdivsum  27703  2vmadivsumlem  27704  logsqvma  27706  log2sumbnd  27708  selberglem1  27709  selberglem2  27710  selberglem3  27711  selberg  27712  selbergb  27713  selberg2lem  27714  selberg2  27715  selberg2b  27716  chpdifbndlem1  27717  logdivbnd  27720  selberg3lem1  27721  selberg3lem2  27722  selberg3  27723  selberg4lem1  27724  selberg4  27725  pntrsumo1  27729  pntrsumbnd2  27731  selbergr  27732  selberg3r  27733  selberg4r  27734  selberg34r  27735  pntsf  27737  pntsval2  27740  pntrlog2bndlem1  27741  pntrlog2bndlem2  27742  pntrlog2bndlem3  27743  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  pntrlog2bndlem6  27747  pntrlog2bnd  27748  pntpbnd1a  27749  pntpbnd1  27750  pntpbnd2  27751  pntibndlem2  27755  pntlemn  27764  pntlemj  27767  pntlemf  27769  pntlemk  27770  pntlemo  27771  pnt  27778  padicabvcxp  27796  ostth2lem2  27798  ostth2lem3  27799  ostth2lem4  27800  ostth2  27801  ostth3  27802  clwwisshclwwslemlem  30364  numclwwlk5  30739  numclwwlk7  30742  nrt2irr  30824  ubthlem2  31223  minvecolem3  31228  lnconi  32385  ltesubnnd  33167  2exple2exp  33178  cshwrnid  33281  cycpmfv2  33434  znfermltl  33681  madjusmdetlem2  34218  eulerpartlemgc  34752  reprle  35001  hgt750lemc  35034  hgt750lemd  35035  hgt750lemb  35043  hgt750leme  35045  tgoldbachgtde  35047  iprodgam  36234  faclimlem1  36235  faclimlem3  36237  faclim  36238  iprodfac  36239  knoppndvlem17  37117  poimirlem29  38300  heiborlem3  38464  heiborlem5  38466  heiborlem6  38467  heiborlem7  38468  heiborlem8  38469  heibor  38472  rrndstprj2  38482  rrncmslem  38483  rrnequiv  38486  lcmineqlem20  42815  lcmineqlem23  42818  3lexlogpow5ineq2  42822  3lexlogpow2ineq2  42826  aks4d1p5  42847  aks4d1p6  42848  aks4d1p8d2  42852  aks4d1p8  42854  remexz  42871  hashscontpow1  42888  aks6d1c2lem4  42894  aks6d1c2  42897  bcled  42945  bcle2d  42946  aks6d1c7lem1  42947  dvdsexpnn  43094  fltne  43376  flt4lem7  43391  fltltc  43393  fltnltalem  43394  fltnlta  43395  irrapxlem5  43553  pell14qrgapw  43603  pellqrexplicit  43604  pellqrex  43606  pellfundge  43609  pellfundgt1  43610  jm3.1lem1  43744  jm3.1lem2  43745  hashnzfz2  45031  xralrple4  46088  recnnltrp  46092  rpgtrecnn  46095  fsumnncl  46288  limsup10exlem  46486  stoweidlem31  46745  stoweidlem59  46773  wallispilem3  46781  wallispi  46784  stirlinglem12  46799  stirlinglem15  46802  fourierdlem73  46893  etransclem23  46971  nnfoctbdjlem  47169  ovnsubaddlem1  47284  ovolval5lem1  47366  ovolval5lem2  47367  vonioolem1  47394  vonioolem2  47395  vonicclem2  47398  2timesltsqm1  48116  fmtnoprmfac1lem  48316  sfprmdvdsmersenne  48355  lighneallem2  48358  proththd  48366  perfectALTVlem2  48487  fppr2odd  48496  fpprwppr  48504  fpprel2  48506  gpgedgvtx1  48827  gpg5nbgrvtx03starlem2  48834  gpg5nbgrvtx13starlem2  48837  gpg3nbgrvtx0  48841  pw2m1lepw2m1  49300  logbge0b  49343  logblt1b  49344  logbpw2m1  49347  nnpw2pmod  49363  nnolog2flm1  49370  blennngt2o2  49372  dignnld  49383  digexp  49387  amgmlemALT  50623