Theorem nnrp 12983

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 12217	. 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
2		nngt0 12241	. 2 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)
3		elrp 12974	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
4	1, 2, 3	sylanbrc 582	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℝ+)

Syntax hints:   → wi 4   ∈ wcel 2098   class class class wbr 5139  ℝcr 11106  0cc0 11107   < clt 11246  ℕcn 12210  ℝ⁺crp 12972

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6291  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-om 7850  df-2nd 7970  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11248  df-mnf 11249  df-xr 11250  df-ltxr 11251  df-le 11252  df-sub 11444  df-neg 11445  df-nn 12211  df-rp 12973

This theorem is referenced by:  nnrpd  13012  nn0ledivnn  13085  adddivflid  13781  divfl0  13787  fldivnn0le  13795  zmodcl  13854  zmodfz  13856  zmodid2  13862  m1modnnsub1  13880  addmodid  13882  modifeq2int  13896  modaddmodup  13897  modaddmodlo  13898  modsumfzodifsn  13907  addmodlteq  13909  nnesq  14188  digit2  14197  digit1  14198  bcrpcl  14266  bcval5  14276  lswccatn0lsw  14539  cshw0  14742  cshwmodn  14743  cshwsublen  14744  cshwidxmod  14751  cshwidxmodr  14752  cshwidxm1  14755  cshwidxm  14756  repswcshw  14760  2cshw  14761  cshweqrep  14769  modfsummods  15737  divcnv  15797  supcvg  15800  harmonic  15803  expcnv  15808  rpnnen2lem11  16166  sqrt2irr  16191  dvdsval3  16200  dvdsmodexp  16204  moddvds  16207  divalgmod  16348  flodddiv4  16355  modgcd  16473  divgcdcoprm0  16601  isprm5  16643  isprm6  16650  nnnn0modprm0  16740  pythagtriplem13  16761  fldivp1  16831  prmreclem5  16854  prmreclem6  16855  4sqlem12  16890  modxai  17002  modsubi  17006  smndex1iidm  18818  smndex1n0mnd  18829  mulgmodid  19032  odmodnn0  19452  gexdvds  19496  sylow1lem1  19510  gexexlem  19764  znf1o  21416  met1stc  24354  lmnn  25115  bcthlem5  25180  minveclem3  25281  vitali  25466  ismbf3d  25507  itg2seq  25596  plyeq0lem  26066  elqaalem3  26177  aalioulem6  26193  aaliou  26194  logtayllem  26512  sqrt2cxp2logb9e3  26650  atan1  26779  leibpi  26793  birthdaylem2  26803  dfef2  26822  divsqrtsumlem  26831  emcllem1  26847  emcllem2  26848  emcllem3  26849  emcllem4  26850  emcllem6  26852  zetacvg  26866  lgam1  26915  ppiub  27056  vmalelog  27057  logfacbnd3  27075  logexprlim  27077  bcmono  27129  bclbnd  27132  bposlem1  27136  bposlem7  27142  bposlem8  27143  bposlem9  27144  gausslemma2dlem1a  27217  gausslemma2dlem4  27221  gausslemma2dlem6  27224  m1lgs  27240  2lgslem1a1  27241  2lgslem3a1  27252  2lgslem3b1  27253  2lgslem3c1  27254  2lgslem3d1  27255  2lgslem4  27258  2lgsoddprmlem2  27261  2sqreultlem  27299  2sqreunnltlem  27302  rplogsumlem1  27336  dchrisumlema  27340  dchrisumlem2  27342  dchrisumlem3  27343  dchrvmasumlem2  27350  dchrvmasumiflem1  27353  dchrisum0lem1b  27367  dchrisum0lem2a  27369  rplogsum  27379  logdivsum  27385  mulog2sumlem2  27387  logsqvma  27394  logsqvma2  27395  log2sumbnd  27396  selberg2lem  27402  logdivbnd  27408  pntrsumo1  27417  pntrsumbnd  27418  pntibndlem1  27441  pntibndlem2  27443  pntibndlem3  27444  pntlemd  27446  pntlema  27448  pntlemb  27449  pntlemr  27454  pntlemj  27455  pntlemf  27457  pntlemo  27459  crctcshwlkn0lem5  29540  crctcshwlkn0lem6  29541  lnconi  31758  rpdp2cl  32518  rpdp2cl2  32519  hgt750lem  34154  hgt750lem2  34155  hgt750leme  34161  circum  35150  bccolsum  35205  faclimlem3  35211  faclim  35212  poimirlem29  37011  poimirlem30  37012  poimirlem31  37013  poimirlem32  37014  mblfinlem3  37021  itg2addnclem2  37034  itg2addnc  37036  3lexlogpow2ineq1  41420  2ap1caineq  41458  pellexlem4  42084  pell1qrgaplem  42125  pellqrex  42131  congrep  42226  acongeq  42236  proot1ex  42457  hashnzfzclim  43595  xrralrecnnle  44603  nnrecrp  44606  xrralrecnnge  44610  iooiinicc  44765  iooiinioc  44779  fprodsubrecnncnvlem  45133  fprodaddrecnncnvlem  45135  wallispilem4  45294  wallispi  45296  wallispi2lem1  45297  wallispi2lem2  45298  stirlinglem1  45300  stirlinglem2  45301  stirlinglem3  45302  stirlinglem4  45303  stirlinglem6  45305  stirlinglem7  45306  stirlinglem10  45309  stirlinglem11  45310  stirlinglem13  45312  stirlinglem14  45313  stirlinglem15  45314  stirlingr  45316  dirkertrigeqlem1  45324  hoicvrrex  45782  ovnsubaddlem2  45797  hoiqssbllem3  45850  iinhoiicc  45900  iunhoiioo  45902  vonioolem1  45906  vonioolem2  45907  vonicclem1  45909  vonicclem2  45910  preimageiingt  45946  preimaleiinlt  45947  fsummmodsndifre  46552  mod42tp1mod8  46780  lighneallem2  46784  3exp4mod41  46794  41prothprmlem2  46796  perfectALTVlem2  46900  2exp340mod341  46911  8exp8mod9  46914  nfermltl8rev  46920  mod0mul  47418  modn0mul  47419  m1modmmod  47420  difmodm1lt  47421  nnlog2ge0lt1  47465  blennnelnn  47475  nnpw2blen  47479  blen1b  47487  blennnt2  47488  blennn0e2  47493  dignn0fr  47500  dignn0ldlem  47501  dignnld  47502  dig2nn1st  47504  dig0  47505