Theorem zre 9375

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

Syntax hints:   → wi 4   ∨ w3o 979   = wceq 1372   ∈ wcel 2175  ℝcr 7923  0cc0 7924  -cneg 8243  ℕcn 9035  ℤcz 9371

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rex 2489  df-rab 2492  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-iota 5231  df-fv 5278  df-ov 5946  df-neg 8245  df-z 9372

This theorem is referenced by:  zcn  9376  zrei  9377  zssre  9378  elnn0z  9384  elnnz1  9394  peano2z  9407  zaddcl  9411  ztri3or0  9413  ztri3or  9414  zletric  9415  zlelttric  9416  zltnle  9417  zleloe  9418  zletr  9421  znnsub  9423  nzadd  9424  zltp1le  9426  zleltp1  9427  znn0sub  9437  zapne  9446  zdceq  9447  zdcle  9448  zdclt  9449  zltlen  9450  nn0ge0div  9459  zextle  9463  btwnnz  9466  suprzclex  9470  msqznn  9472  peano2uz2  9479  uzind  9483  fzind  9487  fnn0ind  9488  eluzuzle  9655  uzid  9661  uzneg  9666  uz11  9670  eluzp1m1  9671  eluzp1p1  9673  eluzaddi  9674  eluzsubi  9675  uzin  9680  uz3m2nn  9693  peano2uz  9703  nn0pzuz  9707  eluz2b2  9723  uz2mulcl  9728  eqreznegel  9734  lbzbi  9736  qre  9745  elpq  9769  zltaddlt1le  10128  elfz1eq  10156  fznlem  10162  fzen  10164  uzsubsubfz  10168  fzaddel  10180  fzsuc2  10200  fzp1disj  10201  fzrev  10205  elfz1b  10211  fzneuz  10222  fzp1nel  10225  elfz0fzfz0  10247  fz0fzelfz0  10248  fznn0sub2  10249  fz0fzdiffz0  10251  elfzmlbp  10253  difelfznle  10256  nelfzo  10273  elfzouz2  10283  fzonlt0  10289  fzossrbm1  10295  fzo1fzo0n0  10305  elfzo0z  10306  fzofzim  10310  eluzgtdifelfzo  10324  fzossfzop1  10339  ssfzo12bi  10352  elfzomelpfzo  10358  fzosplitprm1  10361  fzostep1  10364  infssuzex  10374  flid  10425  flqbi2  10432  2tnp1ge0ge0  10442  flhalf  10443  fldiv4p1lem1div2  10446  fldiv4lem1div2uz2  10447  ceiqle  10456  uzsinds  10587  zsqcl2  10760  ccatsymb  11056  ccatval21sw  11059  lswccatn0lsw  11065  nn0abscl  11338  zmaxcl  11477  2zsupmax  11479  2zinfmin  11496  p1modz1  12047  evennn02n  12135  evennn2n  12136  ltoddhalfle  12146  bitsp1o  12206  dfgcd2  12277  algcvga  12315  isprm3  12382  dvdsnprmd  12389  sqnprm  12400  zgcdsq  12465  hashdvds  12485  fldivp1  12613  zgz  12638  4sqlem4  12657  4sqexercise1  12663  mulgval  13400  coskpi  15262  relogexp  15286  rplogbzexp  15368  zabsle1  15418  lgsne0  15457  gausslemma2dlem1a  15477  gausslemma2dlem3  15482  gausslemma2dlem4  15483  lgsquadlem1  15496  lgsquadlem2  15497  2lgslem1a1  15505  2lgslem1a2  15506  2sqlem2  15534