Theorem nnrp 11345

Description: A positive integer is a positive real. (Contributed by NM, 28-Nov-2008.)

Assertion

Ref	Expression
nnrp	|- ( A e. NN -> A e. RR+ )

Proof of Theorem nnrp

Step	Hyp	Ref	Expression
1		nnre 10649	. 2 |- ( A e. NN -> A e. RR )
2		nngt0 10671	. 2 |- ( A e. NN -> 0 < A )
3		elrp 11338	. 2 |- ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
4	1, 2, 3	sylanbrc 675	1 |- ( A e. NN -> A e. RR+ )

Syntax hints:   -> wi 4   e. wcel 1898   class class class wbr 4418   RRcr 9569   0cc0 9570   < clt 9706   NNcn 10642   RR+crp 11336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-om 6725  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-er 7394  df-en 7601  df-dom 7602  df-sdom 7603  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-nn 10643  df-rp 11337

This theorem is referenced by:  nnrpd  11373  fldivnn0le  12102  zmodcl  12154  zmodfz  12156  modidmul0OLD  12161  zmodid2  12163  addmodid  12177  modifeq2int  12190  modaddmodup  12191  modaddmodlo  12192  nnesq  12434  digit2  12443  digit1  12444  bcrpcl  12531  bcval5  12541  lswccatn0lsw  12776  cshw0  12939  cshwmodn  12940  cshwsublen  12941  cshwidxmod  12948  cshwidxm1  12951  cshwidxm  12952  repswcshw  12954  2cshw  12955  cshweqrep  12963  modfsummods  13908  divcnv  13966  supcvg  13969  harmonic  13972  expcnv  13977  rpnnen2lem11  14332  sqrt2irr  14356  dvdsval3  14364  moddvds  14367  mulmoddvds  14418  divalgmod  14442  modgcd  14555  isprm5  14706  isprm6  14721  nnnn0modprm0  14812  pythagtriplem13  14832  fldivp1  14897  prmreclem5  14919  prmreclem6  14920  4sqlem12  14955  modxai  15095  modsubi  15099  odmodnn0  17244  gexdvds  17290  sylow1lem1  17305  gexexlem  17545  znf1o  19177  met1stc  21591  lmnn  22288  bcthlem5  22351  minveclem3  22426  minveclem3OLD  22438  vitalilem4  22625  vitali  22627  ismbf3d  22666  itg2seq  22756  plyeq0lem  23220  elqaalem3  23330  elqaalem3OLD  23333  aalioulem6  23349  aaliou  23350  logtayllem  23660  atan1  23910  leibpi  23924  birthdaylem2  23934  dfef2  23952  divsqrtsumlem  23961  emcllem1  23977  emcllem2  23978  emcllem3  23979  emcllem4  23980  emcllem6  23982  zetacvg  23996  lgam1  24045  ppiub  24188  vmalelog  24189  logfacbnd3  24207  logexprlim  24209  bcmono  24261  bclbnd  24264  bposlem1  24268  bposlem7  24274  bposlem8  24275  bposlem9  24276  m1lgs  24346  rplogsumlem1  24378  dchrisumlema  24382  dchrisumlem2  24384  dchrisumlem3  24385  dchrvmasumlem2  24392  dchrvmasumiflem1  24395  dchrisum0lem1b  24409  dchrisum0lem2a  24411  rplogsum  24421  logdivsum  24427  mulog2sumlem2  24429  logsqvma  24436  logsqvma2  24437  log2sumbnd  24438  selberg2lem  24444  logdivbnd  24450  pntrsumo1  24459  pntrsumbnd  24460  pntibndlem1  24483  pntibndlem2  24485  pntibndlem3  24486  pntlemd  24488  pntlema  24490  pntlemb  24491  pntlemr  24496  pntlemj  24497  pntlemf  24499  pntlemo  24501  gxmodid  26063  lnconi  27742  circum  30368  bccolsum  30425  faclimlem3  30431  faclim  30432  poimirlem29  32015  poimirlem30  32016  poimirlem31  32017  poimirlem32  32018  mblfinlem3  32025  itg2addnclem2  32040  itg2addnclem3  32041  itg2addnc  32042  pellexlem4  35722  pell1qrgaplem  35765  pellqrex  35772  congrep  35869  acongeq  35879  dvdsabsmod0OLD  35887  proot1ex  36124  hashnzfzclim  36716  wallispilem4  38031  wallispi  38033  wallispi2lem1  38034  wallispi2lem2  38035  stirlinglem1  38037  stirlinglem2  38038  stirlinglem3  38039  stirlinglem4  38040  stirlinglem6  38042  stirlinglem7  38043  stirlinglem10  38046  stirlinglem11  38047  stirlinglem13  38049  stirlinglem14  38050  stirlinglem15  38051  stirlingr  38053  dirkertrigeqlem1  38061  hoicvrrex  38485  ovnsubaddlem2  38500  hoiqssbllem3  38553  perfectALTVlem2  38979  3exp4mod41  39051  41prothprmlem2  39053  fsummmodsndifre  39235  mod0mul  40691  modn0mul  40692  m1modmmod  40693  difmodm1lt  40694  nnlog2ge0lt1  40746  blennnelnn  40756  nnpw2blen  40760  blen1b  40768  blennnt2  40769  blennn0e2  40774  dignn0fr  40781  dignn0ldlem  40782  dignnld  40783  dig2nn1st  40785  dig0  40786