Theorem zsscn 12537

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

Syntax hints:   ⊆ wss 3914  ℂcc 11066  ℤcz 12529

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 11125

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-neg 11408  df-z 12530

This theorem is referenced by:  zex  12538  elq  12909  zexpcl  14041  fsumzcl  15701  fprodzcl  15920  zrisefaccl  15986  zfallfaccl  15987  4sqlem11  16926  cygabl  19821  zringbas  21363  zring0  21368  fermltlchr  21439  lmbrf  23147  lmres  23187  sszcld  24706  lmmbrf  25162  iscauf  25180  caucfil  25183  lmclimf  25204  elqaalem3  26229  iaa  26233  aareccl  26234  wilthlem2  26979  wilthlem3  26980  lgsfcl2  27214  2sqlem6  27334  gsumzrsum  32999  znfermltl  33337  zringnm  33948  fsum2dsub  34598  reprsuc  34606  caures  37754  mzpexpmpt  42733  uzmptshftfval  44335  fzsscn  45309  dvnprodlem2  45945  elaa2lem  46231  oddibas  48161  2zrngbas  48230  2zrng0  48232