Theorem zre 9630

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 9628	. 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 1008   = wceq 1402   e. wcel 2209   RRcr 8171   0cc0 8172   -ucneg 8491   NNcn 9286   ZZcz 9626

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 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 theorem 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 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-iota 5335  df-fv 5383  df-ov 6081  df-neg 8493  df-z 9627

This theorem is referenced by:  zcn  9631  zrei  9632  zssre  9633  elnn0z  9639  elnnz1  9649  peano2z  9662  zaddcl  9666  ztri3or0  9668  ztri3or  9669  zletric  9670  zlelttric  9671  zltnle  9672  zleloe  9673  zletr  9676  znnsub  9678  nzadd  9679  zltp1le  9681  zleltp1  9682  znn0sub  9692  zapne  9701  zdceq  9702  zdcle  9703  zdclt  9704  zltlen  9706  nn0ge0div  9715  zextle  9719  btwnnz  9722  suprzclex  9726  msqznn  9728  peano2uz2  9735  uzind  9739  fzind  9743  fnn0ind  9744  eluzuzle  9912  uzid  9918  uzneg  9923  uz11  9927  eluzp1m1  9928  eluzp1p1  9930  eluzaddi  9931  eluzsubi  9932  uzin  9937  uz3m2nn  9955  peano2uz  9965  nn0pzuz  9969  eluz2b2  9985  uz2mulcl  9990  eqreznegel  9996  lbzbi  9998  qre  10007  elpq  10031  zltaddlt1le  10392  elfz1eq  10421  fznlem  10427  fzen  10429  uzsubsubfz  10433  fzaddel  10446  fzsuc2  10467  fzp1disj  10468  fzrev  10472  elfz1b  10478  fzneuz  10489  fzp1nel  10492  elfz0fzfz0  10514  fz0fzelfz0  10515  fznn0sub2  10516  fz0fzdiffz0  10518  elfzmlbp  10520  difelfznle  10523  nelfzo  10540  elfzouz2  10550  fzo0n  10556  fzonlt0  10557  fzossrbm1  10563  fzo1fzo0n0  10576  elfzo0z  10577  fzofzim  10581  eluzgtdifelfzo  10596  fzossfzop1  10611  ssfzo12bi  10624  elfzomelpfzo  10630  fzosplitprm1  10634  fzostep1  10637  infssuzex  10647  flid  10700  flqbi2  10707  2tnp1ge0ge0  10717  flhalf  10718  fldiv4p1lem1div2  10721  fldiv4lem1div2uz2  10722  ceiqle  10731  uzsinds  10862  zsqcl2  11035  ssenneg  11261  ccatsymb  11351  ccatval21sw  11354  lswccatn0lsw  11360  swrd0g  11413  swrdswrdlem  11457  swrdswrd  11458  swrdccatin2  11482  pfxccatin12lem2  11484  pfxccatin12lem3  11485  nn0abscl  11832  zmaxcl  11971  2zsupmax  11973  2zinfmin  11990  p1modz1  12542  evennn02n  12630  evennn2n  12631  ltoddhalfle  12641  bitsp1o  12701  dfgcd2  12772  algcvga  12810  isprm3  12877  dvdsnprmd  12884  sqnprm  12895  zgcdsq  12960  hashdvds  12980  fldivp1  13108  zgz  13133  4sqlem4  13152  4sqexercise1  13158  mulgval  13905  coskpi  15875  relogexp  15899  rplogbzexp  15982  zabsle1  16035  lgsne0  16074  gausslemma2dlem1a  16094  gausslemma2dlem3  16099  gausslemma2dlem4  16100  lgsquadlem1  16113  lgsquadlem2  16114  2lgslem1a1  16122  2lgslem1a2  16123  2sqlem2  16151  clwwlkext2edg  16580