Theorem zre 9216

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

Syntax hints:   → wi 4   ∨ w3o 972   = wceq 1348   ∈ wcel 2141  ℝcr 7773  0cc0 7774  -cneg 8091  ℕcn 8878  ℤcz 9212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-rab 2457  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-iota 5160  df-fv 5206  df-ov 5856  df-neg 8093  df-z 9213

This theorem is referenced by:  zcn  9217  zrei  9218  zssre  9219  elnn0z  9225  elnnz1  9235  peano2z  9248  zaddcl  9252  ztri3or0  9254  ztri3or  9255  zletric  9256  zlelttric  9257  zltnle  9258  zleloe  9259  zletr  9261  znnsub  9263  nzadd  9264  zltp1le  9266  zleltp1  9267  znn0sub  9277  zapne  9286  zdceq  9287  zdcle  9288  zdclt  9289  zltlen  9290  nn0ge0div  9299  zextle  9303  btwnnz  9306  suprzclex  9310  msqznn  9312  peano2uz2  9319  uzind  9323  fzind  9327  fnn0ind  9328  eluzuzle  9495  uzid  9501  uzneg  9505  uz11  9509  eluzp1m1  9510  eluzp1p1  9512  eluzaddi  9513  eluzsubi  9514  uzin  9519  uz3m2nn  9532  peano2uz  9542  nn0pzuz  9546  eluz2b2  9562  uz2mulcl  9567  eqreznegel  9573  lbzbi  9575  qre  9584  elpq  9607  zltaddlt1le  9964  elfz1eq  9991  fznlem  9997  fzen  9999  uzsubsubfz  10003  fzaddel  10015  fzsuc2  10035  fzp1disj  10036  fzrev  10040  elfz1b  10046  fzneuz  10057  fzp1nel  10060  elfz0fzfz0  10082  fz0fzelfz0  10083  fznn0sub2  10084  fz0fzdiffz0  10086  elfzmlbp  10088  difelfznle  10091  elfzouz2  10117  fzonlt0  10123  fzossrbm1  10129  fzo1fzo0n0  10139  elfzo0z  10140  fzofzim  10144  eluzgtdifelfzo  10153  fzossfzop1  10168  ssfzo12bi  10181  elfzomelpfzo  10187  fzosplitprm1  10190  fzostep1  10193  flid  10240  flqbi2  10247  2tnp1ge0ge0  10257  flhalf  10258  fldiv4p1lem1div2  10261  ceiqle  10269  uzsinds  10398  zsqcl2  10553  nn0abscl  11049  zmaxcl  11188  2zsupmax  11189  2zinfmin  11206  p1modz1  11756  evennn02n  11841  evennn2n  11842  ltoddhalfle  11852  infssuzex  11904  dfgcd2  11969  algcvga  12005  isprm3  12072  dvdsnprmd  12079  sqnprm  12090  zgcdsq  12155  hashdvds  12175  fldivp1  12300  zgz  12325  4sqlem4  12344  coskpi  13563  relogexp  13587  rplogbzexp  13666  zabsle1  13694  lgsne0  13733  2sqlem2  13745