Theorem nnrp 12954

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5085  ℝcr 11037  0cc0 11038   < clt 11179  ℕcn 12174  ℝ⁺crp 12942

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 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

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 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 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-nn 12175  df-rp 12943

This theorem is referenced by:  nnrpd  12984  nn0ledivnn  13057  adddivflid  13777  divfl0  13783  fldivnn0le  13791  zmodcl  13850  zmodfz  13852  zmodid2  13858  m1modnnsub1  13879  addmodid  13881  modifeq2int  13895  modaddmodup  13896  modaddmodlo  13897  modsumfzodifsn  13906  addmodlteq  13908  nnesq  14189  digit2  14198  digit1  14199  bcrpcl  14270  bcval5  14280  lswccatn0lsw  14554  cshw0  14756  cshwmodn  14757  cshwsublen  14758  cshwidxmod  14765  cshwidxmodr  14766  cshwidxm1  14769  cshwidxm  14770  repswcshw  14774  2cshw  14775  cshweqrep  14783  modfsummods  15756  divcnv  15818  supcvg  15821  harmonic  15824  expcnv  15829  rpnnen2lem11  16191  sqrt2irr  16216  dvdsval3  16225  dvdsmodexp  16229  moddvds  16232  divalgmod  16375  flodddiv4  16384  modgcd  16501  divgcdcoprm0  16634  isprm5  16677  isprm6  16684  nnnn0modprm0  16777  pythagtriplem13  16798  fldivp1  16868  prmreclem5  16891  prmreclem6  16892  4sqlem12  16927  modxai  17039  modsubi  17043  smndex1iidm  18869  smndex1n0mnd  18883  mulgmodid  19089  odmodnn0  19515  gexdvds  19559  sylow1lem1  19573  gexexlem  19827  znf1o  21531  met1stc  24486  lmnn  25230  bcthlem5  25295  minveclem3  25396  vitali  25580  ismbf3d  25621  itg2seq  25709  plyeq0lem  26175  elqaalem3  26287  aalioulem6  26303  aaliou  26304  logtayllem  26623  sqrt2cxp2logb9e3  26763  atan1  26892  leibpi  26906  birthdaylem2  26916  dfef2  26934  divsqrtsumlem  26943  emcllem1  26959  emcllem2  26960  emcllem3  26961  emcllem4  26962  emcllem6  26964  zetacvg  26978  lgam1  27027  ppiub  27167  vmalelog  27168  logfacbnd3  27186  logexprlim  27188  bcmono  27240  bclbnd  27243  bposlem1  27247  bposlem7  27253  bposlem8  27254  bposlem9  27255  gausslemma2dlem1a  27328  gausslemma2dlem4  27332  gausslemma2dlem6  27335  m1lgs  27351  2lgslem1a1  27352  2lgslem3a1  27363  2lgslem3b1  27364  2lgslem3c1  27365  2lgslem3d1  27366  2lgslem4  27369  2lgsoddprmlem2  27372  2sqreultlem  27410  2sqreunnltlem  27413  rplogsumlem1  27447  dchrisumlema  27451  dchrisumlem2  27453  dchrisumlem3  27454  dchrvmasumlem2  27461  dchrvmasumiflem1  27464  dchrisum0lem1b  27478  dchrisum0lem2a  27480  rplogsum  27490  logdivsum  27496  mulog2sumlem2  27498  logsqvma  27505  logsqvma2  27506  log2sumbnd  27507  selberg2lem  27513  logdivbnd  27519  pntrsumo1  27528  pntrsumbnd  27529  pntibndlem1  27552  pntibndlem2  27554  pntibndlem3  27555  pntlemd  27557  pntlema  27559  pntlemb  27560  pntlemr  27565  pntlemj  27566  pntlemf  27568  pntlemo  27570  crctcshwlkn0lem5  29882  crctcshwlkn0lem6  29883  lnconi  32104  rpdp2cl  32941  rpdp2cl2  32942  hgt750lem  34795  hgt750lem2  34796  hgt750leme  34802  circum  35856  bccolsum  35921  faclimlem3  35927  faclim  35928  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  mblfinlem3  37980  itg2addnclem2  37993  itg2addnc  37995  3lexlogpow2ineq1  42497  2ap1caineq  42584  pellexlem4  43260  pell1qrgaplem  43301  pellqrex  43307  congrep  43401  acongeq  43411  proot1ex  43624  hashnzfzclim  44749  xrralrecnnle  45812  nnrecrp  45815  xrralrecnnge  45819  iooiinicc  45972  iooiinioc  45986  fprodsubrecnncnvlem  46335  fprodaddrecnncnvlem  46337  wallispilem4  46496  wallispi  46498  wallispi2lem1  46499  wallispi2lem2  46500  stirlinglem1  46502  stirlinglem2  46503  stirlinglem3  46504  stirlinglem4  46505  stirlinglem6  46507  stirlinglem7  46508  stirlinglem10  46511  stirlinglem11  46512  stirlinglem13  46514  stirlinglem14  46515  stirlinglem15  46516  stirlingr  46518  dirkertrigeqlem1  46526  hoicvrrex  46984  ovnsubaddlem2  46999  hoiqssbllem3  47052  iinhoiicc  47102  iunhoiioo  47104  vonioolem1  47108  vonioolem2  47109  vonicclem1  47111  vonicclem2  47112  nnmul2  47778  flmrecm1  47791  addmodne  47798  submodlt  47804  mod0mul  47810  modn0mul  47811  m1modmmod  47812  difmodm1lt  47813  modlt0b  47817  mod2addne  47818  fsummmodsndifre  47830  mod42tp1mod8  48065  lighneallem2  48069  3exp4mod41  48079  41prothprmlem2  48081  perfectALTVlem2  48198  2exp340mod341  48209  8exp8mod9  48212  nfermltl8rev  48218  gpgedgvtx0  48537  gpgedgvtx1  48538  gpgvtxedg0  48539  gpgvtxedg1  48540  gpg3kgrtriexlem1  48559  gpg3kgrtriexlem2  48560  nnlog2ge0lt1  49042  blennnelnn  49052  nnpw2blen  49056  blen1b  49064  blennnt2  49065  blennn0e2  49070  dignn0fr  49077  dignn0ldlem  49078  dignnld  49079  dig2nn1st  49081  dig0  49082