Theorem nnrpd 12591

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

Syntax hints:   → wi 4   ∈ wcel 2112  ℕcn 11795  ℝ⁺crp 12551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501  ax-resscn 10751  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-mulcom 10758  ax-addass 10759  ax-mulass 10760  ax-distr 10761  ax-i2m1 10762  ax-1ne0 10763  ax-1rid 10764  ax-rnegex 10765  ax-rrecex 10766  ax-cnre 10767  ax-pre-lttri 10768  ax-pre-lttrn 10769  ax-pre-ltadd 10770  ax-pre-mulgt0 10771

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6140  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-riota 7148  df-ov 7194  df-oprab 7195  df-mpo 7196  df-om 7623  df-wrecs 8025  df-recs 8086  df-rdg 8124  df-er 8369  df-en 8605  df-dom 8606  df-sdom 8607  df-pnf 10834  df-mnf 10835  df-xr 10836  df-ltxr 10837  df-le 10838  df-sub 11029  df-neg 11030  df-nn 11796  df-rp 12552

This theorem is referenced by:  zgt1rpn0n1  12592  modmulnn  13427  mulp1mod1  13450  modsumfzodifsn  13482  addmodlteq  13484  nnesq  13759  digit1  13769  bcpasc  13852  cshwn  14327  iseralt  15213  climcndslem2  15377  mertenslem1  15411  mertenslem2  15412  fprodmodd  15522  efcllem  15602  ege2le3  15614  eftlub  15633  effsumlt  15635  eirrlem  15728  sqrt2irrlem  15772  p1modz1  15785  dvdsmod  15853  bitsfzo  15957  bitsmod  15958  bitscmp  15960  bitsinv1lem  15963  sadaddlem  15988  sadasslem  15992  bitsres  15995  smumul  16015  bezoutlem3  16064  eucalglt  16105  prmind2  16205  crth  16294  eulerthlem2  16298  fermltl  16300  prmdiv  16301  prmdiveq  16302  odzdvds  16311  vfermltlALT  16318  powm2modprm  16319  modprm0  16321  modprmn0modprm0  16323  prmreclem3  16434  prmreclem5  16436  prmreclem6  16437  4sqlem5  16458  4sqlem6  16459  4sqlem7  16460  4sqlem10  16463  4sqlem12  16472  vdwlem1  16497  mndodcong  18888  odmod  18892  oddvds  18893  dfod2  18909  gexexlem  19191  zringlpirlem3  20405  met1stc  23373  met2ndci  23374  lebnumlem3  23814  lebnumii  23817  ovollb2lem  24339  ovoliunlem1  24353  ovoliunlem3  24355  uniioombllem6  24439  itg2cnlem2  24614  elqaalem2  25167  aalioulem2  25180  aalioulem4  25182  aalioulem5  25183  aaliou2b  25188  aaliou3lem9  25197  logfac  25443  cxpeq  25597  logbgcd1irr  25631  leibpi  25779  birthdaylem2  25789  amgmlem  25826  emcllem1  25832  emcllem2  25833  emcllem3  25834  emcllem5  25836  harmoniclbnd  25845  harmonicubnd  25846  harmonicbnd4  25847  fsumharmonic  25848  zetacvg  25851  lgamgulmlem2  25866  lgamgulmlem3  25867  lgamgulmlem4  25868  lgamgulmlem5  25869  lgamgulmlem6  25870  lgamgulm2  25872  lgambdd  25873  lgamucov  25874  lgamcvg2  25891  gamcvg  25892  gamcvg2lem  25895  regamcl  25897  relgamcl  25898  lgam1  25900  wilthlem1  25904  wilthlem2  25905  basellem1  25917  basellem6  25922  basellem8  25924  chtf  25944  efchtcl  25947  chtge0  25948  vmacl  25954  efvmacl  25956  sgmnncl  25983  chtprm  25989  chtdif  25994  efchtdvds  25995  prmorcht  26014  sgmppw  26032  vmalelog  26040  chtleppi  26045  chtublem  26046  fsumvma2  26049  pclogsum  26050  vmasum  26051  chpchtsum  26054  chpub  26055  logfacubnd  26056  logfaclbnd  26057  logfacbnd3  26058  logfacrlim  26059  logexprlim  26060  logfacrlim2  26061  perfectlem2  26065  bclbnd  26115  bposlem1  26119  bposlem2  26120  bposlem4  26122  bposlem5  26123  bposlem6  26124  bposlem7  26125  bposlem9  26127  lgslem1  26132  lgsvalmod  26151  lgsmod  26158  lgsdirprm  26166  lgsne0  26170  lgsqrlem2  26182  gausslemma2dlem0i  26199  gausslemma2dlem5a  26205  gausslemma2d  26209  lgseisenlem1  26210  lgseisenlem2  26211  lgseisenlem3  26212  lgseisenlem4  26213  lgseisen  26214  lgsquadlem2  26216  lgsquadlem3  26217  m1lgs  26223  2sqlem8  26261  2sqmod  26271  chebbnd1lem1  26304  chebbnd1lem2  26305  chebbnd1lem3  26306  chebbnd1  26307  chtppilimlem1  26308  chtppilimlem2  26309  chtppilim  26310  chebbnd2  26312  chto1lb  26313  vmadivsum  26317  vmadivsumb  26318  rplogsumlem1  26319  rplogsumlem2  26320  dchrisum0lem1a  26321  rpvmasumlem  26322  dchrisumlema  26323  dchrisumlem1  26324  dchrisumlem2  26325  dchrmusum2  26329  dchrvmasumlem1  26330  dchrvmasum2lem  26331  dchrvmasum2if  26332  dchrvmasumlem2  26333  dchrvmasumlem3  26334  dchrvmasumiflem1  26336  dchrvmasumiflem2  26337  dchrisum0flblem2  26344  dchrisum0fno1  26346  dchrisum0lema  26349  dchrisum0lem1b  26350  dchrisum0lem1  26351  dchrisum0lem2a  26352  dchrisum0lem2  26353  dchrisum0lem3  26354  dchrisum0  26355  dirith2  26363  mudivsum  26365  mulogsumlem  26366  mulogsum  26367  mulog2sumlem1  26369  mulog2sumlem2  26370  mulog2sumlem3  26371  vmalogdivsum2  26373  vmalogdivsum  26374  2vmadivsumlem  26375  logsqvma  26377  log2sumbnd  26379  selberglem1  26380  selberglem2  26381  selberglem3  26382  selberg  26383  selbergb  26384  selberg2lem  26385  selberg2  26386  selberg2b  26387  chpdifbndlem1  26388  logdivbnd  26391  selberg3lem1  26392  selberg3lem2  26393  selberg3  26394  selberg4lem1  26395  selberg4  26396  pntrsumo1  26400  pntrsumbnd2  26402  selbergr  26403  selberg3r  26404  selberg4r  26405  selberg34r  26406  pntsf  26408  pntsval2  26411  pntrlog2bndlem1  26412  pntrlog2bndlem2  26413  pntrlog2bndlem3  26414  pntrlog2bndlem4  26415  pntrlog2bndlem5  26416  pntrlog2bndlem6  26418  pntrlog2bnd  26419  pntpbnd1a  26420  pntpbnd1  26421  pntpbnd2  26422  pntibndlem2  26426  pntlemn  26435  pntlemj  26438  pntlemf  26440  pntlemk  26441  pntlemo  26442  pnt  26449  padicabvcxp  26467  ostth2lem2  26469  ostth2lem3  26470  ostth2lem4  26471  ostth2  26472  ostth3  26473  clwwisshclwwslemlem  28050  numclwwlk5  28425  numclwwlk7  28428  ubthlem2  28906  minvecolem3  28911  lnconi  30068  prmdvdsbc  30804  ltesubnnd  30810  cshwrnid  30907  cycpmfv2  31054  znfermltl  31230  madjusmdetlem2  31446  eulerpartlemgc  31995  reprle  32260  hgt750lemc  32293  hgt750lemd  32294  hgt750lemb  32302  hgt750leme  32304  tgoldbachgtde  32306  iprodgam  33377  faclimlem1  33378  faclimlem3  33380  faclim  33381  iprodfac  33382  knoppndvlem17  34394  poimirlem29  35492  heiborlem3  35657  heiborlem5  35659  heiborlem6  35660  heiborlem7  35661  heiborlem8  35662  heibor  35665  rrndstprj2  35675  rrncmslem  35676  rrnequiv  35679  lcmineqlem20  39739  lcmineqlem23  39742  3lexlogpow5ineq2  39746  3lexlogpow2ineq2  39750  metakunt18  39805  metakunt30  39817  dvdsexpnn  39989  zrtelqelz  39994  rtprmirr  39996  fltne  40125  flt4lem7  40140  fltltc  40142  fltnltalem  40143  fltnlta  40144  irrapxlem5  40292  pell14qrgapw  40342  pellqrexplicit  40343  pellqrex  40345  pellfundge  40348  pellfundgt1  40349  jm3.1lem1  40483  jm3.1lem2  40484  hashnzfz2  41553  xralrple4  42526  recnnltrp  42530  rpgtrecnn  42533  fsumnncl  42730  limsup10exlem  42931  stoweidlem31  43190  stoweidlem59  43218  wallispilem3  43226  wallispi  43229  stirlinglem12  43244  stirlinglem15  43247  fourierdlem73  43338  etransclem23  43416  nnfoctbdjlem  43611  ovnsubaddlem1  43726  ovolval5lem1  43808  ovolval5lem2  43809  vonioolem1  43836  vonioolem2  43837  vonicclem2  43840  fmtnoprmfac1lem  44632  sfprmdvdsmersenne  44671  lighneallem2  44674  proththd  44682  perfectALTVlem2  44790  fppr2odd  44799  fpprwppr  44807  fpprel2  44809  pw2m1lepw2m1  45477  logbge0b  45525  logblt1b  45526  logbpw2m1  45529  nnpw2pmod  45545  nnolog2flm1  45552  blennngt2o2  45554  dignnld  45565  digexp  45569  amgmlemALT  46121