Theorem zre 9657

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

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1008   = wceq 1402   ∈ wcel 2209  ℝcr 8184  0cc0 8185   -cneg 8505  ℕcn 9313  ℤcz 9653

This proof depends on 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 proof 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 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-iota 5340  df-fv 5388  df-ov 6091  df-neg 8507  df-z 9654

This theorem is used by:  zcn  9658  zrei  9659  zssre  9660  elnn0z  9666  elnnz1  9676  peano2z  9689  zaddcl  9693  ztri3or0  9695  ztri3or  9696  zletric  9697  zlelttric  9698  zltnle  9699  zleloe  9700  zletr  9703  znnsub  9705  nzadd  9706  zltp1le  9708  zleltp1  9709  znn0sub  9719  zapne  9728  zdceq  9729  zdcle  9730  zdclt  9731  zltlen  9733  nn0ge0div  9742  zextle  9747  btwnnz  9750  suprzclex  9754  msqznn  9756  peano2uz2  9763  uzind  9767  fzind  9771  fnn0ind  9772  eluzuzle  9945  uzid  9951  uzneg  9956  uz11  9960  eluzp1m1  9961  eluzp1p1  9963  eluzaddi  9964  eluzsubi  9965  uzin  9970  uz3m2nn  9988  peano2uz  9998  nn0pzuz  10002  eluz2b2  10018  uz2mulcl  10023  eqreznegel  10029  lbzbi  10031  qre  10040  elpq  10065  zltaddlt1le  10426  elfz1eq  10455  fznlem  10461  fzen  10463  uzsubsubfz  10468  fzaddel  10481  fzsuc2  10502  fzp1disj  10503  fzrev  10507  elfz1b  10513  fzneuz  10524  fzp1nel  10527  elfz0fzfz0  10549  fz0fzelfz0  10550  fznn0sub2  10551  fz0fzdiffz0  10553  elfzmlbp  10555  difelfznle  10558  nelfzo  10575  elfzouz2  10585  fzo0n  10591  fzonlt0  10592  fzossrbm1  10598  fzo1fzo0n0  10611  elfzo0z  10612  fzofzim  10616  eluzgtdifelfzo  10631  fzossfzop1  10646  ssfzo12bi  10659  elfzomelpfzo  10665  fzosplitprm1  10669  fzostep1  10672  infssuzex  10682  flid  10739  flqbi2  10746  2tnp1ge0ge0  10756  flhalf  10757  fldiv4p1lem1div2  10760  fldiv4lem1div2uz2  10761  ceiqle  10770  uzsinds  10901  zsqcl2  11074  ssenneg  11301  ccatsymb  11391  ccatval21sw  11394  lswccatn0lsw  11400  swrd0g  11453  swrdswrdlem  11497  swrdswrd  11498  swrdccatin2  11522  pfxccatin12lem2  11524  pfxccatin12lem3  11525  nn0abscl  11873  zmaxcl  12012  2zsupmax  12014  zmincl  12028  2zinfmin  12033  p1modz1  12585  evennn02n  12673  evennn2n  12674  ltoddhalfle  12684  bitsp1o  12744  dfgcd2  12815  algcvga  12853  isprm3  12920  dvdsnprmd  12927  sqnprm  12939  zgcdsq  13005  hashdvds  13027  fldivp1  13155  zgz  13180  4sqlem4  13199  4sqexercise1  13205  mulgval  13983  coskpi  16092  relogexp  16119  rplogbzexp  16207  ppiprm  16276  chtprm  16278  zabsle1  16340  lgsne0  16379  gausslemma2dlem1a  16399  gausslemma2dlem3  16404  gausslemma2dlem4  16405  lgsquadlem1  16418  lgsquadlem2  16419  2lgslem1a1  16427  2lgslem1a2  16428  2sqlem2  16456  clwwlkext2edg  16885