Theorem zre 8436

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

Syntax hints:   -> wi 4   \/ w3o 919   = wceq 1285   e. wcel 1434   RRcr 7042   0cc0 7043   -ucneg 7347   NNcn 8106   ZZcz 8432

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-3or 921  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-rex 2355  df-rab 2358  df-v 2604  df-un 2978  df-sn 3412  df-pr 3413  df-op 3415  df-uni 3610  df-br 3794  df-iota 4897  df-fv 4940  df-ov 5546  df-neg 7349  df-z 8433

This theorem is referenced by:  zcn  8437  zrei  8438  zssre  8439  elnn0z  8445  elnnz1  8455  peano2z  8468  zaddcl  8472  ztri3or0  8474  ztri3or  8475  zletric  8476  zlelttric  8477  zltnle  8478  zleloe  8479  zletr  8481  znnsub  8483  nzadd  8484  zltp1le  8486  zleltp1  8487  znn0sub  8497  zapne  8503  zdceq  8504  zdcle  8505  zdclt  8506  zltlen  8507  nn0ge0div  8515  zextle  8519  btwnnz  8522  suprzclex  8526  msqznn  8528  peano2uz2  8535  uzind  8539  fzind  8543  fnn0ind  8544  eluzuzle  8708  uzid  8714  uzneg  8718  uz11  8722  eluzp1m1  8723  eluzp1p1  8725  eluzaddi  8726  eluzsubi  8727  uzin  8732  uz3m2nn  8742  peano2uz  8752  nn0pzuz  8756  eluz2b2  8771  uz2mulcl  8776  eqreznegel  8780  lbzbi  8782  qre  8791  zltaddlt1le  9104  elfz1eq  9130  fznlem  9136  fzen  9138  uzsubsubfz  9142  fzaddel  9153  fzsuc2  9172  fzp1disj  9173  fzrev  9177  elfz1b  9183  fzneuz  9194  fzp1nel  9197  elfz0fzfz0  9214  fz0fzelfz0  9215  fznn0sub2  9216  fz0fzdiffz0  9218  elfzmlbp  9220  difelfznle  9223  elfzouz2  9247  fzonlt0  9253  fzossrbm1  9259  fzo1fzo0n0  9269  elfzo0z  9270  fzofzim  9274  eluzgtdifelfzo  9283  fzossfzop1  9298  ssfzo12bi  9311  elfzomelpfzo  9317  fzosplitprm1  9320  fzostep1  9323  flid  9366  flqbi2  9373  2tnp1ge0ge0  9383  flhalf  9384  fldiv4p1lem1div2  9387  ceiqle  9395  uzsinds  9518  zsqcl2  9650  nn0abscl  10109  evennn02n  10426  evennn2n  10427  ltoddhalfle  10437  infssuzex  10489  dfgcd2  10547  ialgcvga  10577  isprm3  10644  dvdsnprmd  10651  sqnprm  10661