Theorem nnre 9117

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

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 7998   NNcn 9110

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4202  ax-cnex 8090  ax-resscn 8091  ax-1re 8093  ax-addrcl 8096

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2801  df-in 3203  df-ss 3210  df-int 3924  df-inn 9111

This theorem is referenced by:  nnrei  9119  peano2nn  9122  nn1suc  9129  nnge1  9133  nnle1eq1  9134  nngt0  9135  nnnlt1  9136  nnap0  9139  nn2ge  9143  nn1gt1  9144  nndivre  9146  nnrecgt0  9148  nnsub  9149  arch  9366  nnrecl  9367  bndndx  9368  nn0ge0  9394  0mnnnnn0  9401  nnnegz  9449  elnnz  9456  elz2  9518  gtndiv  9542  prime  9546  btwnz  9566  qre  9820  elpq  9844  elpqb  9845  nnrp  9859  nnledivrp  9962  fzo1fzo0n0  10383  elfzo0le  10385  fzonmapblen  10387  ubmelfzo  10406  fzonn0p1p1  10419  elfzom1p1elfzo  10420  ubmelm1fzo  10432  subfzo0  10448  adddivflid  10512  flltdivnn0lt  10524  intfracq  10542  flqdiv  10543  m1modnnsub1  10592  addmodid  10594  modfzo0difsn  10617  nnlesq  10865  facndiv  10961  faclbnd  10963  faclbnd3  10965  bcval5  10985  seq3coll  11064  ccatval21sw  11140  caucvgre  11492  efaddlem  12185  nndivdvds  12307  nno  12417  nnoddm1d2  12421  divalglemnn  12429  divalg2  12437  ndvdsadd  12442  gcdmultiple  12541  gcdmultiplez  12542  gcdzeq  12543  sqgcd  12550  dvdssqlem  12551  lcmgcdlem  12599  coprmgcdb  12610  qredeq  12618  qredeu  12619  prmdvdsfz  12661  sqrt2irr  12684  divdenle  12719  phibndlem  12738  hashgcdlem  12760  oddprm  12782  pythagtriplem10  12792  pythagtriplem12  12798  pythagtriplem14  12800  pythagtriplem16  12802  pythagtriplem19  12805  pclemub  12810  pc2dvds  12853  pcmpt  12866  fldivp1  12871  pcbc  12874  infpnlem1  12882  oddennn  12963  exmidunben  12997  mulgnegnn  13669  znidomb  14622  lgsval4a  15701  gausslemma2dlem0c  15730  gausslemma2dlem0d  15731  gausslemma2dlem1a  15737  gausslemma2dlem2  15741  gausslemma2dlem3  15742  lgsquadlem1  15756  lgsquadlem2  15757  2lgslem1a1  15765