Theorem zre 9450

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 9448	. 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 1001   = wceq 1395   e. wcel 2200   RRcr 7998   0cc0 7999   -ucneg 8318   NNcn 9110   ZZcz 9446

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-rab 2517  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6004  df-neg 8320  df-z 9447

This theorem is referenced by:  zcn  9451  zrei  9452  zssre  9453  elnn0z  9459  elnnz1  9469  peano2z  9482  zaddcl  9486  ztri3or0  9488  ztri3or  9489  zletric  9490  zlelttric  9491  zltnle  9492  zleloe  9493  zletr  9496  znnsub  9498  nzadd  9499  zltp1le  9501  zleltp1  9502  znn0sub  9512  zapne  9521  zdceq  9522  zdcle  9523  zdclt  9524  zltlen  9525  nn0ge0div  9534  zextle  9538  btwnnz  9541  suprzclex  9545  msqznn  9547  peano2uz2  9554  uzind  9558  fzind  9562  fnn0ind  9563  eluzuzle  9730  uzid  9736  uzneg  9741  uz11  9745  eluzp1m1  9746  eluzp1p1  9748  eluzaddi  9749  eluzsubi  9750  uzin  9755  uz3m2nn  9768  peano2uz  9778  nn0pzuz  9782  eluz2b2  9798  uz2mulcl  9803  eqreznegel  9809  lbzbi  9811  qre  9820  elpq  9844  zltaddlt1le  10203  elfz1eq  10231  fznlem  10237  fzen  10239  uzsubsubfz  10243  fzaddel  10255  fzsuc2  10275  fzp1disj  10276  fzrev  10280  elfz1b  10286  fzneuz  10297  fzp1nel  10300  elfz0fzfz0  10322  fz0fzelfz0  10323  fznn0sub2  10324  fz0fzdiffz0  10326  elfzmlbp  10328  difelfznle  10331  nelfzo  10348  elfzouz2  10358  fzo0n  10364  fzonlt0  10365  fzossrbm1  10371  fzo1fzo0n0  10383  elfzo0z  10384  fzofzim  10388  eluzgtdifelfzo  10403  fzossfzop1  10418  ssfzo12bi  10431  elfzomelpfzo  10437  fzosplitprm1  10440  fzostep1  10443  infssuzex  10453  flid  10504  flqbi2  10511  2tnp1ge0ge0  10521  flhalf  10522  fldiv4p1lem1div2  10525  fldiv4lem1div2uz2  10526  ceiqle  10535  uzsinds  10666  zsqcl2  10839  ccatsymb  11137  ccatval21sw  11140  lswccatn0lsw  11146  swrd0g  11192  swrdswrdlem  11236  swrdswrd  11237  swrdccatin2  11261  pfxccatin12lem2  11263  pfxccatin12lem3  11264  nn0abscl  11596  zmaxcl  11735  2zsupmax  11737  2zinfmin  11754  p1modz1  12305  evennn02n  12393  evennn2n  12394  ltoddhalfle  12404  bitsp1o  12464  dfgcd2  12535  algcvga  12573  isprm3  12640  dvdsnprmd  12647  sqnprm  12658  zgcdsq  12723  hashdvds  12743  fldivp1  12871  zgz  12896  4sqlem4  12915  4sqexercise1  12921  mulgval  13659  coskpi  15522  relogexp  15546  rplogbzexp  15628  zabsle1  15678  lgsne0  15717  gausslemma2dlem1a  15737  gausslemma2dlem3  15742  gausslemma2dlem4  15743  lgsquadlem1  15756  lgsquadlem2  15757  2lgslem1a1  15765  2lgslem1a2  15766  2sqlem2  15794