Theorem nnrp 13125

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 12335	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nngt0 12362	. 2 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)
3		elrp 13115	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 595	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  ℝcr 11192  0cc0 11193   < clt 11336  ℕcn 12328  ℝ⁺crp 13113

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-om 7876  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-nn 12329  df-rp 13114

This theorem is used by:  nnrpd  13155  nn0ledivnn  13228  adddivflid  13951  divfl0  13957  fldivnn0le  13965  zmodcl  14024  zmodfz  14026  zmodid2  14032  m1modnnsub1  14053  addmodid  14055  modifeq2int  14069  modaddmodup  14070  modaddmodlo  14071  modsumfzodifsn  14080  addmodlteq  14082  nnesq  14364  digit2  14373  digit1  14374  bcrpcl  14445  bcval5  14455  lswccatn0lsw  14731  cshw0  14938  cshwmodn  14939  cshwsublen  14940  cshwidxmod  14947  cshwidxmodr  14948  cshwidxm1  14951  cshwidxm  14952  repswcshw  14956  2cshw  14957  cshweqrep  14965  modfsummods  15953  divcnv  16015  supcvg  16018  harmonic  16021  expcnv  16026  rpnnen2lem11  16385  sqrt2irr  16410  dvdsval3  16419  dvdsmodexp  16423  moddvds  16426  divalgmod  16569  flodddiv4  16578  modgcd  16698  divgcdcoprm0  16833  isprm5  16876  isprm6  16883  nnnn0modprm0  16977  pythagtriplem13  16998  fldivp1  17068  prmreclem5  17091  prmreclem6  17092  4sqlem12  17127  modxai  17239  modsubi  17243  smndex1iidm  19090  smndex1n0mnd  19104  mulgmodid  19316  odmodnn0  19747  gexdvds  19791  sylow1lem1  19805  gexexlem  20059  znf1o  21850  met1stc  24833  lmnn  25577  bcthlem5  25642  minveclem3  25743  vitali  25927  ismbf3d  25968  itg2seq  26056  plyeq0lem  26522  elqaalem3  26637  aalioulem6  26657  aaliou  26658  logtayllem  26980  sqrt2cxp2logb9e3  27120  atan1  27249  leibpi  27263  birthdaylem2  27273  dfef2  27291  divsqrtsumlem  27300  emcllem1  27316  emcllem2  27317  emcllem3  27318  emcllem4  27319  emcllem6  27321  zetacvg  27335  lgam1  27384  ppiub  27524  vmalelog  27525  logfacbnd3  27543  logexprlim  27545  bcmono  27597  bclbnd  27600  bposlem1  27604  bposlem7  27610  bposlem8  27611  bposlem9  27612  gausslemma2dlem1a  27685  gausslemma2dlem4  27689  gausslemma2dlem6  27692  m1lgs  27708  2lgslem1a1  27709  2lgslem3a1  27720  2lgslem3b1  27721  2lgslem3c1  27722  2lgslem3d1  27723  2lgslem4  27726  2lgsoddprmlem2  27729  2sqreultlem  27767  2sqreunnltlem  27770  rplogsumlem1  27804  dchrisumlema  27808  dchrisumlem2  27810  dchrisumlem3  27811  dchrvmasumlem2  27818  dchrvmasumiflem1  27821  dchrisum0lem1b  27835  dchrisum0lem2a  27837  rplogsum  27847  logdivsum  27853  mulog2sumlem2  27855  logsqvma  27862  logsqvma2  27863  log2sumbnd  27864  selberg2lem  27870  logdivbnd  27876  pntrsumo1  27885  pntrsumbnd  27886  pntibndlem1  27909  pntibndlem2  27911  pntibndlem3  27912  pntlemd  27914  pntlema  27916  pntlemb  27917  pntlemr  27922  pntlemj  27923  pntlemf  27925  pntlemo  27927  crctcshwlkn0lem5  30396  crctcshwlkn0lem6  30397  lnconi  32628  rpdp2cl  33441  rpdp2cl2  33442  hgt750lem  35273  hgt750lem2  35274  hgt750leme  35280  circum  36418  bccolsum  36483  faclimlem3  36489  faclim  36490  poimirlem29  38547  poimirlem30  38548  poimirlem31  38549  poimirlem32  38550  mblfinlem3  38557  itg2addnclem2  38570  itg2addnc  38572  3lexlogpow2ineq1  43088  2ap1caineq  43175  pellexlem4  43818  pell1qrgaplem  43859  pellqrex  43865  congrep  43959  acongeq  43969  proot1ex  44182  hashnzfzclim  45291  xrralrecnnle  46363  nnrecrp  46366  xrralrecnnge  46370  iooiinicc  46523  iooiinioc  46537  fprodsubrecnncnvlem  46886  fprodaddrecnncnvlem  46888  wallispilem4  47047  wallispi  47049  wallispi2lem1  47050  wallispi2lem2  47051  stirlinglem1  47053  stirlinglem2  47054  stirlinglem3  47055  stirlinglem4  47056  stirlinglem6  47058  stirlinglem7  47059  stirlinglem10  47062  stirlinglem11  47063  stirlinglem13  47065  stirlinglem14  47066  stirlinglem15  47067  stirlingr  47069  dirkertrigeqlem1  47077  hoicvrrex  47535  ovnsubaddlem2  47550  hoiqssbllem3  47603  iinhoiicc  47653  iunhoiioo  47655  vonioolem1  47659  vonioolem2  47660  vonicclem1  47662  vonicclem2  47663  nnmul2  48369  flmrecm1  48382  addmodne  48389  submodlt  48395  mod0mul  48401  modn0mul  48402  m1modmmod  48403  difmodm1lt  48404  modlt0b  48408  mod2addne  48409  fsummmodsndifre  48421  mod42tp1mod8  48656  lighneallem2  48660  3exp4mod41  48670  41prothprmlem2  48672  perfectALTVlem2  48789  2exp340mod341  48800  8exp8mod9  48803  nfermltl8rev  48809  gpgedgvtx0  49128  gpgedgvtx1  49129  gpgvtxedg0  49130  gpgvtxedg1  49131  gpg3kgrtriexlem1  49150  gpg3kgrtriexlem2  49151  nnlog2ge0lt1  49647  blennnelnn  49657  nnpw2blen  49661  blen1b  49669  blennnt2  49670  blennn0e2  49675  dignn0fr  49682  dignn0ldlem  49683  dignnld  49684  dig2nn1st  49686  dig0  49687