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

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

Proof of Theorem zre
StepHypRef Expression
1 elz 8304 . 2 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
21simplbi 263 1 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  w3o 895   = wceq 1259  wcel 1409  cr 6946  0cc0 6947  -cneg 7246  cn 7990  cz 8302
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-3or 897  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-rex 2329  df-rab 2332  df-v 2576  df-un 2950  df-sn 3409  df-pr 3410  df-op 3412  df-uni 3609  df-br 3793  df-iota 4895  df-fv 4938  df-ov 5543  df-neg 7248  df-z 8303
This theorem is referenced by:  zcn  8307  zrei  8308  zssre  8309  elnn0z  8315  elnnz1  8325  peano2z  8338  zaddcl  8342  ztri3or0  8344  ztri3or  8345  zletric  8346  zlelttric  8347  zltnle  8348  zleloe  8349  zletr  8351  znnsub  8353  nzadd  8354  zltp1le  8356  zleltp1  8357  znn0sub  8367  zapne  8373  zdceq  8374  zdcle  8375  zdclt  8376  zltlen  8377  nn0ge0div  8385  zextle  8389  btwnnz  8392  msqznn  8397  peano2uz2  8404  uzind  8408  fzind  8412  fnn0ind  8413  eluzuzle  8577  uzid  8583  uzneg  8587  uz11  8591  eluzp1m1  8592  eluzp1p1  8594  eluzaddi  8595  eluzsubi  8596  uzin  8601  uz3m2nn  8611  peano2uz  8622  nn0pzuz  8626  eluz2b2  8637  uz2mulcl  8642  eqreznegel  8646  lbzbi  8648  qre  8657  zltaddlt1le  8975  elfz1eq  9001  fznlem  9007  fzen  9009  uzsubsubfz  9013  fzaddel  9024  fzsuc2  9043  fzp1disj  9044  fzrev  9048  elfz1b  9054  fzneuz  9065  fzp1nel  9068  elfz0fzfz0  9085  fz0fzelfz0  9086  fznn0sub2  9087  fz0fzdiffz0  9089  elfzmlbmOLD  9091  elfzmlbp  9092  difelfznle  9095  elfzouz2  9119  fzonlt0  9125  fzossrbm1  9131  fzo1fzo0n0  9141  elfzo0z  9142  fzofzim  9146  eluzgtdifelfzo  9155  fzossfzop1  9170  ssfzo12bi  9183  elfzomelpfzo  9189  fzosplitprm1  9192  fzostep1  9195  flid  9234  flqbi2  9241  2tnp1ge0ge0  9251  flhalf  9252  fldiv4p1lem1div2  9255  ceiqle  9263  zsqcl2  9497  nn0abscl  9912  evennn02n  10194  evennn2n  10195  ltoddhalfle  10205  ialgcvga  10273
  Copyright terms: Public domain W3C validator