Theorem zre 9186

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 9184	. 2 |- ( N e. ZZ <-> ( N e. RR /\ ( N = 0 \/ N e. NN \/ -u N e. NN ) ) )
2	1	simplbi 272	1 |- ( N e. ZZ -> N e. RR )

Syntax hints:   -> wi 4   \/ w3o 966   = wceq 1342   e. wcel 2135   RRcr 7743   0cc0 7744   -ucneg 8061   NNcn 8848   ZZcz 9182

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-3or 968  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-rex 2448  df-rab 2451  df-v 2723  df-un 3115  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-br 3977  df-iota 5147  df-fv 5190  df-ov 5839  df-neg 8063  df-z 9183

This theorem is referenced by:  zcn  9187  zrei  9188  zssre  9189  elnn0z  9195  elnnz1  9205  peano2z  9218  zaddcl  9222  ztri3or0  9224  ztri3or  9225  zletric  9226  zlelttric  9227  zltnle  9228  zleloe  9229  zletr  9231  znnsub  9233  nzadd  9234  zltp1le  9236  zleltp1  9237  znn0sub  9247  zapne  9256  zdceq  9257  zdcle  9258  zdclt  9259  zltlen  9260  nn0ge0div  9269  zextle  9273  btwnnz  9276  suprzclex  9280  msqznn  9282  peano2uz2  9289  uzind  9293  fzind  9297  fnn0ind  9298  eluzuzle  9465  uzid  9471  uzneg  9475  uz11  9479  eluzp1m1  9480  eluzp1p1  9482  eluzaddi  9483  eluzsubi  9484  uzin  9489  uz3m2nn  9502  peano2uz  9512  nn0pzuz  9516  eluz2b2  9532  uz2mulcl  9537  eqreznegel  9543  lbzbi  9545  qre  9554  elpq  9577  zltaddlt1le  9934  elfz1eq  9960  fznlem  9966  fzen  9968  uzsubsubfz  9972  fzaddel  9984  fzsuc2  10004  fzp1disj  10005  fzrev  10009  elfz1b  10015  fzneuz  10026  fzp1nel  10029  elfz0fzfz0  10051  fz0fzelfz0  10052  fznn0sub2  10053  fz0fzdiffz0  10055  elfzmlbp  10057  difelfznle  10060  elfzouz2  10086  fzonlt0  10092  fzossrbm1  10098  fzo1fzo0n0  10108  elfzo0z  10109  fzofzim  10113  eluzgtdifelfzo  10122  fzossfzop1  10137  ssfzo12bi  10150  elfzomelpfzo  10156  fzosplitprm1  10159  fzostep1  10162  flid  10209  flqbi2  10216  2tnp1ge0ge0  10226  flhalf  10227  fldiv4p1lem1div2  10230  ceiqle  10238  uzsinds  10367  zsqcl2  10522  nn0abscl  11013  zmaxcl  11152  2zsupmax  11153  2zinfmin  11170  p1modz1  11720  evennn02n  11804  evennn2n  11805  ltoddhalfle  11815  infssuzex  11867  dfgcd2  11932  algcvga  11962  isprm3  12029  dvdsnprmd  12036  sqnprm  12047  zgcdsq  12110  hashdvds  12130  fldivp1  12255  coskpi  13310  relogexp  13334  rplogbzexp  13413