Theorem nnrp 13028

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

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5123  ℝcr 11136  0cc0 11137   < clt 11277  ℕcn 12248  ℝ⁺crp 13016

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 2706  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737  ax-resscn 11194  ax-1cn 11195  ax-icn 11196  ax-addcl 11197  ax-addrcl 11198  ax-mulcl 11199  ax-mulrcl 11200  ax-mulcom 11201  ax-addass 11202  ax-mulass 11203  ax-distr 11204  ax-i2m1 11205  ax-1ne0 11206  ax-1rid 11207  ax-rnegex 11208  ax-rrecex 11209  ax-cnre 11210  ax-pre-lttri 11211  ax-pre-lttrn 11212  ax-pre-ltadd 11213  ax-pre-mulgt0 11214

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 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-tr 5240  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-pred 6301  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7870  df-2nd 7997  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-er 8727  df-en 8968  df-dom 8969  df-sdom 8970  df-pnf 11279  df-mnf 11280  df-xr 11281  df-ltxr 11282  df-le 11283  df-sub 11476  df-neg 11477  df-nn 12249  df-rp 13017

This theorem is referenced by:  nnrpd  13057  nn0ledivnn  13130  adddivflid  13840  divfl0  13846  fldivnn0le  13854  zmodcl  13913  zmodfz  13915  zmodid2  13921  m1modnnsub1  13940  addmodid  13942  modifeq2int  13956  modaddmodup  13957  modaddmodlo  13958  modsumfzodifsn  13967  addmodlteq  13969  nnesq  14249  digit2  14258  digit1  14259  bcrpcl  14330  bcval5  14340  lswccatn0lsw  14612  cshw0  14815  cshwmodn  14816  cshwsublen  14817  cshwidxmod  14824  cshwidxmodr  14825  cshwidxm1  14828  cshwidxm  14829  repswcshw  14833  2cshw  14834  cshweqrep  14842  modfsummods  15812  divcnv  15872  supcvg  15875  harmonic  15878  expcnv  15883  rpnnen2lem11  16243  sqrt2irr  16268  dvdsval3  16277  dvdsmodexp  16281  moddvds  16284  divalgmod  16426  flodddiv4  16435  modgcd  16552  divgcdcoprm0  16685  isprm5  16727  isprm6  16734  nnnn0modprm0  16827  pythagtriplem13  16848  fldivp1  16918  prmreclem5  16941  prmreclem6  16942  4sqlem12  16977  modxai  17089  modsubi  17093  smndex1iidm  18884  smndex1n0mnd  18895  mulgmodid  19101  odmodnn0  19527  gexdvds  19571  sylow1lem1  19585  gexexlem  19839  znf1o  21525  met1stc  24479  lmnn  25234  bcthlem5  25299  minveclem3  25400  vitali  25585  ismbf3d  25626  itg2seq  25714  plyeq0lem  26186  elqaalem3  26300  aalioulem6  26316  aaliou  26317  logtayllem  26638  sqrt2cxp2logb9e3  26779  atan1  26908  leibpi  26922  birthdaylem2  26932  dfef2  26951  divsqrtsumlem  26960  emcllem1  26976  emcllem2  26977  emcllem3  26978  emcllem4  26979  emcllem6  26981  zetacvg  26995  lgam1  27044  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  29763  crctcshwlkn0lem6  29764  lnconi  31981  rpdp2cl  32809  rpdp2cl2  32810  hgt750lem  34641  hgt750lem2  34642  hgt750leme  34648  circum  35654  bccolsum  35714  faclimlem3  35720  faclim  35721  poimirlem29  37631  poimirlem30  37632  poimirlem31  37633  poimirlem32  37634  mblfinlem3  37641  itg2addnclem2  37654  itg2addnc  37656  3lexlogpow2ineq1  42034  2ap1caineq  42121  pellexlem4  42821  pell1qrgaplem  42862  pellqrex  42868  congrep  42963  acongeq  42973  proot1ex  43186  hashnzfzclim  44313  xrralrecnnle  45366  nnrecrp  45369  xrralrecnnge  45373  iooiinicc  45527  iooiinioc  45541  fprodsubrecnncnvlem  45894  fprodaddrecnncnvlem  45896  wallispilem4  46055  wallispi  46057  wallispi2lem1  46058  wallispi2lem2  46059  stirlinglem1  46061  stirlinglem2  46062  stirlinglem3  46063  stirlinglem4  46064  stirlinglem6  46066  stirlinglem7  46067  stirlinglem10  46070  stirlinglem11  46071  stirlinglem13  46073  stirlinglem14  46074  stirlinglem15  46075  stirlingr  46077  dirkertrigeqlem1  46085  hoicvrrex  46543  ovnsubaddlem2  46558  hoiqssbllem3  46611  iinhoiicc  46661  iunhoiioo  46663  vonioolem1  46667  vonioolem2  46668  vonicclem1  46670  vonicclem2  46671  preimageiingt  46707  preimaleiinlt  46708  addmodne  47319  submodlt  47325  fsummmodsndifre  47334  mod42tp1mod8  47562  lighneallem2  47566  3exp4mod41  47576  41prothprmlem2  47578  perfectALTVlem2  47682  2exp340mod341  47693  8exp8mod9  47696  nfermltl8rev  47702  gpgedgvtx0  47992  gpgedgvtx1  47993  gpgvtxedg0  47994  gpgvtxedg1  47995  gpg3kgrtriexlem1  48012  gpg3kgrtriexlem2  48013  mod0mul  48413  modn0mul  48414  m1modmmod  48415  difmodm1lt  48416  nnlog2ge0lt1  48460  blennnelnn  48470  nnpw2blen  48474  blen1b  48482  blennnt2  48483  blennn0e2  48488  dignn0fr  48495  dignn0ldlem  48496  dignnld  48497  dig2nn1st  48499  dig0  48500