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

Theorem nnre 8113
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 8110 . 2  |-  NN  C_  RR
21sseli 2996 1  |-  ( A  e.  NN  ->  A  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1434   RRcr 7042   NNcn 8106
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-sep 3904  ax-cnex 7129  ax-resscn 7130  ax-1re 7132  ax-addrcl 7135
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-ral 2354  df-v 2604  df-in 2980  df-ss 2987  df-int 3645  df-inn 8107
This theorem is referenced by:  nnrei  8115  peano2nn  8118  nn1suc  8125  nnge1  8129  nnle1eq1  8130  nngt0  8131  nnnlt1  8132  nnap0  8135  nn2ge  8138  nn1gt1  8139  nndivre  8141  nnrecgt0  8143  nnsub  8144  arch  8352  nnrecl  8353  bndndx  8354  nn0ge0  8380  0mnnnnn0  8387  nnnegz  8435  elnnz  8442  elz2  8500  gtndiv  8523  prime  8527  btwnz  8547  qre  8791  nnrp  8824  nnledivrp  8918  fzo1fzo0n0  9269  elfzo0le  9271  fzonmapblen  9273  ubmelfzo  9286  fzonn0p1p1  9299  elfzom1p1elfzo  9300  ubmelm1fzo  9312  subfzo0  9328  adddivflid  9374  flltdivnn0lt  9386  intfracq  9402  flqdiv  9403  m1modnnsub1  9452  addmodid  9454  modfzo0difsn  9477  nnlesq  9675  facndiv  9763  faclbnd  9765  faclbnd3  9767  ibcval5  9787  caucvgre  10005  nndivdvds  10346  nno  10450  nnoddm1d2  10454  divalglemnn  10462  divalg2  10470  ndvdsadd  10475  gcdmultiple  10553  gcdmultiplez  10554  gcdzeq  10555  sqgcd  10562  dvdssqlem  10563  lcmgcdlem  10603  coprmgcdb  10614  qredeq  10622  qredeu  10623  prmdvdsfz  10664  sqrt2irr  10685  oddennn  10703
  Copyright terms: Public domain W3C validator