Theorem zsscn 12257

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

Syntax hints:   ⊆ wss 3883  ℂcc 10800  ℤcz 12249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-neg 11138  df-z 12250

This theorem is referenced by:  zex  12258  elq  12619  zexpcl  13725  fsumzcl  15375  fprodzcl  15592  zrisefaccl  15658  zfallfaccl  15659  4sqlem11  16584  cygabl  19406  zringbas  20588  zring0  20592  lmbrf  22319  lmres  22359  sszcld  23886  lmmbrf  24331  iscauf  24349  caucfil  24352  lmclimf  24373  elqaalem3  25386  iaa  25390  aareccl  25391  wilthlem2  26123  wilthlem3  26124  lgsfcl2  26356  2sqlem6  26476  znfermltl  31464  zringnm  31810  fsum2dsub  32487  reprsuc  32495  caures  35845  mzpexpmpt  40483  uzmptshftfval  41853  fzsscn  42740  dvnprodlem1  43377  dvnprodlem2  43378  elaa2lem  43664  oddibas  45255  2zrngbas  45382  2zrng0  45384