Theorem nnre 9128

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

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 8009   NNcn 9121

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 8101  ax-resscn 8102  ax-1re 8104  ax-addrcl 8107

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 9122

This theorem is referenced by:  nnrei  9130  peano2nn  9133  nn1suc  9140  nnge1  9144  nnle1eq1  9145  nngt0  9146  nnnlt1  9147  nnap0  9150  nn2ge  9154  nn1gt1  9155  nndivre  9157  nnrecgt0  9159  nnsub  9160  arch  9377  nnrecl  9378  bndndx  9379  nn0ge0  9405  0mnnnnn0  9412  nnnegz  9460  elnnz  9467  elz2  9529  gtndiv  9553  prime  9557  btwnz  9577  qre  9832  elpq  9856  elpqb  9857  nnrp  9871  nnledivrp  9974  fzo1fzo0n0  10395  elfzo0le  10397  fzonmapblen  10399  ubmelfzo  10418  fzonn0p1p1  10431  elfzom1p1elfzo  10432  ubmelm1fzo  10444  subfzo0  10460  adddivflid  10524  flltdivnn0lt  10536  intfracq  10554  flqdiv  10555  m1modnnsub1  10604  addmodid  10606  modfzo0difsn  10629  nnlesq  10877  facndiv  10973  faclbnd  10975  faclbnd3  10977  bcval5  10997  seq3coll  11077  ccatval21sw  11153  caucvgre  11508  efaddlem  12201  nndivdvds  12323  nno  12433  nnoddm1d2  12437  divalglemnn  12445  divalg2  12453  ndvdsadd  12458  gcdmultiple  12557  gcdmultiplez  12558  gcdzeq  12559  sqgcd  12566  dvdssqlem  12567  lcmgcdlem  12615  coprmgcdb  12626  qredeq  12634  qredeu  12635  prmdvdsfz  12677  sqrt2irr  12700  divdenle  12735  phibndlem  12754  hashgcdlem  12776  oddprm  12798  pythagtriplem10  12808  pythagtriplem12  12814  pythagtriplem14  12816  pythagtriplem16  12818  pythagtriplem19  12821  pclemub  12826  pc2dvds  12869  pcmpt  12882  fldivp1  12887  pcbc  12890  infpnlem1  12898  oddennn  12979  exmidunben  13013  mulgnegnn  13685  znidomb  14638  lgsval4a  15717  gausslemma2dlem0c  15746  gausslemma2dlem0d  15747  gausslemma2dlem1a  15753  gausslemma2dlem2  15757  gausslemma2dlem3  15758  lgsquadlem1  15772  lgsquadlem2  15773  2lgslem1a1  15781