Theorem zre 8910

Description: An integer is a real. (Contributed by NM, 8-Jan-2002.)

Assertion

Ref	Expression
zre	⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)

Proof of Theorem zre

Step	Hyp	Ref	Expression
1		elz 8908	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
2	1	simplbi 270	1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)

Syntax hints:   → wi 4   ∨ w3o 929   = wceq 1299   ∈ wcel 1448  ℝcr 7499  0cc0 7500  -cneg 7805  ℕcn 8578  ℤcz 8906

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-3or 931  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-rex 2381  df-rab 2384  df-v 2643  df-un 3025  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-br 3876  df-iota 5024  df-fv 5067  df-ov 5709  df-neg 7807  df-z 8907

This theorem is referenced by:  zcn  8911  zrei  8912  zssre  8913  elnn0z  8919  elnnz1  8929  peano2z  8942  zaddcl  8946  ztri3or0  8948  ztri3or  8949  zletric  8950  zlelttric  8951  zltnle  8952  zleloe  8953  zletr  8955  znnsub  8957  nzadd  8958  zltp1le  8960  zleltp1  8961  znn0sub  8971  zapne  8977  zdceq  8978  zdcle  8979  zdclt  8980  zltlen  8981  nn0ge0div  8990  zextle  8994  btwnnz  8997  suprzclex  9001  msqznn  9003  peano2uz2  9010  uzind  9014  fzind  9018  fnn0ind  9019  eluzuzle  9184  uzid  9190  uzneg  9194  uz11  9198  eluzp1m1  9199  eluzp1p1  9201  eluzaddi  9202  eluzsubi  9203  uzin  9208  uz3m2nn  9218  peano2uz  9228  nn0pzuz  9232  eluz2b2  9247  uz2mulcl  9252  eqreznegel  9256  lbzbi  9258  qre  9267  zltaddlt1le  9630  elfz1eq  9656  fznlem  9662  fzen  9664  uzsubsubfz  9668  fzaddel  9680  fzsuc2  9700  fzp1disj  9701  fzrev  9705  elfz1b  9711  fzneuz  9722  fzp1nel  9725  elfz0fzfz0  9744  fz0fzelfz0  9745  fznn0sub2  9746  fz0fzdiffz0  9748  elfzmlbp  9750  difelfznle  9753  elfzouz2  9779  fzonlt0  9785  fzossrbm1  9791  fzo1fzo0n0  9801  elfzo0z  9802  fzofzim  9806  eluzgtdifelfzo  9815  fzossfzop1  9830  ssfzo12bi  9843  elfzomelpfzo  9849  fzosplitprm1  9852  fzostep1  9855  flid  9898  flqbi2  9905  2tnp1ge0ge0  9915  flhalf  9916  fldiv4p1lem1div2  9919  ceiqle  9927  uzsinds  10056  zsqcl2  10211  nn0abscl  10697  zmaxcl  10835  2zsupmax  10836  evennn02n  11374  evennn2n  11375  ltoddhalfle  11385  infssuzex  11437  dfgcd2  11495  algcvga  11525  isprm3  11592  dvdsnprmd  11599  sqnprm  11609  zgcdsq  11671  hashdvds  11689