Theorem zre 9259

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 9257	. 2 |- ( N e. ZZ <-> ( N e. RR /\ ( N = 0 \/ N e. NN \/ -u N e. NN ) ) )
2	1	simplbi 274	1 |- ( N e. ZZ -> N e. RR )

Syntax hints:   -> wi 4   \/ w3o 977   = wceq 1353   e. wcel 2148   RRcr 7812   0cc0 7813   -ucneg 8131   NNcn 8921   ZZcz 9255

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 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-iota 5180  df-fv 5226  df-ov 5880  df-neg 8133  df-z 9256

This theorem is referenced by:  zcn  9260  zrei  9261  zssre  9262  elnn0z  9268  elnnz1  9278  peano2z  9291  zaddcl  9295  ztri3or0  9297  ztri3or  9298  zletric  9299  zlelttric  9300  zltnle  9301  zleloe  9302  zletr  9304  znnsub  9306  nzadd  9307  zltp1le  9309  zleltp1  9310  znn0sub  9320  zapne  9329  zdceq  9330  zdcle  9331  zdclt  9332  zltlen  9333  nn0ge0div  9342  zextle  9346  btwnnz  9349  suprzclex  9353  msqznn  9355  peano2uz2  9362  uzind  9366  fzind  9370  fnn0ind  9371  eluzuzle  9538  uzid  9544  uzneg  9548  uz11  9552  eluzp1m1  9553  eluzp1p1  9555  eluzaddi  9556  eluzsubi  9557  uzin  9562  uz3m2nn  9575  peano2uz  9585  nn0pzuz  9589  eluz2b2  9605  uz2mulcl  9610  eqreznegel  9616  lbzbi  9618  qre  9627  elpq  9650  zltaddlt1le  10009  elfz1eq  10037  fznlem  10043  fzen  10045  uzsubsubfz  10049  fzaddel  10061  fzsuc2  10081  fzp1disj  10082  fzrev  10086  elfz1b  10092  fzneuz  10103  fzp1nel  10106  elfz0fzfz0  10128  fz0fzelfz0  10129  fznn0sub2  10130  fz0fzdiffz0  10132  elfzmlbp  10134  difelfznle  10137  elfzouz2  10163  fzonlt0  10169  fzossrbm1  10175  fzo1fzo0n0  10185  elfzo0z  10186  fzofzim  10190  eluzgtdifelfzo  10199  fzossfzop1  10214  ssfzo12bi  10227  elfzomelpfzo  10233  fzosplitprm1  10236  fzostep1  10239  flid  10286  flqbi2  10293  2tnp1ge0ge0  10303  flhalf  10304  fldiv4p1lem1div2  10307  ceiqle  10315  uzsinds  10444  zsqcl2  10600  nn0abscl  11096  zmaxcl  11235  2zsupmax  11236  2zinfmin  11253  p1modz1  11803  evennn02n  11889  evennn2n  11890  ltoddhalfle  11900  infssuzex  11952  dfgcd2  12017  algcvga  12053  isprm3  12120  dvdsnprmd  12127  sqnprm  12138  zgcdsq  12203  hashdvds  12223  fldivp1  12348  zgz  12373  4sqlem4  12392  mulgval  12991  coskpi  14308  relogexp  14332  rplogbzexp  14411  zabsle1  14439  lgsne0  14478  2sqlem2  14501