Theorem nnre 9313

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 9310	. 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 9306

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 9307

This theorem is used by:  nnrei  9315  peano2nn  9318  nn1suc  9325  nnge1  9329  nnle1eq1  9330  nngt0  9331  nnnlt1  9332  nnap0  9335  nn2ge  9339  nn1gt1  9340  nndivre  9342  nnrecgt0  9344  nnsub  9345  arch  9564  nnrecl  9565  bndndx  9566  nn0ge0  9592  0mnnnnn0  9599  nnnegz  9651  elnnz  9658  elz2  9720  gtndiv  9745  prime  9749  btwnz  9769  qre  10034  elpq  10059  elpqb  10060  nnrp  10074  nnledivrp  10177  fzo1fzo0n0  10605  elfzo0le  10607  fzonmapblen  10609  ubmelfzo  10628  fzonn0p1p1  10641  elfzom1p1elfzo  10642  ubmelm1fzo  10654  subfzo0  10671  adddivflid  10740  flltdivnn0lt  10752  intfracq  10770  flqdiv  10771  m1modnnsub1  10820  addmodid  10822  modfzo0difsn  10845  nnlesq  11093  facndiv  11191  faclbnd  11193  faclbnd3  11195  bcval5  11215  seq3coll  11308  ccatval21sw  11387  caucvgre  11761  efaddlem  12457  nndivdvds  12579  nno  12689  nnoddm1d2  12693  divalglemnn  12701  divalg2  12709  ndvdsadd  12714  gcdmultiple  12813  gcdmultiplez  12814  gcdzeq  12815  sqgcd  12822  dvdssqlem  12823  lcmgcdlem  12871  coprmgcdb  12882  qredeq  12890  qredeu  12891  prmdvdsfz  12934  sqrt2irr  12957  divdenle  12993  phibndlem  13014  hashgcdlem  13036  oddprm  13058  pythagtriplem10  13068  pythagtriplem12  13074  pythagtriplem14  13076  pythagtriplem16  13078  pythagtriplem19  13081  pclemub  13086  pc2dvds  13129  pcmpt  13142  fldivp1  13147  pcbc  13150  infpnlem1  13158  ballotfilemonn  13270  oddennn  13332  exmidunben  13366  mulgnegnn  13984  znidomb  15042  birthdaylem3  16146  pellexlem1  16148  ppiqltx  16183  bcmono  16202  bposlem1  16209  bposlem5  16213  lgsval4a  16239  gausslemma2dlem0c  16268  gausslemma2dlem0d  16269  gausslemma2dlem1a  16275  gausslemma2dlem2  16279  gausslemma2dlem3  16280  lgsquadlem1  16294  lgsquadlem2  16295  2lgslem1a1  16303