Theorem zre 8355

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 8353	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
2	1	simplbi 268	1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)

Syntax hints:   → wi 4   ∨ w3o 918   = wceq 1284   ∈ wcel 1433  ℝcr 6980  0cc0 6981  -cneg 7280  ℕcn 8039  ℤcz 8351

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 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-3or 920  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-rex 2354  df-rab 2357  df-v 2603  df-un 2977  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-br 3786  df-iota 4887  df-fv 4930  df-ov 5535  df-neg 7282  df-z 8352

This theorem is referenced by:  zcn  8356  zrei  8357  zssre  8358  elnn0z  8364  elnnz1  8374  peano2z  8387  zaddcl  8391  ztri3or0  8393  ztri3or  8394  zletric  8395  zlelttric  8396  zltnle  8397  zleloe  8398  zletr  8400  znnsub  8402  nzadd  8403  zltp1le  8405  zleltp1  8406  znn0sub  8416  zapne  8422  zdceq  8423  zdcle  8424  zdclt  8425  zltlen  8426  nn0ge0div  8434  zextle  8438  btwnnz  8441  suprzclex  8445  msqznn  8447  peano2uz2  8454  uzind  8458  fzind  8462  fnn0ind  8463  eluzuzle  8627  uzid  8633  uzneg  8637  uz11  8641  eluzp1m1  8642  eluzp1p1  8644  eluzaddi  8645  eluzsubi  8646  uzin  8651  uz3m2nn  8661  peano2uz  8671  nn0pzuz  8675  eluz2b2  8690  uz2mulcl  8695  eqreznegel  8699  lbzbi  8701  qre  8710  zltaddlt1le  9028  elfz1eq  9054  fznlem  9060  fzen  9062  uzsubsubfz  9066  fzaddel  9077  fzsuc2  9096  fzp1disj  9097  fzrev  9101  elfz1b  9107  fzneuz  9118  fzp1nel  9121  elfz0fzfz0  9137  fz0fzelfz0  9138  fznn0sub2  9139  fz0fzdiffz0  9141  elfzmlbp  9143  difelfznle  9146  elfzouz2  9170  fzonlt0  9176  fzossrbm1  9182  fzo1fzo0n0  9192  elfzo0z  9193  fzofzim  9197  eluzgtdifelfzo  9206  fzossfzop1  9221  ssfzo12bi  9234  elfzomelpfzo  9240  fzosplitprm1  9243  fzostep1  9246  flid  9286  flqbi2  9293  2tnp1ge0ge0  9303  flhalf  9304  fldiv4p1lem1div2  9307  ceiqle  9315  uzsinds  9428  zsqcl2  9553  nn0abscl  9971  evennn02n  10282  evennn2n  10283  ltoddhalfle  10293  infssuzex  10345  dfgcd2  10403  ialgcvga  10433  isprm3  10500  dvdsnprmd  10507  sqnprm  10517