Theorem nnrp 12150

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 11382	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nngt0 11407	. 2 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)
3		elrp 12139	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 578	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 4886  ℝcr 10271  0cc0 10272   < clt 10411  ℕcn 11374  ℝ⁺crp 12137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-nn 11375  df-rp 12138

This theorem is referenced by:  nnrpd  12179  nn0ledivnn  12252  adddivflid  12938  divfl0  12944  fldivnn0le  12952  zmodcl  13009  zmodfz  13011  zmodid2  13017  m1modnnsub1  13035  addmodid  13037  modifeq2int  13051  modaddmodup  13052  modaddmodlo  13053  modsumfzodifsn  13062  addmodlteq  13064  nnesq  13307  digit2  13316  digit1  13317  bcrpcl  13413  bcval5  13423  lswccatn0lsw  13681  cshw0  13945  cshwmodn  13946  cshwsublen  13947  cshwidxmod  13954  cshwidxmodr  13955  cshwidxm1  13958  cshwidxm  13959  repswcshw  13963  2cshw  13964  cshweqrep  13972  modfsummods  14929  divcnv  14989  supcvg  14992  harmonic  14995  expcnv  15000  rpnnen2lem11  15357  sqrt2irr  15382  dvdsval3  15391  dvdsmodexp  15395  moddvds  15398  divalgmod  15536  flodddiv4  15543  modgcd  15659  divgcdcoprm0  15784  isprm5  15823  isprm6  15830  nnnn0modprm0  15915  pythagtriplem13  15936  fldivp1  16005  prmreclem5  16028  prmreclem6  16029  4sqlem12  16064  modxai  16176  modsubi  16180  mulgmodid  17965  odmodnn0  18343  gexdvds  18383  sylow1lem1  18397  gexexlem  18641  znf1o  20295  met1stc  22734  lmnn  23469  bcthlem5  23534  minveclem3  23635  vitalilem4  23815  vitali  23817  ismbf3d  23858  itg2seq  23946  plyeq0lem  24403  elqaalem3  24513  aalioulem6  24529  aaliou  24530  logtayllem  24842  sqrt2cxp2logb9e3  24977  atan1  25106  leibpi  25121  birthdaylem2  25131  dfef2  25149  divsqrtsumlem  25158  emcllem1  25174  emcllem2  25175  emcllem3  25176  emcllem4  25177  emcllem6  25179  zetacvg  25193  lgam1  25242  ppiub  25381  vmalelog  25382  logfacbnd3  25400  logexprlim  25402  bcmono  25454  bclbnd  25457  bposlem1  25461  bposlem7  25467  bposlem8  25468  bposlem9  25469  gausslemma2dlem1a  25542  gausslemma2dlem4  25546  gausslemma2dlem6  25549  m1lgs  25565  2lgslem1a1  25566  2lgslem3a1  25577  2lgslem3b1  25578  2lgslem3c1  25579  2lgslem3d1  25580  2lgslem4  25583  2lgsoddprmlem2  25586  rplogsumlem1  25625  dchrisumlema  25629  dchrisumlem2  25631  dchrisumlem3  25632  dchrvmasumlem2  25639  dchrvmasumiflem1  25642  dchrisum0lem1b  25656  dchrisum0lem2a  25658  rplogsum  25668  logdivsum  25674  mulog2sumlem2  25676  logsqvma  25683  logsqvma2  25684  log2sumbnd  25685  selberg2lem  25691  logdivbnd  25697  pntrsumo1  25706  pntrsumbnd  25707  pntibndlem1  25730  pntibndlem2  25732  pntibndlem3  25733  pntlemd  25735  pntlema  25737  pntlemb  25738  pntlemr  25743  pntlemj  25744  pntlemf  25746  pntlemo  25748  crctcshwlkn0lem5  27163  crctcshwlkn0lem6  27164  lnconi  29464  rpdp2cl  30152  rpdp2cl2  30153  hgt750lem  31331  hgt750lem2  31332  hgt750leme  31338  circum  32165  bccolsum  32219  faclimlem3  32225  faclim  32226  poimirlem29  34066  poimirlem30  34067  poimirlem31  34068  poimirlem32  34069  mblfinlem3  34076  itg2addnclem2  34089  itg2addnclem3  34090  itg2addnc  34091  pellexlem4  38360  pell1qrgaplem  38401  pellqrex  38407  congrep  38503  acongeq  38513  proot1ex  38742  hashnzfzclim  39481  xrralrecnnle  40514  nnrecrp  40517  xrralrecnnge  40523  iooiinicc  40681  iooiinioc  40695  fprodsubrecnncnvlem  41053  fprodaddrecnncnvlem  41055  wallispilem4  41216  wallispi  41218  wallispi2lem1  41219  wallispi2lem2  41220  stirlinglem1  41222  stirlinglem2  41223  stirlinglem3  41224  stirlinglem4  41225  stirlinglem6  41227  stirlinglem7  41228  stirlinglem10  41231  stirlinglem11  41232  stirlinglem13  41234  stirlinglem14  41235  stirlinglem15  41236  stirlingr  41238  dirkertrigeqlem1  41246  hoicvrrex  41701  ovnsubaddlem2  41716  hoiqssbllem3  41769  iinhoiicc  41819  iunhoiioo  41821  vonioolem1  41825  vonioolem2  41826  vonicclem1  41828  vonicclem2  41829  preimageiingt  41861  preimaleiinlt  41862  fsummmodsndifre  42380  mod42tp1mod8  42544  lighneallem2  42548  3exp4mod41  42558  41prothprmlem2  42560  perfectALTVlem2  42660  mod0mul  43333  modn0mul  43334  m1modmmod  43335  difmodm1lt  43336  nnlog2ge0lt1  43379  blennnelnn  43389  nnpw2blen  43393  blen1b  43401  blennnt2  43402  blennn0e2  43407  dignn0fr  43414  dignn0ldlem  43415  dignnld  43416  dig2nn1st  43418  dig0  43419