Theorem zre 9583

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 9581	. 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 1004   = wceq 1398   e. wcel 2205   RRcr 8128   0cc0 8129   -ucneg 8447   NNcn 9239   ZZcz 9579

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-rab 2531  df-v 2817  df-un 3217  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-iota 5314  df-fv 5362  df-ov 6055  df-neg 8449  df-z 9580

This theorem is referenced by:  zcn  9584  zrei  9585  zssre  9586  elnn0z  9592  elnnz1  9602  peano2z  9615  zaddcl  9619  ztri3or0  9621  ztri3or  9622  zletric  9623  zlelttric  9624  zltnle  9625  zleloe  9626  zletr  9629  znnsub  9631  nzadd  9632  zltp1le  9634  zleltp1  9635  znn0sub  9645  zapne  9654  zdceq  9655  zdcle  9656  zdclt  9657  zltlen  9659  nn0ge0div  9668  zextle  9672  btwnnz  9675  suprzclex  9679  msqznn  9681  peano2uz2  9688  uzind  9692  fzind  9696  fnn0ind  9697  eluzuzle  9865  uzid  9871  uzneg  9876  uz11  9880  eluzp1m1  9881  eluzp1p1  9883  eluzaddi  9884  eluzsubi  9885  uzin  9890  uz3m2nn  9908  peano2uz  9918  nn0pzuz  9922  eluz2b2  9938  uz2mulcl  9943  eqreznegel  9949  lbzbi  9951  qre  9960  elpq  9984  zltaddlt1le  10344  elfz1eq  10372  fznlem  10378  fzen  10380  uzsubsubfz  10384  fzaddel  10396  fzsuc2  10417  fzp1disj  10418  fzrev  10422  elfz1b  10428  fzneuz  10439  fzp1nel  10442  elfz0fzfz0  10464  fz0fzelfz0  10465  fznn0sub2  10466  fz0fzdiffz0  10468  elfzmlbp  10470  difelfznle  10473  nelfzo  10490  elfzouz2  10500  fzo0n  10506  fzonlt0  10507  fzossrbm1  10513  fzo1fzo0n0  10526  elfzo0z  10527  fzofzim  10531  eluzgtdifelfzo  10546  fzossfzop1  10561  ssfzo12bi  10574  elfzomelpfzo  10580  fzosplitprm1  10584  fzostep1  10587  infssuzex  10597  flid  10648  flqbi2  10655  2tnp1ge0ge0  10665  flhalf  10666  fldiv4p1lem1div2  10669  fldiv4lem1div2uz2  10670  ceiqle  10679  uzsinds  10810  zsqcl2  10983  ssenneg  11208  ccatsymb  11294  ccatval21sw  11297  lswccatn0lsw  11303  swrd0g  11356  swrdswrdlem  11400  swrdswrd  11401  swrdccatin2  11425  pfxccatin12lem2  11427  pfxccatin12lem3  11428  nn0abscl  11774  zmaxcl  11913  2zsupmax  11915  2zinfmin  11932  p1modz1  12484  evennn02n  12572  evennn2n  12573  ltoddhalfle  12583  bitsp1o  12643  dfgcd2  12714  algcvga  12752  isprm3  12819  dvdsnprmd  12826  sqnprm  12837  zgcdsq  12902  hashdvds  12922  fldivp1  13050  zgz  13075  4sqlem4  13094  4sqexercise1  13100  mulgval  13856  coskpi  15730  relogexp  15754  rplogbzexp  15836  zabsle1  15889  lgsne0  15928  gausslemma2dlem1a  15948  gausslemma2dlem3  15953  gausslemma2dlem4  15954  lgsquadlem1  15967  lgsquadlem2  15968  2lgslem1a1  15976  2lgslem1a2  15977  2sqlem2  16005  clwwlkext2edg  16434