Theorem zsscn 12473

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

Syntax hints:   ⊆ wss 3902  ℂcc 11001  ℤcz 12465

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 2113  ax-9 2121  ax-ext 2703  ax-resscn 11060

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-neg 11344  df-z 12466

This theorem is referenced by:  zex  12474  elq  12845  zexpcl  13980  fsumzcl  15639  fprodzcl  15858  zrisefaccl  15924  zfallfaccl  15925  4sqlem11  16864  cygabl  19801  zringbas  21388  zring0  21393  fermltlchr  21464  lmbrf  23173  lmres  23213  sszcld  24731  lmmbrf  25187  iscauf  25205  caucfil  25208  lmclimf  25229  elqaalem3  26254  iaa  26258  aareccl  26259  wilthlem2  27004  wilthlem3  27005  lgsfcl2  27239  2sqlem6  27359  gsumzrsum  33034  znfermltl  33326  zringnm  33966  fsum2dsub  34615  reprsuc  34623  caures  37799  mzpexpmpt  42777  uzmptshftfval  44378  fzsscn  45351  dvnprodlem2  45984  elaa2lem  46270  oddibas  48203  2zrngbas  48272  2zrng0  48274