Theorem zre 9473

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

Syntax hints:   → wi 4   ∨ w3o 1001   = wceq 1395   ∈ wcel 2200  ℝcr 8021  0cc0 8022  -cneg 8341  ℕcn 9133  ℤcz 9469

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 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016  df-neg 8343  df-z 9470

This theorem is referenced by:  zcn  9474  zrei  9475  zssre  9476  elnn0z  9482  elnnz1  9492  peano2z  9505  zaddcl  9509  ztri3or0  9511  ztri3or  9512  zletric  9513  zlelttric  9514  zltnle  9515  zleloe  9516  zletr  9519  znnsub  9521  nzadd  9522  zltp1le  9524  zleltp1  9525  znn0sub  9535  zapne  9544  zdceq  9545  zdcle  9546  zdclt  9547  zltlen  9548  nn0ge0div  9557  zextle  9561  btwnnz  9564  suprzclex  9568  msqznn  9570  peano2uz2  9577  uzind  9581  fzind  9585  fnn0ind  9586  eluzuzle  9754  uzid  9760  uzneg  9765  uz11  9769  eluzp1m1  9770  eluzp1p1  9772  eluzaddi  9773  eluzsubi  9774  uzin  9779  uz3m2nn  9797  peano2uz  9807  nn0pzuz  9811  eluz2b2  9827  uz2mulcl  9832  eqreznegel  9838  lbzbi  9840  qre  9849  elpq  9873  zltaddlt1le  10232  elfz1eq  10260  fznlem  10266  fzen  10268  uzsubsubfz  10272  fzaddel  10284  fzsuc2  10304  fzp1disj  10305  fzrev  10309  elfz1b  10315  fzneuz  10326  fzp1nel  10329  elfz0fzfz0  10351  fz0fzelfz0  10352  fznn0sub2  10353  fz0fzdiffz0  10355  elfzmlbp  10357  difelfznle  10360  nelfzo  10377  elfzouz2  10387  fzo0n  10393  fzonlt0  10394  fzossrbm1  10400  fzo1fzo0n0  10412  elfzo0z  10413  fzofzim  10417  eluzgtdifelfzo  10432  fzossfzop1  10447  ssfzo12bi  10460  elfzomelpfzo  10466  fzosplitprm1  10470  fzostep1  10473  infssuzex  10483  flid  10534  flqbi2  10541  2tnp1ge0ge0  10551  flhalf  10552  fldiv4p1lem1div2  10555  fldiv4lem1div2uz2  10556  ceiqle  10565  uzsinds  10696  zsqcl2  10869  ccatsymb  11169  ccatval21sw  11172  lswccatn0lsw  11178  swrd0g  11231  swrdswrdlem  11275  swrdswrd  11276  swrdccatin2  11300  pfxccatin12lem2  11302  pfxccatin12lem3  11303  nn0abscl  11636  zmaxcl  11775  2zsupmax  11777  2zinfmin  11794  p1modz1  12345  evennn02n  12433  evennn2n  12434  ltoddhalfle  12444  bitsp1o  12504  dfgcd2  12575  algcvga  12613  isprm3  12680  dvdsnprmd  12687  sqnprm  12698  zgcdsq  12763  hashdvds  12783  fldivp1  12911  zgz  12936  4sqlem4  12955  4sqexercise1  12961  mulgval  13699  coskpi  15562  relogexp  15586  rplogbzexp  15668  zabsle1  15718  lgsne0  15757  gausslemma2dlem1a  15777  gausslemma2dlem3  15782  gausslemma2dlem4  15783  lgsquadlem1  15796  lgsquadlem2  15797  2lgslem1a1  15805  2lgslem1a2  15806  2sqlem2  15834  clwwlkext2edg  16217