Theorem zre 8956

Description: An integer is a real. (Contributed by NM, 8-Jan-2002.)

Assertion

Ref	Expression
zre	|- ( N e. ZZ -> N e. RR )

Proof of Theorem zre

Step	Hyp	Ref	Expression
1		elz 8954	. 2 |- ( N e. ZZ <-> ( N e. RR /\ ( N = 0 \/ N e. NN \/ -u N e. NN ) ) )
2	1	simplbi 270	1 |- ( N e. ZZ -> N e. RR )

Syntax hints:   -> wi 4   \/ w3o 942   = wceq 1312   e. wcel 1461   RRcr 7540   0cc0 7541   -ucneg 7851   NNcn 8624   ZZcz 8952

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-3or 944  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-rex 2394  df-rab 2397  df-v 2657  df-un 3039  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-br 3894  df-iota 5044  df-fv 5087  df-ov 5729  df-neg 7853  df-z 8953

This theorem is referenced by:  zcn  8957  zrei  8958  zssre  8959  elnn0z  8965  elnnz1  8975  peano2z  8988  zaddcl  8992  ztri3or0  8994  ztri3or  8995  zletric  8996  zlelttric  8997  zltnle  8998  zleloe  8999  zletr  9001  znnsub  9003  nzadd  9004  zltp1le  9006  zleltp1  9007  znn0sub  9017  zapne  9023  zdceq  9024  zdcle  9025  zdclt  9026  zltlen  9027  nn0ge0div  9036  zextle  9040  btwnnz  9043  suprzclex  9047  msqznn  9049  peano2uz2  9056  uzind  9060  fzind  9064  fnn0ind  9065  eluzuzle  9230  uzid  9236  uzneg  9240  uz11  9244  eluzp1m1  9245  eluzp1p1  9247  eluzaddi  9248  eluzsubi  9249  uzin  9254  uz3m2nn  9264  peano2uz  9274  nn0pzuz  9278  eluz2b2  9293  uz2mulcl  9298  eqreznegel  9302  lbzbi  9304  qre  9313  zltaddlt1le  9676  elfz1eq  9702  fznlem  9708  fzen  9710  uzsubsubfz  9714  fzaddel  9726  fzsuc2  9746  fzp1disj  9747  fzrev  9751  elfz1b  9757  fzneuz  9768  fzp1nel  9771  elfz0fzfz0  9790  fz0fzelfz0  9791  fznn0sub2  9792  fz0fzdiffz0  9794  elfzmlbp  9796  difelfznle  9799  elfzouz2  9825  fzonlt0  9831  fzossrbm1  9837  fzo1fzo0n0  9847  elfzo0z  9848  fzofzim  9852  eluzgtdifelfzo  9861  fzossfzop1  9876  ssfzo12bi  9889  elfzomelpfzo  9895  fzosplitprm1  9898  fzostep1  9901  flid  9944  flqbi2  9951  2tnp1ge0ge0  9961  flhalf  9962  fldiv4p1lem1div2  9965  ceiqle  9973  uzsinds  10102  zsqcl2  10257  nn0abscl  10743  zmaxcl  10882  2zsupmax  10883  evennn02n  11421  evennn2n  11422  ltoddhalfle  11432  infssuzex  11484  dfgcd2  11542  algcvga  11572  isprm3  11639  dvdsnprmd  11646  sqnprm  11656  zgcdsq  11718  hashdvds  11736