Theorem zsscn 12508

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

Syntax hints:   ⊆ wss 3903  ℂcc 11036  ℤcz 12500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-neg 11379  df-z 12501

This theorem is referenced by:  zex  12509  elq  12875  zexpcl  14011  fsumzcl  15670  fprodzcl  15889  zrisefaccl  15955  zfallfaccl  15956  4sqlem11  16895  cygabl  19832  zringbas  21420  zring0  21425  fermltlchr  21496  lmbrf  23216  lmres  23256  sszcld  24774  lmmbrf  25230  iscauf  25248  caucfil  25251  lmclimf  25272  elqaalem3  26297  iaa  26301  aareccl  26302  wilthlem2  27047  wilthlem3  27048  lgsfcl2  27282  2sqlem6  27402  gsumzrsum  33158  znfermltl  33458  zringnm  34135  fsum2dsub  34784  reprsuc  34792  caures  38005  mzpexpmpt  43096  uzmptshftfval  44696  fzsscn  45667  dvnprodlem2  46299  elaa2lem  46585  nthrucw  47238  oddibas  48527  2zrngbas  48596  2zrng0  48598