Theorem zre 9324

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 9322	. 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 979   = wceq 1364   e. wcel 2164   RRcr 7873   0cc0 7874   -ucneg 8193   NNcn 8984   ZZcz 9320

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-rab 2481  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263  df-ov 5922  df-neg 8195  df-z 9321

This theorem is referenced by:  zcn  9325  zrei  9326  zssre  9327  elnn0z  9333  elnnz1  9343  peano2z  9356  zaddcl  9360  ztri3or0  9362  ztri3or  9363  zletric  9364  zlelttric  9365  zltnle  9366  zleloe  9367  zletr  9369  znnsub  9371  nzadd  9372  zltp1le  9374  zleltp1  9375  znn0sub  9385  zapne  9394  zdceq  9395  zdcle  9396  zdclt  9397  zltlen  9398  nn0ge0div  9407  zextle  9411  btwnnz  9414  suprzclex  9418  msqznn  9420  peano2uz2  9427  uzind  9431  fzind  9435  fnn0ind  9436  eluzuzle  9603  uzid  9609  uzneg  9614  uz11  9618  eluzp1m1  9619  eluzp1p1  9621  eluzaddi  9622  eluzsubi  9623  uzin  9628  uz3m2nn  9641  peano2uz  9651  nn0pzuz  9655  eluz2b2  9671  uz2mulcl  9676  eqreznegel  9682  lbzbi  9684  qre  9693  elpq  9717  zltaddlt1le  10076  elfz1eq  10104  fznlem  10110  fzen  10112  uzsubsubfz  10116  fzaddel  10128  fzsuc2  10148  fzp1disj  10149  fzrev  10153  elfz1b  10159  fzneuz  10170  fzp1nel  10173  elfz0fzfz0  10195  fz0fzelfz0  10196  fznn0sub2  10197  fz0fzdiffz0  10199  elfzmlbp  10201  difelfznle  10204  nelfzo  10221  elfzouz2  10231  fzonlt0  10237  fzossrbm1  10243  fzo1fzo0n0  10253  elfzo0z  10254  fzofzim  10258  eluzgtdifelfzo  10267  fzossfzop1  10282  ssfzo12bi  10295  elfzomelpfzo  10301  fzosplitprm1  10304  fzostep1  10307  flid  10356  flqbi2  10363  2tnp1ge0ge0  10373  flhalf  10374  fldiv4p1lem1div2  10377  fldiv4lem1div2uz2  10378  ceiqle  10387  uzsinds  10518  zsqcl2  10691  nn0abscl  11232  zmaxcl  11371  2zsupmax  11372  2zinfmin  11389  p1modz1  11940  evennn02n  12026  evennn2n  12027  ltoddhalfle  12037  infssuzex  12089  dfgcd2  12154  algcvga  12192  isprm3  12259  dvdsnprmd  12266  sqnprm  12277  zgcdsq  12342  hashdvds  12362  fldivp1  12489  zgz  12514  4sqlem4  12533  4sqexercise1  12539  mulgval  13195  coskpi  15024  relogexp  15048  rplogbzexp  15127  zabsle1  15156  lgsne0  15195  gausslemma2dlem1a  15215  gausslemma2dlem3  15220  gausslemma2dlem4  15221  lgsquadlem1  15234  lgsquadlem2  15235  2lgslem1a1  15243  2lgslem1a2  15244  2sqlem2  15272