Theorem zsscn 11674

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

Syntax hints:   ⊆ wss 3769  ℂcc 10222  ℤcz 11666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-resscn 10281

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-rex 3095  df-rab 3098  df-v 3387  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4844  df-iota 6064  df-fv 6109  df-ov 6881  df-neg 10559  df-z 11667

This theorem is referenced by:  zex  11675  elq  12035  zexpcl  13129  fsumzcl  14807  fprodzcl  15021  zrisefaccl  15087  zfallfaccl  15088  4sqlem11  15992  zringbas  20146  zring0  20150  lmbrf  21393  lmres  21433  sszcld  22948  lmmbrf  23388  iscauf  23406  caucfil  23409  lmclimf  23430  elqaalem3  24417  iaa  24421  aareccl  24422  wilthlem2  25147  wilthlem3  25148  lgsfcl2  25380  2sqlem6  25500  zringnm  30520  fsum2dsub  31205  reprsuc  31213  caures  34043  mzpexpmpt  38094  uzmptshftfval  39327  fzsscn  40270  dvnprodlem1  40905  dvnprodlem2  40906  elaa2lem  41193  oddibas  42612  2zrngbas  42735  2zrng0  42737