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

Theorem zssre 10641
Description: The integers are a subset of the reals. (Contributed by NM, 2-Aug-2004.)
Assertion
Ref Expression
zssre  |-  ZZ  C_  RR

Proof of Theorem zssre
StepHypRef Expression
1 zre 10638 . 2  |-  ( x  e.  ZZ  ->  x  e.  RR )
21ssriv 3348 1  |-  ZZ  C_  RR
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3316   RRcr 9269   ZZcz 10634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083  df-neg 9586  df-z 10635
This theorem is referenced by:  suprzcl  10709  zred  10735  uzwo2  10907  uzinfmi  10922  infmssuzle  10925  infmssuzcl  10926  lbzbi  10931  suprzub  10934  uzwo3  10936  rpnnen1lem3  10969  rpnnen1lem5  10971  fzval2  11427  flval3  11647  uzsup  11686  expcan  11900  ltexp2  11901  seqcoll  12200  limsupgre  12943  rlimclim  13008  isercolllem1  13126  isercolllem2  13127  isercoll  13129  caurcvg  13138  caucvg  13140  summolem2a  13176  summolem2  13177  zsum  13179  fsumcvg3  13190  climfsum  13266  1arith  13971  pgpssslw  16093  gsumval3OLD  16362  gsumval3  16365  zntoslem  17831  zcld  20232  mbflimsup  20986  ig1pdvds  21533  aacjcl  21678  aalioulem3  21685  qqhre  26300  ballotlemfc0  26723  ballotlemfcc  26724  ballotlemiex  26732  erdszelem4  26930  erdszelem8  26934  supfz  27233  inffz  27234  prodmolem2a  27294  prodmolem2  27295  zprod  27297  irrapxlem1  29008  monotuz  29127  monotoddzzfi  29128  rmyeq0  29141  rmyeq  29142  lermy  29143
  Copyright terms: Public domain W3C validator