Theorem zre 9349

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

Syntax hints:   → wi 4   ∨ w3o 979   = wceq 1364   ∈ wcel 2167  ℝcr 7897  0cc0 7898  -cneg 8217  ℕcn 9009  ℤcz 9345

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 8219  df-z 9346

This theorem is referenced by:  zcn  9350  zrei  9351  zssre  9352  elnn0z  9358  elnnz1  9368  peano2z  9381  zaddcl  9385  ztri3or0  9387  ztri3or  9388  zletric  9389  zlelttric  9390  zltnle  9391  zleloe  9392  zletr  9394  znnsub  9396  nzadd  9397  zltp1le  9399  zleltp1  9400  znn0sub  9410  zapne  9419  zdceq  9420  zdcle  9421  zdclt  9422  zltlen  9423  nn0ge0div  9432  zextle  9436  btwnnz  9439  suprzclex  9443  msqznn  9445  peano2uz2  9452  uzind  9456  fzind  9460  fnn0ind  9461  eluzuzle  9628  uzid  9634  uzneg  9639  uz11  9643  eluzp1m1  9644  eluzp1p1  9646  eluzaddi  9647  eluzsubi  9648  uzin  9653  uz3m2nn  9666  peano2uz  9676  nn0pzuz  9680  eluz2b2  9696  uz2mulcl  9701  eqreznegel  9707  lbzbi  9709  qre  9718  elpq  9742  zltaddlt1le  10101  elfz1eq  10129  fznlem  10135  fzen  10137  uzsubsubfz  10141  fzaddel  10153  fzsuc2  10173  fzp1disj  10174  fzrev  10178  elfz1b  10184  fzneuz  10195  fzp1nel  10198  elfz0fzfz0  10220  fz0fzelfz0  10221  fznn0sub2  10222  fz0fzdiffz0  10224  elfzmlbp  10226  difelfznle  10229  nelfzo  10246  elfzouz2  10256  fzonlt0  10262  fzossrbm1  10268  fzo1fzo0n0  10278  elfzo0z  10279  fzofzim  10283  eluzgtdifelfzo  10292  fzossfzop1  10307  ssfzo12bi  10320  elfzomelpfzo  10326  fzosplitprm1  10329  fzostep1  10332  infssuzex  10342  flid  10393  flqbi2  10400  2tnp1ge0ge0  10410  flhalf  10411  fldiv4p1lem1div2  10414  fldiv4lem1div2uz2  10415  ceiqle  10424  uzsinds  10555  zsqcl2  10728  nn0abscl  11269  zmaxcl  11408  2zsupmax  11410  2zinfmin  11427  p1modz1  11978  evennn02n  12066  evennn2n  12067  ltoddhalfle  12077  bitsp1o  12137  dfgcd2  12208  algcvga  12246  isprm3  12313  dvdsnprmd  12320  sqnprm  12331  zgcdsq  12396  hashdvds  12416  fldivp1  12544  zgz  12569  4sqlem4  12588  4sqexercise1  12594  mulgval  13330  coskpi  15192  relogexp  15216  rplogbzexp  15298  zabsle1  15348  lgsne0  15387  gausslemma2dlem1a  15407  gausslemma2dlem3  15412  gausslemma2dlem4  15413  lgsquadlem1  15426  lgsquadlem2  15427  2lgslem1a1  15435  2lgslem1a2  15436  2sqlem2  15464