Theorem zsscn 12532

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

Syntax hints:   ⊆ wss 3889  ℂcc 11036  ℤcz 12524

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 2708  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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-neg 11380  df-z 12525

This theorem is referenced by:  zex  12533  elq  12900  zexpcl  14038  fsumzcl  15697  fprodzcl  15919  zrisefaccl  15985  zfallfaccl  15986  4sqlem11  16926  cygabl  19866  zringbas  21433  zring0  21438  fermltlchr  21509  lmbrf  23225  lmres  23265  sszcld  24783  lmmbrf  25229  iscauf  25247  caucfil  25250  lmclimf  25271  elqaalem3  26287  iaa  26291  aareccl  26292  wilthlem2  27032  wilthlem3  27033  lgsfcl2  27266  2sqlem6  27386  gsumzrsum  33126  znfermltl  33426  zringnm  34102  fsum2dsub  34751  reprsuc  34759  caures  38081  mzpexpmpt  43177  uzmptshftfval  44773  fzsscn  45744  dvnprodlem2  46375  elaa2lem  46661  nthrucw  47316  oddibas  48649  2zrngbas  48718  2zrng0  48720