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

Theorem zssre 10674
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 10671 . 2  |-  ( x  e.  ZZ  ->  x  e.  RR )
21ssriv 3381 1  |-  ZZ  C_  RR
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3349   RRcr 9302   ZZcz 10667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rex 2742  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-iota 5402  df-fv 5447  df-ov 6115  df-neg 9619  df-z 10668
This theorem is referenced by:  suprzcl  10742  zred  10768  uzwo2  10940  uzinfmi  10955  infmssuzle  10958  infmssuzcl  10959  lbzbi  10964  suprzub  10967  uzwo3  10969  rpnnen1lem3  11002  rpnnen1lem5  11004  fzval2  11461  flval3  11684  uzsup  11723  expcan  11937  ltexp2  11938  seqcoll  12237  limsupgre  12980  rlimclim  13045  isercolllem1  13163  isercolllem2  13164  isercoll  13166  caurcvg  13175  caucvg  13177  summolem2a  13213  summolem2  13214  zsum  13216  fsumcvg3  13227  climfsum  13304  1arith  14009  pgpssslw  16134  gsumval3OLD  16403  gsumval3  16406  zntoslem  18011  zcld  20412  mbflimsup  21166  ig1pdvds  21670  aacjcl  21815  aalioulem3  21822  qqhre  26468  ballotlemfc0  26897  ballotlemfcc  26898  ballotlemiex  26906  erdszelem4  27104  erdszelem8  27108  supfz  27408  inffz  27409  prodmolem2a  27469  prodmolem2  27470  zprod  27472  irrapxlem1  29189  monotuz  29308  monotoddzzfi  29309  rmyeq0  29322  rmyeq  29323  lermy  29324  suprfinzcl  30774
  Copyright terms: Public domain W3C validator