Theorem zsscn 12573

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

Syntax hints:   ⊆ wss 3904  ℂcc 11068  ℤcz 12565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-resscn 11127

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395  df-neg 11414  df-z 12566

This theorem is referenced by:  zex  12574  elq  12948  zexpcl  14086  fsumzcl  15745  fprodzcl  15967  zrisefaccl  16033  zfallfaccl  16034  4sqlem11  16974  cygabl  19914  zringbas  21485  zring0  21490  fermltlchr  21561  lmbrf  23300  lmres  23340  sszcld  24858  lmmbrf  25304  iscauf  25322  caucfil  25325  lmclimf  25346  elqaalem3  26362  iaa  26366  aareccl  26367  wilthlem2  27110  wilthlem3  27111  lgsfcl2  27344  2sqlem6  27464  gsumzrsum  33206  znfermltl  33513  zringnm  34216  fsum2dsub  34865  reprsuc  34873  caures  38223  mzpexpmpt  43290  uzmptshftfval  44886  fzsscn  45854  dvnprodlem2  46485  elaa2lem  46771  nthrucw  47426  oddibas  48759  2zrngbas  48828  2zrng0  48830