Theorem nnre 9311

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   RRcr 8178   NNcn 9304

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4249  ax-cnex 8270  ax-resscn 8271  ax-1re 8273  ax-addrcl 8276

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823  df-in 3226  df-ss 3233  df-int 3971  df-inn 9305

This theorem is used by:  nnrei  9313  peano2nn  9316  nn1suc  9323  nnge1  9327  nnle1eq1  9328  nngt0  9329  nnnlt1  9330  nnap0  9333  nn2ge  9337  nn1gt1  9338  nndivre  9340  nnrecgt0  9342  nnsub  9343  arch  9560  nnrecl  9561  bndndx  9562  nn0ge0  9588  0mnnnnn0  9595  nnnegz  9647  elnnz  9654  elz2  9716  gtndiv  9741  prime  9745  btwnz  9765  qre  10025  elpq  10049  elpqb  10050  nnrp  10064  nnledivrp  10167  fzo1fzo0n0  10595  elfzo0le  10597  fzonmapblen  10599  ubmelfzo  10618  fzonn0p1p1  10631  elfzom1p1elfzo  10632  ubmelm1fzo  10644  subfzo0  10661  adddivflid  10727  flltdivnn0lt  10739  intfracq  10757  flqdiv  10758  m1modnnsub1  10807  addmodid  10809  modfzo0difsn  10832  nnlesq  11080  facndiv  11177  faclbnd  11179  faclbnd3  11181  bcval5  11201  seq3coll  11294  ccatval21sw  11373  caucvgre  11747  efaddlem  12441  nndivdvds  12563  nno  12673  nnoddm1d2  12677  divalglemnn  12685  divalg2  12693  ndvdsadd  12698  gcdmultiple  12797  gcdmultiplez  12798  gcdzeq  12799  sqgcd  12806  dvdssqlem  12807  lcmgcdlem  12855  coprmgcdb  12866  qredeq  12874  qredeu  12875  prmdvdsfz  12917  sqrt2irr  12940  divdenle  12975  phibndlem  12994  hashgcdlem  13016  oddprm  13038  pythagtriplem10  13048  pythagtriplem12  13054  pythagtriplem14  13056  pythagtriplem16  13058  pythagtriplem19  13061  pclemub  13066  pc2dvds  13109  pcmpt  13122  fldivp1  13127  pcbc  13130  infpnlem1  13138  ballotfilemonn  13221  oddennn  13283  exmidunben  13317  mulgnegnn  13935  znidomb  14993  birthdaylem3  16089  pellexlem1  16091  lgsval4a  16141  gausslemma2dlem0c  16170  gausslemma2dlem0d  16171  gausslemma2dlem1a  16177  gausslemma2dlem2  16181  gausslemma2dlem3  16182  lgsquadlem1  16196  lgsquadlem2  16197  2lgslem1a1  16205