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

Theorem zsscn 10861
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 10858 . 2  |-  ( x  e.  ZZ  ->  x  e.  CC )
21ssriv 3501 1  |-  ZZ  C_  CC
Colors of variables: wff setvar class
Syntax hints:    C_ wss 3469   CCcc 9479   ZZcz 10853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-resscn 9538
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-iota 5542  df-fv 5587  df-ov 6278  df-neg 9797  df-z 10854
This theorem is referenced by:  zex  10862  elq  11173  zexpcl  12137  seqshft  12868  fsumzcl  13506  4sqlem11  14321  zringbas  18255  zring0  18259  zrngbas  18261  zrng0  18265  dvdsrz  18268  zlpirlem1  18274  zlpirlem3  18276  lmbrf  19520  lmres  19560  sszcld  21050  lmmbrf  21429  iscauf  21447  caucfil  21450  lmclimf  21470  elqaalem3  22444  iaa  22448  aareccl  22449  wilthlem2  23064  wilthlem3  23065  lgsfcl2  23298  2sqlem6  23365  zaddsubgo  24882  zringnm  27426  zzsnmOLD  27428  cnzh  27437  rezh  27438  fprodzcl  28513  zrisefaccl  28569  zfallfaccl  28570  caures  29707  mzpexpmpt  30132  mzpmfpOLD  30135
  Copyright terms: Public domain W3C validator