Theorem nnrpd 13011

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℕcn 12209  ℝ⁺crp 12971

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-nn 12210  df-rp 12972

This theorem is referenced by:  zgt1rpn0n1  13012  modmulnn  13851  mulp1mod1  13874  modsumfzodifsn  13906  addmodlteq  13908  nnesq  14187  digit1  14197  bcpasc  14278  cshwn  14744  iseralt  15628  climcndslem2  15793  mertenslem1  15827  mertenslem2  15828  fprodmodd  15938  efcllem  16018  ege2le3  16030  eftlub  16049  effsumlt  16051  eirrlem  16144  sqrt2irrlem  16188  p1modz1  16201  dvdsmod  16269  bitsfzo  16373  bitsmod  16374  bitscmp  16376  bitsinv1lem  16379  sadaddlem  16404  sadasslem  16408  bitsres  16411  smumul  16431  bezoutlem3  16480  eucalglt  16519  prmind2  16619  crth  16708  eulerthlem2  16712  fermltl  16714  prmdiv  16715  prmdiveq  16716  odzdvds  16725  vfermltlALT  16732  powm2modprm  16733  modprm0  16735  modprmn0modprm0  16737  prmreclem3  16848  prmreclem5  16850  prmreclem6  16851  4sqlem5  16872  4sqlem6  16873  4sqlem7  16874  4sqlem10  16877  4sqlem12  16886  vdwlem1  16911  mndodcong  19405  odmod  19409  oddvds  19410  dfod2  19427  gexexlem  19715  zringlpirlem3  21026  met1stc  24022  met2ndci  24023  lebnumlem3  24471  lebnumii  24474  ovollb2lem  24997  ovoliunlem1  25011  ovoliunlem3  25013  uniioombllem6  25097  itg2cnlem2  25272  elqaalem2  25825  aalioulem2  25838  aalioulem4  25840  aalioulem5  25841  aaliou2b  25846  aaliou3lem9  25855  logfac  26101  cxpeq  26255  logbgcd1irr  26289  leibpi  26437  birthdaylem2  26447  amgmlem  26484  emcllem1  26490  emcllem2  26491  emcllem3  26492  emcllem5  26494  harmoniclbnd  26503  harmonicubnd  26504  harmonicbnd4  26505  fsumharmonic  26506  zetacvg  26509  lgamgulmlem2  26524  lgamgulmlem3  26525  lgamgulmlem4  26526  lgamgulmlem5  26527  lgamgulmlem6  26528  lgamgulm2  26530  lgambdd  26531  lgamucov  26532  lgamcvg2  26549  gamcvg  26550  gamcvg2lem  26553  regamcl  26555  relgamcl  26556  lgam1  26558  wilthlem1  26562  wilthlem2  26563  basellem1  26575  basellem6  26580  basellem8  26582  chtf  26602  efchtcl  26605  chtge0  26606  vmacl  26612  efvmacl  26614  sgmnncl  26641  chtprm  26647  chtdif  26652  efchtdvds  26653  prmorcht  26672  sgmppw  26690  vmalelog  26698  chtleppi  26703  chtublem  26704  fsumvma2  26707  pclogsum  26708  vmasum  26709  chpchtsum  26712  chpub  26713  logfacubnd  26714  logfaclbnd  26715  logfacbnd3  26716  logfacrlim  26717  logexprlim  26718  logfacrlim2  26719  perfectlem2  26723  bclbnd  26773  bposlem1  26777  bposlem2  26778  bposlem4  26780  bposlem5  26781  bposlem6  26782  bposlem7  26783  bposlem9  26785  lgslem1  26790  lgsvalmod  26809  lgsmod  26816  lgsdirprm  26824  lgsne0  26828  lgsqrlem2  26840  gausslemma2dlem0i  26857  gausslemma2dlem5a  26863  gausslemma2d  26867  lgseisenlem1  26868  lgseisenlem2  26869  lgseisenlem3  26870  lgseisenlem4  26871  lgseisen  26872  lgsquadlem2  26874  lgsquadlem3  26875  m1lgs  26881  2sqlem8  26919  2sqmod  26929  chebbnd1lem1  26962  chebbnd1lem2  26963  chebbnd1lem3  26964  chebbnd1  26965  chtppilimlem1  26966  chtppilimlem2  26967  chtppilim  26968  chebbnd2  26970  chto1lb  26971  vmadivsum  26975  vmadivsumb  26976  rplogsumlem1  26977  rplogsumlem2  26978  dchrisum0lem1a  26979  rpvmasumlem  26980  dchrisumlema  26981  dchrisumlem1  26982  dchrisumlem2  26983  dchrmusum2  26987  dchrvmasumlem1  26988  dchrvmasum2lem  26989  dchrvmasum2if  26990  dchrvmasumlem2  26991  dchrvmasumlem3  26992  dchrvmasumiflem1  26994  dchrvmasumiflem2  26995  dchrisum0flblem2  27002  dchrisum0fno1  27004  dchrisum0lema  27007  dchrisum0lem1b  27008  dchrisum0lem1  27009  dchrisum0lem2a  27010  dchrisum0lem2  27011  dchrisum0lem3  27012  dchrisum0  27013  dirith2  27021  mudivsum  27023  mulogsumlem  27024  mulogsum  27025  mulog2sumlem1  27027  mulog2sumlem2  27028  mulog2sumlem3  27029  vmalogdivsum2  27031  vmalogdivsum  27032  2vmadivsumlem  27033  logsqvma  27035  log2sumbnd  27037  selberglem1  27038  selberglem2  27039  selberglem3  27040  selberg  27041  selbergb  27042  selberg2lem  27043  selberg2  27044  selberg2b  27045  chpdifbndlem1  27046  logdivbnd  27049  selberg3lem1  27050  selberg3lem2  27051  selberg3  27052  selberg4lem1  27053  selberg4  27054  pntrsumo1  27058  pntrsumbnd2  27060  selbergr  27061  selberg3r  27062  selberg4r  27063  selberg34r  27064  pntsf  27066  pntsval2  27069  pntrlog2bndlem1  27070  pntrlog2bndlem2  27071  pntrlog2bndlem3  27072  pntrlog2bndlem4  27073  pntrlog2bndlem5  27074  pntrlog2bndlem6  27076  pntrlog2bnd  27077  pntpbnd1a  27078  pntpbnd1  27079  pntpbnd2  27080  pntibndlem2  27084  pntlemn  27093  pntlemj  27096  pntlemf  27098  pntlemk  27099  pntlemo  27100  pnt  27107  padicabvcxp  27125  ostth2lem2  27127  ostth2lem3  27128  ostth2lem4  27129  ostth2  27130  ostth3  27131  clwwisshclwwslemlem  29256  numclwwlk5  29631  numclwwlk7  29634  ubthlem2  30112  minvecolem3  30117  lnconi  31274  prmdvdsbc  32010  ltesubnnd  32016  cshwrnid  32113  cycpmfv2  32261  fermltlchr  32467  znfermltl  32468  madjusmdetlem2  32797  eulerpartlemgc  33350  reprle  33615  hgt750lemc  33648  hgt750lemd  33649  hgt750lemb  33657  hgt750leme  33659  tgoldbachgtde  33661  iprodgam  34701  faclimlem1  34702  faclimlem3  34704  faclim  34705  iprodfac  34706  knoppndvlem17  35393  poimirlem29  36506  heiborlem3  36670  heiborlem5  36672  heiborlem6  36673  heiborlem7  36674  heiborlem8  36675  heibor  36678  rrndstprj2  36688  rrncmslem  36689  rrnequiv  36692  lcmineqlem20  40902  lcmineqlem23  40905  3lexlogpow5ineq2  40909  3lexlogpow2ineq2  40913  aks4d1p5  40934  aks4d1p6  40935  aks4d1p8d2  40939  aks4d1p8  40941  metakunt18  40991  metakunt30  41003  dvdsexpnn  41227  zrtelqelz  41232  rtprmirr  41234  fltne  41383  flt4lem7  41398  fltltc  41400  fltnltalem  41401  fltnlta  41402  irrapxlem5  41550  pell14qrgapw  41600  pellqrexplicit  41601  pellqrex  41603  pellfundge  41606  pellfundgt1  41607  jm3.1lem1  41742  jm3.1lem2  41743  hashnzfz2  43066  xralrple4  44070  recnnltrp  44074  rpgtrecnn  44077  fsumnncl  44275  limsup10exlem  44475  stoweidlem31  44734  stoweidlem59  44762  wallispilem3  44770  wallispi  44773  stirlinglem12  44788  stirlinglem15  44791  fourierdlem73  44882  etransclem23  44960  nnfoctbdjlem  45158  ovnsubaddlem1  45273  ovolval5lem1  45355  ovolval5lem2  45356  vonioolem1  45383  vonioolem2  45384  vonicclem2  45387  fmtnoprmfac1lem  46219  sfprmdvdsmersenne  46258  lighneallem2  46261  proththd  46269  perfectALTVlem2  46377  fppr2odd  46386  fpprwppr  46394  fpprel2  46396  pw2m1lepw2m1  47155  logbge0b  47203  logblt1b  47204  logbpw2m1  47207  nnpw2pmod  47223  nnolog2flm1  47230  blennngt2o2  47232  dignnld  47243  digexp  47247  amgmlemALT  47804