Theorem nnrp 12948

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 12175	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nngt0 12202	. 2 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)
3		elrp 12938	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 584	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  ℝcr 11031  0cc0 11032   < clt 11173  ℕcn 12168  ℝ⁺crp 12936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7812  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-nn 12169  df-rp 12937

This theorem is referenced by:  nnrpd  12978  nn0ledivnn  13051  adddivflid  13771  divfl0  13777  fldivnn0le  13785  zmodcl  13844  zmodfz  13846  zmodid2  13852  m1modnnsub1  13873  addmodid  13875  modifeq2int  13889  modaddmodup  13890  modaddmodlo  13891  modsumfzodifsn  13900  addmodlteq  13902  nnesq  14183  digit2  14192  digit1  14193  bcrpcl  14264  bcval5  14274  lswccatn0lsw  14548  cshw0  14750  cshwmodn  14751  cshwsublen  14752  cshwidxmod  14759  cshwidxmodr  14760  cshwidxm1  14763  cshwidxm  14764  repswcshw  14768  2cshw  14769  cshweqrep  14777  modfsummods  15750  divcnv  15812  supcvg  15815  harmonic  15818  expcnv  15823  rpnnen2lem11  16185  sqrt2irr  16210  dvdsval3  16219  dvdsmodexp  16223  moddvds  16226  divalgmod  16369  flodddiv4  16378  modgcd  16495  divgcdcoprm0  16628  isprm5  16671  isprm6  16678  nnnn0modprm0  16771  pythagtriplem13  16792  fldivp1  16862  prmreclem5  16885  prmreclem6  16886  4sqlem12  16921  modxai  17033  modsubi  17037  smndex1iidm  18863  smndex1n0mnd  18877  mulgmodid  19083  odmodnn0  19509  gexdvds  19553  sylow1lem1  19567  gexexlem  19821  znf1o  21544  met1stc  24499  lmnn  25243  bcthlem5  25308  minveclem3  25409  vitali  25593  ismbf3d  25634  itg2seq  25722  plyeq0lem  26188  elqaalem3  26301  aalioulem6  26317  aaliou  26318  logtayllem  26639  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  27184  vmalelog  27185  logfacbnd3  27203  logexprlim  27205  bcmono  27257  bclbnd  27260  bposlem1  27264  bposlem7  27270  bposlem8  27271  bposlem9  27272  gausslemma2dlem1a  27345  gausslemma2dlem4  27349  gausslemma2dlem6  27352  m1lgs  27368  2lgslem1a1  27369  2lgslem3a1  27380  2lgslem3b1  27381  2lgslem3c1  27382  2lgslem3d1  27383  2lgslem4  27386  2lgsoddprmlem2  27389  2sqreultlem  27427  2sqreunnltlem  27430  rplogsumlem1  27464  dchrisumlema  27468  dchrisumlem2  27470  dchrisumlem3  27471  dchrvmasumlem2  27478  dchrvmasumiflem1  27481  dchrisum0lem1b  27495  dchrisum0lem2a  27497  rplogsum  27507  logdivsum  27513  mulog2sumlem2  27515  logsqvma  27522  logsqvma2  27523  log2sumbnd  27524  selberg2lem  27530  logdivbnd  27536  pntrsumo1  27545  pntrsumbnd  27546  pntibndlem1  27569  pntibndlem2  27571  pntibndlem3  27572  pntlemd  27574  pntlema  27576  pntlemb  27577  pntlemr  27582  pntlemj  27583  pntlemf  27585  pntlemo  27587  crctcshwlkn0lem5  29900  crctcshwlkn0lem6  29901  lnconi  32122  rpdp2cl  32959  rpdp2cl2  32960  hgt750lem  34814  hgt750lem2  34815  hgt750leme  34821  circum  35875  bccolsum  35940  faclimlem3  35946  faclim  35947  poimirlem29  37987  poimirlem30  37988  poimirlem31  37989  poimirlem32  37990  mblfinlem3  37997  itg2addnclem2  38010  itg2addnc  38012  3lexlogpow2ineq1  42514  2ap1caineq  42601  pellexlem4  43281  pell1qrgaplem  43322  pellqrex  43328  congrep  43422  acongeq  43432  proot1ex  43645  hashnzfzclim  44770  xrralrecnnle  45833  nnrecrp  45836  xrralrecnnge  45840  iooiinicc  45993  iooiinioc  46007  fprodsubrecnncnvlem  46356  fprodaddrecnncnvlem  46358  wallispilem4  46517  wallispi  46519  wallispi2lem1  46520  wallispi2lem2  46521  stirlinglem1  46523  stirlinglem2  46524  stirlinglem3  46525  stirlinglem4  46526  stirlinglem6  46528  stirlinglem7  46529  stirlinglem10  46532  stirlinglem11  46533  stirlinglem13  46535  stirlinglem14  46536  stirlinglem15  46537  stirlingr  46539  dirkertrigeqlem1  46547  hoicvrrex  47005  ovnsubaddlem2  47020  hoiqssbllem3  47073  iinhoiicc  47123  iunhoiioo  47125  vonioolem1  47129  vonioolem2  47130  vonicclem1  47132  vonicclem2  47133  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