Theorem nnrpd 13035

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

Syntax hints:   → wi 4   ∈ wcel 2142  ℕcn 12210  ℝ⁺crp 12993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149  ax-pre-mulgt0 11150

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-sub 11416  df-neg 11417  df-nn 12211  df-rp 12994

This theorem is referenced by:  zgt1rpn0n1  13036  modmulnn  13899  modaddid  13920  mulp1mod1  13924  modsumfzodifsn  13957  addmodlteq  13959  nnesq  14240  digit1  14250  bcpasc  14334  cshwn  14810  iseralt  15712  climcndslem2  15880  mertenslem1  15914  mertenslem2  15915  fprodmodd  16027  efcllem  16107  ege2le3  16120  eftlub  16141  effsumlt  16143  eirrlem  16236  sqrt2irrlem  16280  p1modz1  16293  dvdsmod  16363  bitsfzo  16469  bitsmod  16470  bitscmp  16472  bitsinv1lem  16475  sadaddlem  16500  sadasslem  16504  bitsres  16507  smumul  16527  bezoutlem3  16575  eucalglt  16619  prmind2  16719  prmdvdsbc  16761  crth  16813  eulerthlem2  16817  fermltl  16819  prmdiv  16820  prmdiveq  16821  odzdvds  16831  vfermltlALT  16838  powm2modprm  16839  modprm0  16841  modprmn0modprm0  16843  prmreclem3  16954  prmreclem5  16956  prmreclem6  16957  4sqlem5  16978  4sqlem6  16979  4sqlem7  16980  4sqlem10  16983  4sqlem12  16992  vdwlem1  17017  mndodcong  19582  odmod  19586  oddvds  19587  dfod2  19604  gexexlem  19892  zringlpirlem3  21516  fermltlchr  21581  met1stc  24581  met2ndci  24582  lebnumlem3  25025  lebnumii  25028  ovollb2lem  25550  ovoliunlem1  25564  ovoliunlem3  25566  uniioombllem6  25650  itg2cnlem2  25824  elqaalem2  26384  aalioulem2  26397  aalioulem4  26399  aalioulem5  26400  aaliou2b  26405  aaliou3lem9  26414  logfac  26666  cxpeq  26822  zrtelqelz  26823  rtprmirr  26825  logbgcd1irr  26859  leibpi  27007  birthdaylem2  27017  amgmlem  27054  emcllem1  27060  emcllem2  27061  emcllem3  27062  emcllem5  27064  harmoniclbnd  27073  harmonicubnd  27074  harmonicbnd4  27075  fsumharmonic  27076  zetacvg  27079  lgamgulmlem2  27094  lgamgulmlem3  27095  lgamgulmlem4  27096  lgamgulmlem5  27097  lgamgulmlem6  27098  lgamgulm2  27100  lgambdd  27101  lgamucov  27102  lgamcvg2  27119  gamcvg  27120  gamcvg2lem  27123  regamcl  27125  relgamcl  27126  lgam1  27128  wilthlem1  27132  wilthlem2  27133  basellem1  27145  basellem6  27150  basellem8  27152  chtf  27172  efchtcl  27175  chtge0  27176  vmacl  27182  efvmacl  27184  sgmnncl  27211  chtprm  27217  chtdif  27222  efchtdvds  27223  prmorcht  27242  sgmppw  27261  vmalelog  27269  chtleppi  27274  chtublem  27275  fsumvma2  27278  pclogsum  27279  vmasum  27280  chpchtsum  27283  chpub  27284  logfacubnd  27285  logfaclbnd  27286  logfacbnd3  27287  logfacrlim  27288  logexprlim  27289  logfacrlim2  27290  perfectlem2  27294  bclbnd  27344  bposlem1  27348  bposlem2  27349  bposlem4  27351  bposlem5  27352  bposlem6  27353  bposlem7  27354  bposlem9  27356  lgslem1  27361  lgsvalmod  27380  lgsmod  27387  lgsdirprm  27395  lgsne0  27399  lgsqrlem2  27411  gausslemma2dlem0i  27428  gausslemma2dlem5a  27434  gausslemma2d  27438  lgseisenlem1  27439  lgseisenlem2  27440  lgseisenlem3  27441  lgseisenlem4  27442  lgseisen  27443  lgsquadlem2  27445  lgsquadlem3  27446  m1lgs  27452  2sqlem8  27490  2sqmod  27500  chebbnd1lem1  27533  chebbnd1lem2  27534  chebbnd1lem3  27535  chebbnd1  27536  chtppilimlem1  27537  chtppilimlem2  27538  chtppilim  27539  chebbnd2  27541  chto1lb  27542  vmadivsum  27546  vmadivsumb  27547  rplogsumlem1  27548  rplogsumlem2  27549  dchrisum0lem1a  27550  rpvmasumlem  27551  dchrisumlema  27552  dchrisumlem1  27553  dchrisumlem2  27554  dchrmusum2  27558  dchrvmasumlem1  27559  dchrvmasum2lem  27560  dchrvmasum2if  27561  dchrvmasumlem2  27562  dchrvmasumlem3  27563  dchrvmasumiflem1  27565  dchrvmasumiflem2  27566  dchrisum0flblem2  27573  dchrisum0fno1  27575  dchrisum0lema  27578  dchrisum0lem1b  27579  dchrisum0lem1  27580  dchrisum0lem2a  27581  dchrisum0lem2  27582  dchrisum0lem3  27583  dchrisum0  27584  dirith2  27592  mudivsum  27594  mulogsumlem  27595  mulogsum  27596  mulog2sumlem1  27598  mulog2sumlem2  27599  mulog2sumlem3  27600  vmalogdivsum2  27602  vmalogdivsum  27603  2vmadivsumlem  27604  logsqvma  27606  log2sumbnd  27608  selberglem1  27609  selberglem2  27610  selberglem3  27611  selberg  27612  selbergb  27613  selberg2lem  27614  selberg2  27615  selberg2b  27616  chpdifbndlem1  27617  logdivbnd  27620  selberg3lem1  27621  selberg3lem2  27622  selberg3  27623  selberg4lem1  27624  selberg4  27625  pntrsumo1  27629  pntrsumbnd2  27631  selbergr  27632  selberg3r  27633  selberg4r  27634  selberg34r  27635  pntsf  27637  pntsval2  27640  pntrlog2bndlem1  27641  pntrlog2bndlem2  27642  pntrlog2bndlem3  27643  pntrlog2bndlem4  27644  pntrlog2bndlem5  27645  pntrlog2bndlem6  27647  pntrlog2bnd  27648  pntpbnd1a  27649  pntpbnd1  27650  pntpbnd2  27651  pntibndlem2  27655  pntlemn  27664  pntlemj  27667  pntlemf  27669  pntlemk  27670  pntlemo  27671  pnt  27678  padicabvcxp  27696  ostth2lem2  27698  ostth2lem3  27699  ostth2lem4  27700  ostth2  27701  ostth3  27702  clwwisshclwwslemlem  30215  numclwwlk5  30590  numclwwlk7  30593  nrt2irr  30675  ubthlem2  31074  minvecolem3  31079  lnconi  32236  ltesubnnd  33025  2exple2exp  33036  cshwrnid  33139  cycpmfv2  33294  znfermltl  33552  madjusmdetlem2  34125  eulerpartlemgc  34659  reprle  34908  hgt750lemc  34941  hgt750lemd  34942  hgt750lemb  34950  hgt750leme  34952  tgoldbachgtde  34954  iprodgam  36092  faclimlem1  36093  faclimlem3  36095  faclim  36096  iprodfac  36097  knoppndvlem17  36966  poimirlem29  38148  heiborlem3  38312  heiborlem5  38314  heiborlem6  38315  heiborlem7  38316  heiborlem8  38317  heibor  38320  rrndstprj2  38330  rrncmslem  38331  rrnequiv  38334  lcmineqlem20  42665  lcmineqlem23  42668  3lexlogpow5ineq2  42672  3lexlogpow2ineq2  42676  aks4d1p5  42697  aks4d1p6  42698  aks4d1p8d2  42702  aks4d1p8  42704  remexz  42721  hashscontpow1  42738  aks6d1c2lem4  42744  aks6d1c2  42747  bcled  42795  bcle2d  42796  aks6d1c7lem1  42797  dvdsexpnn  42942  fltne  43226  flt4lem7  43241  fltltc  43243  fltnltalem  43244  fltnlta  43245  irrapxlem5  43403  pell14qrgapw  43453  pellqrexplicit  43454  pellqrex  43456  pellfundge  43459  pellfundgt1  43460  jm3.1lem1  43594  jm3.1lem2  43595  hashnzfz2  44897  xralrple4  45948  recnnltrp  45952  rpgtrecnn  45955  fsumnncl  46148  limsup10exlem  46346  stoweidlem31  46605  stoweidlem59  46633  wallispilem3  46641  wallispi  46644  stirlinglem12  46659  stirlinglem15  46662  fourierdlem73  46753  etransclem23  46831  nnfoctbdjlem  47029  ovnsubaddlem1  47144  ovolval5lem1  47226  ovolval5lem2  47227  vonioolem1  47254  vonioolem2  47255  vonicclem2  47258  2timesltsqm1  47973  fmtnoprmfac1lem  48173  sfprmdvdsmersenne  48212  lighneallem2  48215  proththd  48223  perfectALTVlem2  48344  fppr2odd  48353  fpprwppr  48361  fpprel2  48363  gpgedgvtx1  48684  gpg5nbgrvtx03starlem2  48691  gpg5nbgrvtx13starlem2  48694  gpg3nbgrvtx0  48698  pw2m1lepw2m1  49142  logbge0b  49185  logblt1b  49186  logbpw2m1  49189  nnpw2pmod  49205  nnolog2flm1  49212  blennngt2o2  49214  dignnld  49225  digexp  49229  amgmlemALT  50424