Theorem nnre 8585

Description: A positive integer is a real number. (Contributed by NM, 18-Aug-1999.)

Assertion

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

Proof of Theorem nnre

Step	Hyp	Ref	Expression
1		nnssre 8582	. 2 |- NN C_ RR
2	1	sseli 3043	1 |- ( A e. NN -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1448   RRcr 7499   NNcn 8578

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986  ax-cnex 7586  ax-resscn 7587  ax-1re 7589  ax-addrcl 7592

This theorem depends on definitions:  df-bi 116  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ral 2380  df-v 2643  df-in 3027  df-ss 3034  df-int 3719  df-inn 8579

This theorem is referenced by:  nnrei  8587  peano2nn  8590  nn1suc  8597  nnge1  8601  nnle1eq1  8602  nngt0  8603  nnnlt1  8604  nnap0  8607  nn2ge  8611  nn1gt1  8612  nndivre  8614  nnrecgt0  8616  nnsub  8617  arch  8826  nnrecl  8827  bndndx  8828  nn0ge0  8854  0mnnnnn0  8861  nnnegz  8909  elnnz  8916  elz2  8974  gtndiv  8998  prime  9002  btwnz  9022  qre  9267  nnrp  9300  nnledivrp  9394  fzo1fzo0n0  9801  elfzo0le  9803  fzonmapblen  9805  ubmelfzo  9818  fzonn0p1p1  9831  elfzom1p1elfzo  9832  ubmelm1fzo  9844  subfzo0  9860  adddivflid  9906  flltdivnn0lt  9918  intfracq  9934  flqdiv  9935  m1modnnsub1  9984  addmodid  9986  modfzo0difsn  10009  nnlesq  10237  facndiv  10326  faclbnd  10328  faclbnd3  10330  bcval5  10350  seq3coll  10426  caucvgre  10593  efaddlem  11178  nndivdvds  11294  nno  11398  nnoddm1d2  11402  divalglemnn  11410  divalg2  11418  ndvdsadd  11423  gcdmultiple  11501  gcdmultiplez  11502  gcdzeq  11503  sqgcd  11510  dvdssqlem  11511  lcmgcdlem  11551  coprmgcdb  11562  qredeq  11570  qredeu  11571  prmdvdsfz  11612  sqrt2irr  11633  divdenle  11667  phibndlem  11684  hashgcdlem  11695  oddennn  11697  exmidunben  11731