Theorem zre 9627

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

Syntax hints:   → wi 4   ∨ w3o 1008   = wceq 1402   ∈ wcel 2209  ℝcr 8168  0cc0 8169  -cneg 8488  ℕcn 9283  ℤcz 9623

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-rab 2537  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-iota 5332  df-fv 5380  df-ov 6078  df-neg 8490  df-z 9624

This theorem is referenced by:  zcn  9628  zrei  9629  zssre  9630  elnn0z  9636  elnnz1  9646  peano2z  9659  zaddcl  9663  ztri3or0  9665  ztri3or  9666  zletric  9667  zlelttric  9668  zltnle  9669  zleloe  9670  zletr  9673  znnsub  9675  nzadd  9676  zltp1le  9678  zleltp1  9679  znn0sub  9689  zapne  9698  zdceq  9699  zdcle  9700  zdclt  9701  zltlen  9703  nn0ge0div  9712  zextle  9716  btwnnz  9719  suprzclex  9723  msqznn  9725  peano2uz2  9732  uzind  9736  fzind  9740  fnn0ind  9741  eluzuzle  9909  uzid  9915  uzneg  9920  uz11  9924  eluzp1m1  9925  eluzp1p1  9927  eluzaddi  9928  eluzsubi  9929  uzin  9934  uz3m2nn  9952  peano2uz  9962  nn0pzuz  9966  eluz2b2  9982  uz2mulcl  9987  eqreznegel  9993  lbzbi  9995  qre  10004  elpq  10028  zltaddlt1le  10389  elfz1eq  10418  fznlem  10424  fzen  10426  uzsubsubfz  10430  fzaddel  10443  fzsuc2  10464  fzp1disj  10465  fzrev  10469  elfz1b  10475  fzneuz  10486  fzp1nel  10489  elfz0fzfz0  10511  fz0fzelfz0  10512  fznn0sub2  10513  fz0fzdiffz0  10515  elfzmlbp  10517  difelfznle  10520  nelfzo  10537  elfzouz2  10547  fzo0n  10553  fzonlt0  10554  fzossrbm1  10560  fzo1fzo0n0  10573  elfzo0z  10574  fzofzim  10578  eluzgtdifelfzo  10593  fzossfzop1  10608  ssfzo12bi  10621  elfzomelpfzo  10627  fzosplitprm1  10631  fzostep1  10634  infssuzex  10644  flid  10697  flqbi2  10704  2tnp1ge0ge0  10714  flhalf  10715  fldiv4p1lem1div2  10718  fldiv4lem1div2uz2  10719  ceiqle  10728  uzsinds  10859  zsqcl2  11032  ssenneg  11258  ccatsymb  11348  ccatval21sw  11351  lswccatn0lsw  11357  swrd0g  11410  swrdswrdlem  11454  swrdswrd  11455  swrdccatin2  11479  pfxccatin12lem2  11481  pfxccatin12lem3  11482  nn0abscl  11829  zmaxcl  11968  2zsupmax  11970  2zinfmin  11987  p1modz1  12539  evennn02n  12627  evennn2n  12628  ltoddhalfle  12638  bitsp1o  12698  dfgcd2  12769  algcvga  12807  isprm3  12874  dvdsnprmd  12881  sqnprm  12892  zgcdsq  12957  hashdvds  12977  fldivp1  13105  zgz  13130  4sqlem4  13149  4sqexercise1  13155  mulgval  13902  coskpi  15872  relogexp  15896  rplogbzexp  15979  zabsle1  16032  lgsne0  16071  gausslemma2dlem1a  16091  gausslemma2dlem3  16096  gausslemma2dlem4  16097  lgsquadlem1  16110  lgsquadlem2  16111  2lgslem1a1  16119  2lgslem1a2  16120  2sqlem2  16148  clwwlkext2edg  16577