Theorem nnrp 11318

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 10623	. 2 |- ( A e. NN -> A e. RR )
2		nngt0 10645	. 2 |- ( A e. NN -> 0 < A )
3		elrp 11311	. 2 |- ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
4	1, 2, 3	sylanbrc 668	1 |- ( A e. NN -> A e. RR+ )

Syntax hints:   -> wi 4   e. wcel 1872   class class class wbr 4423   RRcr 9545   0cc0 9546   < clt 9682   NNcn 10616   RR+crp 11309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-resscn 9603  ax-1cn 9604  ax-icn 9605  ax-addcl 9606  ax-addrcl 9607  ax-mulcl 9608  ax-mulrcl 9609  ax-mulcom 9610  ax-addass 9611  ax-mulass 9612  ax-distr 9613  ax-i2m1 9614  ax-1ne0 9615  ax-1rid 9616  ax-rnegex 9617  ax-rrecex 9618  ax-cnre 9619  ax-pre-lttri 9620  ax-pre-lttrn 9621  ax-pre-ltadd 9622  ax-pre-mulgt0 9623

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-wrecs 7039  df-recs 7101  df-rdg 7139  df-er 7374  df-en 7581  df-dom 7582  df-sdom 7583  df-pnf 9684  df-mnf 9685  df-xr 9686  df-ltxr 9687  df-le 9688  df-sub 9869  df-neg 9870  df-nn 10617  df-rp 11310

This theorem is referenced by:  nnrpd  11346  fldivnn0le  12070  zmodcl  12122  zmodfz  12124  modidmul0OLD  12129  zmodid2  12131  addmodid  12145  modifeq2int  12158  modaddmodup  12159  modaddmodlo  12160  nnesq  12402  digit2  12411  digit1  12412  bcrpcl  12499  bcval5  12509  lswccatn0lsw  12738  cshw0  12898  cshwmodn  12899  cshwsublen  12900  cshwidxmod  12907  cshwidxm1  12910  cshwidxm  12911  repswcshw  12913  2cshw  12914  cshweqrep  12922  modfsummods  13852  divcnv  13910  supcvg  13913  harmonic  13916  expcnv  13921  rpnnen2lem11  14276  sqrt2irr  14300  dvdsval3  14308  moddvds  14311  mulmoddvds  14362  divalgmod  14386  modgcd  14499  isprm5  14650  isprm6  14665  nnnn0modprm0  14756  pythagtriplem13  14776  fldivp1  14841  prmreclem5  14863  prmreclem6  14864  4sqlem12  14899  modxai  15039  modsubi  15043  odmodnn0  17188  gexdvds  17234  sylow1lem1  17249  gexexlem  17489  znf1o  19120  met1stc  21534  lmnn  22231  bcthlem5  22294  minveclem3  22369  minveclem3OLD  22381  vitalilem4  22567  vitali  22569  ismbf3d  22608  itg2seq  22698  plyeq0lem  23162  elqaalem3  23272  elqaalem3OLD  23275  aalioulem6  23291  aaliou  23292  logtayllem  23602  atan1  23852  leibpi  23866  birthdaylem2  23876  dfef2  23894  divsqrtsumlem  23903  emcllem1  23919  emcllem2  23920  emcllem3  23921  emcllem4  23922  emcllem6  23924  zetacvg  23938  lgam1  23987  ppiub  24130  vmalelog  24131  logfacbnd3  24149  logexprlim  24151  bcmono  24203  bclbnd  24206  bposlem1  24210  bposlem7  24216  bposlem8  24217  bposlem9  24218  m1lgs  24288  rplogsumlem1  24320  dchrisumlema  24324  dchrisumlem2  24326  dchrisumlem3  24327  dchrvmasumlem2  24334  dchrvmasumiflem1  24337  dchrisum0lem1b  24351  dchrisum0lem2a  24353  rplogsum  24363  logdivsum  24369  mulog2sumlem2  24371  logsqvma  24378  logsqvma2  24379  log2sumbnd  24380  selberg2lem  24386  logdivbnd  24392  pntrsumo1  24401  pntrsumbnd  24402  pntibndlem1  24425  pntibndlem2  24427  pntibndlem3  24428  pntlemd  24430  pntlema  24432  pntlemb  24433  pntlemr  24438  pntlemj  24439  pntlemf  24441  pntlemo  24443  gxmodid  26005  lnconi  27684  circum  30326  bccolsum  30382  faclimlem3  30388  faclim  30389  poimirlem29  31933  poimirlem30  31934  poimirlem31  31935  poimirlem32  31936  mblfinlem3  31943  itg2addnclem2  31958  itg2addnclem3  31959  itg2addnc  31960  pellexlem4  35646  pell1qrgaplem  35689  pellqrex  35696  congrep  35793  acongeq  35803  dvdsabsmod0OLD  35811  proot1ex  36048  hashnzfzclim  36641  wallispilem4  37870  wallispi  37872  wallispi2lem1  37873  wallispi2lem2  37874  stirlinglem1  37876  stirlinglem2  37877  stirlinglem3  37878  stirlinglem4  37879  stirlinglem6  37881  stirlinglem7  37882  stirlinglem10  37885  stirlinglem11  37886  stirlinglem13  37888  stirlinglem14  37889  stirlinglem15  37890  stirlingr  37892  dirkertrigeqlem1  37900  hoicvrrex  38282  ovnsubaddlem2  38297  perfectALTVlem2  38714  3exp4mod41  38786  41prothprmlem2  38788  fsummmodsndifre  38923  mod0mul  39944  modn0mul  39945  m1modmmod  39946  difmodm1lt  39947  nnlog2ge0lt1  39999  blennnelnn  40009  nnpw2blen  40013  blen1b  40021  blennnt2  40022  blennn0e2  40027  dignn0fr  40034  dignn0ldlem  40035  dignnld  40036  dig2nn1st  40038  dig0  40039