Theorem zsscn 12355

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

Syntax hints:   ⊆ wss 3889  ℂcc 10897  ℤcz 12347

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-ext 2704  ax-resscn 10956

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2063  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3224  df-v 3436  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4260  df-if 4463  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4842  df-br 5078  df-iota 6399  df-fv 6455  df-ov 7298  df-neg 11236  df-z 12348

This theorem is referenced by:  zex  12356  elq  12718  zexpcl  13825  fsumzcl  15475  fprodzcl  15692  zrisefaccl  15758  zfallfaccl  15759  4sqlem11  16684  cygabl  19519  zringbas  20704  zring0  20708  lmbrf  22439  lmres  22479  sszcld  24008  lmmbrf  24454  iscauf  24472  caucfil  24475  lmclimf  24496  elqaalem3  25509  iaa  25513  aareccl  25514  wilthlem2  26246  wilthlem3  26247  lgsfcl2  26479  2sqlem6  26599  znfermltl  31590  zringnm  31936  fsum2dsub  32615  reprsuc  32623  caures  35946  mzpexpmpt  40590  uzmptshftfval  41988  fzsscn  42884  dvnprodlem1  43522  dvnprodlem2  43523  elaa2lem  43809  oddibas  45407  2zrngbas  45534  2zrng0  45536