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

Theorem zssre 10245
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 10242 . 2  |-  ( x  e.  ZZ  ->  x  e.  RR )
21ssriv 3312 1  |-  ZZ  C_  RR
Colors of variables: wff set class
Syntax hints:    C_ wss 3280   RRcr 8945   ZZcz 10238
This theorem is referenced by:  suprzcl  10305  zred  10331  uzwo2  10497  uzinfmi  10511  infmssuzle  10514  infmssuzcl  10515  lbzbi  10520  suprzub  10523  uzwo3  10525  rpnnen1lem3  10558  rpnnen1lem5  10560  fzval2  11002  flval3  11177  uzsup  11199  expcan  11387  ltexp2  11388  seqcoll  11667  limsupgre  12230  rlimclim  12295  isercolllem1  12413  isercolllem2  12414  isercoll  12416  caurcvg  12425  caucvg  12427  summolem2a  12464  summolem2  12465  zsum  12467  fsumcvg3  12478  climfsum  12554  1arith  13250  pgpssslw  15203  gsumval3  15469  zntoslem  16792  zcld  18797  mbflimsup  19511  ig1pdvds  20052  aacjcl  20197  aalioulem3  20204  qqhre  24339  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemiex  24712  erdszelem4  24833  erdszelem8  24837  supfz  25152  inffz  25153  prodmolem2a  25213  prodmolem2  25214  zprod  25216  irrapxlem1  26775  monotuz  26894  monotoddzzfi  26895  rmyeq0  26908  rmyeq  26909  lermy  26910
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-neg 9250  df-z 10239
  Copyright terms: Public domain W3C validator