Theorem nnre 9045

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

Syntax hints:   -> wi 4   e. wcel 2176   RRcr 7926   NNcn 9038

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-sep 4163  ax-cnex 8018  ax-resscn 8019  ax-1re 8021  ax-addrcl 8024

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-v 2774  df-in 3172  df-ss 3179  df-int 3886  df-inn 9039

This theorem is referenced by:  nnrei  9047  peano2nn  9050  nn1suc  9057  nnge1  9061  nnle1eq1  9062  nngt0  9063  nnnlt1  9064  nnap0  9067  nn2ge  9071  nn1gt1  9072  nndivre  9074  nnrecgt0  9076  nnsub  9077  arch  9294  nnrecl  9295  bndndx  9296  nn0ge0  9322  0mnnnnn0  9329  nnnegz  9377  elnnz  9384  elz2  9446  gtndiv  9470  prime  9474  btwnz  9494  qre  9748  elpq  9772  elpqb  9773  nnrp  9787  nnledivrp  9890  fzo1fzo0n0  10309  elfzo0le  10311  fzonmapblen  10313  ubmelfzo  10331  fzonn0p1p1  10344  elfzom1p1elfzo  10345  ubmelm1fzo  10357  subfzo0  10373  adddivflid  10437  flltdivnn0lt  10449  intfracq  10467  flqdiv  10468  m1modnnsub1  10517  addmodid  10519  modfzo0difsn  10542  nnlesq  10790  facndiv  10886  faclbnd  10888  faclbnd3  10890  bcval5  10910  seq3coll  10989  ccatval21sw  11064  caucvgre  11325  efaddlem  12018  nndivdvds  12140  nno  12250  nnoddm1d2  12254  divalglemnn  12262  divalg2  12270  ndvdsadd  12275  gcdmultiple  12374  gcdmultiplez  12375  gcdzeq  12376  sqgcd  12383  dvdssqlem  12384  lcmgcdlem  12432  coprmgcdb  12443  qredeq  12451  qredeu  12452  prmdvdsfz  12494  sqrt2irr  12517  divdenle  12552  phibndlem  12571  hashgcdlem  12593  oddprm  12615  pythagtriplem10  12625  pythagtriplem12  12631  pythagtriplem14  12633  pythagtriplem16  12635  pythagtriplem19  12638  pclemub  12643  pc2dvds  12686  pcmpt  12699  fldivp1  12704  pcbc  12707  infpnlem1  12715  oddennn  12796  exmidunben  12830  mulgnegnn  13501  znidomb  14453  lgsval4a  15532  gausslemma2dlem0c  15561  gausslemma2dlem0d  15562  gausslemma2dlem1a  15568  gausslemma2dlem2  15572  gausslemma2dlem3  15573  lgsquadlem1  15587  lgsquadlem2  15588  2lgslem1a1  15596