Theorem zre 9321

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 9319	. 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 7871   0cc0 7872   -ucneg 8191   NNcn 8982   ZZcz 9317

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 3157  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262  df-ov 5921  df-neg 8193  df-z 9318

This theorem is referenced by:  zcn  9322  zrei  9323  zssre  9324  elnn0z  9330  elnnz1  9340  peano2z  9353  zaddcl  9357  ztri3or0  9359  ztri3or  9360  zletric  9361  zlelttric  9362  zltnle  9363  zleloe  9364  zletr  9366  znnsub  9368  nzadd  9369  zltp1le  9371  zleltp1  9372  znn0sub  9382  zapne  9391  zdceq  9392  zdcle  9393  zdclt  9394  zltlen  9395  nn0ge0div  9404  zextle  9408  btwnnz  9411  suprzclex  9415  msqznn  9417  peano2uz2  9424  uzind  9428  fzind  9432  fnn0ind  9433  eluzuzle  9600  uzid  9606  uzneg  9611  uz11  9615  eluzp1m1  9616  eluzp1p1  9618  eluzaddi  9619  eluzsubi  9620  uzin  9625  uz3m2nn  9638  peano2uz  9648  nn0pzuz  9652  eluz2b2  9668  uz2mulcl  9673  eqreznegel  9679  lbzbi  9681  qre  9690  elpq  9714  zltaddlt1le  10073  elfz1eq  10101  fznlem  10107  fzen  10109  uzsubsubfz  10113  fzaddel  10125  fzsuc2  10145  fzp1disj  10146  fzrev  10150  elfz1b  10156  fzneuz  10167  fzp1nel  10170  elfz0fzfz0  10192  fz0fzelfz0  10193  fznn0sub2  10194  fz0fzdiffz0  10196  elfzmlbp  10198  difelfznle  10201  nelfzo  10218  elfzouz2  10228  fzonlt0  10234  fzossrbm1  10240  fzo1fzo0n0  10250  elfzo0z  10251  fzofzim  10255  eluzgtdifelfzo  10264  fzossfzop1  10279  ssfzo12bi  10292  elfzomelpfzo  10298  fzosplitprm1  10301  fzostep1  10304  flid  10353  flqbi2  10360  2tnp1ge0ge0  10370  flhalf  10371  fldiv4p1lem1div2  10374  fldiv4lem1div2uz2  10375  ceiqle  10384  uzsinds  10515  zsqcl2  10688  nn0abscl  11229  zmaxcl  11368  2zsupmax  11369  2zinfmin  11386  p1modz1  11937  evennn02n  12023  evennn2n  12024  ltoddhalfle  12034  infssuzex  12086  dfgcd2  12151  algcvga  12189  isprm3  12256  dvdsnprmd  12263  sqnprm  12274  zgcdsq  12339  hashdvds  12359  fldivp1  12486  zgz  12511  4sqlem4  12530  4sqexercise1  12536  mulgval  13192  coskpi  14983  relogexp  15007  rplogbzexp  15086  zabsle1  15115  lgsne0  15154  gausslemma2dlem1a  15174  gausslemma2dlem3  15179  gausslemma2dlem4  15180  lgsquadlem1  15191  2sqlem2  15202