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

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

Proof of Theorem zre
StepHypRef Expression
1 elz 8247 . 2 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
21simplbi 259 1 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  w3o 884   = wceq 1243  wcel 1393  cr 6888  0cc0 6889  -cneg 7183  cn 7914  cz 8245
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-3or 886  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2312  df-rab 2315  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-iota 4867  df-fv 4910  df-ov 5515  df-neg 7185  df-z 8246
This theorem is referenced by:  zcn  8250  zrei  8251  zssre  8252  elnn0z  8258  elnnz1  8268  peano2z  8281  zaddcl  8285  ztri3or0  8287  ztri3or  8288  zletric  8289  zlelttric  8290  zltnle  8291  zleloe  8292  zletr  8294  znnsub  8296  zltp1le  8298  zleltp1  8299  znn0sub  8309  zapne  8315  zdceq  8316  zdcle  8317  zdclt  8318  zltlen  8319  nn0ge0div  8327  zextle  8331  btwnnz  8334  msqznn  8338  peano2uz2  8345  uzind  8349  fzind  8353  fnn0ind  8354  eluzuzle  8481  uzid  8487  uzneg  8491  uz11  8495  eluzp1m1  8496  eluzp1p1  8498  eluzaddi  8499  eluzsubi  8500  uzin  8505  uz3m2nn  8515  peano2uz  8526  nn0pzuz  8530  eluz2b2  8540  uz2mulcl  8545  eqreznegel  8549  lbzbi  8551  qre  8560  elfz1eq  8899  fznlem  8905  fzen  8907  uzsubsubfz  8911  fzaddel  8922  fzsuc2  8941  fzp1disj  8942  fzrev  8946  elfz1b  8952  fzneuz  8963  fzp1nel  8966  elfz0fzfz0  8983  fz0fzelfz0  8984  fznn0sub2  8985  fz0fzdiffz0  8987  elfzmlbmOLD  8989  elfzmlbp  8990  difelfznle  8993  elfzouz2  9017  fzonlt0  9023  fzossrbm1  9029  fzo1fzo0n0  9039  elfzo0z  9040  fzofzim  9044  eluzgtdifelfzo  9053  fzossfzop1  9068  ssfzo12bi  9081  elfzomelpfzo  9087  fzosplitprm1  9090  fzostep1  9093  flid  9126  flqbi2  9133  2tnp1ge0ge0  9143  flhalf  9144  fldiv4p1lem1div2  9147  ceiqle  9155  zsqcl2  9331  nn0abscl  9681  ialgcvga  9890
  Copyright terms: Public domain W3C validator