Theorem nnrpd 12996

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℕcn 12194  ℝ⁺crp 12956

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708  ax-resscn 11149  ax-1cn 11150  ax-icn 11151  ax-addcl 11152  ax-addrcl 11153  ax-mulcl 11154  ax-mulrcl 11155  ax-mulcom 11156  ax-addass 11157  ax-mulass 11158  ax-distr 11159  ax-i2m1 11160  ax-1ne0 11161  ax-1rid 11162  ax-rnegex 11163  ax-rrecex 11164  ax-cnre 11165  ax-pre-lttri 11166  ax-pre-lttrn 11167  ax-pre-ltadd 11168  ax-pre-mulgt0 11169

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6289  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-riota 7349  df-ov 7396  df-oprab 7397  df-mpo 7398  df-om 7839  df-2nd 7958  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-rdg 8392  df-er 8686  df-en 8923  df-dom 8924  df-sdom 8925  df-pnf 11232  df-mnf 11233  df-xr 11234  df-ltxr 11235  df-le 11236  df-sub 11428  df-neg 11429  df-nn 12195  df-rp 12957

This theorem is referenced by:  zgt1rpn0n1  12997  modmulnn  13836  mulp1mod1  13859  modsumfzodifsn  13891  addmodlteq  13893  nnesq  14172  digit1  14182  bcpasc  14263  cshwn  14729  iseralt  15613  climcndslem2  15778  mertenslem1  15812  mertenslem2  15813  fprodmodd  15923  efcllem  16003  ege2le3  16015  eftlub  16034  effsumlt  16036  eirrlem  16129  sqrt2irrlem  16173  p1modz1  16186  dvdsmod  16254  bitsfzo  16358  bitsmod  16359  bitscmp  16361  bitsinv1lem  16364  sadaddlem  16389  sadasslem  16393  bitsres  16396  smumul  16416  bezoutlem3  16465  eucalglt  16504  prmind2  16604  crth  16693  eulerthlem2  16697  fermltl  16699  prmdiv  16700  prmdiveq  16701  odzdvds  16710  vfermltlALT  16717  powm2modprm  16718  modprm0  16720  modprmn0modprm0  16722  prmreclem3  16833  prmreclem5  16835  prmreclem6  16836  4sqlem5  16857  4sqlem6  16858  4sqlem7  16859  4sqlem10  16862  4sqlem12  16871  vdwlem1  16896  mndodcong  19374  odmod  19378  oddvds  19379  dfod2  19396  gexexlem  19680  zringlpirlem3  20967  met1stc  23959  met2ndci  23960  lebnumlem3  24408  lebnumii  24411  ovollb2lem  24934  ovoliunlem1  24948  ovoliunlem3  24950  uniioombllem6  25034  itg2cnlem2  25209  elqaalem2  25762  aalioulem2  25775  aalioulem4  25777  aalioulem5  25778  aaliou2b  25783  aaliou3lem9  25792  logfac  26038  cxpeq  26192  logbgcd1irr  26226  leibpi  26374  birthdaylem2  26384  amgmlem  26421  emcllem1  26427  emcllem2  26428  emcllem3  26429  emcllem5  26431  harmoniclbnd  26440  harmonicubnd  26441  harmonicbnd4  26442  fsumharmonic  26443  zetacvg  26446  lgamgulmlem2  26461  lgamgulmlem3  26462  lgamgulmlem4  26463  lgamgulmlem5  26464  lgamgulmlem6  26465  lgamgulm2  26467  lgambdd  26468  lgamucov  26469  lgamcvg2  26486  gamcvg  26487  gamcvg2lem  26490  regamcl  26492  relgamcl  26493  lgam1  26495  wilthlem1  26499  wilthlem2  26500  basellem1  26512  basellem6  26517  basellem8  26519  chtf  26539  efchtcl  26542  chtge0  26543  vmacl  26549  efvmacl  26551  sgmnncl  26578  chtprm  26584  chtdif  26589  efchtdvds  26590  prmorcht  26609  sgmppw  26627  vmalelog  26635  chtleppi  26640  chtublem  26641  fsumvma2  26644  pclogsum  26645  vmasum  26646  chpchtsum  26649  chpub  26650  logfacubnd  26651  logfaclbnd  26652  logfacbnd3  26653  logfacrlim  26654  logexprlim  26655  logfacrlim2  26656  perfectlem2  26660  bclbnd  26710  bposlem1  26714  bposlem2  26715  bposlem4  26717  bposlem5  26718  bposlem6  26719  bposlem7  26720  bposlem9  26722  lgslem1  26727  lgsvalmod  26746  lgsmod  26753  lgsdirprm  26761  lgsne0  26765  lgsqrlem2  26777  gausslemma2dlem0i  26794  gausslemma2dlem5a  26800  gausslemma2d  26804  lgseisenlem1  26805  lgseisenlem2  26806  lgseisenlem3  26807  lgseisenlem4  26808  lgseisen  26809  lgsquadlem2  26811  lgsquadlem3  26812  m1lgs  26818  2sqlem8  26856  2sqmod  26866  chebbnd1lem1  26899  chebbnd1lem2  26900  chebbnd1lem3  26901  chebbnd1  26902  chtppilimlem1  26903  chtppilimlem2  26904  chtppilim  26905  chebbnd2  26907  chto1lb  26908  vmadivsum  26912  vmadivsumb  26913  rplogsumlem1  26914  rplogsumlem2  26915  dchrisum0lem1a  26916  rpvmasumlem  26917  dchrisumlema  26918  dchrisumlem1  26919  dchrisumlem2  26920  dchrmusum2  26924  dchrvmasumlem1  26925  dchrvmasum2lem  26926  dchrvmasum2if  26927  dchrvmasumlem2  26928  dchrvmasumlem3  26929  dchrvmasumiflem1  26931  dchrvmasumiflem2  26932  dchrisum0flblem2  26939  dchrisum0fno1  26941  dchrisum0lema  26944  dchrisum0lem1b  26945  dchrisum0lem1  26946  dchrisum0lem2a  26947  dchrisum0lem2  26948  dchrisum0lem3  26949  dchrisum0  26950  dirith2  26958  mudivsum  26960  mulogsumlem  26961  mulogsum  26962  mulog2sumlem1  26964  mulog2sumlem2  26965  mulog2sumlem3  26966  vmalogdivsum2  26968  vmalogdivsum  26969  2vmadivsumlem  26970  logsqvma  26972  log2sumbnd  26974  selberglem1  26975  selberglem2  26976  selberglem3  26977  selberg  26978  selbergb  26979  selberg2lem  26980  selberg2  26981  selberg2b  26982  chpdifbndlem1  26983  logdivbnd  26986  selberg3lem1  26987  selberg3lem2  26988  selberg3  26989  selberg4lem1  26990  selberg4  26991  pntrsumo1  26995  pntrsumbnd2  26997  selbergr  26998  selberg3r  26999  selberg4r  27000  selberg34r  27001  pntsf  27003  pntsval2  27006  pntrlog2bndlem1  27007  pntrlog2bndlem2  27008  pntrlog2bndlem3  27009  pntrlog2bndlem4  27010  pntrlog2bndlem5  27011  pntrlog2bndlem6  27013  pntrlog2bnd  27014  pntpbnd1a  27015  pntpbnd1  27016  pntpbnd2  27017  pntibndlem2  27021  pntlemn  27030  pntlemj  27033  pntlemf  27035  pntlemk  27036  pntlemo  27037  pnt  27044  padicabvcxp  27062  ostth2lem2  27064  ostth2lem3  27065  ostth2lem4  27066  ostth2  27067  ostth3  27068  clwwisshclwwslemlem  29131  numclwwlk5  29506  numclwwlk7  29509  ubthlem2  29987  minvecolem3  29992  lnconi  31149  prmdvdsbc  31893  ltesubnnd  31899  cshwrnid  31996  cycpmfv2  32144  fermltlchr  32340  znfermltl  32341  madjusmdetlem2  32637  eulerpartlemgc  33190  reprle  33455  hgt750lemc  33488  hgt750lemd  33489  hgt750lemb  33497  hgt750leme  33499  tgoldbachgtde  33501  iprodgam  34540  faclimlem1  34541  faclimlem3  34543  faclim  34544  iprodfac  34545  knoppndvlem17  35206  poimirlem29  36319  heiborlem3  36484  heiborlem5  36486  heiborlem6  36487  heiborlem7  36488  heiborlem8  36489  heibor  36492  rrndstprj2  36502  rrncmslem  36503  rrnequiv  36506  lcmineqlem20  40716  lcmineqlem23  40719  3lexlogpow5ineq2  40723  3lexlogpow2ineq2  40727  aks4d1p5  40748  aks4d1p6  40749  aks4d1p8d2  40753  aks4d1p8  40755  metakunt18  40805  metakunt30  40817  dvdsexpnn  41010  zrtelqelz  41015  rtprmirr  41017  fltne  41166  flt4lem7  41181  fltltc  41183  fltnltalem  41184  fltnlta  41185  irrapxlem5  41333  pell14qrgapw  41383  pellqrexplicit  41384  pellqrex  41386  pellfundge  41389  pellfundgt1  41390  jm3.1lem1  41525  jm3.1lem2  41526  hashnzfz2  42849  xralrple4  43854  recnnltrp  43858  rpgtrecnn  43861  fsumnncl  44059  limsup10exlem  44259  stoweidlem31  44518  stoweidlem59  44546  wallispilem3  44554  wallispi  44557  stirlinglem12  44572  stirlinglem15  44575  fourierdlem73  44666  etransclem23  44744  nnfoctbdjlem  44942  ovnsubaddlem1  45057  ovolval5lem1  45139  ovolval5lem2  45140  vonioolem1  45167  vonioolem2  45168  vonicclem2  45171  fmtnoprmfac1lem  46002  sfprmdvdsmersenne  46041  lighneallem2  46044  proththd  46052  perfectALTVlem2  46160  fppr2odd  46169  fpprwppr  46177  fpprel2  46179  pw2m1lepw2m1  46847  logbge0b  46895  logblt1b  46896  logbpw2m1  46899  nnpw2pmod  46915  nnolog2flm1  46922  blennngt2o2  46924  dignnld  46935  digexp  46939  amgmlemALT  47496