Theorem zre 9544

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 9542	. 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 1004   = wceq 1398   e. wcel 2202   RRcr 8091   0cc0 8092   -ucneg 8410   NNcn 9202   ZZcz 9540

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-rab 2520  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031  df-neg 8412  df-z 9541

This theorem is referenced by:  zcn  9545  zrei  9546  zssre  9547  elnn0z  9553  elnnz1  9563  peano2z  9576  zaddcl  9580  ztri3or0  9582  ztri3or  9583  zletric  9584  zlelttric  9585  zltnle  9586  zleloe  9587  zletr  9590  znnsub  9592  nzadd  9593  zltp1le  9595  zleltp1  9596  znn0sub  9606  zapne  9615  zdceq  9616  zdcle  9617  zdclt  9618  zltlen  9619  nn0ge0div  9628  zextle  9632  btwnnz  9635  suprzclex  9639  msqznn  9641  peano2uz2  9648  uzind  9652  fzind  9656  fnn0ind  9657  eluzuzle  9825  uzid  9831  uzneg  9836  uz11  9840  eluzp1m1  9841  eluzp1p1  9843  eluzaddi  9844  eluzsubi  9845  uzin  9850  uz3m2nn  9868  peano2uz  9878  nn0pzuz  9882  eluz2b2  9898  uz2mulcl  9903  eqreznegel  9909  lbzbi  9911  qre  9920  elpq  9944  zltaddlt1le  10304  elfz1eq  10332  fznlem  10338  fzen  10340  uzsubsubfz  10344  fzaddel  10356  fzsuc2  10376  fzp1disj  10377  fzrev  10381  elfz1b  10387  fzneuz  10398  fzp1nel  10401  elfz0fzfz0  10423  fz0fzelfz0  10424  fznn0sub2  10425  fz0fzdiffz0  10427  elfzmlbp  10429  difelfznle  10432  nelfzo  10449  elfzouz2  10459  fzo0n  10465  fzonlt0  10466  fzossrbm1  10472  fzo1fzo0n0  10485  elfzo0z  10486  fzofzim  10490  eluzgtdifelfzo  10505  fzossfzop1  10520  ssfzo12bi  10533  elfzomelpfzo  10539  fzosplitprm1  10543  fzostep1  10546  infssuzex  10556  flid  10607  flqbi2  10614  2tnp1ge0ge0  10624  flhalf  10625  fldiv4p1lem1div2  10628  fldiv4lem1div2uz2  10629  ceiqle  10638  uzsinds  10769  zsqcl2  10942  ccatsymb  11245  ccatval21sw  11248  lswccatn0lsw  11254  swrd0g  11307  swrdswrdlem  11351  swrdswrd  11352  swrdccatin2  11376  pfxccatin12lem2  11378  pfxccatin12lem3  11379  nn0abscl  11725  zmaxcl  11864  2zsupmax  11866  2zinfmin  11883  p1modz1  12435  evennn02n  12523  evennn2n  12524  ltoddhalfle  12534  bitsp1o  12594  dfgcd2  12665  algcvga  12703  isprm3  12770  dvdsnprmd  12777  sqnprm  12788  zgcdsq  12853  hashdvds  12873  fldivp1  13001  zgz  13026  4sqlem4  13045  4sqexercise1  13051  mulgval  13789  coskpi  15659  relogexp  15683  rplogbzexp  15765  zabsle1  15818  lgsne0  15857  gausslemma2dlem1a  15877  gausslemma2dlem3  15882  gausslemma2dlem4  15883  lgsquadlem1  15896  lgsquadlem2  15897  2lgslem1a1  15905  2lgslem1a2  15906  2sqlem2  15934  clwwlkext2edg  16363