Theorem zre 9458

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 9456	. 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 8006   0cc0 8007   -ucneg 8326   NNcn 9118   ZZcz 9454

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 6010  df-neg 8328  df-z 9455

This theorem is referenced by:  zcn  9459  zrei  9460  zssre  9461  elnn0z  9467  elnnz1  9477  peano2z  9490  zaddcl  9494  ztri3or0  9496  ztri3or  9497  zletric  9498  zlelttric  9499  zltnle  9500  zleloe  9501  zletr  9504  znnsub  9506  nzadd  9507  zltp1le  9509  zleltp1  9510  znn0sub  9520  zapne  9529  zdceq  9530  zdcle  9531  zdclt  9532  zltlen  9533  nn0ge0div  9542  zextle  9546  btwnnz  9549  suprzclex  9553  msqznn  9555  peano2uz2  9562  uzind  9566  fzind  9570  fnn0ind  9571  eluzuzle  9738  uzid  9744  uzneg  9749  uz11  9753  eluzp1m1  9754  eluzp1p1  9756  eluzaddi  9757  eluzsubi  9758  uzin  9763  uz3m2nn  9776  peano2uz  9786  nn0pzuz  9790  eluz2b2  9806  uz2mulcl  9811  eqreznegel  9817  lbzbi  9819  qre  9828  elpq  9852  zltaddlt1le  10211  elfz1eq  10239  fznlem  10245  fzen  10247  uzsubsubfz  10251  fzaddel  10263  fzsuc2  10283  fzp1disj  10284  fzrev  10288  elfz1b  10294  fzneuz  10305  fzp1nel  10308  elfz0fzfz0  10330  fz0fzelfz0  10331  fznn0sub2  10332  fz0fzdiffz0  10334  elfzmlbp  10336  difelfznle  10339  nelfzo  10356  elfzouz2  10366  fzo0n  10372  fzonlt0  10373  fzossrbm1  10379  fzo1fzo0n0  10391  elfzo0z  10392  fzofzim  10396  eluzgtdifelfzo  10411  fzossfzop1  10426  ssfzo12bi  10439  elfzomelpfzo  10445  fzosplitprm1  10448  fzostep1  10451  infssuzex  10461  flid  10512  flqbi2  10519  2tnp1ge0ge0  10529  flhalf  10530  fldiv4p1lem1div2  10533  fldiv4lem1div2uz2  10534  ceiqle  10543  uzsinds  10674  zsqcl2  10847  ccatsymb  11145  ccatval21sw  11148  lswccatn0lsw  11154  swrd0g  11200  swrdswrdlem  11244  swrdswrd  11245  swrdccatin2  11269  pfxccatin12lem2  11271  pfxccatin12lem3  11272  nn0abscl  11604  zmaxcl  11743  2zsupmax  11745  2zinfmin  11762  p1modz1  12313  evennn02n  12401  evennn2n  12402  ltoddhalfle  12412  bitsp1o  12472  dfgcd2  12543  algcvga  12581  isprm3  12648  dvdsnprmd  12655  sqnprm  12666  zgcdsq  12731  hashdvds  12751  fldivp1  12879  zgz  12904  4sqlem4  12923  4sqexercise1  12929  mulgval  13667  coskpi  15530  relogexp  15554  rplogbzexp  15636  zabsle1  15686  lgsne0  15725  gausslemma2dlem1a  15745  gausslemma2dlem3  15750  gausslemma2dlem4  15751  lgsquadlem1  15764  lgsquadlem2  15765  2lgslem1a1  15773  2lgslem1a2  15774  2sqlem2  15802