Theorem nnrp 13025

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5124  ℝcr 11133  0cc0 11134   < clt 11274  ℕcn 12245  ℝ⁺crp 13013

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  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 4889  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-nn 12246  df-rp 13014

This theorem is referenced by:  nnrpd  13054  nn0ledivnn  13127  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  14250  digit2  14259  digit1  14260  bcrpcl  14331  bcval5  14341  lswccatn0lsw  14614  cshw0  14817  cshwmodn  14818  cshwsublen  14819  cshwidxmod  14826  cshwidxmodr  14827  cshwidxm1  14830  cshwidxm  14831  repswcshw  14835  2cshw  14836  cshweqrep  14844  modfsummods  15814  divcnv  15874  supcvg  15877  harmonic  15880  expcnv  15885  rpnnen2lem11  16247  sqrt2irr  16272  dvdsval3  16281  dvdsmodexp  16285  moddvds  16288  divalgmod  16430  flodddiv4  16439  modgcd  16556  divgcdcoprm0  16689  isprm5  16731  isprm6  16738  nnnn0modprm0  16831  pythagtriplem13  16852  fldivp1  16922  prmreclem5  16945  prmreclem6  16946  4sqlem12  16981  modxai  17093  modsubi  17097  smndex1iidm  18884  smndex1n0mnd  18895  mulgmodid  19101  odmodnn0  19526  gexdvds  19570  sylow1lem1  19584  gexexlem  19838  znf1o  21517  met1stc  24465  lmnn  25220  bcthlem5  25285  minveclem3  25386  vitali  25571  ismbf3d  25612  itg2seq  25700  plyeq0lem  26172  elqaalem3  26286  aalioulem6  26302  aaliou  26303  logtayllem  26625  sqrt2cxp2logb9e3  26766  atan1  26895  leibpi  26909  birthdaylem2  26919  dfef2  26938  divsqrtsumlem  26947  emcllem1  26963  emcllem2  26964  emcllem3  26965  emcllem4  26966  emcllem6  26968  zetacvg  26982  lgam1  27031  ppiub  27172  vmalelog  27173  logfacbnd3  27191  logexprlim  27193  bcmono  27245  bclbnd  27248  bposlem1  27252  bposlem7  27258  bposlem8  27259  bposlem9  27260  gausslemma2dlem1a  27333  gausslemma2dlem4  27337  gausslemma2dlem6  27340  m1lgs  27356  2lgslem1a1  27357  2lgslem3a1  27368  2lgslem3b1  27369  2lgslem3c1  27370  2lgslem3d1  27371  2lgslem4  27374  2lgsoddprmlem2  27377  2sqreultlem  27415  2sqreunnltlem  27418  rplogsumlem1  27452  dchrisumlema  27456  dchrisumlem2  27458  dchrisumlem3  27459  dchrvmasumlem2  27466  dchrvmasumiflem1  27469  dchrisum0lem1b  27483  dchrisum0lem2a  27485  rplogsum  27495  logdivsum  27501  mulog2sumlem2  27503  logsqvma  27510  logsqvma2  27511  log2sumbnd  27512  selberg2lem  27518  logdivbnd  27524  pntrsumo1  27533  pntrsumbnd  27534  pntibndlem1  27557  pntibndlem2  27559  pntibndlem3  27560  pntlemd  27562  pntlema  27564  pntlemb  27565  pntlemr  27570  pntlemj  27571  pntlemf  27573  pntlemo  27575  crctcshwlkn0lem5  29801  crctcshwlkn0lem6  29802  lnconi  32019  rpdp2cl  32861  rpdp2cl2  32862  hgt750lem  34688  hgt750lem2  34689  hgt750leme  34695  circum  35701  bccolsum  35761  faclimlem3  35767  faclim  35768  poimirlem29  37678  poimirlem30  37679  poimirlem31  37680  poimirlem32  37681  mblfinlem3  37688  itg2addnclem2  37701  itg2addnc  37703  3lexlogpow2ineq1  42076  2ap1caineq  42163  pellexlem4  42830  pell1qrgaplem  42871  pellqrex  42877  congrep  42972  acongeq  42982  proot1ex  43195  hashnzfzclim  44321  xrralrecnnle  45390  nnrecrp  45393  xrralrecnnge  45397  iooiinicc  45551  iooiinioc  45565  fprodsubrecnncnvlem  45916  fprodaddrecnncnvlem  45918  wallispilem4  46077  wallispi  46079  wallispi2lem1  46080  wallispi2lem2  46081  stirlinglem1  46083  stirlinglem2  46084  stirlinglem3  46085  stirlinglem4  46086  stirlinglem6  46088  stirlinglem7  46089  stirlinglem10  46092  stirlinglem11  46093  stirlinglem13  46095  stirlinglem14  46096  stirlinglem15  46097  stirlingr  46099  dirkertrigeqlem1  46107  hoicvrrex  46565  ovnsubaddlem2  46580  hoiqssbllem3  46633  iinhoiicc  46683  iunhoiioo  46685  vonioolem1  46689  vonioolem2  46690  vonicclem1  46692  vonicclem2  46693  preimageiingt  46729  preimaleiinlt  46730  addmodne  47353  submodlt  47359  fsummmodsndifre  47368  mod42tp1mod8  47596  lighneallem2  47600  3exp4mod41  47610  41prothprmlem2  47612  perfectALTVlem2  47716  2exp340mod341  47727  8exp8mod9  47730  nfermltl8rev  47736  gpgedgvtx0  48045  gpgedgvtx1  48046  gpgvtxedg0  48047  gpgvtxedg1  48048  gpg3kgrtriexlem1  48065  gpg3kgrtriexlem2  48066  mod0mul  48479  modn0mul  48480  m1modmmod  48481  difmodm1lt  48482  nnlog2ge0lt1  48526  blennnelnn  48536  nnpw2blen  48540  blen1b  48548  blennnt2  48549  blennn0e2  48554  dignn0fr  48561  dignn0ldlem  48562  dignnld  48563  dig2nn1st  48565  dig0  48566