Theorem nnre 9150

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

Syntax hints:   -> wi 4   e. wcel 2202   RRcr 8031   NNcn 9143

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8123  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804  df-in 3206  df-ss 3213  df-int 3929  df-inn 9144

This theorem is referenced by:  nnrei  9152  peano2nn  9155  nn1suc  9162  nnge1  9166  nnle1eq1  9167  nngt0  9168  nnnlt1  9169  nnap0  9172  nn2ge  9176  nn1gt1  9177  nndivre  9179  nnrecgt0  9181  nnsub  9182  arch  9399  nnrecl  9400  bndndx  9401  nn0ge0  9427  0mnnnnn0  9434  nnnegz  9482  elnnz  9489  elz2  9551  gtndiv  9575  prime  9579  btwnz  9599  qre  9859  elpq  9883  elpqb  9884  nnrp  9898  nnledivrp  10001  fzo1fzo0n0  10423  elfzo0le  10425  fzonmapblen  10427  ubmelfzo  10446  fzonn0p1p1  10459  elfzom1p1elfzo  10460  ubmelm1fzo  10472  subfzo0  10489  adddivflid  10553  flltdivnn0lt  10565  intfracq  10583  flqdiv  10584  m1modnnsub1  10633  addmodid  10635  modfzo0difsn  10658  nnlesq  10906  facndiv  11002  faclbnd  11004  faclbnd3  11006  bcval5  11026  seq3coll  11107  ccatval21sw  11186  caucvgre  11559  efaddlem  12253  nndivdvds  12375  nno  12485  nnoddm1d2  12489  divalglemnn  12497  divalg2  12505  ndvdsadd  12510  gcdmultiple  12609  gcdmultiplez  12610  gcdzeq  12611  sqgcd  12618  dvdssqlem  12619  lcmgcdlem  12667  coprmgcdb  12678  qredeq  12686  qredeu  12687  prmdvdsfz  12729  sqrt2irr  12752  divdenle  12787  phibndlem  12806  hashgcdlem  12828  oddprm  12850  pythagtriplem10  12860  pythagtriplem12  12866  pythagtriplem14  12868  pythagtriplem16  12870  pythagtriplem19  12873  pclemub  12878  pc2dvds  12921  pcmpt  12934  fldivp1  12939  pcbc  12942  infpnlem1  12950  oddennn  13031  exmidunben  13065  mulgnegnn  13737  znidomb  14691  lgsval4a  15770  gausslemma2dlem0c  15799  gausslemma2dlem0d  15800  gausslemma2dlem1a  15806  gausslemma2dlem2  15810  gausslemma2dlem3  15811  lgsquadlem1  15825  lgsquadlem2  15826  2lgslem1a1  15834