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

Theorem zre 10762
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 10760 . 2  |-  ( N  e.  ZZ  <->  ( N  e.  RR  /\  ( N  =  0  \/  N  e.  NN  \/  -u N  e.  NN ) ) )
21simplbi 460 1  |-  ( N  e.  ZZ  ->  N  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ w3o 964    = wceq 1370    e. wcel 1758   RRcr 9393   0cc0 9394   -ucneg 9708   NNcn 10434   ZZcz 10758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2805  df-rab 2808  df-v 3080  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-sn 3987  df-pr 3989  df-op 3993  df-uni 4201  df-br 4402  df-iota 5490  df-fv 5535  df-ov 6204  df-neg 9710  df-z 10759
This theorem is referenced by:  zcn  10763  zrei  10764  zssre  10765  elnn0z  10771  elnnz1  10784  znnnlt1  10785  zletr  10801  znnsub  10803  znn0sub  10804  zltp1le  10806  zleltp1  10807  nn0ge0div  10823  zextle  10827  btwnnz  10830  suprzcl  10833  msqznn  10835  peano2uz2  10841  uzind  10845  uzindOLD  10848  fzind  10852  fnn0ind  10853  uzletr  10981  uzid  10987  uztrn  10989  uzneg  10991  uzss  10993  uztric  10994  uz11  10995  eluzp1m1  10996  eluzp1p1  10998  eluzaddi  10999  eluzsubi  11000  uzin  11005  peano2uz  11020  uzwo  11029  uzwoOLD  11030  eluz2b2  11039  uz2mulcl  11044  eqreznegel  11052  lbzbi  11055  uzsupss  11059  zmin  11061  zmax  11062  zbtwnre  11063  rebtwnz  11064  qre  11070  rpnnen1lem1  11091  rpnnen1lem2  11092  rpnnen1lem3  11093  rpnnen1lem5  11095  z2ge  11280  qbtwnre  11281  elfz1eq  11580  fzn  11584  fzen  11585  uzsubsubfz  11589  elfz0fzfz0  11603  fz0fzelfz0  11604  fznn0sub2  11606  fz0fzdiffz0  11607  elfzmlbm  11608  elfzmlbp  11609  fzaddel  11611  fzsuc2  11632  fzrev  11637  elfz1b  11645  fzm1  11658  fznuz  11660  uznfz  11661  elfzouz2  11684  fzonlt0  11690  fzospliti  11699  fzo1fzo0n0  11706  elfzo0z  11707  fzofzim  11711  fzossfzop1  11728  ssfzoulel  11739  ssfzo12bi  11740  elfzonelfzo  11745  elfzomelpfzo  11747  elfznelfzob  11749  fzostep1  11753  fllt  11774  flid  11775  flbi2  11783  flhalf  11792  dfceil2  11798  ceile  11806  ceilid  11808  quoremz  11812  intfracq  11816  uzsup  11820  zmod10  11842  zmodcl  11845  zmodfz  11847  modidmul0  11852  zmodid2  11854  modcyc  11861  modmul1  11870  modaddmodup  11880  modaddmodlo  11881  modaddmulmod  11883  leexp2  12036  zsqcl2  12061  iexpcyc  12088  brfi1uzind  12338  wrdsymb0  12378  ccatsymb  12400  swrdlend  12444  swrdnd  12445  swrd0  12446  swrdvalodm2  12452  swrdswrdlem  12472  swrdswrd  12473  swrdccatin2  12497  swrdccatin12lem2  12499  swrdccatin12lem3  12500  repswswrd  12541  cshwmodn  12551  cshwsublen  12552  cshwidxmod  12559  cshwidxm1  12562  repswcshw  12565  2cshw  12566  cshweqrep  12574  cshw1  12575  swrd2lsw  12671  nn0abscl  12920  rexuzre  12959  znnenlem  13613  dvdsval3  13658  moddvds  13661  absdvdsb  13670  dvdsabsb  13671  dvdsle  13697  alzdvds  13702  divalgmod  13729  bitsp1o  13748  gcdabs  13836  gcdabs1  13837  modgcd  13839  bezoutlem1  13841  algcvga  13873  isprm3  13891  sqnprm  13903  zgcdsq  13950  hashdvds  13969  modprm0  13992  modprmn0modprm0  13994  fldivp1  14078  zgz  14113  4sqlem4  14132  cshwshashlem2  14242  gexdvds  16205  zringunit  18040  zrngunit  18041  prmirred  18045  prmirredOLD  18048  znf1o  18110  dyadf  21205  dyadovol  21207  degltlem1  21677  coskpi  22116  cosne0  22120  relogexp  22178  cxpeq  22329  ppival2  22600  ppival2g  22601  ppiprm  22623  chtprm  22625  chtnprm  22626  ppip1le  22633  efexple  22754  lgsdir2lem4  22799  lgsne0  22806  lgsquadlem1  22827  lgsquadlem2  22828  2sqlem2  22837  rplogsumlem2  22868  pntrsumbnd  22949  axlowdim  23360  gxnval  23900  gxmodid  23919  rezh  26546  zrhre  26591  hashf2  26679  ballotlemfc0  27020  ballotlemfcc  27021  elfzm12  27465  fzp1nel  27542  mblfinlem1  28577  mblfinlem2  28578  dvtanlem  28590  itg2addnclem2  28593  nn0prpwlem  28666  fzmul  28785  fzadd2  28786  incsequz2  28794  ellz1  29254  lzunuz  29255  lzenom  29257  nerabdioph  29296  pell14qrgt0  29349  rmxycomplete  29407  monotuz  29431  monotoddzzfi  29432  oddcomabszz  29434  zindbi  29436  jm2.24  29455  congrep  29465  fzneg  29474  jm2.19  29491  climsuse  29930  stoweidlem26  29970  stoweidlem34  29978  nn01to3  30336  eluzge0nn0  30338  uzuzle  30339  uz3m2nn  30344  nn0pzuz  30345  elfz2z  30347  2elfz2melfz  30351  elfzlble  30357  elfzelfzlble  30358  el2fzo  30361  elfzom1elp1fzo  30367  eluzgtdifelfzo  30368  fzosplitprm1  30373  fsummmodsndifre  30388  mulmoddvds  30395  powm2modprm  30397  prmn2uzge3  30398  clwlkisclwwlklem2fv2  30594  clwlkisclwwlklem2a  30596  clwwlkext2edg  30613  wwlksubclwwlk  30615  zm1nn  30617  clwwisshclwwlem1  30618  difelfznle  30637  usg2cwwkdifex  30644  clwlkfclwwlk  30666  extwwlkfablem2  30820  numclwwlkovf2ex  30828  numclwlk1lem2f1  30836  frgrareg  30859  frgraregord013  30860  chfacfscmul0  31345  chfacfscmulgsum  31347  chfacfpmmul0  31349  chfacfpmmulgsum  31351
  Copyright terms: Public domain W3C validator