Theorem zsscn 11977

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

Syntax hints:   ⊆ wss 3881  ℂcc 10524  ℤcz 11969

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-resscn 10583

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-neg 10862  df-z 11970

This theorem is referenced by:  zex  11978  elq  12338  zexpcl  13440  fsumzcl  15084  fprodzcl  15300  zrisefaccl  15366  zfallfaccl  15367  4sqlem11  16281  cygabl  19003  zringbas  20169  zring0  20173  lmbrf  21865  lmres  21905  sszcld  23422  lmmbrf  23866  iscauf  23884  caucfil  23887  lmclimf  23908  elqaalem3  24917  iaa  24921  aareccl  24922  wilthlem2  25654  wilthlem3  25655  lgsfcl2  25887  2sqlem6  26007  zringnm  31311  fsum2dsub  31988  reprsuc  31996  caures  35198  mzpexpmpt  39686  uzmptshftfval  41050  fzsscn  41943  dvnprodlem1  42588  dvnprodlem2  42589  elaa2lem  42875  oddibas  44433  2zrngbas  44560  2zrng0  44562