Theorem zre 9378

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 9376	. 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 980   = wceq 1373   e. wcel 2176   RRcr 7926   0cc0 7927   -ucneg 8246   NNcn 9038   ZZcz 9374

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-rab 2493  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4046  df-iota 5233  df-fv 5280  df-ov 5949  df-neg 8248  df-z 9375

This theorem is referenced by:  zcn  9379  zrei  9380  zssre  9381  elnn0z  9387  elnnz1  9397  peano2z  9410  zaddcl  9414  ztri3or0  9416  ztri3or  9417  zletric  9418  zlelttric  9419  zltnle  9420  zleloe  9421  zletr  9424  znnsub  9426  nzadd  9427  zltp1le  9429  zleltp1  9430  znn0sub  9440  zapne  9449  zdceq  9450  zdcle  9451  zdclt  9452  zltlen  9453  nn0ge0div  9462  zextle  9466  btwnnz  9469  suprzclex  9473  msqznn  9475  peano2uz2  9482  uzind  9486  fzind  9490  fnn0ind  9491  eluzuzle  9658  uzid  9664  uzneg  9669  uz11  9673  eluzp1m1  9674  eluzp1p1  9676  eluzaddi  9677  eluzsubi  9678  uzin  9683  uz3m2nn  9696  peano2uz  9706  nn0pzuz  9710  eluz2b2  9726  uz2mulcl  9731  eqreznegel  9737  lbzbi  9739  qre  9748  elpq  9772  zltaddlt1le  10131  elfz1eq  10159  fznlem  10165  fzen  10167  uzsubsubfz  10171  fzaddel  10183  fzsuc2  10203  fzp1disj  10204  fzrev  10208  elfz1b  10214  fzneuz  10225  fzp1nel  10228  elfz0fzfz0  10250  fz0fzelfz0  10251  fznn0sub2  10252  fz0fzdiffz0  10254  elfzmlbp  10256  difelfznle  10259  nelfzo  10276  elfzouz2  10286  fzo0n  10292  fzonlt0  10293  fzossrbm1  10299  fzo1fzo0n0  10309  elfzo0z  10310  fzofzim  10314  eluzgtdifelfzo  10328  fzossfzop1  10343  ssfzo12bi  10356  elfzomelpfzo  10362  fzosplitprm1  10365  fzostep1  10368  infssuzex  10378  flid  10429  flqbi2  10436  2tnp1ge0ge0  10446  flhalf  10447  fldiv4p1lem1div2  10450  fldiv4lem1div2uz2  10451  ceiqle  10460  uzsinds  10591  zsqcl2  10764  ccatsymb  11061  ccatval21sw  11064  lswccatn0lsw  11070  swrd0g  11116  nn0abscl  11429  zmaxcl  11568  2zsupmax  11570  2zinfmin  11587  p1modz1  12138  evennn02n  12226  evennn2n  12227  ltoddhalfle  12237  bitsp1o  12297  dfgcd2  12368  algcvga  12406  isprm3  12473  dvdsnprmd  12480  sqnprm  12491  zgcdsq  12556  hashdvds  12576  fldivp1  12704  zgz  12729  4sqlem4  12748  4sqexercise1  12754  mulgval  13491  coskpi  15353  relogexp  15377  rplogbzexp  15459  zabsle1  15509  lgsne0  15548  gausslemma2dlem1a  15568  gausslemma2dlem3  15573  gausslemma2dlem4  15574  lgsquadlem1  15587  lgsquadlem2  15588  2lgslem1a1  15596  2lgslem1a2  15597  2sqlem2  15625