Theorem zre 9648

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

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1008   = wceq 1402   ∈ wcel 2209  ℝcr 8178  0cc0 8179  -cneg 8498  ℕcn 9304  ℤcz 9644

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 4131  df-iota 5337  df-fv 5385  df-ov 6088  df-neg 8500  df-z 9645

This theorem is used by:  zcn  9649  zrei  9650  zssre  9651  elnn0z  9657  elnnz1  9667  peano2z  9680  zaddcl  9684  ztri3or0  9686  ztri3or  9687  zletric  9688  zlelttric  9689  zltnle  9690  zleloe  9691  zletr  9694  znnsub  9696  nzadd  9697  zltp1le  9699  zleltp1  9700  znn0sub  9710  zapne  9719  zdceq  9720  zdcle  9721  zdclt  9722  zltlen  9724  nn0ge0div  9733  zextle  9737  btwnnz  9740  suprzclex  9744  msqznn  9746  peano2uz2  9753  uzind  9757  fzind  9761  fnn0ind  9762  eluzuzle  9930  uzid  9936  uzneg  9941  uz11  9945  eluzp1m1  9946  eluzp1p1  9948  eluzaddi  9949  eluzsubi  9950  uzin  9955  uz3m2nn  9973  peano2uz  9983  nn0pzuz  9987  eluz2b2  10003  uz2mulcl  10008  eqreznegel  10014  lbzbi  10016  qre  10025  elpq  10049  zltaddlt1le  10410  elfz1eq  10439  fznlem  10445  fzen  10447  uzsubsubfz  10452  fzaddel  10465  fzsuc2  10486  fzp1disj  10487  fzrev  10491  elfz1b  10497  fzneuz  10508  fzp1nel  10511  elfz0fzfz0  10533  fz0fzelfz0  10534  fznn0sub2  10535  fz0fzdiffz0  10537  elfzmlbp  10539  difelfznle  10542  nelfzo  10559  elfzouz2  10569  fzo0n  10575  fzonlt0  10576  fzossrbm1  10582  fzo1fzo0n0  10595  elfzo0z  10596  fzofzim  10600  eluzgtdifelfzo  10615  fzossfzop1  10630  ssfzo12bi  10643  elfzomelpfzo  10649  fzosplitprm1  10653  fzostep1  10656  infssuzex  10666  flid  10719  flqbi2  10726  2tnp1ge0ge0  10736  flhalf  10737  fldiv4p1lem1div2  10740  fldiv4lem1div2uz2  10741  ceiqle  10750  uzsinds  10881  zsqcl2  11054  ssenneg  11280  ccatsymb  11370  ccatval21sw  11373  lswccatn0lsw  11379  swrd0g  11432  swrdswrdlem  11476  swrdswrd  11477  swrdccatin2  11501  pfxccatin12lem2  11503  pfxccatin12lem3  11504  nn0abscl  11851  zmaxcl  11990  2zsupmax  11992  2zinfmin  12009  p1modz1  12561  evennn02n  12649  evennn2n  12650  ltoddhalfle  12660  bitsp1o  12720  dfgcd2  12791  algcvga  12829  isprm3  12896  dvdsnprmd  12903  sqnprm  12914  zgcdsq  12979  hashdvds  12999  fldivp1  13127  zgz  13152  4sqlem4  13171  4sqexercise1  13177  mulgval  13925  coskpi  15949  relogexp  15973  rplogbzexp  16056  zabsle1  16118  lgsne0  16157  gausslemma2dlem1a  16177  gausslemma2dlem3  16182  gausslemma2dlem4  16183  lgsquadlem1  16196  lgsquadlem2  16197  2lgslem1a1  16205  2lgslem1a2  16206  2sqlem2  16234  clwwlkext2edg  16663