Theorem nnrpd 13085

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℕcn 12258  ℝ⁺crp 13043

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-resscn 11182  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-addrcl 11186  ax-mulcl 11187  ax-mulrcl 11188  ax-mulcom 11189  ax-addass 11190  ax-mulass 11191  ax-distr 11192  ax-i2m1 11193  ax-1ne0 11194  ax-1rid 11195  ax-rnegex 11196  ax-rrecex 11197  ax-cnre 11198  ax-pre-lttri 11199  ax-pre-lttrn 11200  ax-pre-ltadd 11201  ax-pre-mulgt0 11202

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  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 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7864  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-er 8697  df-en 8954  df-dom 8955  df-sdom 8956  df-pnf 11270  df-mnf 11271  df-xr 11272  df-ltxr 11273  df-le 11274  df-sub 11468  df-neg 11469  df-nn 12259  df-rp 13044

This theorem is used by:  zgt1rpn0n1  13086  modmulnn  13951  modaddid  13972  mulp1mod1  13976  modsumfzodifsn  14009  addmodlteq  14011  nnesq  14292  digit1  14302  bcpasc  14386  cshwn  14869  iseralt  15773  climcndslem2  15940  mertenslem1  15974  mertenslem2  15975  fprodmodd  16085  efcllem  16164  ege2le3  16177  eftlub  16198  effsumlt  16200  eirrlem  16293  sqrt2irrlem  16337  p1modz1  16350  dvdsmod  16420  bitsfzo  16526  bitsmod  16527  bitscmp  16529  bitsinv1lem  16532  sadaddlem  16557  sadasslem  16561  bitsres  16564  smumul  16584  bezoutlem3  16632  eucalglt  16676  prmind2  16776  prmdvdsbc  16818  crth  16870  eulerthlem2  16874  fermltl  16876  prmdiv  16877  prmdiveq  16878  odzdvds  16888  vfermltlALT  16895  powm2modprm  16896  modprm0  16898  modprmn0modprm0  16900  prmreclem3  17011  prmreclem5  17013  prmreclem6  17014  4sqlem5  17035  4sqlem6  17036  4sqlem7  17037  4sqlem10  17040  4sqlem12  17049  vdwlem1  17074  mndodcong  19670  odmod  19674  oddvds  19675  dfod2  19692  gexexlem  19980  zringlpirlem3  21678  fermltlchr  21743  met1stc  24748  met2ndci  24749  lebnumlem3  25192  lebnumii  25195  ovollb2lem  25717  ovoliunlem1  25731  ovoliunlem3  25733  uniioombllem6  25817  itg2cnlem2  25991  elqaalem2  26553  aalioulem2  26570  aalioulem4  26572  aalioulem5  26573  aaliou2b  26578  aaliou3lem9  26587  logfac  26839  cxpeq  26995  zrtelqelz  26996  rtprmirr  26998  logbgcd1irr  27032  leibpi  27180  birthdaylem2  27190  amgmlem  27227  emcllem1  27233  emcllem2  27234  emcllem3  27235  emcllem5  27237  harmoniclbnd  27246  harmonicubnd  27247  harmonicbnd4  27248  fsumharmonic  27249  zetacvg  27252  lgamgulmlem2  27267  lgamgulmlem3  27268  lgamgulmlem4  27269  lgamgulmlem5  27270  lgamgulmlem6  27271  lgamgulm2  27273  lgambdd  27274  lgamucov  27275  lgamcvg2  27292  gamcvg  27293  gamcvg2lem  27296  regamcl  27298  relgamcl  27299  lgam1  27301  wilthlem1  27305  wilthlem2  27306  basellem1  27318  basellem6  27323  basellem8  27325  chtf  27345  efchtcl  27348  chtge0  27349  vmacl  27355  efvmacl  27357  sgmnncl  27384  chtprm  27390  chtdif  27395  efchtdvds  27396  prmorcht  27415  sgmppw  27434  vmalelog  27442  chtleppi  27447  chtublem  27448  fsumvma2  27451  pclogsum  27452  vmasum  27453  chpchtsum  27456  chpub  27457  logfacubnd  27458  logfaclbnd  27459  logfacbnd3  27460  logfacrlim  27461  logexprlim  27462  logfacrlim2  27463  perfectlem2  27467  bclbnd  27517  bposlem1  27521  bposlem2  27522  bposlem4  27524  bposlem5  27525  bposlem6  27526  bposlem7  27527  bposlem9  27529  lgslem1  27534  lgsvalmod  27553  lgsmod  27560  lgsdirprm  27568  lgsne0  27572  lgsqrlem2  27584  gausslemma2dlem0i  27601  gausslemma2dlem5a  27607  gausslemma2d  27611  lgseisenlem1  27612  lgseisenlem2  27613  lgseisenlem3  27614  lgseisenlem4  27615  lgseisen  27616  lgsquadlem2  27618  lgsquadlem3  27619  m1lgs  27625  2sqlem8  27663  2sqmod  27673  chebbnd1lem1  27706  chebbnd1lem2  27707  chebbnd1lem3  27708  chebbnd1  27709  chtppilimlem1  27710  chtppilimlem2  27711  chtppilim  27712  chebbnd2  27714  chto1lb  27715  vmadivsum  27719  vmadivsumb  27720  rplogsumlem1  27721  rplogsumlem2  27722  dchrisum0lem1a  27723  rpvmasumlem  27724  dchrisumlema  27725  dchrisumlem1  27726  dchrisumlem2  27727  dchrmusum2  27731  dchrvmasumlem1  27732  dchrvmasum2lem  27733  dchrvmasum2if  27734  dchrvmasumlem2  27735  dchrvmasumlem3  27736  dchrvmasumiflem1  27738  dchrvmasumiflem2  27739  dchrisum0flblem2  27746  dchrisum0fno1  27748  dchrisum0lema  27751  dchrisum0lem1b  27752  dchrisum0lem1  27753  dchrisum0lem2a  27754  dchrisum0lem2  27755  dchrisum0lem3  27756  dchrisum0  27757  dirith2  27765  mudivsum  27767  mulogsumlem  27768  mulogsum  27769  mulog2sumlem1  27771  mulog2sumlem2  27772  mulog2sumlem3  27773  vmalogdivsum2  27775  vmalogdivsum  27776  2vmadivsumlem  27777  logsqvma  27779  log2sumbnd  27781  selberglem1  27782  selberglem2  27783  selberglem3  27784  selberg  27785  selbergb  27786  selberg2lem  27787  selberg2  27788  selberg2b  27789  chpdifbndlem1  27790  logdivbnd  27793  selberg3lem1  27794  selberg3lem2  27795  selberg3  27796  selberg4lem1  27797  selberg4  27798  pntrsumo1  27802  pntrsumbnd2  27804  selbergr  27805  selberg3r  27806  selberg4r  27807  selberg34r  27808  pntsf  27810  pntsval2  27813  pntrlog2bndlem1  27814  pntrlog2bndlem2  27815  pntrlog2bndlem3  27816  pntrlog2bndlem4  27817  pntrlog2bndlem5  27818  pntrlog2bndlem6  27820  pntrlog2bnd  27821  pntpbnd1a  27822  pntpbnd1  27823  pntpbnd2  27824  pntibndlem2  27828  pntlemn  27837  pntlemj  27840  pntlemf  27842  pntlemk  27843  pntlemo  27844  pnt  27851  padicabvcxp  27869  ostth2lem2  27871  ostth2lem3  27872  ostth2lem4  27873  ostth2  27874  ostth3  27875  clwwisshclwwslemlem  30484  numclwwlk5  30869  numclwwlk7  30872  nrt2irr  30954  ubthlem2  31353  minvecolem3  31358  lnconi  32515  ltesubnnd  33294  2exple2exp  33305  cshwrnid  33402  cycpmfv2  33555  znfermltl  33802  madjusmdetlem2  34339  eulerpartlemgc  34874  reprle  35123  hgt750lemc  35156  hgt750lemd  35157  hgt750lemb  35165  hgt750leme  35167  tgoldbachgtde  35169  iprodgam  36322  faclimlem1  36323  faclimlem3  36325  faclim  36326  iprodfac  36327  knoppndvlem17  37226  poimirlem29  38399  heiborlem3  38564  heiborlem5  38566  heiborlem6  38567  heiborlem7  38568  heiborlem8  38569  heibor  38572  rrndstprj2  38582  rrncmslem  38583  rrnequiv  38586  lcmineqlem20  42915  lcmineqlem23  42918  3lexlogpow5ineq2  42922  3lexlogpow2ineq2  42926  aks4d1p5  42947  aks4d1p6  42948  aks4d1p8d2  42952  aks4d1p8  42954  remexz  42971  hashscontpow1  42988  aks6d1c2lem4  42994  aks6d1c2  42997  bcled  43045  bcle2d  43046  aks6d1c7lem1  43047  dvdsexpnn  43209  fltne  43491  flt4lem7  43506  fltltc  43508  fltnltalem  43509  fltnlta  43510  irrapxlem5  43668  pell14qrgapw  43718  pellqrexplicit  43719  pellqrex  43721  pellfundge  43724  pellfundgt1  43725  jm3.1lem1  43859  jm3.1lem2  43860  hashnzfz2  45146  xralrple4  46203  recnnltrp  46207  rpgtrecnn  46210  fsumnncl  46403  limsup10exlem  46601  stoweidlem31  46860  stoweidlem59  46888  wallispilem3  46896  wallispi  46899  stirlinglem12  46914  stirlinglem15  46917  fourierdlem73  47008  etransclem23  47086  nnfoctbdjlem  47284  ovnsubaddlem1  47399  ovolval5lem1  47481  ovolval5lem2  47482  vonioolem1  47509  vonioolem2  47510  vonicclem2  47513  2timesltsqm1  48268  fmtnoprmfac1lem  48468  sfprmdvdsmersenne  48507  lighneallem2  48510  proththd  48518  perfectALTVlem2  48639  fppr2odd  48648  fpprwppr  48656  fpprel2  48658  gpgedgvtx1  48979  gpg5nbgrvtx03starlem2  48986  gpg5nbgrvtx13starlem2  48989  gpg3nbgrvtx0  48993  pw2m1lepw2m1  49451  logbge0b  49494  logblt1b  49495  logbpw2m1  49498  nnpw2pmod  49514  nnolog2flm1  49521  blennngt2o2  49523  dignnld  49534  digexp  49538  amgmlemALT  50822