Theorem nnre 8940

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 8937	. 2 |- NN C_ RR
2	1	sseli 3163	1 |- ( A e. NN -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2158   RRcr 7824   NNcn 8933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169  ax-sep 4133  ax-cnex 7916  ax-resscn 7917  ax-1re 7919  ax-addrcl 7922

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ral 2470  df-v 2751  df-in 3147  df-ss 3154  df-int 3857  df-inn 8934

This theorem is referenced by:  nnrei  8942  peano2nn  8945  nn1suc  8952  nnge1  8956  nnle1eq1  8957  nngt0  8958  nnnlt1  8959  nnap0  8962  nn2ge  8966  nn1gt1  8967  nndivre  8969  nnrecgt0  8971  nnsub  8972  arch  9187  nnrecl  9188  bndndx  9189  nn0ge0  9215  0mnnnnn0  9222  nnnegz  9270  elnnz  9277  elz2  9338  gtndiv  9362  prime  9366  btwnz  9386  qre  9639  elpq  9662  elpqb  9663  nnrp  9677  nnledivrp  9780  fzo1fzo0n0  10197  elfzo0le  10199  fzonmapblen  10201  ubmelfzo  10214  fzonn0p1p1  10227  elfzom1p1elfzo  10228  ubmelm1fzo  10240  subfzo0  10256  adddivflid  10306  flltdivnn0lt  10318  intfracq  10334  flqdiv  10335  m1modnnsub1  10384  addmodid  10386  modfzo0difsn  10409  nnlesq  10638  facndiv  10733  faclbnd  10735  faclbnd3  10737  bcval5  10757  seq3coll  10836  caucvgre  11004  efaddlem  11696  nndivdvds  11817  nno  11925  nnoddm1d2  11929  divalglemnn  11937  divalg2  11945  ndvdsadd  11950  gcdmultiple  12035  gcdmultiplez  12036  gcdzeq  12037  sqgcd  12044  dvdssqlem  12045  lcmgcdlem  12091  coprmgcdb  12102  qredeq  12110  qredeu  12111  prmdvdsfz  12153  sqrt2irr  12176  divdenle  12211  phibndlem  12230  hashgcdlem  12252  oddprm  12273  pythagtriplem10  12283  pythagtriplem12  12289  pythagtriplem14  12291  pythagtriplem16  12293  pythagtriplem19  12296  pclemub  12301  pc2dvds  12343  pcmpt  12355  fldivp1  12360  pcbc  12363  infpnlem1  12371  oddennn  12407  exmidunben  12441  mulgnegnn  13025  lgsval4a  14719