Theorem zsscn 12617

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

This proof depends on syntax axioms:   ⊆ wss 3908  ℂcc 11116  ℤcz 12609

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-resscn 11175

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426  df-neg 11462  df-z 12610

This theorem is used by:  zex  12618  elq  12992  zexpcl  14132  fsumzcl  15812  fprodzcl  16034  zrisefaccl  16100  zfallfaccl  16101  4sqlem11  17040  cygabl  19992  zringbas  21640  zring0  21645  fermltlchr  21716  lmbrf  23454  lmres  23494  sszcld  25012  lmmbrf  25458  iscauf  25476  caucfil  25479  lmclimf  25500  elqaalem3  26519  iaa  26525  aareccl  26526  wilthlem2  27270  wilthlem3  27271  lgsfcl2  27504  2sqlem6  27624  gsumzrsum  33416  znfermltl  33712  zringnm  34379  fsum2dsub  35025  reprsuc  35033  caures  38451  mzpexpmpt  43516  uzmptshftfval  45096  fzsscn  46070  dvnprodlem2  46701  elaa2lem  46987  sqrtnnaa  47644  oddibas  48978  2zrngbas  49047  2zrng0  49049