Theorem zre 9461

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 9459	. 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 8009   0cc0 8010   -ucneg 8329   NNcn 9121   ZZcz 9457

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 8331  df-z 9458

This theorem is referenced by:  zcn  9462  zrei  9463  zssre  9464  elnn0z  9470  elnnz1  9480  peano2z  9493  zaddcl  9497  ztri3or0  9499  ztri3or  9500  zletric  9501  zlelttric  9502  zltnle  9503  zleloe  9504  zletr  9507  znnsub  9509  nzadd  9510  zltp1le  9512  zleltp1  9513  znn0sub  9523  zapne  9532  zdceq  9533  zdcle  9534  zdclt  9535  zltlen  9536  nn0ge0div  9545  zextle  9549  btwnnz  9552  suprzclex  9556  msqznn  9558  peano2uz2  9565  uzind  9569  fzind  9573  fnn0ind  9574  eluzuzle  9742  uzid  9748  uzneg  9753  uz11  9757  eluzp1m1  9758  eluzp1p1  9760  eluzaddi  9761  eluzsubi  9762  uzin  9767  uz3m2nn  9780  peano2uz  9790  nn0pzuz  9794  eluz2b2  9810  uz2mulcl  9815  eqreznegel  9821  lbzbi  9823  qre  9832  elpq  9856  zltaddlt1le  10215  elfz1eq  10243  fznlem  10249  fzen  10251  uzsubsubfz  10255  fzaddel  10267  fzsuc2  10287  fzp1disj  10288  fzrev  10292  elfz1b  10298  fzneuz  10309  fzp1nel  10312  elfz0fzfz0  10334  fz0fzelfz0  10335  fznn0sub2  10336  fz0fzdiffz0  10338  elfzmlbp  10340  difelfznle  10343  nelfzo  10360  elfzouz2  10370  fzo0n  10376  fzonlt0  10377  fzossrbm1  10383  fzo1fzo0n0  10395  elfzo0z  10396  fzofzim  10400  eluzgtdifelfzo  10415  fzossfzop1  10430  ssfzo12bi  10443  elfzomelpfzo  10449  fzosplitprm1  10452  fzostep1  10455  infssuzex  10465  flid  10516  flqbi2  10523  2tnp1ge0ge0  10533  flhalf  10534  fldiv4p1lem1div2  10537  fldiv4lem1div2uz2  10538  ceiqle  10547  uzsinds  10678  zsqcl2  10851  ccatsymb  11150  ccatval21sw  11153  lswccatn0lsw  11159  swrd0g  11208  swrdswrdlem  11252  swrdswrd  11253  swrdccatin2  11277  pfxccatin12lem2  11279  pfxccatin12lem3  11280  nn0abscl  11612  zmaxcl  11751  2zsupmax  11753  2zinfmin  11770  p1modz1  12321  evennn02n  12409  evennn2n  12410  ltoddhalfle  12420  bitsp1o  12480  dfgcd2  12551  algcvga  12589  isprm3  12656  dvdsnprmd  12663  sqnprm  12674  zgcdsq  12739  hashdvds  12759  fldivp1  12887  zgz  12912  4sqlem4  12931  4sqexercise1  12937  mulgval  13675  coskpi  15538  relogexp  15562  rplogbzexp  15644  zabsle1  15694  lgsne0  15733  gausslemma2dlem1a  15753  gausslemma2dlem3  15758  gausslemma2dlem4  15759  lgsquadlem1  15772  lgsquadlem2  15773  2lgslem1a1  15781  2lgslem1a2  15782  2sqlem2  15810  clwwlkext2edg  16164