Theorem zsscn 12600

Description: The integers are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)

Assertion

Ref	Expression
zsscn	⊢ ℤ ⊆ ℂ

Proof of Theorem zsscn

Step	Hyp	Ref	Expression
1		zcn 12597	. 2 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℂ)
2	1	ssriv 3942	1 ⊢ ℤ ⊆ ℂ

Syntax hints:   ⊆ wss 3906  ℂcc 11099  ℤcz 12592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11158

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-neg 11445  df-z 12593

This theorem is referenced by:  zex  12601  elq  12975  zexpcl  14114  fsumzcl  15788  fprodzcl  16010  zrisefaccl  16076  zfallfaccl  16077  4sqlem11  17016  cygabl  19962  zringbas  21584  zring0  21589  fermltlchr  21660  lmbrf  23398  lmres  23438  sszcld  24956  lmmbrf  25402  iscauf  25420  caucfil  25423  lmclimf  25444  elqaalem3  26463  iaa  26467  aareccl  26468  wilthlem2  27211  wilthlem3  27212  lgsfcl2  27445  2sqlem6  27565  gsumzrsum  33363  znfermltl  33659  zringnm  34326  fsum2dsub  34972  reprsuc  34980  caures  38389  mzpexpmpt  43456  uzmptshftfval  45036  fzsscn  46010  dvnprodlem2  46641  elaa2lem  46927  nthrucw  47582  oddibas  48915  2zrngbas  48984  2zrng0  48986