Theorem zsscn 12603

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

This proof depends on syntax axioms:   ⊆ wss 3905  ℂcc 11102  ℤcz 12595

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-resscn 11161

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-neg 11448  df-z 12596

This theorem is used by:  zex  12604  elq  12978  zexpcl  14117  fsumzcl  15791  fprodzcl  16013  zrisefaccl  16079  zfallfaccl  16080  4sqlem11  17019  cygabl  19965  zringbas  21612  zring0  21617  fermltlchr  21688  lmbrf  23426  lmres  23466  sszcld  24984  lmmbrf  25430  iscauf  25448  caucfil  25451  lmclimf  25472  elqaalem3  26491  iaa  26497  aareccl  26498  wilthlem2  27242  wilthlem3  27243  lgsfcl2  27476  2sqlem6  27596  gsumzrsum  33394  znfermltl  33690  zringnm  34357  fsum2dsub  35003  reprsuc  35011  caures  38439  mzpexpmpt  43504  uzmptshftfval  45084  fzsscn  46058  dvnprodlem2  46689  elaa2lem  46975  sqrtnnaa  47632  oddibas  48966  2zrngbas  49035  2zrng0  49037