Theorem nnre 8991

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

Syntax hints:   -> wi 4   e. wcel 2164   RRcr 7873   NNcn 8984

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-sep 4148  ax-cnex 7965  ax-resscn 7966  ax-1re 7968  ax-addrcl 7971

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-v 2762  df-in 3160  df-ss 3167  df-int 3872  df-inn 8985

This theorem is referenced by:  nnrei  8993  peano2nn  8996  nn1suc  9003  nnge1  9007  nnle1eq1  9008  nngt0  9009  nnnlt1  9010  nnap0  9013  nn2ge  9017  nn1gt1  9018  nndivre  9020  nnrecgt0  9022  nnsub  9023  arch  9240  nnrecl  9241  bndndx  9242  nn0ge0  9268  0mnnnnn0  9275  nnnegz  9323  elnnz  9330  elz2  9391  gtndiv  9415  prime  9419  btwnz  9439  qre  9693  elpq  9717  elpqb  9718  nnrp  9732  nnledivrp  9835  fzo1fzo0n0  10253  elfzo0le  10255  fzonmapblen  10257  ubmelfzo  10270  fzonn0p1p1  10283  elfzom1p1elfzo  10284  ubmelm1fzo  10296  subfzo0  10312  adddivflid  10364  flltdivnn0lt  10376  intfracq  10394  flqdiv  10395  m1modnnsub1  10444  addmodid  10446  modfzo0difsn  10469  nnlesq  10717  facndiv  10813  faclbnd  10815  faclbnd3  10817  bcval5  10837  seq3coll  10916  caucvgre  11128  efaddlem  11820  nndivdvds  11942  nno  12050  nnoddm1d2  12054  divalglemnn  12062  divalg2  12070  ndvdsadd  12075  gcdmultiple  12160  gcdmultiplez  12161  gcdzeq  12162  sqgcd  12169  dvdssqlem  12170  lcmgcdlem  12218  coprmgcdb  12229  qredeq  12237  qredeu  12238  prmdvdsfz  12280  sqrt2irr  12303  divdenle  12338  phibndlem  12357  hashgcdlem  12379  oddprm  12400  pythagtriplem10  12410  pythagtriplem12  12416  pythagtriplem14  12418  pythagtriplem16  12420  pythagtriplem19  12423  pclemub  12428  pc2dvds  12471  pcmpt  12484  fldivp1  12489  pcbc  12492  infpnlem1  12500  oddennn  12552  exmidunben  12586  mulgnegnn  13205  znidomb  14157  lgsval4a  15179  gausslemma2dlem0c  15208  gausslemma2dlem0d  15209  gausslemma2dlem1a  15215  gausslemma2dlem2  15219  gausslemma2dlem3  15220  lgsquadlem1  15234  lgsquadlem2  15235  2lgslem1a1  15243