Theorem zre 9347

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

Syntax hints:   → wi 4   ∨ w3o 979   = wceq 1364   ∈ wcel 2167  ℝcr 7895  0cc0 7896  -cneg 8215  ℕcn 9007  ℤcz 9343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-rab 2484  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5928  df-neg 8217  df-z 9344

This theorem is referenced by:  zcn  9348  zrei  9349  zssre  9350  elnn0z  9356  elnnz1  9366  peano2z  9379  zaddcl  9383  ztri3or0  9385  ztri3or  9386  zletric  9387  zlelttric  9388  zltnle  9389  zleloe  9390  zletr  9392  znnsub  9394  nzadd  9395  zltp1le  9397  zleltp1  9398  znn0sub  9408  zapne  9417  zdceq  9418  zdcle  9419  zdclt  9420  zltlen  9421  nn0ge0div  9430  zextle  9434  btwnnz  9437  suprzclex  9441  msqznn  9443  peano2uz2  9450  uzind  9454  fzind  9458  fnn0ind  9459  eluzuzle  9626  uzid  9632  uzneg  9637  uz11  9641  eluzp1m1  9642  eluzp1p1  9644  eluzaddi  9645  eluzsubi  9646  uzin  9651  uz3m2nn  9664  peano2uz  9674  nn0pzuz  9678  eluz2b2  9694  uz2mulcl  9699  eqreznegel  9705  lbzbi  9707  qre  9716  elpq  9740  zltaddlt1le  10099  elfz1eq  10127  fznlem  10133  fzen  10135  uzsubsubfz  10139  fzaddel  10151  fzsuc2  10171  fzp1disj  10172  fzrev  10176  elfz1b  10182  fzneuz  10193  fzp1nel  10196  elfz0fzfz0  10218  fz0fzelfz0  10219  fznn0sub2  10220  fz0fzdiffz0  10222  elfzmlbp  10224  difelfznle  10227  nelfzo  10244  elfzouz2  10254  fzonlt0  10260  fzossrbm1  10266  fzo1fzo0n0  10276  elfzo0z  10277  fzofzim  10281  eluzgtdifelfzo  10290  fzossfzop1  10305  ssfzo12bi  10318  elfzomelpfzo  10324  fzosplitprm1  10327  fzostep1  10330  infssuzex  10340  flid  10391  flqbi2  10398  2tnp1ge0ge0  10408  flhalf  10409  fldiv4p1lem1div2  10412  fldiv4lem1div2uz2  10413  ceiqle  10422  uzsinds  10553  zsqcl2  10726  nn0abscl  11267  zmaxcl  11406  2zsupmax  11408  2zinfmin  11425  p1modz1  11976  evennn02n  12064  evennn2n  12065  ltoddhalfle  12075  bitsp1o  12135  dfgcd2  12206  algcvga  12244  isprm3  12311  dvdsnprmd  12318  sqnprm  12329  zgcdsq  12394  hashdvds  12414  fldivp1  12542  zgz  12567  4sqlem4  12586  4sqexercise1  12592  mulgval  13328  coskpi  15168  relogexp  15192  rplogbzexp  15274  zabsle1  15324  lgsne0  15363  gausslemma2dlem1a  15383  gausslemma2dlem3  15388  gausslemma2dlem4  15389  lgsquadlem1  15402  lgsquadlem2  15403  2lgslem1a1  15411  2lgslem1a2  15412  2sqlem2  15440