Theorem nnrp 12401

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 11645	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nngt0 11669	. 2 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)
3		elrp 12392	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 585	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5066  ℝcr 10536  0cc0 10537   < clt 10675  ℕcn 11638  ℝ⁺crp 12390

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-nn 11639  df-rp 12391

This theorem is referenced by:  nnrpd  12430  nn0ledivnn  12503  adddivflid  13189  divfl0  13195  fldivnn0le  13203  zmodcl  13260  zmodfz  13262  zmodid2  13268  m1modnnsub1  13286  addmodid  13288  modifeq2int  13302  modaddmodup  13303  modaddmodlo  13304  modsumfzodifsn  13313  addmodlteq  13315  nnesq  13589  digit2  13598  digit1  13599  bcrpcl  13669  bcval5  13679  lswccatn0lsw  13945  cshw0  14156  cshwmodn  14157  cshwsublen  14158  cshwidxmod  14165  cshwidxmodr  14166  cshwidxm1  14169  cshwidxm  14170  repswcshw  14174  2cshw  14175  cshweqrep  14183  modfsummods  15148  divcnv  15208  supcvg  15211  harmonic  15214  expcnv  15219  rpnnen2lem11  15577  sqrt2irr  15602  dvdsval3  15611  dvdsmodexp  15615  moddvds  15618  divalgmod  15757  flodddiv4  15764  modgcd  15880  divgcdcoprm0  16009  isprm5  16051  isprm6  16058  nnnn0modprm0  16143  pythagtriplem13  16164  fldivp1  16233  prmreclem5  16256  prmreclem6  16257  4sqlem12  16292  modxai  16404  modsubi  16408  smndex1iidm  18066  smndex1n0mnd  18077  mulgmodid  18266  odmodnn0  18668  gexdvds  18709  sylow1lem1  18723  gexexlem  18972  znf1o  20698  met1stc  23131  lmnn  23866  bcthlem5  23931  minveclem3  24032  vitali  24214  ismbf3d  24255  itg2seq  24343  plyeq0lem  24800  elqaalem3  24910  aalioulem6  24926  aaliou  24927  logtayllem  25242  sqrt2cxp2logb9e3  25377  atan1  25506  leibpi  25520  birthdaylem2  25530  dfef2  25548  divsqrtsumlem  25557  emcllem1  25573  emcllem2  25574  emcllem3  25575  emcllem4  25576  emcllem6  25578  zetacvg  25592  lgam1  25641  ppiub  25780  vmalelog  25781  logfacbnd3  25799  logexprlim  25801  bcmono  25853  bclbnd  25856  bposlem1  25860  bposlem7  25866  bposlem8  25867  bposlem9  25868  gausslemma2dlem1a  25941  gausslemma2dlem4  25945  gausslemma2dlem6  25948  m1lgs  25964  2lgslem1a1  25965  2lgslem3a1  25976  2lgslem3b1  25977  2lgslem3c1  25978  2lgslem3d1  25979  2lgslem4  25982  2lgsoddprmlem2  25985  2sqreultlem  26023  2sqreunnltlem  26026  rplogsumlem1  26060  dchrisumlema  26064  dchrisumlem2  26066  dchrisumlem3  26067  dchrvmasumlem2  26074  dchrvmasumiflem1  26077  dchrisum0lem1b  26091  dchrisum0lem2a  26093  rplogsum  26103  logdivsum  26109  mulog2sumlem2  26111  logsqvma  26118  logsqvma2  26119  log2sumbnd  26120  selberg2lem  26126  logdivbnd  26132  pntrsumo1  26141  pntrsumbnd  26142  pntibndlem1  26165  pntibndlem2  26167  pntibndlem3  26168  pntlemd  26170  pntlema  26172  pntlemb  26173  pntlemr  26178  pntlemj  26179  pntlemf  26181  pntlemo  26183  crctcshwlkn0lem5  27592  crctcshwlkn0lem6  27593  lnconi  29810  rpdp2cl  30558  rpdp2cl2  30559  hgt750lem  31922  hgt750lem2  31923  hgt750leme  31929  circum  32917  bccolsum  32971  faclimlem3  32977  faclim  32978  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  poimirlem32  34939  mblfinlem3  34946  itg2addnclem2  34959  itg2addnclem3  34960  itg2addnc  34961  pellexlem4  39478  pell1qrgaplem  39519  pellqrex  39525  congrep  39619  acongeq  39629  proot1ex  39850  hashnzfzclim  40703  xrralrecnnle  41702  nnrecrp  41705  xrralrecnnge  41711  iooiinicc  41867  iooiinioc  41881  fprodsubrecnncnvlem  42240  fprodaddrecnncnvlem  42242  wallispilem4  42402  wallispi  42404  wallispi2lem1  42405  wallispi2lem2  42406  stirlinglem1  42408  stirlinglem2  42409  stirlinglem3  42410  stirlinglem4  42411  stirlinglem6  42413  stirlinglem7  42414  stirlinglem10  42417  stirlinglem11  42418  stirlinglem13  42420  stirlinglem14  42421  stirlinglem15  42422  stirlingr  42424  dirkertrigeqlem1  42432  hoicvrrex  42887  ovnsubaddlem2  42902  hoiqssbllem3  42955  iinhoiicc  43005  iunhoiioo  43007  vonioolem1  43011  vonioolem2  43012  vonicclem1  43014  vonicclem2  43015  preimageiingt  43047  preimaleiinlt  43048  fsummmodsndifre  43583  mod42tp1mod8  43816  lighneallem2  43820  3exp4mod41  43830  41prothprmlem2  43832  perfectALTVlem2  43936  2exp340mod341  43947  8exp8mod9  43950  nfermltl8rev  43956  mod0mul  44628  modn0mul  44629  m1modmmod  44630  difmodm1lt  44631  nnlog2ge0lt1  44675  blennnelnn  44685  nnpw2blen  44689  blen1b  44697  blennnt2  44698  blennn0e2  44703  dignn0fr  44710  dignn0ldlem  44711  dignnld  44712  dig2nn1st  44714  dig0  44715