Theorem nnrp 13023

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 12235	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nngt0 12262	. 2 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)
3		elrp 13013	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 594	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2143   class class class wbr 5109  ℝcr 11094  0cc0 11095   < clt 11238  ℕcn 12228  ℝ⁺crp 13011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-nn 12229  df-rp 13012

This theorem is referenced by:  nnrpd  13053  nn0ledivnn  13126  adddivflid  13847  divfl0  13853  fldivnn0le  13861  zmodcl  13920  zmodfz  13922  zmodid2  13928  m1modnnsub1  13949  addmodid  13951  modifeq2int  13965  modaddmodup  13966  modaddmodlo  13967  modsumfzodifsn  13976  addmodlteq  13978  nnesq  14259  digit2  14268  digit1  14269  bcrpcl  14340  bcval5  14350  lswccatn0lsw  14625  cshw0  14827  cshwmodn  14828  cshwsublen  14829  cshwidxmod  14836  cshwidxmodr  14837  cshwidxm1  14840  cshwidxm  14841  repswcshw  14845  2cshw  14846  cshweqrep  14854  modfsummods  15841  divcnv  15903  supcvg  15906  harmonic  15909  expcnv  15914  rpnnen2lem11  16275  sqrt2irr  16300  dvdsval3  16309  dvdsmodexp  16313  moddvds  16316  divalgmod  16459  flodddiv4  16468  modgcd  16585  divgcdcoprm0  16718  isprm5  16761  isprm6  16768  nnnn0modprm0  16861  pythagtriplem13  16882  fldivp1  16952  prmreclem5  16975  prmreclem6  16976  4sqlem12  17011  modxai  17123  modsubi  17127  smndex1iidm  18955  smndex1n0mnd  18969  mulgmodid  19174  odmodnn0  19605  gexdvds  19649  sylow1lem1  19663  gexexlem  19917  znf1o  21701  met1stc  24678  lmnn  25422  bcthlem5  25487  minveclem3  25588  vitali  25772  ismbf3d  25813  itg2seq  25901  plyeq0lem  26367  elqaalem3  26482  aalioulem6  26500  aaliou  26501  logtayllem  26824  sqrt2cxp2logb9e3  26964  atan1  27093  leibpi  27107  birthdaylem2  27117  dfef2  27135  divsqrtsumlem  27144  emcllem1  27160  emcllem2  27161  emcllem3  27162  emcllem4  27163  emcllem6  27165  zetacvg  27179  lgam1  27228  ppiub  27368  vmalelog  27369  logfacbnd3  27387  logexprlim  27389  bcmono  27441  bclbnd  27444  bposlem1  27448  bposlem7  27454  bposlem8  27455  bposlem9  27456  gausslemma2dlem1a  27529  gausslemma2dlem4  27533  gausslemma2dlem6  27536  m1lgs  27552  2lgslem1a1  27553  2lgslem3a1  27564  2lgslem3b1  27565  2lgslem3c1  27566  2lgslem3d1  27567  2lgslem4  27570  2lgsoddprmlem2  27573  2sqreultlem  27611  2sqreunnltlem  27614  rplogsumlem1  27648  dchrisumlema  27652  dchrisumlem2  27654  dchrisumlem3  27655  dchrvmasumlem2  27662  dchrvmasumiflem1  27665  dchrisum0lem1b  27679  dchrisum0lem2a  27681  rplogsum  27691  logdivsum  27697  mulog2sumlem2  27699  logsqvma  27706  logsqvma2  27707  log2sumbnd  27708  selberg2lem  27714  logdivbnd  27720  pntrsumo1  27729  pntrsumbnd  27730  pntibndlem1  27753  pntibndlem2  27755  pntibndlem3  27756  pntlemd  27758  pntlema  27760  pntlemb  27761  pntlemr  27766  pntlemj  27767  pntlemf  27769  pntlemo  27771  crctcshwlkn0lem5  30163  crctcshwlkn0lem6  30164  lnconi  32385  rpdp2cl  33201  rpdp2cl2  33202  hgt750lem  35038  hgt750lem2  35039  hgt750leme  35045  circum  36166  bccolsum  36231  faclimlem3  36237  faclim  36238  poimirlem29  38300  poimirlem30  38301  poimirlem31  38302  poimirlem32  38303  mblfinlem3  38310  itg2addnclem2  38323  itg2addnc  38325  3lexlogpow2ineq1  42825  2ap1caineq  42912  pellexlem4  43559  pell1qrgaplem  43600  pellqrex  43606  congrep  43700  acongeq  43710  proot1ex  43923  hashnzfzclim  45032  xrralrecnnle  46098  nnrecrp  46101  xrralrecnnge  46105  iooiinicc  46258  iooiinioc  46272  fprodsubrecnncnvlem  46621  fprodaddrecnncnvlem  46623  wallispilem4  46782  wallispi  46784  wallispi2lem1  46785  wallispi2lem2  46786  stirlinglem1  46788  stirlinglem2  46789  stirlinglem3  46790  stirlinglem4  46791  stirlinglem6  46793  stirlinglem7  46794  stirlinglem10  46797  stirlinglem11  46798  stirlinglem13  46800  stirlinglem14  46801  stirlinglem15  46802  stirlingr  46804  dirkertrigeqlem1  46812  hoicvrrex  47270  ovnsubaddlem2  47285  hoiqssbllem3  47338  iinhoiicc  47388  iunhoiioo  47390  vonioolem1  47394  vonioolem2  47395  vonicclem1  47397  vonicclem2  47398  nnmul2  48067  flmrecm1  48080  addmodne  48087  submodlt  48093  mod0mul  48099  modn0mul  48100  m1modmmod  48101  difmodm1lt  48102  modlt0b  48106  mod2addne  48107  fsummmodsndifre  48119  mod42tp1mod8  48354  lighneallem2  48358  3exp4mod41  48368  41prothprmlem2  48370  perfectALTVlem2  48487  2exp340mod341  48498  8exp8mod9  48501  nfermltl8rev  48507  gpgedgvtx0  48826  gpgedgvtx1  48827  gpgvtxedg0  48828  gpgvtxedg1  48829  gpg3kgrtriexlem1  48848  gpg3kgrtriexlem2  48849  nnlog2ge0lt1  49346  blennnelnn  49356  nnpw2blen  49360  blen1b  49368  blennnt2  49369  blennn0e2  49374  dignn0fr  49381  dignn0ldlem  49382  dignnld  49383  dig2nn1st  49385  dig0  49386