Theorem zre 9446

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

Syntax hints:   → wi 4   ∨ w3o 1001   = wceq 1395   ∈ wcel 2200  ℝcr 7994  0cc0 7995  -cneg 8314  ℕcn 9106  ℤcz 9442

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-rab 2517  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-br 4083  df-iota 5277  df-fv 5325  df-ov 6003  df-neg 8316  df-z 9443

This theorem is referenced by:  zcn  9447  zrei  9448  zssre  9449  elnn0z  9455  elnnz1  9465  peano2z  9478  zaddcl  9482  ztri3or0  9484  ztri3or  9485  zletric  9486  zlelttric  9487  zltnle  9488  zleloe  9489  zletr  9492  znnsub  9494  nzadd  9495  zltp1le  9497  zleltp1  9498  znn0sub  9508  zapne  9517  zdceq  9518  zdcle  9519  zdclt  9520  zltlen  9521  nn0ge0div  9530  zextle  9534  btwnnz  9537  suprzclex  9541  msqznn  9543  peano2uz2  9550  uzind  9554  fzind  9558  fnn0ind  9559  eluzuzle  9726  uzid  9732  uzneg  9737  uz11  9741  eluzp1m1  9742  eluzp1p1  9744  eluzaddi  9745  eluzsubi  9746  uzin  9751  uz3m2nn  9764  peano2uz  9774  nn0pzuz  9778  eluz2b2  9794  uz2mulcl  9799  eqreznegel  9805  lbzbi  9807  qre  9816  elpq  9840  zltaddlt1le  10199  elfz1eq  10227  fznlem  10233  fzen  10235  uzsubsubfz  10239  fzaddel  10251  fzsuc2  10271  fzp1disj  10272  fzrev  10276  elfz1b  10282  fzneuz  10293  fzp1nel  10296  elfz0fzfz0  10318  fz0fzelfz0  10319  fznn0sub2  10320  fz0fzdiffz0  10322  elfzmlbp  10324  difelfznle  10327  nelfzo  10344  elfzouz2  10354  fzo0n  10360  fzonlt0  10361  fzossrbm1  10367  fzo1fzo0n0  10379  elfzo0z  10380  fzofzim  10384  eluzgtdifelfzo  10398  fzossfzop1  10413  ssfzo12bi  10426  elfzomelpfzo  10432  fzosplitprm1  10435  fzostep1  10438  infssuzex  10448  flid  10499  flqbi2  10506  2tnp1ge0ge0  10516  flhalf  10517  fldiv4p1lem1div2  10520  fldiv4lem1div2uz2  10521  ceiqle  10530  uzsinds  10661  zsqcl2  10834  ccatsymb  11132  ccatval21sw  11135  lswccatn0lsw  11141  swrd0g  11187  swrdswrdlem  11231  swrdswrd  11232  swrdccatin2  11256  pfxccatin12lem2  11258  pfxccatin12lem3  11259  nn0abscl  11591  zmaxcl  11730  2zsupmax  11732  2zinfmin  11749  p1modz1  12300  evennn02n  12388  evennn2n  12389  ltoddhalfle  12399  bitsp1o  12459  dfgcd2  12530  algcvga  12568  isprm3  12635  dvdsnprmd  12642  sqnprm  12653  zgcdsq  12718  hashdvds  12738  fldivp1  12866  zgz  12891  4sqlem4  12910  4sqexercise1  12916  mulgval  13654  coskpi  15516  relogexp  15540  rplogbzexp  15622  zabsle1  15672  lgsne0  15711  gausslemma2dlem1a  15731  gausslemma2dlem3  15736  gausslemma2dlem4  15737  lgsquadlem1  15750  lgsquadlem2  15751  2lgslem1a1  15759  2lgslem1a2  15760  2sqlem2  15788