Theorem zre 9330

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 9328	. 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 979   = wceq 1364   e. wcel 2167   RRcr 7878   0cc0 7879   -ucneg 8198   NNcn 8990   ZZcz 9326

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-rab 2484  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-iota 5219  df-fv 5266  df-ov 5925  df-neg 8200  df-z 9327

This theorem is referenced by:  zcn  9331  zrei  9332  zssre  9333  elnn0z  9339  elnnz1  9349  peano2z  9362  zaddcl  9366  ztri3or0  9368  ztri3or  9369  zletric  9370  zlelttric  9371  zltnle  9372  zleloe  9373  zletr  9375  znnsub  9377  nzadd  9378  zltp1le  9380  zleltp1  9381  znn0sub  9391  zapne  9400  zdceq  9401  zdcle  9402  zdclt  9403  zltlen  9404  nn0ge0div  9413  zextle  9417  btwnnz  9420  suprzclex  9424  msqznn  9426  peano2uz2  9433  uzind  9437  fzind  9441  fnn0ind  9442  eluzuzle  9609  uzid  9615  uzneg  9620  uz11  9624  eluzp1m1  9625  eluzp1p1  9627  eluzaddi  9628  eluzsubi  9629  uzin  9634  uz3m2nn  9647  peano2uz  9657  nn0pzuz  9661  eluz2b2  9677  uz2mulcl  9682  eqreznegel  9688  lbzbi  9690  qre  9699  elpq  9723  zltaddlt1le  10082  elfz1eq  10110  fznlem  10116  fzen  10118  uzsubsubfz  10122  fzaddel  10134  fzsuc2  10154  fzp1disj  10155  fzrev  10159  elfz1b  10165  fzneuz  10176  fzp1nel  10179  elfz0fzfz0  10201  fz0fzelfz0  10202  fznn0sub2  10203  fz0fzdiffz0  10205  elfzmlbp  10207  difelfznle  10210  nelfzo  10227  elfzouz2  10237  fzonlt0  10243  fzossrbm1  10249  fzo1fzo0n0  10259  elfzo0z  10260  fzofzim  10264  eluzgtdifelfzo  10273  fzossfzop1  10288  ssfzo12bi  10301  elfzomelpfzo  10307  fzosplitprm1  10310  fzostep1  10313  infssuzex  10323  flid  10374  flqbi2  10381  2tnp1ge0ge0  10391  flhalf  10392  fldiv4p1lem1div2  10395  fldiv4lem1div2uz2  10396  ceiqle  10405  uzsinds  10536  zsqcl2  10709  nn0abscl  11250  zmaxcl  11389  2zsupmax  11391  2zinfmin  11408  p1modz1  11959  evennn02n  12047  evennn2n  12048  ltoddhalfle  12058  bitsp1o  12117  dfgcd2  12181  algcvga  12219  isprm3  12286  dvdsnprmd  12293  sqnprm  12304  zgcdsq  12369  hashdvds  12389  fldivp1  12517  zgz  12542  4sqlem4  12561  4sqexercise1  12567  mulgval  13252  coskpi  15084  relogexp  15108  rplogbzexp  15190  zabsle1  15240  lgsne0  15279  gausslemma2dlem1a  15299  gausslemma2dlem3  15304  gausslemma2dlem4  15305  lgsquadlem1  15318  lgsquadlem2  15319  2lgslem1a1  15327  2lgslem1a2  15328  2sqlem2  15356