MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zre Unicode version

Theorem zre 10219
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
StepHypRef Expression
1 elz 10217 . 2  |-  ( N  e.  ZZ  <->  ( N  e.  RR  /\  ( N  =  0  \/  N  e.  NN  \/  -u N  e.  NN ) ) )
21simplbi 447 1  |-  ( N  e.  ZZ  ->  N  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ w3o 935    = wceq 1649    e. wcel 1717   RRcr 8923   0cc0 8924   -ucneg 9225   NNcn 9933   ZZcz 10215
This theorem is referenced by:  zcn  10220  zrei  10221  zssre  10222  elnn0z  10227  elnnz1  10240  znnnlt1  10241  znnsub  10255  znn0sub  10256  zltp1le  10258  zleltp1  10259  zextle  10276  btwnnz  10279  suprzcl  10282  msqznn  10284  peano2uz2  10290  uzind  10294  uzindOLD  10297  fzind  10301  fnn0ind  10302  uzid  10433  uztrn  10435  uzneg  10437  uzss  10439  uztric  10440  uz11  10441  eluzp1m1  10442  eluzp1p1  10444  eluzaddi  10445  eluzsubi  10446  uzin  10451  peano2uz  10463  uzwo  10472  uzwoOLD  10473  eluz2b2  10481  uz2mulcl  10486  eqreznegel  10494  lbzbi  10497  uzsupss  10501  zmin  10503  zmax  10504  zbtwnre  10505  rebtwnz  10506  qre  10512  rpnnen1lem1  10533  rpnnen1lem2  10534  rpnnen1lem3  10535  rpnnen1lem5  10537  z2ge  10717  qbtwnre  10718  elfz1eq  11001  fzn  11004  fzen  11005  fznn0sub2  11019  fzaddel  11020  fzsuc2  11036  fzrev  11040  fzm1  11058  fznuz  11060  uznfz  11061  elfzouz2  11084  fzospliti  11096  elfznelfzob  11121  fzostep1  11125  fllt  11143  flid  11144  flbi2  11152  flhalf  11159  ceile  11163  quoremz  11164  intfracq  11168  uzsup  11172  zmod10  11192  zmodcl  11194  zmodfz  11196  modcyc  11204  modmul1  11207  leexp2  11362  zsqcl2  11387  iexpcyc  11413  brfi1uzind  11643  nn0abscl  12045  rexuzre  12084  znnenlem  12739  dvdsval3  12784  moddvds  12787  absdvdsb  12796  dvdsabsb  12797  dvdsle  12823  alzdvds  12827  divalgmod  12854  bitsp1o  12873  gcdabs  12961  gcdabs1  12962  modgcd  12964  bezoutlem1  12966  algcvga  12998  isprm3  13016  sqnprm  13026  zgcdsq  13073  hashdvds  13092  fldivp1  13194  zgz  13229  4sqlem4  13248  gexdvds  15146  zrngunit  16689  prmirred  16699  znf1o  16756  dyadf  19351  dyadovol  19353  degltlem1  19863  coskpi  20296  cosne0  20300  relogexp  20358  cxpeq  20509  ppival2  20779  ppival2g  20780  ppiprm  20802  chtprm  20804  chtnprm  20805  ppip1le  20812  efexple  20933  lgsdir2lem4  20978  lgsne0  20985  lgsquadlem1  21006  lgsquadlem2  21007  2sqlem2  21016  rplogsumlem2  21047  pntrsumbnd  21128  gxnval  21697  gxmodid  21716  zrhre  24182  rrhre  24184  hashf2  24271  ballotlemfc0  24530  ballotlemfcc  24531  elfzm12  24892  zmodid2  24894  fzp1nel  24990  axlowdim  25615  itg2addnclem2  25959  nn0prpwlem  26017  fzmul  26136  fzadd2  26137  incsequz2  26145  ellz1  26517  lzunuz  26518  lzenom  26520  nerabdioph  26561  pell14qrgt0  26614  rmxycomplete  26672  monotuz  26696  monotoddzzfi  26697  oddcomabszz  26699  zindbi  26701  jm2.24  26720  congrep  26730  fzneg  26739  jm2.19  26756  climsuse  27403  stoweidlem26  27444  stoweidlem34  27452
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-rex 2656  df-rab 2659  df-v 2902  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-sn 3764  df-pr 3765  df-op 3767  df-uni 3959  df-br 4155  df-iota 5359  df-fv 5403  df-ov 6024  df-neg 9227  df-z 10216
  Copyright terms: Public domain W3C validator