Theorem nnrpd 11746

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

Syntax hints:   → wi 4   ∈ wcel 1977  ℕcn 10897  ℝ⁺crp 11708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-rp 11709

This theorem is referenced by:  zgt1rpn0n1  11747  modmulnn  12550  mulp1mod1  12573  modsumfzodifsn  12605  addmodlteq  12607  nnesq  12850  digit1  12860  bcpasc  12970  cshwn  13394  iseralt  14263  mertenslem1  14455  mertenslem2  14456  fprodmodd  14567  ege2le3  14659  eftlub  14678  effsumlt  14680  eirrlem  14771  sqr2irrlem  14816  dvdsmod  14888  bitsfzo  14995  bitsmod  14996  bitscmp  14998  bitsinv1lem  15001  sadaddlem  15026  sadasslem  15030  bitsres  15033  smumul  15053  bezoutlem3  15096  eucalglt  15136  prmind2  15236  crth  15321  eulerthlem2  15325  fermltl  15327  prmdiv  15328  prmdiveq  15329  odzdvds  15338  vfermltlALT  15345  powm2modprm  15346  modprm0  15348  modprmn0modprm0  15350  prmreclem3  15460  prmreclem5  15462  prmreclem6  15463  4sqlem5  15484  4sqlem6  15485  4sqlem7  15486  4sqlem10  15489  4sqlem12  15498  vdwlem1  15523  mndodcong  17784  odmod  17788  oddvds  17789  dfod2  17804  gexexlem  18078  zringlpirlem3  19653  met1stc  22136  met2ndci  22137  lebnumlem3  22570  lebnumii  22573  ovollb2lem  23063  ovoliunlem1  23077  ovoliunlem3  23079  uniioombllem6  23162  itg2cnlem2  23335  elqaalem2  23879  aalioulem2  23892  aalioulem4  23894  aalioulem5  23895  aaliou2b  23900  aaliou3lem9  23909  logfac  24151  cxpeq  24298  leibpi  24469  amgmlem  24516  emcllem1  24522  emcllem2  24523  emcllem3  24524  emcllem5  24526  harmoniclbnd  24535  harmonicubnd  24536  harmonicbnd4  24537  fsumharmonic  24538  zetacvg  24541  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamgulmlem4  24558  lgamgulmlem5  24559  lgamgulmlem6  24560  lgamgulm2  24562  lgambdd  24563  lgamucov  24564  lgamcvg2  24581  gamcvg  24582  gamcvg2lem  24585  regamcl  24587  relgamcl  24588  lgam1  24590  wilthlem1  24594  wilthlem2  24595  basellem1  24607  basellem6  24612  basellem8  24614  chtf  24634  efchtcl  24637  chtge0  24638  vmacl  24644  efvmacl  24646  sgmnncl  24673  chtprm  24679  chtdif  24684  efchtdvds  24685  prmorcht  24704  sgmppw  24722  vmalelog  24730  chtleppi  24735  chtublem  24736  fsumvma2  24739  pclogsum  24740  vmasum  24741  chpchtsum  24744  chpub  24745  logfacubnd  24746  logfaclbnd  24747  logfacbnd3  24748  logfacrlim  24749  logexprlim  24750  logfacrlim2  24751  perfectlem2  24755  bclbnd  24805  bposlem1  24809  bposlem2  24810  bposlem4  24812  bposlem5  24813  bposlem6  24814  bposlem7  24815  bposlem9  24817  lgslem1  24822  lgslem4  24825  lgsvalmod  24841  lgsmod  24848  lgsdirprm  24856  lgsne0  24860  lgsqrlem2  24872  gausslemma2dlem0i  24889  gausslemma2dlem5a  24895  gausslemma2d  24899  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem3  24902  lgseisenlem4  24903  lgseisen  24904  lgsquadlem2  24906  lgsquadlem3  24907  m1lgs  24913  2sqlem8  24951  chebbnd1lem1  24958  chebbnd1lem2  24959  chebbnd1lem3  24960  chebbnd1  24961  chtppilimlem1  24962  chtppilimlem2  24963  chtppilim  24964  chebbnd2  24966  chto1lb  24967  vmadivsum  24971  vmadivsumb  24972  rplogsumlem1  24973  rplogsumlem2  24974  dchrisum0lem1a  24975  rpvmasumlem  24976  dchrisumlema  24977  dchrisumlem1  24978  dchrisumlem2  24979  dchrmusum2  24983  dchrvmasumlem1  24984  dchrvmasum2lem  24985  dchrvmasum2if  24986  dchrvmasumlem2  24987  dchrvmasumlem3  24988  dchrvmasumiflem1  24990  dchrvmasumiflem2  24991  dchrisum0flblem2  24998  dchrisum0fno1  25000  dchrisum0lema  25003  dchrisum0lem1b  25004  dchrisum0lem1  25005  dchrisum0lem2a  25006  dchrisum0lem2  25007  dchrisum0lem3  25008  dchrisum0  25009  dirith2  25017  mudivsum  25019  mulogsumlem  25020  mulogsum  25021  mulog2sumlem1  25023  mulog2sumlem2  25024  mulog2sumlem3  25025  vmalogdivsum2  25027  vmalogdivsum  25028  2vmadivsumlem  25029  logsqvma  25031  log2sumbnd  25033  selberglem1  25034  selberglem2  25035  selberglem3  25036  selberg  25037  selbergb  25038  selberg2lem  25039  selberg2  25040  selberg2b  25041  chpdifbndlem1  25042  logdivbnd  25045  selberg3lem1  25046  selberg3lem2  25047  selberg3  25048  selberg4lem1  25049  selberg4  25050  pntrsumo1  25054  pntrsumbnd2  25056  selbergr  25057  selberg3r  25058  selberg4r  25059  selberg34r  25060  pntsf  25062  pntsval2  25065  pntrlog2bndlem1  25066  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntrlog2bndlem6  25072  pntrlog2bnd  25073  pntpbnd1a  25074  pntpbnd1  25075  pntpbnd2  25076  pntibndlem2  25080  pntlemn  25089  pntlemj  25092  pntlemf  25094  pntlemk  25095  pntlemo  25096  pnt  25103  padicabvcxp  25121  ostth2lem2  25123  ostth2lem3  25124  ostth2lem4  25125  ostth2  25126  ostth3  25127  clwwisshclwwlem1  26333  numclwwlk5  26639  numclwwlk7  26641  ubthlem2  27111  minvecolem3  27116  lnconi  28276  ltesubnnd  28955  2sqmod  28979  madjusmdetlem2  29222  eulerpartlemgc  29751  iprodgam  30881  faclimlem1  30882  faclimlem3  30884  faclim  30885  iprodfac  30886  knoppndvlem17  31689  poimirlem29  32608  heiborlem3  32782  heiborlem5  32784  heiborlem6  32785  heiborlem7  32786  heiborlem8  32787  heibor  32790  rrndstprj2  32800  rrncmslem  32801  rrnequiv  32804  irrapxlem5  36408  pell14qrgapw  36458  pellqrexplicit  36459  pellqrex  36461  pellfundge  36464  pellfundgt1  36465  jm3.1lem1  36602  jm3.1lem2  36603  hashnzfz2  37542  xralrple4  38530  recnnltrp  38534  rpgtrecnn  38538  fsumnncl  38638  stoweidlem31  38924  stoweidlem59  38952  wallispilem3  38960  wallispi  38963  stirlinglem12  38978  stirlinglem15  38981  fourierdlem73  39072  etransclem23  39150  nnfoctbdjlem  39348  ovnsubaddlem1  39460  ovolval5lem1  39542  ovolval5lem2  39543  vonioolem1  39571  vonioolem2  39572  vonicclem2  39575  fmtnoprmfac1lem  40014  sfprmdvdsmersenne  40058  lighneallem2  40061  proththd  40069  perfectALTVlem2  40165  clwwisshclwwslemlem  41233  av-numclwwlk5  41542  av-numclwwlk7  41545  pw2m1lepw2m1  42104  logbge0b  42155  logblt1b  42156  logbpw2m1  42159  nnpw2pmod  42175  nnolog2flm1  42182  blennngt2o2  42184  dignnld  42195  digexp  42199  amgmlemALT  42358