Theorem zsscn 12496

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

Syntax hints:   ⊆ wss 3901  ℂcc 11024  ℤcz 12488

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 2708  ax-resscn 11083

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-neg 11367  df-z 12489

This theorem is referenced by:  zex  12497  elq  12863  zexpcl  13999  fsumzcl  15658  fprodzcl  15877  zrisefaccl  15943  zfallfaccl  15944  4sqlem11  16883  cygabl  19820  zringbas  21408  zring0  21413  fermltlchr  21484  lmbrf  23204  lmres  23244  sszcld  24762  lmmbrf  25218  iscauf  25236  caucfil  25239  lmclimf  25260  elqaalem3  26285  iaa  26289  aareccl  26290  wilthlem2  27035  wilthlem3  27036  lgsfcl2  27270  2sqlem6  27390  gsumzrsum  33148  znfermltl  33447  zringnm  34115  fsum2dsub  34764  reprsuc  34772  caures  37957  mzpexpmpt  42983  uzmptshftfval  44583  fzsscn  45555  dvnprodlem2  46187  elaa2lem  46473  nthrucw  47126  oddibas  48415  2zrngbas  48484  2zrng0  48486