Theorem zre 9376

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 9374	. 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 7924   0cc0 7925   -ucneg 8244   NNcn 9036   ZZcz 9372

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 4045  df-iota 5232  df-fv 5279  df-ov 5947  df-neg 8246  df-z 9373

This theorem is referenced by:  zcn  9377  zrei  9378  zssre  9379  elnn0z  9385  elnnz1  9395  peano2z  9408  zaddcl  9412  ztri3or0  9414  ztri3or  9415  zletric  9416  zlelttric  9417  zltnle  9418  zleloe  9419  zletr  9422  znnsub  9424  nzadd  9425  zltp1le  9427  zleltp1  9428  znn0sub  9438  zapne  9447  zdceq  9448  zdcle  9449  zdclt  9450  zltlen  9451  nn0ge0div  9460  zextle  9464  btwnnz  9467  suprzclex  9471  msqznn  9473  peano2uz2  9480  uzind  9484  fzind  9488  fnn0ind  9489  eluzuzle  9656  uzid  9662  uzneg  9667  uz11  9671  eluzp1m1  9672  eluzp1p1  9674  eluzaddi  9675  eluzsubi  9676  uzin  9681  uz3m2nn  9694  peano2uz  9704  nn0pzuz  9708  eluz2b2  9724  uz2mulcl  9729  eqreznegel  9735  lbzbi  9737  qre  9746  elpq  9770  zltaddlt1le  10129  elfz1eq  10157  fznlem  10163  fzen  10165  uzsubsubfz  10169  fzaddel  10181  fzsuc2  10201  fzp1disj  10202  fzrev  10206  elfz1b  10212  fzneuz  10223  fzp1nel  10226  elfz0fzfz0  10248  fz0fzelfz0  10249  fznn0sub2  10250  fz0fzdiffz0  10252  elfzmlbp  10254  difelfznle  10257  nelfzo  10274  elfzouz2  10284  fzo0n  10290  fzonlt0  10291  fzossrbm1  10297  fzo1fzo0n0  10307  elfzo0z  10308  fzofzim  10312  eluzgtdifelfzo  10326  fzossfzop1  10341  ssfzo12bi  10354  elfzomelpfzo  10360  fzosplitprm1  10363  fzostep1  10366  infssuzex  10376  flid  10427  flqbi2  10434  2tnp1ge0ge0  10444  flhalf  10445  fldiv4p1lem1div2  10448  fldiv4lem1div2uz2  10449  ceiqle  10458  uzsinds  10589  zsqcl2  10762  ccatsymb  11058  ccatval21sw  11061  lswccatn0lsw  11067  swrd0g  11113  nn0abscl  11396  zmaxcl  11535  2zsupmax  11537  2zinfmin  11554  p1modz1  12105  evennn02n  12193  evennn2n  12194  ltoddhalfle  12204  bitsp1o  12264  dfgcd2  12335  algcvga  12373  isprm3  12440  dvdsnprmd  12447  sqnprm  12458  zgcdsq  12523  hashdvds  12543  fldivp1  12671  zgz  12696  4sqlem4  12715  4sqexercise1  12721  mulgval  13458  coskpi  15320  relogexp  15344  rplogbzexp  15426  zabsle1  15476  lgsne0  15515  gausslemma2dlem1a  15535  gausslemma2dlem3  15540  gausslemma2dlem4  15541  lgsquadlem1  15554  lgsquadlem2  15555  2lgslem1a1  15563  2lgslem1a2  15564  2sqlem2  15592