Theorem zre 9411

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 9409	. 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 980   = wceq 1373   e. wcel 2178   RRcr 7959   0cc0 7960   -ucneg 8279   NNcn 9071   ZZcz 9407

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-rab 2495  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298  df-ov 5970  df-neg 8281  df-z 9408

This theorem is referenced by:  zcn  9412  zrei  9413  zssre  9414  elnn0z  9420  elnnz1  9430  peano2z  9443  zaddcl  9447  ztri3or0  9449  ztri3or  9450  zletric  9451  zlelttric  9452  zltnle  9453  zleloe  9454  zletr  9457  znnsub  9459  nzadd  9460  zltp1le  9462  zleltp1  9463  znn0sub  9473  zapne  9482  zdceq  9483  zdcle  9484  zdclt  9485  zltlen  9486  nn0ge0div  9495  zextle  9499  btwnnz  9502  suprzclex  9506  msqznn  9508  peano2uz2  9515  uzind  9519  fzind  9523  fnn0ind  9524  eluzuzle  9691  uzid  9697  uzneg  9702  uz11  9706  eluzp1m1  9707  eluzp1p1  9709  eluzaddi  9710  eluzsubi  9711  uzin  9716  uz3m2nn  9729  peano2uz  9739  nn0pzuz  9743  eluz2b2  9759  uz2mulcl  9764  eqreznegel  9770  lbzbi  9772  qre  9781  elpq  9805  zltaddlt1le  10164  elfz1eq  10192  fznlem  10198  fzen  10200  uzsubsubfz  10204  fzaddel  10216  fzsuc2  10236  fzp1disj  10237  fzrev  10241  elfz1b  10247  fzneuz  10258  fzp1nel  10261  elfz0fzfz0  10283  fz0fzelfz0  10284  fznn0sub2  10285  fz0fzdiffz0  10287  elfzmlbp  10289  difelfznle  10292  nelfzo  10309  elfzouz2  10319  fzo0n  10325  fzonlt0  10326  fzossrbm1  10332  fzo1fzo0n0  10344  elfzo0z  10345  fzofzim  10349  eluzgtdifelfzo  10363  fzossfzop1  10378  ssfzo12bi  10391  elfzomelpfzo  10397  fzosplitprm1  10400  fzostep1  10403  infssuzex  10413  flid  10464  flqbi2  10471  2tnp1ge0ge0  10481  flhalf  10482  fldiv4p1lem1div2  10485  fldiv4lem1div2uz2  10486  ceiqle  10495  uzsinds  10626  zsqcl2  10799  ccatsymb  11096  ccatval21sw  11099  lswccatn0lsw  11105  swrd0g  11151  swrdswrdlem  11195  swrdswrd  11196  swrdccatin2  11220  pfxccatin12lem2  11222  pfxccatin12lem3  11223  nn0abscl  11511  zmaxcl  11650  2zsupmax  11652  2zinfmin  11669  p1modz1  12220  evennn02n  12308  evennn2n  12309  ltoddhalfle  12319  bitsp1o  12379  dfgcd2  12450  algcvga  12488  isprm3  12555  dvdsnprmd  12562  sqnprm  12573  zgcdsq  12638  hashdvds  12658  fldivp1  12786  zgz  12811  4sqlem4  12830  4sqexercise1  12836  mulgval  13573  coskpi  15435  relogexp  15459  rplogbzexp  15541  zabsle1  15591  lgsne0  15630  gausslemma2dlem1a  15650  gausslemma2dlem3  15655  gausslemma2dlem4  15656  lgsquadlem1  15669  lgsquadlem2  15670  2lgslem1a1  15678  2lgslem1a2  15679  2sqlem2  15707