Theorem nnrp 12915

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5096  ℝcr 11023  0cc0 11024   < clt 11164  ℕcn 12143  ℝ⁺crp 12903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100  ax-pre-mulgt0 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  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 8882  df-dom 8883  df-sdom 8884  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170  df-sub 11364  df-neg 11365  df-nn 12144  df-rp 12904

This theorem is referenced by:  nnrpd  12945  nn0ledivnn  13018  adddivflid  13736  divfl0  13742  fldivnn0le  13750  zmodcl  13809  zmodfz  13811  zmodid2  13817  m1modnnsub1  13838  addmodid  13840  modifeq2int  13854  modaddmodup  13855  modaddmodlo  13856  modsumfzodifsn  13865  addmodlteq  13867  nnesq  14148  digit2  14157  digit1  14158  bcrpcl  14229  bcval5  14239  lswccatn0lsw  14513  cshw0  14715  cshwmodn  14716  cshwsublen  14717  cshwidxmod  14724  cshwidxmodr  14725  cshwidxm1  14728  cshwidxm  14729  repswcshw  14733  2cshw  14734  cshweqrep  14742  modfsummods  15714  divcnv  15774  supcvg  15777  harmonic  15780  expcnv  15785  rpnnen2lem11  16147  sqrt2irr  16172  dvdsval3  16181  dvdsmodexp  16185  moddvds  16188  divalgmod  16331  flodddiv4  16340  modgcd  16457  divgcdcoprm0  16590  isprm5  16632  isprm6  16639  nnnn0modprm0  16732  pythagtriplem13  16753  fldivp1  16823  prmreclem5  16846  prmreclem6  16847  4sqlem12  16882  modxai  16994  modsubi  16998  smndex1iidm  18824  smndex1n0mnd  18835  mulgmodid  19041  odmodnn0  19467  gexdvds  19511  sylow1lem1  19525  gexexlem  19779  znf1o  21504  met1stc  24463  lmnn  25217  bcthlem5  25282  minveclem3  25383  vitali  25568  ismbf3d  25609  itg2seq  25697  plyeq0lem  26169  elqaalem3  26283  aalioulem6  26299  aaliou  26300  logtayllem  26622  sqrt2cxp2logb9e3  26763  atan1  26892  leibpi  26906  birthdaylem2  26916  dfef2  26935  divsqrtsumlem  26944  emcllem1  26960  emcllem2  26961  emcllem3  26962  emcllem4  26963  emcllem6  26965  zetacvg  26979  lgam1  27028  ppiub  27169  vmalelog  27170  logfacbnd3  27188  logexprlim  27190  bcmono  27242  bclbnd  27245  bposlem1  27249  bposlem7  27255  bposlem8  27256  bposlem9  27257  gausslemma2dlem1a  27330  gausslemma2dlem4  27334  gausslemma2dlem6  27337  m1lgs  27353  2lgslem1a1  27354  2lgslem3a1  27365  2lgslem3b1  27366  2lgslem3c1  27367  2lgslem3d1  27368  2lgslem4  27371  2lgsoddprmlem2  27374  2sqreultlem  27412  2sqreunnltlem  27415  rplogsumlem1  27449  dchrisumlema  27453  dchrisumlem2  27455  dchrisumlem3  27456  dchrvmasumlem2  27463  dchrvmasumiflem1  27466  dchrisum0lem1b  27480  dchrisum0lem2a  27482  rplogsum  27492  logdivsum  27498  mulog2sumlem2  27500  logsqvma  27507  logsqvma2  27508  log2sumbnd  27509  selberg2lem  27515  logdivbnd  27521  pntrsumo1  27530  pntrsumbnd  27531  pntibndlem1  27554  pntibndlem2  27556  pntibndlem3  27557  pntlemd  27559  pntlema  27561  pntlemb  27562  pntlemr  27567  pntlemj  27568  pntlemf  27570  pntlemo  27572  crctcshwlkn0lem5  29836  crctcshwlkn0lem6  29837  lnconi  32057  rpdp2cl  32912  rpdp2cl2  32913  hgt750lem  34757  hgt750lem2  34758  hgt750leme  34764  circum  35817  bccolsum  35882  faclimlem3  35888  faclim  35889  poimirlem29  37789  poimirlem30  37790  poimirlem31  37791  poimirlem32  37792  mblfinlem3  37799  itg2addnclem2  37812  itg2addnc  37814  3lexlogpow2ineq1  42251  2ap1caineq  42338  pellexlem4  43016  pell1qrgaplem  43057  pellqrex  43063  congrep  43157  acongeq  43167  proot1ex  43380  hashnzfzclim  44505  xrralrecnnle  45569  nnrecrp  45572  xrralrecnnge  45576  iooiinicc  45730  iooiinioc  45744  fprodsubrecnncnvlem  46093  fprodaddrecnncnvlem  46095  wallispilem4  46254  wallispi  46256  wallispi2lem1  46257  wallispi2lem2  46258  stirlinglem1  46260  stirlinglem2  46261  stirlinglem3  46262  stirlinglem4  46263  stirlinglem6  46265  stirlinglem7  46266  stirlinglem10  46269  stirlinglem11  46270  stirlinglem13  46272  stirlinglem14  46273  stirlinglem15  46274  stirlingr  46276  dirkertrigeqlem1  46284  hoicvrrex  46742  ovnsubaddlem2  46757  hoiqssbllem3  46810  iinhoiicc  46860  iunhoiioo  46862  vonioolem1  46866  vonioolem2  46867  vonicclem1  46869  vonicclem2  46870  addmodne  47532  submodlt  47538  mod0mul  47544  modn0mul  47545  m1modmmod  47546  difmodm1lt  47547  modlt0b  47551  mod2addne  47552  fsummmodsndifre  47562  mod42tp1mod8  47790  lighneallem2  47794  3exp4mod41  47804  41prothprmlem2  47806  perfectALTVlem2  47910  2exp340mod341  47921  8exp8mod9  47924  nfermltl8rev  47930  gpgedgvtx0  48249  gpgedgvtx1  48250  gpgvtxedg0  48251  gpgvtxedg1  48252  gpg3kgrtriexlem1  48271  gpg3kgrtriexlem2  48272  nnlog2ge0lt1  48754  blennnelnn  48764  nnpw2blen  48768  blen1b  48776  blennnt2  48777  blennn0e2  48782  dignn0fr  48789  dignn0ldlem  48790  dignnld  48791  dig2nn1st  48793  dig0  48794