Theorem zre 9527

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

Syntax hints:   → wi 4   ∨ w3o 1004   = wceq 1398   ∈ wcel 2202  ℝcr 8074  0cc0 8075  -cneg 8393  ℕcn 9185  ℤcz 9523

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-rab 2520  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031  df-neg 8395  df-z 9524

This theorem is referenced by:  zcn  9528  zrei  9529  zssre  9530  elnn0z  9536  elnnz1  9546  peano2z  9559  zaddcl  9563  ztri3or0  9565  ztri3or  9566  zletric  9567  zlelttric  9568  zltnle  9569  zleloe  9570  zletr  9573  znnsub  9575  nzadd  9576  zltp1le  9578  zleltp1  9579  znn0sub  9589  zapne  9598  zdceq  9599  zdcle  9600  zdclt  9601  zltlen  9602  nn0ge0div  9611  zextle  9615  btwnnz  9618  suprzclex  9622  msqznn  9624  peano2uz2  9631  uzind  9635  fzind  9639  fnn0ind  9640  eluzuzle  9808  uzid  9814  uzneg  9819  uz11  9823  eluzp1m1  9824  eluzp1p1  9826  eluzaddi  9827  eluzsubi  9828  uzin  9833  uz3m2nn  9851  peano2uz  9861  nn0pzuz  9865  eluz2b2  9881  uz2mulcl  9886  eqreznegel  9892  lbzbi  9894  qre  9903  elpq  9927  zltaddlt1le  10287  elfz1eq  10315  fznlem  10321  fzen  10323  uzsubsubfz  10327  fzaddel  10339  fzsuc2  10359  fzp1disj  10360  fzrev  10364  elfz1b  10370  fzneuz  10381  fzp1nel  10384  elfz0fzfz0  10406  fz0fzelfz0  10407  fznn0sub2  10408  fz0fzdiffz0  10410  elfzmlbp  10412  difelfznle  10415  nelfzo  10432  elfzouz2  10442  fzo0n  10448  fzonlt0  10449  fzossrbm1  10455  fzo1fzo0n0  10468  elfzo0z  10469  fzofzim  10473  eluzgtdifelfzo  10488  fzossfzop1  10503  ssfzo12bi  10516  elfzomelpfzo  10522  fzosplitprm1  10526  fzostep1  10529  infssuzex  10539  flid  10590  flqbi2  10597  2tnp1ge0ge0  10607  flhalf  10608  fldiv4p1lem1div2  10611  fldiv4lem1div2uz2  10612  ceiqle  10621  uzsinds  10752  zsqcl2  10925  ccatsymb  11228  ccatval21sw  11231  lswccatn0lsw  11237  swrd0g  11290  swrdswrdlem  11334  swrdswrd  11335  swrdccatin2  11359  pfxccatin12lem2  11361  pfxccatin12lem3  11362  nn0abscl  11708  zmaxcl  11847  2zsupmax  11849  2zinfmin  11866  p1modz1  12418  evennn02n  12506  evennn2n  12507  ltoddhalfle  12517  bitsp1o  12577  dfgcd2  12648  algcvga  12686  isprm3  12753  dvdsnprmd  12760  sqnprm  12771  zgcdsq  12836  hashdvds  12856  fldivp1  12984  zgz  13009  4sqlem4  13028  4sqexercise1  13034  mulgval  13772  coskpi  15642  relogexp  15666  rplogbzexp  15748  zabsle1  15801  lgsne0  15840  gausslemma2dlem1a  15860  gausslemma2dlem3  15865  gausslemma2dlem4  15866  lgsquadlem1  15879  lgsquadlem2  15880  2lgslem1a1  15888  2lgslem1a2  15889  2sqlem2  15917  clwwlkext2edg  16346