Theorem nnrp 12917

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5098  ℝcr 11025  0cc0 11026   < clt 11166  ℕcn 12145  ℝ⁺crp 12905

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 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-nn 12146  df-rp 12906

This theorem is referenced by:  nnrpd  12947  nn0ledivnn  13020  adddivflid  13738  divfl0  13744  fldivnn0le  13752  zmodcl  13811  zmodfz  13813  zmodid2  13819  m1modnnsub1  13840  addmodid  13842  modifeq2int  13856  modaddmodup  13857  modaddmodlo  13858  modsumfzodifsn  13867  addmodlteq  13869  nnesq  14150  digit2  14159  digit1  14160  bcrpcl  14231  bcval5  14241  lswccatn0lsw  14515  cshw0  14717  cshwmodn  14718  cshwsublen  14719  cshwidxmod  14726  cshwidxmodr  14727  cshwidxm1  14730  cshwidxm  14731  repswcshw  14735  2cshw  14736  cshweqrep  14744  modfsummods  15716  divcnv  15776  supcvg  15779  harmonic  15782  expcnv  15787  rpnnen2lem11  16149  sqrt2irr  16174  dvdsval3  16183  dvdsmodexp  16187  moddvds  16190  divalgmod  16333  flodddiv4  16342  modgcd  16459  divgcdcoprm0  16592  isprm5  16634  isprm6  16641  nnnn0modprm0  16734  pythagtriplem13  16755  fldivp1  16825  prmreclem5  16848  prmreclem6  16849  4sqlem12  16884  modxai  16996  modsubi  17000  smndex1iidm  18826  smndex1n0mnd  18837  mulgmodid  19043  odmodnn0  19469  gexdvds  19513  sylow1lem1  19527  gexexlem  19781  znf1o  21506  met1stc  24465  lmnn  25219  bcthlem5  25284  minveclem3  25385  vitali  25570  ismbf3d  25611  itg2seq  25699  plyeq0lem  26171  elqaalem3  26285  aalioulem6  26301  aaliou  26302  logtayllem  26624  sqrt2cxp2logb9e3  26765  atan1  26894  leibpi  26908  birthdaylem2  26918  dfef2  26937  divsqrtsumlem  26946  emcllem1  26962  emcllem2  26963  emcllem3  26964  emcllem4  26965  emcllem6  26967  zetacvg  26981  lgam1  27030  ppiub  27171  vmalelog  27172  logfacbnd3  27190  logexprlim  27192  bcmono  27244  bclbnd  27247  bposlem1  27251  bposlem7  27257  bposlem8  27258  bposlem9  27259  gausslemma2dlem1a  27332  gausslemma2dlem4  27336  gausslemma2dlem6  27339  m1lgs  27355  2lgslem1a1  27356  2lgslem3a1  27367  2lgslem3b1  27368  2lgslem3c1  27369  2lgslem3d1  27370  2lgslem4  27373  2lgsoddprmlem2  27376  2sqreultlem  27414  2sqreunnltlem  27417  rplogsumlem1  27451  dchrisumlema  27455  dchrisumlem2  27457  dchrisumlem3  27458  dchrvmasumlem2  27465  dchrvmasumiflem1  27468  dchrisum0lem1b  27482  dchrisum0lem2a  27484  rplogsum  27494  logdivsum  27500  mulog2sumlem2  27502  logsqvma  27509  logsqvma2  27510  log2sumbnd  27511  selberg2lem  27517  logdivbnd  27523  pntrsumo1  27532  pntrsumbnd  27533  pntibndlem1  27556  pntibndlem2  27558  pntibndlem3  27559  pntlemd  27561  pntlema  27563  pntlemb  27564  pntlemr  27569  pntlemj  27570  pntlemf  27572  pntlemo  27574  crctcshwlkn0lem5  29887  crctcshwlkn0lem6  29888  lnconi  32108  rpdp2cl  32963  rpdp2cl2  32964  hgt750lem  34808  hgt750lem2  34809  hgt750leme  34815  circum  35868  bccolsum  35933  faclimlem3  35939  faclim  35940  poimirlem29  37850  poimirlem30  37851  poimirlem31  37852  poimirlem32  37853  mblfinlem3  37860  itg2addnclem2  37873  itg2addnc  37875  3lexlogpow2ineq1  42312  2ap1caineq  42399  pellexlem4  43074  pell1qrgaplem  43115  pellqrex  43121  congrep  43215  acongeq  43225  proot1ex  43438  hashnzfzclim  44563  xrralrecnnle  45627  nnrecrp  45630  xrralrecnnge  45634  iooiinicc  45788  iooiinioc  45802  fprodsubrecnncnvlem  46151  fprodaddrecnncnvlem  46153  wallispilem4  46312  wallispi  46314  wallispi2lem1  46315  wallispi2lem2  46316  stirlinglem1  46318  stirlinglem2  46319  stirlinglem3  46320  stirlinglem4  46321  stirlinglem6  46323  stirlinglem7  46324  stirlinglem10  46327  stirlinglem11  46328  stirlinglem13  46330  stirlinglem14  46331  stirlinglem15  46332  stirlingr  46334  dirkertrigeqlem1  46342  hoicvrrex  46800  ovnsubaddlem2  46815  hoiqssbllem3  46868  iinhoiicc  46918  iunhoiioo  46920  vonioolem1  46924  vonioolem2  46925  vonicclem1  46927  vonicclem2  46928  addmodne  47590  submodlt  47596  mod0mul  47602  modn0mul  47603  m1modmmod  47604  difmodm1lt  47605  modlt0b  47609  mod2addne  47610  fsummmodsndifre  47620  mod42tp1mod8  47848  lighneallem2  47852  3exp4mod41  47862  41prothprmlem2  47864  perfectALTVlem2  47968  2exp340mod341  47979  8exp8mod9  47982  nfermltl8rev  47988  gpgedgvtx0  48307  gpgedgvtx1  48308  gpgvtxedg0  48309  gpgvtxedg1  48310  gpg3kgrtriexlem1  48329  gpg3kgrtriexlem2  48330  nnlog2ge0lt1  48812  blennnelnn  48822  nnpw2blen  48826  blen1b  48834  blennnt2  48835  blennn0e2  48840  dignn0fr  48847  dignn0ldlem  48848  dignnld  48849  dig2nn1st  48851  dig0  48852