Theorem nnrp 13047

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 12274	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nngt0 12298	. 2 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)
3		elrp 13037	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 583	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5142  ℝcr 11155  0cc0 11156   < clt 11296  ℕcn 12267  ℝ⁺crp 13035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-er 8746  df-en 8987  df-dom 8988  df-sdom 8989  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-nn 12268  df-rp 13036

This theorem is referenced by:  nnrpd  13076  nn0ledivnn  13149  adddivflid  13859  divfl0  13865  fldivnn0le  13873  zmodcl  13932  zmodfz  13934  zmodid2  13940  m1modnnsub1  13959  addmodid  13961  modifeq2int  13975  modaddmodup  13976  modaddmodlo  13977  modsumfzodifsn  13986  addmodlteq  13988  nnesq  14267  digit2  14276  digit1  14277  bcrpcl  14348  bcval5  14358  lswccatn0lsw  14630  cshw0  14833  cshwmodn  14834  cshwsublen  14835  cshwidxmod  14842  cshwidxmodr  14843  cshwidxm1  14846  cshwidxm  14847  repswcshw  14851  2cshw  14852  cshweqrep  14860  modfsummods  15830  divcnv  15890  supcvg  15893  harmonic  15896  expcnv  15901  rpnnen2lem11  16261  sqrt2irr  16286  dvdsval3  16295  dvdsmodexp  16299  moddvds  16302  divalgmod  16444  flodddiv4  16453  modgcd  16570  divgcdcoprm0  16703  isprm5  16745  isprm6  16752  nnnn0modprm0  16845  pythagtriplem13  16866  fldivp1  16936  prmreclem5  16959  prmreclem6  16960  4sqlem12  16995  modxai  17107  modsubi  17111  smndex1iidm  18915  smndex1n0mnd  18926  mulgmodid  19132  odmodnn0  19559  gexdvds  19603  sylow1lem1  19617  gexexlem  19871  znf1o  21571  met1stc  24535  lmnn  25298  bcthlem5  25363  minveclem3  25464  vitali  25649  ismbf3d  25690  itg2seq  25778  plyeq0lem  26250  elqaalem3  26364  aalioulem6  26380  aaliou  26381  logtayllem  26702  sqrt2cxp2logb9e3  26843  atan1  26972  leibpi  26986  birthdaylem2  26996  dfef2  27015  divsqrtsumlem  27024  emcllem1  27040  emcllem2  27041  emcllem3  27042  emcllem4  27043  emcllem6  27045  zetacvg  27059  lgam1  27108  ppiub  27249  vmalelog  27250  logfacbnd3  27268  logexprlim  27270  bcmono  27322  bclbnd  27325  bposlem1  27329  bposlem7  27335  bposlem8  27336  bposlem9  27337  gausslemma2dlem1a  27410  gausslemma2dlem4  27414  gausslemma2dlem6  27417  m1lgs  27433  2lgslem1a1  27434  2lgslem3a1  27445  2lgslem3b1  27446  2lgslem3c1  27447  2lgslem3d1  27448  2lgslem4  27451  2lgsoddprmlem2  27454  2sqreultlem  27492  2sqreunnltlem  27495  rplogsumlem1  27529  dchrisumlema  27533  dchrisumlem2  27535  dchrisumlem3  27536  dchrvmasumlem2  27543  dchrvmasumiflem1  27546  dchrisum0lem1b  27560  dchrisum0lem2a  27562  rplogsum  27572  logdivsum  27578  mulog2sumlem2  27580  logsqvma  27587  logsqvma2  27588  log2sumbnd  27589  selberg2lem  27595  logdivbnd  27601  pntrsumo1  27610  pntrsumbnd  27611  pntibndlem1  27634  pntibndlem2  27636  pntibndlem3  27637  pntlemd  27639  pntlema  27641  pntlemb  27642  pntlemr  27647  pntlemj  27648  pntlemf  27650  pntlemo  27652  crctcshwlkn0lem5  29835  crctcshwlkn0lem6  29836  lnconi  32053  rpdp2cl  32865  rpdp2cl2  32866  hgt750lem  34667  hgt750lem2  34668  hgt750leme  34674  circum  35680  bccolsum  35740  faclimlem3  35746  faclim  35747  poimirlem29  37657  poimirlem30  37658  poimirlem31  37659  poimirlem32  37660  mblfinlem3  37667  itg2addnclem2  37680  itg2addnc  37682  3lexlogpow2ineq1  42060  2ap1caineq  42147  pellexlem4  42848  pell1qrgaplem  42889  pellqrex  42895  congrep  42990  acongeq  43000  proot1ex  43213  hashnzfzclim  44346  xrralrecnnle  45399  nnrecrp  45402  xrralrecnnge  45406  iooiinicc  45560  iooiinioc  45574  fprodsubrecnncnvlem  45927  fprodaddrecnncnvlem  45929  wallispilem4  46088  wallispi  46090  wallispi2lem1  46091  wallispi2lem2  46092  stirlinglem1  46094  stirlinglem2  46095  stirlinglem3  46096  stirlinglem4  46097  stirlinglem6  46099  stirlinglem7  46100  stirlinglem10  46103  stirlinglem11  46104  stirlinglem13  46106  stirlinglem14  46107  stirlinglem15  46108  stirlingr  46110  dirkertrigeqlem1  46118  hoicvrrex  46576  ovnsubaddlem2  46591  hoiqssbllem3  46644  iinhoiicc  46694  iunhoiioo  46696  vonioolem1  46700  vonioolem2  46701  vonicclem1  46703  vonicclem2  46704  preimageiingt  46740  preimaleiinlt  46741  addmodne  47351  submodlt  47357  fsummmodsndifre  47366  mod42tp1mod8  47594  lighneallem2  47598  3exp4mod41  47608  41prothprmlem2  47610  perfectALTVlem2  47714  2exp340mod341  47725  8exp8mod9  47728  nfermltl8rev  47734  gpgedgvtx0  48024  gpgedgvtx1  48025  gpgvtxedg0  48026  gpgvtxedg1  48027  gpg3kgrtriexlem1  48044  gpg3kgrtriexlem2  48045  mod0mul  48445  modn0mul  48446  m1modmmod  48447  difmodm1lt  48448  nnlog2ge0lt1  48492  blennnelnn  48502  nnpw2blen  48506  blen1b  48514  blennnt2  48515  blennn0e2  48520  dignn0fr  48527  dignn0ldlem  48528  dignnld  48529  dig2nn1st  48531  dig0  48532