Theorem nnre 8897

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

Syntax hints:   -> wi 4   e. wcel 2146   RRcr 7785   NNcn 8890

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157  ax-sep 4116  ax-cnex 7877  ax-resscn 7878  ax-1re 7880  ax-addrcl 7883

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458  df-v 2737  df-in 3133  df-ss 3140  df-int 3841  df-inn 8891

This theorem is referenced by:  nnrei  8899  peano2nn  8902  nn1suc  8909  nnge1  8913  nnle1eq1  8914  nngt0  8915  nnnlt1  8916  nnap0  8919  nn2ge  8923  nn1gt1  8924  nndivre  8926  nnrecgt0  8928  nnsub  8929  arch  9144  nnrecl  9145  bndndx  9146  nn0ge0  9172  0mnnnnn0  9179  nnnegz  9227  elnnz  9234  elz2  9295  gtndiv  9319  prime  9323  btwnz  9343  qre  9596  elpq  9619  elpqb  9620  nnrp  9632  nnledivrp  9735  fzo1fzo0n0  10151  elfzo0le  10153  fzonmapblen  10155  ubmelfzo  10168  fzonn0p1p1  10181  elfzom1p1elfzo  10182  ubmelm1fzo  10194  subfzo0  10210  adddivflid  10260  flltdivnn0lt  10272  intfracq  10288  flqdiv  10289  m1modnnsub1  10338  addmodid  10340  modfzo0difsn  10363  nnlesq  10591  facndiv  10685  faclbnd  10687  faclbnd3  10689  bcval5  10709  seq3coll  10788  caucvgre  10956  efaddlem  11648  nndivdvds  11769  nno  11876  nnoddm1d2  11880  divalglemnn  11888  divalg2  11896  ndvdsadd  11901  gcdmultiple  11986  gcdmultiplez  11987  gcdzeq  11988  sqgcd  11995  dvdssqlem  11996  lcmgcdlem  12042  coprmgcdb  12053  qredeq  12061  qredeu  12062  prmdvdsfz  12104  sqrt2irr  12127  divdenle  12162  phibndlem  12181  hashgcdlem  12203  oddprm  12224  pythagtriplem10  12234  pythagtriplem12  12240  pythagtriplem14  12242  pythagtriplem16  12244  pythagtriplem19  12247  pclemub  12252  pc2dvds  12294  pcmpt  12306  fldivp1  12311  pcbc  12314  infpnlem1  12322  oddennn  12358  exmidunben  12392  mulgnegnn  12852  lgsval4a  13974