ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nnre Unicode version

Theorem nnre 8739
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
StepHypRef Expression
1 nnssre 8736 . 2  |-  NN  C_  RR
21sseli 3093 1  |-  ( A  e.  NN  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1480   RRcr 7631   NNcn 8732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-cnex 7723  ax-resscn 7724  ax-1re 7726  ax-addrcl 7729
This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-v 2688  df-in 3077  df-ss 3084  df-int 3772  df-inn 8733
This theorem is referenced by:  nnrei  8741  peano2nn  8744  nn1suc  8751  nnge1  8755  nnle1eq1  8756  nngt0  8757  nnnlt1  8758  nnap0  8761  nn2ge  8765  nn1gt1  8766  nndivre  8768  nnrecgt0  8770  nnsub  8771  arch  8986  nnrecl  8987  bndndx  8988  nn0ge0  9014  0mnnnnn0  9021  nnnegz  9069  elnnz  9076  elz2  9134  gtndiv  9158  prime  9162  btwnz  9182  qre  9429  nnrp  9463  nnledivrp  9565  fzo1fzo0n0  9972  elfzo0le  9974  fzonmapblen  9976  ubmelfzo  9989  fzonn0p1p1  10002  elfzom1p1elfzo  10003  ubmelm1fzo  10015  subfzo0  10031  adddivflid  10077  flltdivnn0lt  10089  intfracq  10105  flqdiv  10106  m1modnnsub1  10155  addmodid  10157  modfzo0difsn  10180  nnlesq  10408  facndiv  10497  faclbnd  10499  faclbnd3  10501  bcval5  10521  seq3coll  10597  caucvgre  10765  efaddlem  11392  nndivdvds  11510  nno  11614  nnoddm1d2  11618  divalglemnn  11626  divalg2  11634  ndvdsadd  11639  gcdmultiple  11719  gcdmultiplez  11720  gcdzeq  11721  sqgcd  11728  dvdssqlem  11729  lcmgcdlem  11769  coprmgcdb  11780  qredeq  11788  qredeu  11789  prmdvdsfz  11830  sqrt2irr  11851  divdenle  11886  phibndlem  11903  hashgcdlem  11914  oddennn  11916  exmidunben  11950
  Copyright terms: Public domain W3C validator