Theorem zre 9257

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

Syntax hints:   → wi 4   ∨ w3o 977   = wceq 1353   ∈ wcel 2148  ℝcr 7810  0cc0 7811  -cneg 8129  ℕcn 8919  ℤcz 9253

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-rab 2464  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225  df-ov 5878  df-neg 8131  df-z 9254

This theorem is referenced by:  zcn  9258  zrei  9259  zssre  9260  elnn0z  9266  elnnz1  9276  peano2z  9289  zaddcl  9293  ztri3or0  9295  ztri3or  9296  zletric  9297  zlelttric  9298  zltnle  9299  zleloe  9300  zletr  9302  znnsub  9304  nzadd  9305  zltp1le  9307  zleltp1  9308  znn0sub  9318  zapne  9327  zdceq  9328  zdcle  9329  zdclt  9330  zltlen  9331  nn0ge0div  9340  zextle  9344  btwnnz  9347  suprzclex  9351  msqznn  9353  peano2uz2  9360  uzind  9364  fzind  9368  fnn0ind  9369  eluzuzle  9536  uzid  9542  uzneg  9546  uz11  9550  eluzp1m1  9551  eluzp1p1  9553  eluzaddi  9554  eluzsubi  9555  uzin  9560  uz3m2nn  9573  peano2uz  9583  nn0pzuz  9587  eluz2b2  9603  uz2mulcl  9608  eqreznegel  9614  lbzbi  9616  qre  9625  elpq  9648  zltaddlt1le  10007  elfz1eq  10035  fznlem  10041  fzen  10043  uzsubsubfz  10047  fzaddel  10059  fzsuc2  10079  fzp1disj  10080  fzrev  10084  elfz1b  10090  fzneuz  10101  fzp1nel  10104  elfz0fzfz0  10126  fz0fzelfz0  10127  fznn0sub2  10128  fz0fzdiffz0  10130  elfzmlbp  10132  difelfznle  10135  elfzouz2  10161  fzonlt0  10167  fzossrbm1  10173  fzo1fzo0n0  10183  elfzo0z  10184  fzofzim  10188  eluzgtdifelfzo  10197  fzossfzop1  10212  ssfzo12bi  10225  elfzomelpfzo  10231  fzosplitprm1  10234  fzostep1  10237  flid  10284  flqbi2  10291  2tnp1ge0ge0  10301  flhalf  10302  fldiv4p1lem1div2  10305  ceiqle  10313  uzsinds  10442  zsqcl2  10598  nn0abscl  11094  zmaxcl  11233  2zsupmax  11234  2zinfmin  11251  p1modz1  11801  evennn02n  11887  evennn2n  11888  ltoddhalfle  11898  infssuzex  11950  dfgcd2  12015  algcvga  12051  isprm3  12118  dvdsnprmd  12125  sqnprm  12136  zgcdsq  12201  hashdvds  12221  fldivp1  12346  zgz  12371  4sqlem4  12390  mulgval  12986  coskpi  14272  relogexp  14296  rplogbzexp  14375  zabsle1  14403  lgsne0  14442  2sqlem2  14465