Theorem nnrp 12945

Description: A positive integer is a positive real. (Contributed by NM, 28-Nov-2008.)

Assertion

Ref	Expression
nnrp	⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)

Proof of Theorem nnrp

Step	Hyp	Ref	Expression
1		nnre 12172	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nngt0 12199	. 2 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)
3		elrp 12935	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 589	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2119   class class class wbr 5072  ℝcr 11028  0cc0 11029   < clt 11170  ℕcn 12165  ℝ⁺crp 12933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-rp 12934

This theorem is referenced by:  nnrpd  12975  nn0ledivnn  13048  adddivflid  13768  divfl0  13774  fldivnn0le  13782  zmodcl  13841  zmodfz  13843  zmodid2  13849  m1modnnsub1  13870  addmodid  13872  modifeq2int  13886  modaddmodup  13887  modaddmodlo  13888  modsumfzodifsn  13897  addmodlteq  13899  nnesq  14180  digit2  14189  digit1  14190  bcrpcl  14261  bcval5  14271  lswccatn0lsw  14545  cshw0  14747  cshwmodn  14748  cshwsublen  14749  cshwidxmod  14756  cshwidxmodr  14757  cshwidxm1  14760  cshwidxm  14761  repswcshw  14765  2cshw  14766  cshweqrep  14774  modfsummods  15747  divcnv  15809  supcvg  15812  harmonic  15815  expcnv  15820  rpnnen2lem11  16182  sqrt2irr  16207  dvdsval3  16216  dvdsmodexp  16220  moddvds  16223  divalgmod  16366  flodddiv4  16375  modgcd  16492  divgcdcoprm0  16625  isprm5  16668  isprm6  16675  nnnn0modprm0  16768  pythagtriplem13  16789  fldivp1  16859  prmreclem5  16882  prmreclem6  16883  4sqlem12  16918  modxai  17030  modsubi  17034  smndex1iidm  18860  smndex1n0mnd  18874  mulgmodid  19080  odmodnn0  19506  gexdvds  19550  sylow1lem1  19564  gexexlem  19818  znf1o  21526  met1stc  24504  lmnn  25248  bcthlem5  25313  minveclem3  25414  vitali  25598  ismbf3d  25639  itg2seq  25727  plyeq0lem  26193  elqaalem3  26305  aalioulem6  26321  aaliou  26322  logtayllem  26641  sqrt2cxp2logb9e3  26781  atan1  26910  leibpi  26924  birthdaylem2  26934  dfef2  26952  divsqrtsumlem  26961  emcllem1  26977  emcllem2  26978  emcllem3  26979  emcllem4  26980  emcllem6  26982  zetacvg  26996  lgam1  27045  ppiub  27185  vmalelog  27186  logfacbnd3  27204  logexprlim  27206  bcmono  27258  bclbnd  27261  bposlem1  27265  bposlem7  27271  bposlem8  27272  bposlem9  27273  gausslemma2dlem1a  27346  gausslemma2dlem4  27350  gausslemma2dlem6  27353  m1lgs  27369  2lgslem1a1  27370  2lgslem3a1  27381  2lgslem3b1  27382  2lgslem3c1  27383  2lgslem3d1  27384  2lgslem4  27387  2lgsoddprmlem2  27390  2sqreultlem  27428  2sqreunnltlem  27431  rplogsumlem1  27465  dchrisumlema  27469  dchrisumlem2  27471  dchrisumlem3  27472  dchrvmasumlem2  27479  dchrvmasumiflem1  27482  dchrisum0lem1b  27496  dchrisum0lem2a  27498  rplogsum  27508  logdivsum  27514  mulog2sumlem2  27516  logsqvma  27523  logsqvma2  27524  log2sumbnd  27525  selberg2lem  27531  logdivbnd  27537  pntrsumo1  27546  pntrsumbnd  27547  pntibndlem1  27570  pntibndlem2  27572  pntibndlem3  27573  pntlemd  27575  pntlema  27577  pntlemb  27578  pntlemr  27583  pntlemj  27584  pntlemf  27586  pntlemo  27588  crctcshwlkn0lem5  29900  crctcshwlkn0lem6  29901  lnconi  32122  rpdp2cl  32960  rpdp2cl2  32961  hgt750lem  34835  hgt750lem2  34836  hgt750leme  34842  circum  35902  bccolsum  35967  faclimlem3  35973  faclim  35974  poimirlem29  38016  poimirlem30  38017  poimirlem31  38018  poimirlem32  38019  mblfinlem3  38026  itg2addnclem2  38039  itg2addnc  38041  3lexlogpow2ineq1  42543  2ap1caineq  42630  pellexlem4  43277  pell1qrgaplem  43318  pellqrex  43324  congrep  43418  acongeq  43428  proot1ex  43641  hashnzfzclim  44766  xrralrecnnle  45827  nnrecrp  45830  xrralrecnnge  45834  iooiinicc  45987  iooiinioc  46001  fprodsubrecnncnvlem  46350  fprodaddrecnncnvlem  46352  wallispilem4  46511  wallispi  46513  wallispi2lem1  46514  wallispi2lem2  46515  stirlinglem1  46517  stirlinglem2  46518  stirlinglem3  46519  stirlinglem4  46520  stirlinglem6  46522  stirlinglem7  46523  stirlinglem10  46526  stirlinglem11  46527  stirlinglem13  46529  stirlinglem14  46530  stirlinglem15  46531  stirlingr  46533  dirkertrigeqlem1  46541  hoicvrrex  46999  ovnsubaddlem2  47014  hoiqssbllem3  47067  iinhoiicc  47117  iunhoiioo  47119  vonioolem1  47123  vonioolem2  47124  vonicclem1  47126  vonicclem2  47127  nnmul2  47793  flmrecm1  47806  addmodne  47813  submodlt  47819  mod0mul  47825  modn0mul  47826  m1modmmod  47827  difmodm1lt  47828  modlt0b  47832  mod2addne  47833  fsummmodsndifre  47845  mod42tp1mod8  48080  lighneallem2  48084  3exp4mod41  48094  41prothprmlem2  48096  perfectALTVlem2  48213  2exp340mod341  48224  8exp8mod9  48227  nfermltl8rev  48233  gpgedgvtx0  48552  gpgedgvtx1  48553  gpgvtxedg0  48554  gpgvtxedg1  48555  gpg3kgrtriexlem1  48574  gpg3kgrtriexlem2  48575  nnlog2ge0lt1  49057  blennnelnn  49067  nnpw2blen  49071  blen1b  49079  blennnt2  49080  blennn0e2  49085  dignn0fr  49092  dignn0ldlem  49093  dignnld  49094  dig2nn1st  49096  dig0  49097