Theorem nnrpd 12932

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℕcn 12125  ℝ⁺crp 12890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-i2m1 11074  ax-1ne0 11075  ax-1rid 11076  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081  ax-pre-ltadd 11082  ax-pre-mulgt0 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-om 7797  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152  df-sub 11346  df-neg 11347  df-nn 12126  df-rp 12891

This theorem is referenced by:  zgt1rpn0n1  12933  modmulnn  13793  modaddid  13814  mulp1mod1  13818  modsumfzodifsn  13851  addmodlteq  13853  nnesq  14134  digit1  14144  bcpasc  14228  cshwn  14704  iseralt  15592  climcndslem2  15757  mertenslem1  15791  mertenslem2  15792  fprodmodd  15904  efcllem  15984  ege2le3  15997  eftlub  16018  effsumlt  16020  eirrlem  16113  sqrt2irrlem  16157  p1modz1  16170  dvdsmod  16240  bitsfzo  16346  bitsmod  16347  bitscmp  16349  bitsinv1lem  16352  sadaddlem  16377  sadasslem  16381  bitsres  16384  smumul  16404  bezoutlem3  16452  eucalglt  16496  prmind2  16596  prmdvdsbc  16637  crth  16689  eulerthlem2  16693  fermltl  16695  prmdiv  16696  prmdiveq  16697  odzdvds  16707  vfermltlALT  16714  powm2modprm  16715  modprm0  16717  modprmn0modprm0  16719  prmreclem3  16830  prmreclem5  16832  prmreclem6  16833  4sqlem5  16854  4sqlem6  16855  4sqlem7  16856  4sqlem10  16859  4sqlem12  16868  vdwlem1  16893  mndodcong  19454  odmod  19458  oddvds  19459  dfod2  19476  gexexlem  19764  zringlpirlem3  21401  fermltlchr  21466  met1stc  24436  met2ndci  24437  lebnumlem3  24889  lebnumii  24892  ovollb2lem  25416  ovoliunlem1  25430  ovoliunlem3  25432  uniioombllem6  25516  itg2cnlem2  25690  elqaalem2  26255  aalioulem2  26268  aalioulem4  26270  aalioulem5  26271  aaliou2b  26276  aaliou3lem9  26285  logfac  26537  cxpeq  26694  zrtelqelz  26695  rtprmirr  26697  logbgcd1irr  26731  leibpi  26879  birthdaylem2  26889  amgmlem  26927  emcllem1  26933  emcllem2  26934  emcllem3  26935  emcllem5  26937  harmoniclbnd  26946  harmonicubnd  26947  harmonicbnd4  26948  fsumharmonic  26949  zetacvg  26952  lgamgulmlem2  26967  lgamgulmlem3  26968  lgamgulmlem4  26969  lgamgulmlem5  26970  lgamgulmlem6  26971  lgamgulm2  26973  lgambdd  26974  lgamucov  26975  lgamcvg2  26992  gamcvg  26993  gamcvg2lem  26996  regamcl  26998  relgamcl  26999  lgam1  27001  wilthlem1  27005  wilthlem2  27006  basellem1  27018  basellem6  27023  basellem8  27025  chtf  27045  efchtcl  27048  chtge0  27049  vmacl  27055  efvmacl  27057  sgmnncl  27084  chtprm  27090  chtdif  27095  efchtdvds  27096  prmorcht  27115  sgmppw  27135  vmalelog  27143  chtleppi  27148  chtublem  27149  fsumvma2  27152  pclogsum  27153  vmasum  27154  chpchtsum  27157  chpub  27158  logfacubnd  27159  logfaclbnd  27160  logfacbnd3  27161  logfacrlim  27162  logexprlim  27163  logfacrlim2  27164  perfectlem2  27168  bclbnd  27218  bposlem1  27222  bposlem2  27223  bposlem4  27225  bposlem5  27226  bposlem6  27227  bposlem7  27228  bposlem9  27230  lgslem1  27235  lgsvalmod  27254  lgsmod  27261  lgsdirprm  27269  lgsne0  27273  lgsqrlem2  27285  gausslemma2dlem0i  27302  gausslemma2dlem5a  27308  gausslemma2d  27312  lgseisenlem1  27313  lgseisenlem2  27314  lgseisenlem3  27315  lgseisenlem4  27316  lgseisen  27317  lgsquadlem2  27319  lgsquadlem3  27320  m1lgs  27326  2sqlem8  27364  2sqmod  27374  chebbnd1lem1  27407  chebbnd1lem2  27408  chebbnd1lem3  27409  chebbnd1  27410  chtppilimlem1  27411  chtppilimlem2  27412  chtppilim  27413  chebbnd2  27415  chto1lb  27416  vmadivsum  27420  vmadivsumb  27421  rplogsumlem1  27422  rplogsumlem2  27423  dchrisum0lem1a  27424  rpvmasumlem  27425  dchrisumlema  27426  dchrisumlem1  27427  dchrisumlem2  27428  dchrmusum2  27432  dchrvmasumlem1  27433  dchrvmasum2lem  27434  dchrvmasum2if  27435  dchrvmasumlem2  27436  dchrvmasumlem3  27437  dchrvmasumiflem1  27439  dchrvmasumiflem2  27440  dchrisum0flblem2  27447  dchrisum0fno1  27449  dchrisum0lema  27452  dchrisum0lem1b  27453  dchrisum0lem1  27454  dchrisum0lem2a  27455  dchrisum0lem2  27456  dchrisum0lem3  27457  dchrisum0  27458  dirith2  27466  mudivsum  27468  mulogsumlem  27469  mulogsum  27470  mulog2sumlem1  27472  mulog2sumlem2  27473  mulog2sumlem3  27474  vmalogdivsum2  27476  vmalogdivsum  27477  2vmadivsumlem  27478  logsqvma  27480  log2sumbnd  27482  selberglem1  27483  selberglem2  27484  selberglem3  27485  selberg  27486  selbergb  27487  selberg2lem  27488  selberg2  27489  selberg2b  27490  chpdifbndlem1  27491  logdivbnd  27494  selberg3lem1  27495  selberg3lem2  27496  selberg3  27497  selberg4lem1  27498  selberg4  27499  pntrsumo1  27503  pntrsumbnd2  27505  selbergr  27506  selberg3r  27507  selberg4r  27508  selberg34r  27509  pntsf  27511  pntsval2  27514  pntrlog2bndlem1  27515  pntrlog2bndlem2  27516  pntrlog2bndlem3  27517  pntrlog2bndlem4  27518  pntrlog2bndlem5  27519  pntrlog2bndlem6  27521  pntrlog2bnd  27522  pntpbnd1a  27523  pntpbnd1  27524  pntpbnd2  27525  pntibndlem2  27529  pntlemn  27538  pntlemj  27541  pntlemf  27543  pntlemk  27544  pntlemo  27545  pnt  27552  padicabvcxp  27570  ostth2lem2  27572  ostth2lem3  27573  ostth2lem4  27574  ostth2  27575  ostth3  27576  clwwisshclwwslemlem  29993  numclwwlk5  30368  numclwwlk7  30371  nrt2irr  30453  ubthlem2  30851  minvecolem3  30856  lnconi  32013  ltesubnnd  32805  2exple2exp  32828  cshwrnid  32942  cycpmfv2  33083  znfermltl  33331  madjusmdetlem2  33841  eulerpartlemgc  34375  reprle  34627  hgt750lemc  34660  hgt750lemd  34661  hgt750lemb  34669  hgt750leme  34671  tgoldbachgtde  34673  iprodgam  35786  faclimlem1  35787  faclimlem3  35789  faclim  35790  iprodfac  35791  knoppndvlem17  36570  poimirlem29  37697  heiborlem3  37861  heiborlem5  37863  heiborlem6  37864  heiborlem7  37865  heiborlem8  37866  heibor  37869  rrndstprj2  37879  rrncmslem  37880  rrnequiv  37883  lcmineqlem20  42089  lcmineqlem23  42092  3lexlogpow5ineq2  42096  3lexlogpow2ineq2  42100  aks4d1p5  42121  aks4d1p6  42122  aks4d1p8d2  42126  aks4d1p8  42128  remexz  42145  hashscontpow1  42162  aks6d1c2lem4  42168  aks6d1c2  42171  bcled  42219  bcle2d  42220  aks6d1c7lem1  42221  dvdsexpnn  42374  fltne  42685  flt4lem7  42700  fltltc  42702  fltnltalem  42703  fltnlta  42704  irrapxlem5  42867  pell14qrgapw  42917  pellqrexplicit  42918  pellqrex  42920  pellfundge  42923  pellfundgt1  42924  jm3.1lem1  43058  jm3.1lem2  43059  hashnzfz2  44362  xralrple4  45419  recnnltrp  45423  rpgtrecnn  45426  fsumnncl  45620  limsup10exlem  45818  stoweidlem31  46077  stoweidlem59  46105  wallispilem3  46113  wallispi  46116  stirlinglem12  46131  stirlinglem15  46134  fourierdlem73  46225  etransclem23  46303  nnfoctbdjlem  46501  ovnsubaddlem1  46616  ovolval5lem1  46698  ovolval5lem2  46699  vonioolem1  46726  vonioolem2  46727  vonicclem2  46730  fmtnoprmfac1lem  47603  sfprmdvdsmersenne  47642  lighneallem2  47645  proththd  47653  perfectALTVlem2  47761  fppr2odd  47770  fpprwppr  47778  fpprel2  47780  gpgedgvtx1  48101  gpg5nbgrvtx03starlem2  48108  gpg5nbgrvtx13starlem2  48111  gpg3nbgrvtx0  48115  pw2m1lepw2m1  48560  logbge0b  48603  logblt1b  48604  logbpw2m1  48607  nnpw2pmod  48623  nnolog2flm1  48630  blennngt2o2  48632  dignnld  48643  digexp  48647  amgmlemALT  49843