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

Theorem zre 9078
Description: An integer is a real. (Contributed by NM, 8-Jan-2002.)
Assertion
Ref Expression
zre  |-  ( N  e.  ZZ  ->  N  e.  RR )

Proof of Theorem zre
StepHypRef Expression
1 elz 9076 . 2  |-  ( N  e.  ZZ  <->  ( N  e.  RR  /\  ( N  =  0  \/  N  e.  NN  \/  -u N  e.  NN ) ) )
21simplbi 272 1  |-  ( N  e.  ZZ  ->  N  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ w3o 962    = wceq 1332    e. wcel 1481   RRcr 7639   0cc0 7640   -ucneg 7954   NNcn 8740   ZZcz 9074
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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-rab 2426  df-v 2689  df-un 3076  df-sn 3534  df-pr 3535  df-op 3537  df-uni 3741  df-br 3934  df-iota 5092  df-fv 5135  df-ov 5781  df-neg 7956  df-z 9075
This theorem is referenced by:  zcn  9079  zrei  9080  zssre  9081  elnn0z  9087  elnnz1  9097  peano2z  9110  zaddcl  9114  ztri3or0  9116  ztri3or  9117  zletric  9118  zlelttric  9119  zltnle  9120  zleloe  9121  zletr  9123  znnsub  9125  nzadd  9126  zltp1le  9128  zleltp1  9129  znn0sub  9139  zapne  9145  zdceq  9146  zdcle  9147  zdclt  9148  zltlen  9149  nn0ge0div  9158  zextle  9162  btwnnz  9165  suprzclex  9169  msqznn  9171  peano2uz2  9178  uzind  9182  fzind  9186  fnn0ind  9187  eluzuzle  9354  uzid  9360  uzneg  9364  uz11  9368  eluzp1m1  9369  eluzp1p1  9371  eluzaddi  9372  eluzsubi  9373  uzin  9378  uz3m2nn  9391  peano2uz  9401  nn0pzuz  9405  eluz2b2  9420  uz2mulcl  9425  eqreznegel  9429  lbzbi  9431  qre  9440  elpq  9463  zltaddlt1le  9816  elfz1eq  9842  fznlem  9848  fzen  9850  uzsubsubfz  9854  fzaddel  9866  fzsuc2  9886  fzp1disj  9887  fzrev  9891  elfz1b  9897  fzneuz  9908  fzp1nel  9911  elfz0fzfz0  9930  fz0fzelfz0  9931  fznn0sub2  9932  fz0fzdiffz0  9934  elfzmlbp  9936  difelfznle  9939  elfzouz2  9965  fzonlt0  9971  fzossrbm1  9977  fzo1fzo0n0  9987  elfzo0z  9988  fzofzim  9992  eluzgtdifelfzo  10001  fzossfzop1  10016  ssfzo12bi  10029  elfzomelpfzo  10035  fzosplitprm1  10038  fzostep1  10041  flid  10084  flqbi2  10091  2tnp1ge0ge0  10101  flhalf  10102  fldiv4p1lem1div2  10105  ceiqle  10113  uzsinds  10242  zsqcl2  10397  nn0abscl  10885  zmaxcl  11024  2zsupmax  11025  evennn02n  11606  evennn2n  11607  ltoddhalfle  11617  infssuzex  11669  dfgcd2  11729  algcvga  11759  isprm3  11826  dvdsnprmd  11833  sqnprm  11843  zgcdsq  11906  hashdvds  11924  coskpi  12968  relogexp  12992  rplogbzexp  13070
  Copyright terms: Public domain W3C validator