Theorem zre 9058

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 9056	. 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 961   = wceq 1331   e. wcel 1480   RRcr 7619   0cc0 7620   -ucneg 7934   NNcn 8720   ZZcz 9054

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3or 963  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rex 2422  df-rab 2425  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-iota 5088  df-fv 5131  df-ov 5777  df-neg 7936  df-z 9055

This theorem is referenced by:  zcn  9059  zrei  9060  zssre  9061  elnn0z  9067  elnnz1  9077  peano2z  9090  zaddcl  9094  ztri3or0  9096  ztri3or  9097  zletric  9098  zlelttric  9099  zltnle  9100  zleloe  9101  zletr  9103  znnsub  9105  nzadd  9106  zltp1le  9108  zleltp1  9109  znn0sub  9119  zapne  9125  zdceq  9126  zdcle  9127  zdclt  9128  zltlen  9129  nn0ge0div  9138  zextle  9142  btwnnz  9145  suprzclex  9149  msqznn  9151  peano2uz2  9158  uzind  9162  fzind  9166  fnn0ind  9167  eluzuzle  9334  uzid  9340  uzneg  9344  uz11  9348  eluzp1m1  9349  eluzp1p1  9351  eluzaddi  9352  eluzsubi  9353  uzin  9358  uz3m2nn  9368  peano2uz  9378  nn0pzuz  9382  eluz2b2  9397  uz2mulcl  9402  eqreznegel  9406  lbzbi  9408  qre  9417  zltaddlt1le  9789  elfz1eq  9815  fznlem  9821  fzen  9823  uzsubsubfz  9827  fzaddel  9839  fzsuc2  9859  fzp1disj  9860  fzrev  9864  elfz1b  9870  fzneuz  9881  fzp1nel  9884  elfz0fzfz0  9903  fz0fzelfz0  9904  fznn0sub2  9905  fz0fzdiffz0  9907  elfzmlbp  9909  difelfznle  9912  elfzouz2  9938  fzonlt0  9944  fzossrbm1  9950  fzo1fzo0n0  9960  elfzo0z  9961  fzofzim  9965  eluzgtdifelfzo  9974  fzossfzop1  9989  ssfzo12bi  10002  elfzomelpfzo  10008  fzosplitprm1  10011  fzostep1  10014  flid  10057  flqbi2  10064  2tnp1ge0ge0  10074  flhalf  10075  fldiv4p1lem1div2  10078  ceiqle  10086  uzsinds  10215  zsqcl2  10370  nn0abscl  10857  zmaxcl  10996  2zsupmax  10997  evennn02n  11579  evennn2n  11580  ltoddhalfle  11590  infssuzex  11642  dfgcd2  11702  algcvga  11732  isprm3  11799  dvdsnprmd  11806  sqnprm  11816  zgcdsq  11879  hashdvds  11897  coskpi  12929