Theorem nnrpd 13169

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℕcn 12342  ℝ⁺crp 13127

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755  ax-resscn 11264  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-addrcl 11268  ax-mulcl 11269  ax-mulrcl 11270  ax-mulcom 11271  ax-addass 11272  ax-mulass 11273  ax-distr 11274  ax-i2m1 11275  ax-1ne0 11276  ax-1rid 11277  ax-rnegex 11278  ax-rrecex 11279  ax-cnre 11280  ax-pre-lttri 11281  ax-pre-lttrn 11282  ax-pre-ltadd 11283  ax-pre-mulgt0 11284

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6307  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7381  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7882  df-2nd 8006  df-frecs 8307  df-wrecs 8338  df-recs 8387  df-rdg 8426  df-er 8725  df-en 8982  df-dom 8983  df-sdom 8984  df-pnf 11352  df-mnf 11353  df-xr 11354  df-ltxr 11355  df-le 11356  df-sub 11550  df-neg 11551  df-nn 12343  df-rp 13128

This theorem is used by:  zgt1rpn0n1  13170  modmulnn  14036  modaddid  14057  mulp1mod1  14061  modsumfzodifsn  14094  addmodlteq  14096  nnesq  14378  digit1  14388  bcpasc  14472  cshwn  14956  iseralt  15861  climcndslem2  16028  mertenslem1  16062  mertenslem2  16063  fprodmodd  16173  efcllem  16252  ege2le3  16265  eftlub  16286  effsumlt  16288  eirrlem  16381  sqrt2irrlem  16425  p1modz1  16438  dvdsmod  16508  bitsfzo  16614  bitsmod  16615  bitscmp  16617  bitsinv1lem  16620  sadaddlem  16645  sadasslem  16649  bitsres  16652  smumul  16672  bezoutlem3  16723  dvdsexpnn  16749  eucalglt  16769  prmind2  16869  prmdvdsbc  16911  crth  16964  eulerthlem2  16968  fermltl  16970  prmdiv  16971  prmdiveq  16972  odzdvds  16982  vfermltlALT  16989  powm2modprm  16990  modprm0  16992  modprmn0modprm0  16994  prmreclem3  17105  prmreclem5  17107  prmreclem6  17108  4sqlem5  17129  4sqlem6  17130  4sqlem7  17131  4sqlem10  17134  4sqlem12  17143  vdwlem1  17168  mndodcong  19765  odmod  19769  oddvds  19770  dfod2  19787  gexexlem  20075  zringlpirlem3  21779  fermltlchr  21844  met1stc  24849  met2ndci  24850  lebnumlem3  25293  lebnumii  25296  ovollb2lem  25818  ovoliunlem1  25832  ovoliunlem3  25834  uniioombllem6  25918  itg2cnlem2  26092  elqaalem2  26652  aalioulem2  26669  aalioulem4  26671  aalioulem5  26672  aaliou2b  26677  aaliou3lem9  26686  logfac  26938  cxpeq  27094  zrtelqelz  27095  rtprmirr  27097  logbgcd1irr  27131  leibpi  27279  birthdaylem2  27289  amgmlem  27326  emcllem1  27332  emcllem2  27333  emcllem3  27334  emcllem5  27336  harmoniclbnd  27345  harmonicubnd  27346  harmonicbnd4  27347  fsumharmonic  27348  zetacvg  27351  lgamgulmlem2  27366  lgamgulmlem3  27367  lgamgulmlem4  27368  lgamgulmlem5  27369  lgamgulmlem6  27370  lgamgulm2  27372  lgambdd  27373  lgamucov  27374  lgamcvg2  27391  gamcvg  27392  gamcvg2lem  27395  regamcl  27397  relgamcl  27398  lgam1  27400  wilthlem1  27404  wilthlem2  27405  basellem1  27417  basellem6  27422  basellem8  27424  chtf  27444  efchtcl  27447  chtge0  27448  vmacl  27454  efvmacl  27456  sgmnncl  27483  chtprm  27489  chtdif  27494  efchtdvds  27495  prmorcht  27514  sgmppw  27533  vmalelog  27541  chtleppi  27546  chtublem  27547  fsumvma2  27550  pclogsum  27551  vmasum  27552  chpchtsum  27555  chpub  27556  logfacubnd  27557  logfaclbnd  27558  logfacbnd3  27559  logfacrlim  27560  logexprlim  27561  logfacrlim2  27562  perfectlem2  27566  bclbnd  27616  bposlem1  27620  bposlem2  27621  bposlem4  27623  bposlem5  27624  bposlem6  27625  bposlem7  27626  bposlem9  27628  lgslem1  27633  lgsvalmod  27652  lgsmod  27659  lgsdirprm  27667  lgsne0  27671  lgsqrlem2  27683  gausslemma2dlem0i  27700  gausslemma2dlem5a  27706  gausslemma2d  27710  lgseisenlem1  27711  lgseisenlem2  27712  lgseisenlem3  27713  lgseisenlem4  27714  lgseisen  27715  lgsquadlem2  27717  lgsquadlem3  27718  m1lgs  27724  2sqlem8  27762  2sqmod  27772  chebbnd1lem1  27805  chebbnd1lem2  27806  chebbnd1lem3  27807  chebbnd1  27808  chtppilimlem1  27809  chtppilimlem2  27810  chtppilim  27811  chebbnd2  27813  chto1lb  27814  vmadivsum  27818  vmadivsumb  27819  rplogsumlem1  27820  rplogsumlem2  27821  dchrisum0lem1a  27822  rpvmasumlem  27823  dchrisumlema  27824  dchrisumlem1  27825  dchrisumlem2  27826  dchrmusum2  27830  dchrvmasumlem1  27831  dchrvmasum2lem  27832  dchrvmasum2if  27833  dchrvmasumlem2  27834  dchrvmasumlem3  27835  dchrvmasumiflem1  27837  dchrvmasumiflem2  27838  dchrisum0flblem2  27845  dchrisum0fno1  27847  dchrisum0lema  27850  dchrisum0lem1b  27851  dchrisum0lem1  27852  dchrisum0lem2a  27853  dchrisum0lem2  27854  dchrisum0lem3  27855  dchrisum0  27856  dirith2  27864  mudivsum  27866  mulogsumlem  27867  mulogsum  27868  mulog2sumlem1  27870  mulog2sumlem2  27871  mulog2sumlem3  27872  vmalogdivsum2  27874  vmalogdivsum  27875  2vmadivsumlem  27876  logsqvma  27878  log2sumbnd  27880  selberglem1  27881  selberglem2  27882  selberglem3  27883  selberg  27884  selbergb  27885  selberg2lem  27886  selberg2  27887  selberg2b  27888  chpdifbndlem1  27889  logdivbnd  27892  selberg3lem1  27893  selberg3lem2  27894  selberg3  27895  selberg4lem1  27896  selberg4  27897  pntrsumo1  27901  pntrsumbnd2  27903  selbergr  27904  selberg3r  27905  selberg4r  27906  selberg34r  27907  pntsf  27909  pntsval2  27912  pntrlog2bndlem1  27913  pntrlog2bndlem2  27914  pntrlog2bndlem3  27915  pntrlog2bndlem4  27916  pntrlog2bndlem5  27917  pntrlog2bndlem6  27919  pntrlog2bnd  27920  pntpbnd1a  27921  pntpbnd1  27922  pntpbnd2  27923  pntibndlem2  27927  pntlemn  27936  pntlemj  27939  pntlemf  27941  pntlemk  27942  pntlemo  27943  pnt  27950  padicabvcxp  27968  ostth2lem2  27970  ostth2lem3  27971  ostth2lem4  27972  ostth2  27973  ostth3  27974  fltne  27984  flt4lem7  27998  clwwisshclwwslemlem  30613  numclwwlk5  30998  numclwwlk7  31001  nrt2irr  31083  ubthlem2  31482  minvecolem3  31487  lnconi  32644  ltesubnnd  33464  2exple2exp  33475  cshwrnid  33572  cycpmfv2  33725  znfermltl  33972  madjusmdetlem2  34510  eulerpartlemgc  35044  reprle  35293  hgt750lemc  35326  hgt750lemd  35327  hgt750lemb  35335  hgt750leme  35337  tgoldbachgtde  35339  iprodgam  36631  faclimlem1  36632  faclimlem3  36634  faclim  36635  iprodfac  36636  knoppndvlem17  37518  poimirlem29  38704  heiborlem3  38884  heiborlem5  38886  heiborlem6  38887  heiborlem7  38888  heiborlem8  38889  heibor  38892  rrndstprj2  38902  rrncmslem  38903  rrnequiv  38906  lcmineqlem20  43235  lcmineqlem23  43238  3lexlogpow5ineq2  43242  3lexlogpow2ineq2  43246  aks4d1p5  43267  aks4d1p6  43268  aks4d1p8d2  43272  aks4d1p8  43274  remexz  43291  hashscontpow1  43308  aks6d1c2lem4  43314  aks6d1c2  43317  bcled  43365  bcle2d  43366  aks6d1c7lem1  43367  fltltc  43809  fltnltalem  43810  fltnlta  43811  irrapxlem5  43970  pell14qrgapw  44020  pellqrexplicit  44021  pellqrex  44023  pellfundge  44026  pellfundgt1  44027  jm3.1lem1  44161  jm3.1lem2  44162  hashnzfz2  45442  xralrple4  46520  recnnltrp  46524  rpgtrecnn  46527  fsumnncl  46720  limsup10exlem  46918  stoweidlem31  47177  stoweidlem59  47205  wallispilem3  47213  wallispi  47216  stirlinglem12  47231  stirlinglem15  47234  fourierdlem73  47325  etransclem23  47403  nnfoctbdjlem  47601  ovnsubaddlem1  47716  ovolval5lem1  47798  ovolval5lem2  47799  vonioolem1  47826  vonioolem2  47827  vonicclem2  47830  2timesltsqm1  48585  fmtnoprmfac1lem  48785  sfprmdvdsmersenne  48824  lighneallem2  48827  proththd  48835  perfectALTVlem2  48956  fppr2odd  48965  fpprwppr  48973  fpprel2  48975  gpgedgvtx1  49296  gpg5nbgrvtx03starlem2  49303  gpg5nbgrvtx13starlem2  49306  gpg3nbgrvtx0  49310  pw2m1lepw2m1  49768  logbge0b  49811  logblt1b  49812  logbpw2m1  49815  nnpw2pmod  49831  nnolog2flm1  49838  blennngt2o2  49840  dignnld  49851  digexp  49855  amgmlemALT  51199