Theorem zre 9486

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 9484	. 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 8034   0cc0 8035   -ucneg 8354   NNcn 9146   ZZcz 9482

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 6024  df-neg 8356  df-z 9483

This theorem is referenced by:  zcn  9487  zrei  9488  zssre  9489  elnn0z  9495  elnnz1  9505  peano2z  9518  zaddcl  9522  ztri3or0  9524  ztri3or  9525  zletric  9526  zlelttric  9527  zltnle  9528  zleloe  9529  zletr  9532  znnsub  9534  nzadd  9535  zltp1le  9537  zleltp1  9538  znn0sub  9548  zapne  9557  zdceq  9558  zdcle  9559  zdclt  9560  zltlen  9561  nn0ge0div  9570  zextle  9574  btwnnz  9577  suprzclex  9581  msqznn  9583  peano2uz2  9590  uzind  9594  fzind  9598  fnn0ind  9599  eluzuzle  9767  uzid  9773  uzneg  9778  uz11  9782  eluzp1m1  9783  eluzp1p1  9785  eluzaddi  9786  eluzsubi  9787  uzin  9792  uz3m2nn  9810  peano2uz  9820  nn0pzuz  9824  eluz2b2  9840  uz2mulcl  9845  eqreznegel  9851  lbzbi  9853  qre  9862  elpq  9886  zltaddlt1le  10245  elfz1eq  10273  fznlem  10279  fzen  10281  uzsubsubfz  10285  fzaddel  10297  fzsuc2  10317  fzp1disj  10318  fzrev  10322  elfz1b  10328  fzneuz  10339  fzp1nel  10342  elfz0fzfz0  10364  fz0fzelfz0  10365  fznn0sub2  10366  fz0fzdiffz0  10368  elfzmlbp  10370  difelfznle  10373  nelfzo  10390  elfzouz2  10400  fzo0n  10406  fzonlt0  10407  fzossrbm1  10413  fzo1fzo0n0  10426  elfzo0z  10427  fzofzim  10431  eluzgtdifelfzo  10446  fzossfzop1  10461  ssfzo12bi  10474  elfzomelpfzo  10480  fzosplitprm1  10484  fzostep1  10487  infssuzex  10497  flid  10548  flqbi2  10555  2tnp1ge0ge0  10565  flhalf  10566  fldiv4p1lem1div2  10569  fldiv4lem1div2uz2  10570  ceiqle  10579  uzsinds  10710  zsqcl2  10883  ccatsymb  11186  ccatval21sw  11189  lswccatn0lsw  11195  swrd0g  11248  swrdswrdlem  11292  swrdswrd  11293  swrdccatin2  11317  pfxccatin12lem2  11319  pfxccatin12lem3  11320  nn0abscl  11666  zmaxcl  11805  2zsupmax  11807  2zinfmin  11824  p1modz1  12376  evennn02n  12464  evennn2n  12465  ltoddhalfle  12475  bitsp1o  12535  dfgcd2  12606  algcvga  12644  isprm3  12711  dvdsnprmd  12718  sqnprm  12729  zgcdsq  12794  hashdvds  12814  fldivp1  12942  zgz  12967  4sqlem4  12986  4sqexercise1  12992  mulgval  13730  coskpi  15599  relogexp  15623  rplogbzexp  15705  zabsle1  15755  lgsne0  15794  gausslemma2dlem1a  15814  gausslemma2dlem3  15819  gausslemma2dlem4  15820  lgsquadlem1  15833  lgsquadlem2  15834  2lgslem1a1  15842  2lgslem1a2  15843  2sqlem2  15871  clwwlkext2edg  16300