Theorem zsscn 12497

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

Syntax hints:   ⊆ wss 3905  ℂcc 11026  ℤcz 12489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-neg 11368  df-z 12490

This theorem is referenced by:  zex  12498  elq  12869  zexpcl  14001  fsumzcl  15660  fprodzcl  15879  zrisefaccl  15945  zfallfaccl  15946  4sqlem11  16885  cygabl  19788  zringbas  21378  zring0  21383  fermltlchr  21454  lmbrf  23163  lmres  23203  sszcld  24722  lmmbrf  25178  iscauf  25196  caucfil  25199  lmclimf  25220  elqaalem3  26245  iaa  26249  aareccl  26250  wilthlem2  26995  wilthlem3  26996  lgsfcl2  27230  2sqlem6  27350  gsumzrsum  33025  znfermltl  33313  zringnm  33924  fsum2dsub  34574  reprsuc  34582  caures  37739  mzpexpmpt  42718  uzmptshftfval  44319  fzsscn  45293  dvnprodlem2  45929  elaa2lem  46215  oddibas  48158  2zrngbas  48227  2zrng0  48229