Theorem nnrpd 12699

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℕcn 11903  ℝ⁺crp 12659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-nn 11904  df-rp 12660

This theorem is referenced by:  zgt1rpn0n1  12700  modmulnn  13537  mulp1mod1  13560  modsumfzodifsn  13592  addmodlteq  13594  nnesq  13870  digit1  13880  bcpasc  13963  cshwn  14438  iseralt  15324  climcndslem2  15490  mertenslem1  15524  mertenslem2  15525  fprodmodd  15635  efcllem  15715  ege2le3  15727  eftlub  15746  effsumlt  15748  eirrlem  15841  sqrt2irrlem  15885  p1modz1  15898  dvdsmod  15966  bitsfzo  16070  bitsmod  16071  bitscmp  16073  bitsinv1lem  16076  sadaddlem  16101  sadasslem  16105  bitsres  16108  smumul  16128  bezoutlem3  16177  eucalglt  16218  prmind2  16318  crth  16407  eulerthlem2  16411  fermltl  16413  prmdiv  16414  prmdiveq  16415  odzdvds  16424  vfermltlALT  16431  powm2modprm  16432  modprm0  16434  modprmn0modprm0  16436  prmreclem3  16547  prmreclem5  16549  prmreclem6  16550  4sqlem5  16571  4sqlem6  16572  4sqlem7  16573  4sqlem10  16576  4sqlem12  16585  vdwlem1  16610  mndodcong  19065  odmod  19069  oddvds  19070  dfod2  19086  gexexlem  19368  zringlpirlem3  20598  met1stc  23583  met2ndci  23584  lebnumlem3  24032  lebnumii  24035  ovollb2lem  24557  ovoliunlem1  24571  ovoliunlem3  24573  uniioombllem6  24657  itg2cnlem2  24832  elqaalem2  25385  aalioulem2  25398  aalioulem4  25400  aalioulem5  25401  aaliou2b  25406  aaliou3lem9  25415  logfac  25661  cxpeq  25815  logbgcd1irr  25849  leibpi  25997  birthdaylem2  26007  amgmlem  26044  emcllem1  26050  emcllem2  26051  emcllem3  26052  emcllem5  26054  harmoniclbnd  26063  harmonicubnd  26064  harmonicbnd4  26065  fsumharmonic  26066  zetacvg  26069  lgamgulmlem2  26084  lgamgulmlem3  26085  lgamgulmlem4  26086  lgamgulmlem5  26087  lgamgulmlem6  26088  lgamgulm2  26090  lgambdd  26091  lgamucov  26092  lgamcvg2  26109  gamcvg  26110  gamcvg2lem  26113  regamcl  26115  relgamcl  26116  lgam1  26118  wilthlem1  26122  wilthlem2  26123  basellem1  26135  basellem6  26140  basellem8  26142  chtf  26162  efchtcl  26165  chtge0  26166  vmacl  26172  efvmacl  26174  sgmnncl  26201  chtprm  26207  chtdif  26212  efchtdvds  26213  prmorcht  26232  sgmppw  26250  vmalelog  26258  chtleppi  26263  chtublem  26264  fsumvma2  26267  pclogsum  26268  vmasum  26269  chpchtsum  26272  chpub  26273  logfacubnd  26274  logfaclbnd  26275  logfacbnd3  26276  logfacrlim  26277  logexprlim  26278  logfacrlim2  26279  perfectlem2  26283  bclbnd  26333  bposlem1  26337  bposlem2  26338  bposlem4  26340  bposlem5  26341  bposlem6  26342  bposlem7  26343  bposlem9  26345  lgslem1  26350  lgsvalmod  26369  lgsmod  26376  lgsdirprm  26384  lgsne0  26388  lgsqrlem2  26400  gausslemma2dlem0i  26417  gausslemma2dlem5a  26423  gausslemma2d  26427  lgseisenlem1  26428  lgseisenlem2  26429  lgseisenlem3  26430  lgseisenlem4  26431  lgseisen  26432  lgsquadlem2  26434  lgsquadlem3  26435  m1lgs  26441  2sqlem8  26479  2sqmod  26489  chebbnd1lem1  26522  chebbnd1lem2  26523  chebbnd1lem3  26524  chebbnd1  26525  chtppilimlem1  26526  chtppilimlem2  26527  chtppilim  26528  chebbnd2  26530  chto1lb  26531  vmadivsum  26535  vmadivsumb  26536  rplogsumlem1  26537  rplogsumlem2  26538  dchrisum0lem1a  26539  rpvmasumlem  26540  dchrisumlema  26541  dchrisumlem1  26542  dchrisumlem2  26543  dchrmusum2  26547  dchrvmasumlem1  26548  dchrvmasum2lem  26549  dchrvmasum2if  26550  dchrvmasumlem2  26551  dchrvmasumlem3  26552  dchrvmasumiflem1  26554  dchrvmasumiflem2  26555  dchrisum0flblem2  26562  dchrisum0fno1  26564  dchrisum0lema  26567  dchrisum0lem1b  26568  dchrisum0lem1  26569  dchrisum0lem2a  26570  dchrisum0lem2  26571  dchrisum0lem3  26572  dchrisum0  26573  dirith2  26581  mudivsum  26583  mulogsumlem  26584  mulogsum  26585  mulog2sumlem1  26587  mulog2sumlem2  26588  mulog2sumlem3  26589  vmalogdivsum2  26591  vmalogdivsum  26592  2vmadivsumlem  26593  logsqvma  26595  log2sumbnd  26597  selberglem1  26598  selberglem2  26599  selberglem3  26600  selberg  26601  selbergb  26602  selberg2lem  26603  selberg2  26604  selberg2b  26605  chpdifbndlem1  26606  logdivbnd  26609  selberg3lem1  26610  selberg3lem2  26611  selberg3  26612  selberg4lem1  26613  selberg4  26614  pntrsumo1  26618  pntrsumbnd2  26620  selbergr  26621  selberg3r  26622  selberg4r  26623  selberg34r  26624  pntsf  26626  pntsval2  26629  pntrlog2bndlem1  26630  pntrlog2bndlem2  26631  pntrlog2bndlem3  26632  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntrlog2bndlem6  26636  pntrlog2bnd  26637  pntpbnd1a  26638  pntpbnd1  26639  pntpbnd2  26640  pntibndlem2  26644  pntlemn  26653  pntlemj  26656  pntlemf  26658  pntlemk  26659  pntlemo  26660  pnt  26667  padicabvcxp  26685  ostth2lem2  26687  ostth2lem3  26688  ostth2lem4  26689  ostth2  26690  ostth3  26691  clwwisshclwwslemlem  28278  numclwwlk5  28653  numclwwlk7  28656  ubthlem2  29134  minvecolem3  29139  lnconi  30296  prmdvdsbc  31032  ltesubnnd  31038  cshwrnid  31135  cycpmfv2  31283  znfermltl  31464  madjusmdetlem2  31680  eulerpartlemgc  32229  reprle  32494  hgt750lemc  32527  hgt750lemd  32528  hgt750lemb  32536  hgt750leme  32538  tgoldbachgtde  32540  iprodgam  33614  faclimlem1  33615  faclimlem3  33617  faclim  33618  iprodfac  33619  knoppndvlem17  34635  poimirlem29  35733  heiborlem3  35898  heiborlem5  35900  heiborlem6  35901  heiborlem7  35902  heiborlem8  35903  heibor  35906  rrndstprj2  35916  rrncmslem  35917  rrnequiv  35920  lcmineqlem20  39984  lcmineqlem23  39987  3lexlogpow5ineq2  39991  3lexlogpow2ineq2  39995  aks4d1p5  40016  aks4d1p6  40017  aks4d1p8d2  40021  aks4d1p8  40023  metakunt18  40070  metakunt30  40082  dvdsexpnn  40261  zrtelqelz  40266  rtprmirr  40268  fltne  40397  flt4lem7  40412  fltltc  40414  fltnltalem  40415  fltnlta  40416  irrapxlem5  40564  pell14qrgapw  40614  pellqrexplicit  40615  pellqrex  40617  pellfundge  40620  pellfundgt1  40621  jm3.1lem1  40755  jm3.1lem2  40756  hashnzfz2  41828  xralrple4  42802  recnnltrp  42806  rpgtrecnn  42809  fsumnncl  43003  limsup10exlem  43203  stoweidlem31  43462  stoweidlem59  43490  wallispilem3  43498  wallispi  43501  stirlinglem12  43516  stirlinglem15  43519  fourierdlem73  43610  etransclem23  43688  nnfoctbdjlem  43883  ovnsubaddlem1  43998  ovolval5lem1  44080  ovolval5lem2  44081  vonioolem1  44108  vonioolem2  44109  vonicclem2  44112  fmtnoprmfac1lem  44904  sfprmdvdsmersenne  44943  lighneallem2  44946  proththd  44954  perfectALTVlem2  45062  fppr2odd  45071  fpprwppr  45079  fpprel2  45081  pw2m1lepw2m1  45749  logbge0b  45797  logblt1b  45798  logbpw2m1  45801  nnpw2pmod  45817  nnolog2flm1  45824  blennngt2o2  45826  dignnld  45837  digexp  45841  amgmlemALT  46393