Theorem zre 9195

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 9193	. 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 967   = wceq 1343   e. wcel 2136   RRcr 7752   0cc0 7753   -ucneg 8070   NNcn 8857   ZZcz 9191

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3or 969  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-rex 2450  df-rab 2453  df-v 2728  df-un 3120  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-br 3983  df-iota 5153  df-fv 5196  df-ov 5845  df-neg 8072  df-z 9192

This theorem is referenced by:  zcn  9196  zrei  9197  zssre  9198  elnn0z  9204  elnnz1  9214  peano2z  9227  zaddcl  9231  ztri3or0  9233  ztri3or  9234  zletric  9235  zlelttric  9236  zltnle  9237  zleloe  9238  zletr  9240  znnsub  9242  nzadd  9243  zltp1le  9245  zleltp1  9246  znn0sub  9256  zapne  9265  zdceq  9266  zdcle  9267  zdclt  9268  zltlen  9269  nn0ge0div  9278  zextle  9282  btwnnz  9285  suprzclex  9289  msqznn  9291  peano2uz2  9298  uzind  9302  fzind  9306  fnn0ind  9307  eluzuzle  9474  uzid  9480  uzneg  9484  uz11  9488  eluzp1m1  9489  eluzp1p1  9491  eluzaddi  9492  eluzsubi  9493  uzin  9498  uz3m2nn  9511  peano2uz  9521  nn0pzuz  9525  eluz2b2  9541  uz2mulcl  9546  eqreznegel  9552  lbzbi  9554  qre  9563  elpq  9586  zltaddlt1le  9943  elfz1eq  9970  fznlem  9976  fzen  9978  uzsubsubfz  9982  fzaddel  9994  fzsuc2  10014  fzp1disj  10015  fzrev  10019  elfz1b  10025  fzneuz  10036  fzp1nel  10039  elfz0fzfz0  10061  fz0fzelfz0  10062  fznn0sub2  10063  fz0fzdiffz0  10065  elfzmlbp  10067  difelfznle  10070  elfzouz2  10096  fzonlt0  10102  fzossrbm1  10108  fzo1fzo0n0  10118  elfzo0z  10119  fzofzim  10123  eluzgtdifelfzo  10132  fzossfzop1  10147  ssfzo12bi  10160  elfzomelpfzo  10166  fzosplitprm1  10169  fzostep1  10172  flid  10219  flqbi2  10226  2tnp1ge0ge0  10236  flhalf  10237  fldiv4p1lem1div2  10240  ceiqle  10248  uzsinds  10377  zsqcl2  10532  nn0abscl  11027  zmaxcl  11166  2zsupmax  11167  2zinfmin  11184  p1modz1  11734  evennn02n  11819  evennn2n  11820  ltoddhalfle  11830  infssuzex  11882  dfgcd2  11947  algcvga  11983  isprm3  12050  dvdsnprmd  12057  sqnprm  12068  zgcdsq  12133  hashdvds  12153  fldivp1  12278  zgz  12303  4sqlem4  12322  coskpi  13409  relogexp  13433  rplogbzexp  13512  zabsle1  13540  lgsne0  13579  2sqlem2  13591