Theorem zsscn 12483

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 12480	. 2 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℂ)
2	1	ssriv 3934	1 ⊢ ℤ ⊆ ℂ

Syntax hints:   ⊆ wss 3898  ℂcc 11011  ℤcz 12475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-resscn 11070

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355  df-neg 11354  df-z 12476

This theorem is referenced by:  zex  12484  elq  12850  zexpcl  13985  fsumzcl  15644  fprodzcl  15863  zrisefaccl  15929  zfallfaccl  15930  4sqlem11  16869  cygabl  19805  zringbas  21392  zring0  21397  fermltlchr  21468  lmbrf  23176  lmres  23216  sszcld  24734  lmmbrf  25190  iscauf  25208  caucfil  25211  lmclimf  25232  elqaalem3  26257  iaa  26261  aareccl  26262  wilthlem2  27007  wilthlem3  27008  lgsfcl2  27242  2sqlem6  27362  gsumzrsum  33046  znfermltl  33338  zringnm  33992  fsum2dsub  34641  reprsuc  34649  caures  37820  mzpexpmpt  42862  uzmptshftfval  44463  fzsscn  45436  dvnprodlem2  46069  elaa2lem  46355  nthrucw  47008  oddibas  48297  2zrngbas  48366  2zrng0  48368