Theorem nnre 9209

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

Syntax hints:   -> wi 4   e. wcel 2202   RRcr 8091   NNcn 9202

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-sep 4212  ax-cnex 8183  ax-resscn 8184  ax-1re 8186  ax-addrcl 8189

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-v 2805  df-in 3207  df-ss 3214  df-int 3934  df-inn 9203

This theorem is referenced by:  nnrei  9211  peano2nn  9214  nn1suc  9221  nnge1  9225  nnle1eq1  9226  nngt0  9227  nnnlt1  9228  nnap0  9231  nn2ge  9235  nn1gt1  9236  nndivre  9238  nnrecgt0  9240  nnsub  9241  arch  9458  nnrecl  9459  bndndx  9460  nn0ge0  9486  0mnnnnn0  9493  nnnegz  9543  elnnz  9550  elz2  9612  gtndiv  9636  prime  9640  btwnz  9660  qre  9920  elpq  9944  elpqb  9945  nnrp  9959  nnledivrp  10062  fzo1fzo0n0  10485  elfzo0le  10487  fzonmapblen  10489  ubmelfzo  10508  fzonn0p1p1  10521  elfzom1p1elfzo  10522  ubmelm1fzo  10534  subfzo0  10551  adddivflid  10615  flltdivnn0lt  10627  intfracq  10645  flqdiv  10646  m1modnnsub1  10695  addmodid  10697  modfzo0difsn  10720  nnlesq  10968  facndiv  11064  faclbnd  11066  faclbnd3  11068  bcval5  11088  seq3coll  11169  ccatval21sw  11248  caucvgre  11621  efaddlem  12315  nndivdvds  12437  nno  12547  nnoddm1d2  12551  divalglemnn  12559  divalg2  12567  ndvdsadd  12572  gcdmultiple  12671  gcdmultiplez  12672  gcdzeq  12673  sqgcd  12680  dvdssqlem  12681  lcmgcdlem  12729  coprmgcdb  12740  qredeq  12748  qredeu  12749  prmdvdsfz  12791  sqrt2irr  12814  divdenle  12849  phibndlem  12868  hashgcdlem  12890  oddprm  12912  pythagtriplem10  12922  pythagtriplem12  12928  pythagtriplem14  12930  pythagtriplem16  12932  pythagtriplem19  12935  pclemub  12940  pc2dvds  12983  pcmpt  12996  fldivp1  13001  pcbc  13004  infpnlem1  13012  oddennn  13093  exmidunben  13127  mulgnegnn  13799  znidomb  14754  pellexlem1  15791  lgsval4a  15841  gausslemma2dlem0c  15870  gausslemma2dlem0d  15871  gausslemma2dlem1a  15877  gausslemma2dlem2  15881  gausslemma2dlem3  15882  lgsquadlem1  15896  lgsquadlem2  15897  2lgslem1a1  15905