Theorem zre 9483

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 9481	. 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 1003   = wceq 1397   e. wcel 2202   RRcr 8031   0cc0 8032   -ucneg 8351   NNcn 9143   ZZcz 9479

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-rab 2519  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021  df-neg 8353  df-z 9480

This theorem is referenced by:  zcn  9484  zrei  9485  zssre  9486  elnn0z  9492  elnnz1  9502  peano2z  9515  zaddcl  9519  ztri3or0  9521  ztri3or  9522  zletric  9523  zlelttric  9524  zltnle  9525  zleloe  9526  zletr  9529  znnsub  9531  nzadd  9532  zltp1le  9534  zleltp1  9535  znn0sub  9545  zapne  9554  zdceq  9555  zdcle  9556  zdclt  9557  zltlen  9558  nn0ge0div  9567  zextle  9571  btwnnz  9574  suprzclex  9578  msqznn  9580  peano2uz2  9587  uzind  9591  fzind  9595  fnn0ind  9596  eluzuzle  9764  uzid  9770  uzneg  9775  uz11  9779  eluzp1m1  9780  eluzp1p1  9782  eluzaddi  9783  eluzsubi  9784  uzin  9789  uz3m2nn  9807  peano2uz  9817  nn0pzuz  9821  eluz2b2  9837  uz2mulcl  9842  eqreznegel  9848  lbzbi  9850  qre  9859  elpq  9883  zltaddlt1le  10242  elfz1eq  10270  fznlem  10276  fzen  10278  uzsubsubfz  10282  fzaddel  10294  fzsuc2  10314  fzp1disj  10315  fzrev  10319  elfz1b  10325  fzneuz  10336  fzp1nel  10339  elfz0fzfz0  10361  fz0fzelfz0  10362  fznn0sub2  10363  fz0fzdiffz0  10365  elfzmlbp  10367  difelfznle  10370  nelfzo  10387  elfzouz2  10397  fzo0n  10403  fzonlt0  10404  fzossrbm1  10410  fzo1fzo0n0  10422  elfzo0z  10423  fzofzim  10427  eluzgtdifelfzo  10442  fzossfzop1  10457  ssfzo12bi  10470  elfzomelpfzo  10476  fzosplitprm1  10480  fzostep1  10483  infssuzex  10493  flid  10544  flqbi2  10551  2tnp1ge0ge0  10561  flhalf  10562  fldiv4p1lem1div2  10565  fldiv4lem1div2uz2  10566  ceiqle  10575  uzsinds  10706  zsqcl2  10879  ccatsymb  11179  ccatval21sw  11182  lswccatn0lsw  11188  swrd0g  11241  swrdswrdlem  11285  swrdswrd  11286  swrdccatin2  11310  pfxccatin12lem2  11312  pfxccatin12lem3  11313  nn0abscl  11646  zmaxcl  11785  2zsupmax  11787  2zinfmin  11804  p1modz1  12356  evennn02n  12444  evennn2n  12445  ltoddhalfle  12455  bitsp1o  12515  dfgcd2  12586  algcvga  12624  isprm3  12691  dvdsnprmd  12698  sqnprm  12709  zgcdsq  12774  hashdvds  12794  fldivp1  12922  zgz  12947  4sqlem4  12966  4sqexercise1  12972  mulgval  13710  coskpi  15574  relogexp  15598  rplogbzexp  15680  zabsle1  15730  lgsne0  15769  gausslemma2dlem1a  15789  gausslemma2dlem3  15794  gausslemma2dlem4  15795  lgsquadlem1  15808  lgsquadlem2  15809  2lgslem1a1  15817  2lgslem1a2  15818  2sqlem2  15846  clwwlkext2edg  16275