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

Theorem zsscn 10079
Description: The integers are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
Assertion
Ref Expression
zsscn  |-  ZZ  C_  CC

Proof of Theorem zsscn
StepHypRef Expression
1 zcn 10076 . 2  |-  ( x  e.  ZZ  ->  x  e.  CC )
21ssriv 3218 1  |-  ZZ  C_  CC
Colors of variables: wff set class
Syntax hints:    C_ wss 3186   CCcc 8780   ZZcz 10071
This theorem is referenced by:  zex  10080  elq  10365  zexpcl  11165  seqshft  11627  fsumzcl  12255  4sqlem11  13049  dvdsrz  16496  zlpirlem1  16497  zlpirlem3  16499  chrrhm  16541  domnchr  16542  lmbrf  17046  lmres  17084  lmmbrf  18741  iscauf  18759  caucfil  18762  lmclimf  18782  elqaalem3  19754  iaa  19758  aareccl  19759  wilthlem2  20360  wilthlem3  20361  dchrzrhmul  20538  lgsfcl2  20594  lgsdchr  20640  2sqlem6  20661  zaddsubgo  21074  zzsbase  23520  zzs0  23524  zzsnm  23526  qqhval2lem  23560  qqhghm  23567  qqhrhm  23568  fprodzcl  24457  caures  25625  mzpexpmpt  25971  mzpmfp  25973
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-resscn 8839
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-iota 5256  df-fv 5300  df-ov 5903  df-neg 9085  df-z 10072
  Copyright terms: Public domain W3C validator