Theorem zsscn 12621

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

Syntax hints:   ⊆ wss 3951  ℂcc 11153  ℤcz 12613

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-resscn 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-neg 11495  df-z 12614

This theorem is referenced by:  zex  12622  elq  12992  zexpcl  14117  fsumzcl  15771  fprodzcl  15990  zrisefaccl  16056  zfallfaccl  16057  4sqlem11  16993  cygabl  19909  zringbas  21464  zring0  21469  fermltlchr  21544  lmbrf  23268  lmres  23308  sszcld  24839  lmmbrf  25296  iscauf  25314  caucfil  25317  lmclimf  25338  elqaalem3  26363  iaa  26367  aareccl  26368  wilthlem2  27112  wilthlem3  27113  lgsfcl2  27347  2sqlem6  27467  gsumzrsum  33062  znfermltl  33394  zringnm  33957  fsum2dsub  34622  reprsuc  34630  caures  37767  mzpexpmpt  42756  uzmptshftfval  44365  fzsscn  45323  dvnprodlem2  45962  elaa2lem  46248  oddibas  48089  2zrngbas  48158  2zrng0  48160