Theorem zre 9298

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 9296	. 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 2160   RRcr 7850   0cc0 7851   -ucneg 8170   NNcn 8960   ZZcz 9294

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 2171

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 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-rab 2477  df-v 2758  df-un 3152  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3832  df-br 4026  df-iota 5203  df-fv 5250  df-ov 5907  df-neg 8172  df-z 9295

This theorem is referenced by:  zcn  9299  zrei  9300  zssre  9301  elnn0z  9307  elnnz1  9317  peano2z  9330  zaddcl  9334  ztri3or0  9336  ztri3or  9337  zletric  9338  zlelttric  9339  zltnle  9340  zleloe  9341  zletr  9343  znnsub  9345  nzadd  9346  zltp1le  9348  zleltp1  9349  znn0sub  9359  zapne  9368  zdceq  9369  zdcle  9370  zdclt  9371  zltlen  9372  nn0ge0div  9381  zextle  9385  btwnnz  9388  suprzclex  9392  msqznn  9394  peano2uz2  9401  uzind  9405  fzind  9409  fnn0ind  9410  eluzuzle  9577  uzid  9583  uzneg  9588  uz11  9592  eluzp1m1  9593  eluzp1p1  9595  eluzaddi  9596  eluzsubi  9597  uzin  9602  uz3m2nn  9615  peano2uz  9625  nn0pzuz  9629  eluz2b2  9645  uz2mulcl  9650  eqreznegel  9656  lbzbi  9658  qre  9667  elpq  9690  zltaddlt1le  10049  elfz1eq  10077  fznlem  10083  fzen  10085  uzsubsubfz  10089  fzaddel  10101  fzsuc2  10121  fzp1disj  10122  fzrev  10126  elfz1b  10132  fzneuz  10143  fzp1nel  10146  elfz0fzfz0  10168  fz0fzelfz0  10169  fznn0sub2  10170  fz0fzdiffz0  10172  elfzmlbp  10174  difelfznle  10177  elfzouz2  10203  fzonlt0  10209  fzossrbm1  10215  fzo1fzo0n0  10225  elfzo0z  10226  fzofzim  10230  eluzgtdifelfzo  10239  fzossfzop1  10254  ssfzo12bi  10267  elfzomelpfzo  10273  fzosplitprm1  10276  fzostep1  10279  flid  10327  flqbi2  10334  2tnp1ge0ge0  10344  flhalf  10345  fldiv4p1lem1div2  10348  ceiqle  10356  uzsinds  10487  zsqcl2  10644  nn0abscl  11141  zmaxcl  11280  2zsupmax  11281  2zinfmin  11298  p1modz1  11848  evennn02n  11934  evennn2n  11935  ltoddhalfle  11945  infssuzex  11997  dfgcd2  12062  algcvga  12100  isprm3  12167  dvdsnprmd  12174  sqnprm  12185  zgcdsq  12250  hashdvds  12270  fldivp1  12397  zgz  12422  4sqlem4  12441  4sqexercise1  12447  mulgval  13095  coskpi  14807  relogexp  14831  rplogbzexp  14910  zabsle1  14939  lgsne0  14978  2sqlem2  15001