Theorem zre 9482

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

Syntax hints:   → wi 4   ∨ w3o 1003   = wceq 1397   ∈ wcel 2202  ℝcr 8030  0cc0 8031  -cneg 8350  ℕcn 9142  ℤcz 9478

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-rab 2519  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6020  df-neg 8352  df-z 9479

This theorem is referenced by:  zcn  9483  zrei  9484  zssre  9485  elnn0z  9491  elnnz1  9501  peano2z  9514  zaddcl  9518  ztri3or0  9520  ztri3or  9521  zletric  9522  zlelttric  9523  zltnle  9524  zleloe  9525  zletr  9528  znnsub  9530  nzadd  9531  zltp1le  9533  zleltp1  9534  znn0sub  9544  zapne  9553  zdceq  9554  zdcle  9555  zdclt  9556  zltlen  9557  nn0ge0div  9566  zextle  9570  btwnnz  9573  suprzclex  9577  msqznn  9579  peano2uz2  9586  uzind  9590  fzind  9594  fnn0ind  9595  eluzuzle  9763  uzid  9769  uzneg  9774  uz11  9778  eluzp1m1  9779  eluzp1p1  9781  eluzaddi  9782  eluzsubi  9783  uzin  9788  uz3m2nn  9806  peano2uz  9816  nn0pzuz  9820  eluz2b2  9836  uz2mulcl  9841  eqreznegel  9847  lbzbi  9849  qre  9858  elpq  9882  zltaddlt1le  10241  elfz1eq  10269  fznlem  10275  fzen  10277  uzsubsubfz  10281  fzaddel  10293  fzsuc2  10313  fzp1disj  10314  fzrev  10318  elfz1b  10324  fzneuz  10335  fzp1nel  10338  elfz0fzfz0  10360  fz0fzelfz0  10361  fznn0sub2  10362  fz0fzdiffz0  10364  elfzmlbp  10366  difelfznle  10369  nelfzo  10386  elfzouz2  10396  fzo0n  10402  fzonlt0  10403  fzossrbm1  10409  fzo1fzo0n0  10421  elfzo0z  10422  fzofzim  10426  eluzgtdifelfzo  10441  fzossfzop1  10456  ssfzo12bi  10469  elfzomelpfzo  10475  fzosplitprm1  10479  fzostep1  10482  infssuzex  10492  flid  10543  flqbi2  10550  2tnp1ge0ge0  10560  flhalf  10561  fldiv4p1lem1div2  10564  fldiv4lem1div2uz2  10565  ceiqle  10574  uzsinds  10705  zsqcl2  10878  ccatsymb  11178  ccatval21sw  11181  lswccatn0lsw  11187  swrd0g  11240  swrdswrdlem  11284  swrdswrd  11285  swrdccatin2  11309  pfxccatin12lem2  11311  pfxccatin12lem3  11312  nn0abscl  11645  zmaxcl  11784  2zsupmax  11786  2zinfmin  11803  p1modz1  12354  evennn02n  12442  evennn2n  12443  ltoddhalfle  12453  bitsp1o  12513  dfgcd2  12584  algcvga  12622  isprm3  12689  dvdsnprmd  12696  sqnprm  12707  zgcdsq  12772  hashdvds  12792  fldivp1  12920  zgz  12945  4sqlem4  12964  4sqexercise1  12970  mulgval  13708  coskpi  15571  relogexp  15595  rplogbzexp  15677  zabsle1  15727  lgsne0  15766  gausslemma2dlem1a  15786  gausslemma2dlem3  15791  gausslemma2dlem4  15792  lgsquadlem1  15805  lgsquadlem2  15806  2lgslem1a1  15814  2lgslem1a2  15815  2sqlem2  15843  clwwlkext2edg  16272