Theorem nnre 9314

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 9311	. 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 8179   NNcn 9307

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 8271  ax-resscn 8272  ax-1re 8274  ax-addrcl 8277

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 9308

This theorem is used by:  nnrei  9316  peano2nn  9319  nn1suc  9326  nnge1  9330  nnle1eq1  9331  nngt0  9332  nnnlt1  9333  nnap0  9336  nn2ge  9340  nn1gt1  9341  nndivre  9343  nnrecgt0  9345  nnsub  9346  arch  9565  nnrecl  9566  bndndx  9567  nn0ge0  9593  0mnnnnn0  9600  nnnegz  9652  elnnz  9659  elz2  9721  gtndiv  9746  prime  9750  btwnz  9770  qre  10035  elpq  10060  elpqb  10061  nnrp  10075  nnledivrp  10178  fzo1fzo0n0  10606  elfzo0le  10608  fzonmapblen  10610  ubmelfzo  10629  fzonn0p1p1  10642  elfzom1p1elfzo  10643  ubmelm1fzo  10655  subfzo0  10672  adddivflid  10742  flltdivnn0lt  10754  intfracq  10772  flqdiv  10773  m1modnnsub1  10822  addmodid  10824  modfzo0difsn  10847  nnlesq  11095  facndiv  11193  faclbnd  11195  faclbnd3  11197  bcval5  11217  seq3coll  11310  ccatval21sw  11389  caucvgre  11763  efaddlem  12460  nndivdvds  12582  nno  12692  nnoddm1d2  12696  divalglemnn  12704  divalg2  12712  ndvdsadd  12717  gcdmultiple  12816  gcdmultiplez  12817  gcdzeq  12818  sqgcd  12825  dvdssqlem  12826  lcmgcdlem  12874  coprmgcdb  12885  qredeq  12893  qredeu  12894  prmdvdsfz  12937  sqrt2irr  12960  divdenle  12996  phibndlem  13017  hashgcdlem  13039  oddprm  13061  pythagtriplem10  13071  pythagtriplem12  13077  pythagtriplem14  13079  pythagtriplem16  13081  pythagtriplem19  13084  pclemub  13089  pc2dvds  13132  pcmpt  13145  fldivp1  13150  pcbc  13153  infpnlem1  13161  ballotfilemonn  13273  oddennn  13335  exmidunben  13369  mulgnegnn  13988  znidomb  15077  birthdaylem3  16188  pellexlem1  16190  ppiqltx  16242  chtublem  16256  bcmono  16265  bposlem1  16272  bposlem5  16276  bposlem6  16277  lgsval4a  16307  gausslemma2dlem0c  16336  gausslemma2dlem0d  16337  gausslemma2dlem1a  16343  gausslemma2dlem2  16347  gausslemma2dlem3  16348  lgsquadlem1  16362  lgsquadlem2  16363  2lgslem1a1  16371