Theorem nnrpd 13057

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

Syntax hints:   → wi 4   ∈ wcel 2149  ℕcn 12232  ℝ⁺crp 13015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175  ax-pre-mulgt0 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7862  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-sub 11442  df-neg 11443  df-nn 12233  df-rp 13016

This theorem is referenced by:  zgt1rpn0n1  13058  modmulnn  13921  modaddid  13942  mulp1mod1  13946  modsumfzodifsn  13979  addmodlteq  13981  nnesq  14262  digit1  14272  bcpasc  14356  cshwn  14833  iseralt  15735  climcndslem2  15903  mertenslem1  15937  mertenslem2  15938  fprodmodd  16050  efcllem  16130  ege2le3  16143  eftlub  16164  effsumlt  16166  eirrlem  16259  sqrt2irrlem  16303  p1modz1  16316  dvdsmod  16386  bitsfzo  16492  bitsmod  16493  bitscmp  16495  bitsinv1lem  16498  sadaddlem  16523  sadasslem  16527  bitsres  16530  smumul  16550  bezoutlem3  16598  eucalglt  16642  prmind2  16742  prmdvdsbc  16784  crth  16836  eulerthlem2  16840  fermltl  16842  prmdiv  16843  prmdiveq  16844  odzdvds  16854  vfermltlALT  16861  powm2modprm  16862  modprm0  16864  modprmn0modprm0  16866  prmreclem3  16977  prmreclem5  16979  prmreclem6  16980  4sqlem5  17001  4sqlem6  17002  4sqlem7  17003  4sqlem10  17006  4sqlem12  17015  vdwlem1  17040  mndodcong  19611  odmod  19615  oddvds  19616  dfod2  19633  gexexlem  19921  zringlpirlem3  21582  fermltlchr  21647  met1stc  24646  met2ndci  24647  lebnumlem3  25090  lebnumii  25093  ovollb2lem  25615  ovoliunlem1  25629  ovoliunlem3  25631  uniioombllem6  25715  itg2cnlem2  25889  elqaalem2  26449  aalioulem2  26462  aalioulem4  26464  aalioulem5  26465  aaliou2b  26470  aaliou3lem9  26479  logfac  26731  cxpeq  26887  zrtelqelz  26888  rtprmirr  26890  logbgcd1irr  26924  leibpi  27072  birthdaylem2  27082  amgmlem  27119  emcllem1  27125  emcllem2  27126  emcllem3  27127  emcllem5  27129  harmoniclbnd  27138  harmonicubnd  27139  harmonicbnd4  27140  fsumharmonic  27141  zetacvg  27144  lgamgulmlem2  27159  lgamgulmlem3  27160  lgamgulmlem4  27161  lgamgulmlem5  27162  lgamgulmlem6  27163  lgamgulm2  27165  lgambdd  27166  lgamucov  27167  lgamcvg2  27184  gamcvg  27185  gamcvg2lem  27188  regamcl  27190  relgamcl  27191  lgam1  27193  wilthlem1  27197  wilthlem2  27198  basellem1  27210  basellem6  27215  basellem8  27217  chtf  27237  efchtcl  27240  chtge0  27241  vmacl  27247  efvmacl  27249  sgmnncl  27276  chtprm  27282  chtdif  27287  efchtdvds  27288  prmorcht  27307  sgmppw  27326  vmalelog  27334  chtleppi  27339  chtublem  27340  fsumvma2  27343  pclogsum  27344  vmasum  27345  chpchtsum  27348  chpub  27349  logfacubnd  27350  logfaclbnd  27351  logfacbnd3  27352  logfacrlim  27353  logexprlim  27354  logfacrlim2  27355  perfectlem2  27359  bclbnd  27409  bposlem1  27413  bposlem2  27414  bposlem4  27416  bposlem5  27417  bposlem6  27418  bposlem7  27419  bposlem9  27421  lgslem1  27426  lgsvalmod  27445  lgsmod  27452  lgsdirprm  27460  lgsne0  27464  lgsqrlem2  27476  gausslemma2dlem0i  27493  gausslemma2dlem5a  27499  gausslemma2d  27503  lgseisenlem1  27504  lgseisenlem2  27505  lgseisenlem3  27506  lgseisenlem4  27507  lgseisen  27508  lgsquadlem2  27510  lgsquadlem3  27511  m1lgs  27517  2sqlem8  27555  2sqmod  27565  chebbnd1lem1  27598  chebbnd1lem2  27599  chebbnd1lem3  27600  chebbnd1  27601  chtppilimlem1  27602  chtppilimlem2  27603  chtppilim  27604  chebbnd2  27606  chto1lb  27607  vmadivsum  27611  vmadivsumb  27612  rplogsumlem1  27613  rplogsumlem2  27614  dchrisum0lem1a  27615  rpvmasumlem  27616  dchrisumlema  27617  dchrisumlem1  27618  dchrisumlem2  27619  dchrmusum2  27623  dchrvmasumlem1  27624  dchrvmasum2lem  27625  dchrvmasum2if  27626  dchrvmasumlem2  27627  dchrvmasumlem3  27628  dchrvmasumiflem1  27630  dchrvmasumiflem2  27631  dchrisum0flblem2  27638  dchrisum0fno1  27640  dchrisum0lema  27643  dchrisum0lem1b  27644  dchrisum0lem1  27645  dchrisum0lem2a  27646  dchrisum0lem2  27647  dchrisum0lem3  27648  dchrisum0  27649  dirith2  27657  mudivsum  27659  mulogsumlem  27660  mulogsum  27661  mulog2sumlem1  27663  mulog2sumlem2  27664  mulog2sumlem3  27665  vmalogdivsum2  27667  vmalogdivsum  27668  2vmadivsumlem  27669  logsqvma  27671  log2sumbnd  27673  selberglem1  27674  selberglem2  27675  selberglem3  27676  selberg  27677  selbergb  27678  selberg2lem  27679  selberg2  27680  selberg2b  27681  chpdifbndlem1  27682  logdivbnd  27685  selberg3lem1  27686  selberg3lem2  27687  selberg3  27688  selberg4lem1  27689  selberg4  27690  pntrsumo1  27694  pntrsumbnd2  27696  selbergr  27697  selberg3r  27698  selberg4r  27699  selberg34r  27700  pntsf  27702  pntsval2  27705  pntrlog2bndlem1  27706  pntrlog2bndlem2  27707  pntrlog2bndlem3  27708  pntrlog2bndlem4  27709  pntrlog2bndlem5  27710  pntrlog2bndlem6  27712  pntrlog2bnd  27713  pntpbnd1a  27714  pntpbnd1  27715  pntpbnd2  27716  pntibndlem2  27720  pntlemn  27729  pntlemj  27732  pntlemf  27734  pntlemk  27735  pntlemo  27736  pnt  27743  padicabvcxp  27761  ostth2lem2  27763  ostth2lem3  27764  ostth2lem4  27765  ostth2  27766  ostth3  27767  clwwisshclwwslemlem  30304  numclwwlk5  30679  numclwwlk7  30682  nrt2irr  30764  ubthlem2  31163  minvecolem3  31168  lnconi  32325  ltesubnnd  33107  2exple2exp  33118  cshwrnid  33221  cycpmfv2  33374  znfermltl  33623  madjusmdetlem2  34162  eulerpartlemgc  34696  reprle  34945  hgt750lemc  34978  hgt750lemd  34979  hgt750lemb  34987  hgt750leme  34989  tgoldbachgtde  34991  iprodgam  36132  faclimlem1  36133  faclimlem3  36135  faclim  36136  iprodfac  36137  knoppndvlem17  37005  poimirlem29  38187  heiborlem3  38351  heiborlem5  38353  heiborlem6  38354  heiborlem7  38355  heiborlem8  38356  heibor  38359  rrndstprj2  38369  rrncmslem  38370  rrnequiv  38373  lcmineqlem20  42704  lcmineqlem23  42707  3lexlogpow5ineq2  42711  3lexlogpow2ineq2  42715  aks4d1p5  42736  aks4d1p6  42737  aks4d1p8d2  42741  aks4d1p8  42743  remexz  42760  hashscontpow1  42777  aks6d1c2lem4  42783  aks6d1c2  42786  bcled  42834  bcle2d  42835  aks6d1c7lem1  42836  dvdsexpnn  42983  fltne  43267  flt4lem7  43282  fltltc  43284  fltnltalem  43285  fltnlta  43286  irrapxlem5  43444  pell14qrgapw  43494  pellqrexplicit  43495  pellqrex  43497  pellfundge  43500  pellfundgt1  43501  jm3.1lem1  43635  jm3.1lem2  43636  hashnzfz2  44922  xralrple4  45979  recnnltrp  45983  rpgtrecnn  45986  fsumnncl  46179  limsup10exlem  46377  stoweidlem31  46636  stoweidlem59  46664  wallispilem3  46672  wallispi  46675  stirlinglem12  46690  stirlinglem15  46693  fourierdlem73  46784  etransclem23  46862  nnfoctbdjlem  47060  ovnsubaddlem1  47175  ovolval5lem1  47257  ovolval5lem2  47258  vonioolem1  47285  vonioolem2  47286  vonicclem2  47289  2timesltsqm1  48004  fmtnoprmfac1lem  48204  sfprmdvdsmersenne  48243  lighneallem2  48246  proththd  48254  perfectALTVlem2  48375  fppr2odd  48384  fpprwppr  48392  fpprel2  48394  gpgedgvtx1  48715  gpg5nbgrvtx03starlem2  48722  gpg5nbgrvtx13starlem2  48725  gpg3nbgrvtx0  48729  pw2m1lepw2m1  49184  logbge0b  49227  logblt1b  49228  logbpw2m1  49231  nnpw2pmod  49247  nnolog2flm1  49254  blennngt2o2  49256  dignnld  49267  digexp  49271  amgmlemALT  50476