Theorem zre 9653

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 9651	. 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 )

This proof depends on syntax axioms:   -> wi 4   \/ w3o 1008   = wceq 1402   e. wcel 2209   RRcr 8179   0cc0 8180   -ucneg 8500   NNcn 9307   ZZcz 9649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-rab 2537  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088  df-neg 8502  df-z 9650

This theorem is used by:  zcn  9654  zrei  9655  zssre  9656  elnn0z  9662  elnnz1  9672  peano2z  9685  zaddcl  9689  ztri3or0  9691  ztri3or  9692  zletric  9693  zlelttric  9694  zltnle  9695  zleloe  9696  zletr  9699  znnsub  9701  nzadd  9702  zltp1le  9704  zleltp1  9705  znn0sub  9715  zapne  9724  zdceq  9725  zdcle  9726  zdclt  9727  zltlen  9729  nn0ge0div  9738  zextle  9742  btwnnz  9745  suprzclex  9749  msqznn  9751  peano2uz2  9758  uzind  9762  fzind  9766  fnn0ind  9767  eluzuzle  9940  uzid  9946  uzneg  9951  uz11  9955  eluzp1m1  9956  eluzp1p1  9958  eluzaddi  9959  eluzsubi  9960  uzin  9965  uz3m2nn  9983  peano2uz  9993  nn0pzuz  9997  eluz2b2  10013  uz2mulcl  10018  eqreznegel  10024  lbzbi  10026  qre  10035  elpq  10060  zltaddlt1le  10421  elfz1eq  10450  fznlem  10456  fzen  10458  uzsubsubfz  10463  fzaddel  10476  fzsuc2  10497  fzp1disj  10498  fzrev  10502  elfz1b  10508  fzneuz  10519  fzp1nel  10522  elfz0fzfz0  10544  fz0fzelfz0  10545  fznn0sub2  10546  fz0fzdiffz0  10548  elfzmlbp  10550  difelfznle  10553  nelfzo  10570  elfzouz2  10580  fzo0n  10586  fzonlt0  10587  fzossrbm1  10593  fzo1fzo0n0  10606  elfzo0z  10607  fzofzim  10611  eluzgtdifelfzo  10626  fzossfzop1  10641  ssfzo12bi  10654  elfzomelpfzo  10660  fzosplitprm1  10664  fzostep1  10667  infssuzex  10677  flid  10734  flqbi2  10741  2tnp1ge0ge0  10751  flhalf  10752  fldiv4p1lem1div2  10755  fldiv4lem1div2uz2  10756  ceiqle  10765  uzsinds  10896  zsqcl2  11069  ssenneg  11296  ccatsymb  11386  ccatval21sw  11389  lswccatn0lsw  11395  swrd0g  11448  swrdswrdlem  11492  swrdswrd  11493  swrdccatin2  11517  pfxccatin12lem2  11519  pfxccatin12lem3  11520  nn0abscl  11868  zmaxcl  12007  2zsupmax  12009  zmincl  12023  2zinfmin  12028  p1modz1  12580  evennn02n  12668  evennn2n  12669  ltoddhalfle  12679  bitsp1o  12739  dfgcd2  12810  algcvga  12848  isprm3  12915  dvdsnprmd  12922  sqnprm  12934  zgcdsq  13000  hashdvds  13022  fldivp1  13150  zgz  13175  4sqlem4  13194  4sqexercise1  13200  mulgval  13978  coskpi  16041  relogexp  16066  rplogbzexp  16151  ppiprm  16220  chtprm  16222  zabsle1  16284  lgsne0  16323  gausslemma2dlem1a  16343  gausslemma2dlem3  16348  gausslemma2dlem4  16349  lgsquadlem1  16362  lgsquadlem2  16363  2lgslem1a1  16371  2lgslem1a2  16372  2sqlem2  16400  clwwlkext2edg  16829