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

Theorem zre 8690
Description: An integer is a real. (Contributed by NM, 8-Jan-2002.)
Assertion
Ref Expression
zre (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)

Proof of Theorem zre
StepHypRef Expression
1 elz 8688 . 2 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
21simplbi 268 1 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  w3o 921   = wceq 1287  wcel 1436  cr 7296  0cc0 7297  -cneg 7601  cn 8360  cz 8686
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-3or 923  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-rex 2361  df-rab 2364  df-v 2617  df-un 2992  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-br 3823  df-iota 4948  df-fv 4991  df-ov 5618  df-neg 7603  df-z 8687
This theorem is referenced by:  zcn  8691  zrei  8692  zssre  8693  elnn0z  8699  elnnz1  8709  peano2z  8722  zaddcl  8726  ztri3or0  8728  ztri3or  8729  zletric  8730  zlelttric  8731  zltnle  8732  zleloe  8733  zletr  8735  znnsub  8737  nzadd  8738  zltp1le  8740  zleltp1  8741  znn0sub  8751  zapne  8757  zdceq  8758  zdcle  8759  zdclt  8760  zltlen  8761  nn0ge0div  8769  zextle  8773  btwnnz  8776  suprzclex  8780  msqznn  8782  peano2uz2  8789  uzind  8793  fzind  8797  fnn0ind  8798  eluzuzle  8962  uzid  8968  uzneg  8972  uz11  8976  eluzp1m1  8977  eluzp1p1  8979  eluzaddi  8980  eluzsubi  8981  uzin  8986  uz3m2nn  8996  peano2uz  9006  nn0pzuz  9010  eluz2b2  9025  uz2mulcl  9030  eqreznegel  9034  lbzbi  9036  qre  9045  zltaddlt1le  9358  elfz1eq  9384  fznlem  9390  fzen  9392  uzsubsubfz  9396  fzaddel  9407  fzsuc2  9426  fzp1disj  9427  fzrev  9431  elfz1b  9437  fzneuz  9448  fzp1nel  9451  elfz0fzfz0  9468  fz0fzelfz0  9469  fznn0sub2  9470  fz0fzdiffz0  9472  elfzmlbp  9474  difelfznle  9477  elfzouz2  9503  fzonlt0  9509  fzossrbm1  9515  fzo1fzo0n0  9525  elfzo0z  9526  fzofzim  9530  eluzgtdifelfzo  9539  fzossfzop1  9554  ssfzo12bi  9567  elfzomelpfzo  9573  fzosplitprm1  9576  fzostep1  9579  flid  9622  flqbi2  9629  2tnp1ge0ge0  9639  flhalf  9640  fldiv4p1lem1div2  9643  ceiqle  9651  uzsinds  9779  zsqcl2  9952  nn0abscl  10435  zmaxcl  10573  evennn02n  10807  evennn2n  10808  ltoddhalfle  10818  infssuzex  10870  dfgcd2  10928  ialgcvga  10958  isprm3  11025  dvdsnprmd  11032  sqnprm  11042  zgcdsq  11104  hashdvds  11122
  Copyright terms: Public domain W3C validator