Theorem zre 9256

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

Syntax hints:   → wi 4   ∨ w3o 977   = wceq 1353   ∈ wcel 2148  ℝcr 7809  0cc0 7810  -cneg 8128  ℕcn 8918  ℤcz 9252

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 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877  df-neg 8130  df-z 9253

This theorem is referenced by:  zcn  9257  zrei  9258  zssre  9259  elnn0z  9265  elnnz1  9275  peano2z  9288  zaddcl  9292  ztri3or0  9294  ztri3or  9295  zletric  9296  zlelttric  9297  zltnle  9298  zleloe  9299  zletr  9301  znnsub  9303  nzadd  9304  zltp1le  9306  zleltp1  9307  znn0sub  9317  zapne  9326  zdceq  9327  zdcle  9328  zdclt  9329  zltlen  9330  nn0ge0div  9339  zextle  9343  btwnnz  9346  suprzclex  9350  msqznn  9352  peano2uz2  9359  uzind  9363  fzind  9367  fnn0ind  9368  eluzuzle  9535  uzid  9541  uzneg  9545  uz11  9549  eluzp1m1  9550  eluzp1p1  9552  eluzaddi  9553  eluzsubi  9554  uzin  9559  uz3m2nn  9572  peano2uz  9582  nn0pzuz  9586  eluz2b2  9602  uz2mulcl  9607  eqreznegel  9613  lbzbi  9615  qre  9624  elpq  9647  zltaddlt1le  10006  elfz1eq  10034  fznlem  10040  fzen  10042  uzsubsubfz  10046  fzaddel  10058  fzsuc2  10078  fzp1disj  10079  fzrev  10083  elfz1b  10089  fzneuz  10100  fzp1nel  10103  elfz0fzfz0  10125  fz0fzelfz0  10126  fznn0sub2  10127  fz0fzdiffz0  10129  elfzmlbp  10131  difelfznle  10134  elfzouz2  10160  fzonlt0  10166  fzossrbm1  10172  fzo1fzo0n0  10182  elfzo0z  10183  fzofzim  10187  eluzgtdifelfzo  10196  fzossfzop1  10211  ssfzo12bi  10224  elfzomelpfzo  10230  fzosplitprm1  10233  fzostep1  10236  flid  10283  flqbi2  10290  2tnp1ge0ge0  10300  flhalf  10301  fldiv4p1lem1div2  10304  ceiqle  10312  uzsinds  10441  zsqcl2  10597  nn0abscl  11093  zmaxcl  11232  2zsupmax  11233  2zinfmin  11250  p1modz1  11800  evennn02n  11886  evennn2n  11887  ltoddhalfle  11897  infssuzex  11949  dfgcd2  12014  algcvga  12050  isprm3  12117  dvdsnprmd  12124  sqnprm  12135  zgcdsq  12200  hashdvds  12220  fldivp1  12345  zgz  12370  4sqlem4  12389  mulgval  12985  coskpi  14239  relogexp  14263  rplogbzexp  14342  zabsle1  14370  lgsne0  14409  2sqlem2  14432