Theorem zsscn 12467

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

Syntax hints:   ⊆ wss 3899  ℂcc 10995  ℤcz 12459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-resscn 11054

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3393  df-v 3435  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5089  df-iota 6432  df-fv 6484  df-ov 7343  df-neg 11338  df-z 12460

This theorem is referenced by:  zex  12468  elq  12839  zexpcl  13971  fsumzcl  15629  fprodzcl  15848  zrisefaccl  15914  zfallfaccl  15915  4sqlem11  16854  cygabl  19757  zringbas  21344  zring0  21349  fermltlchr  21420  lmbrf  23129  lmres  23169  sszcld  24687  lmmbrf  25143  iscauf  25161  caucfil  25164  lmclimf  25185  elqaalem3  26210  iaa  26214  aareccl  26215  wilthlem2  26960  wilthlem3  26961  lgsfcl2  27195  2sqlem6  27315  gsumzrsum  33007  znfermltl  33299  zringnm  33939  fsum2dsub  34588  reprsuc  34596  caures  37757  mzpexpmpt  42735  uzmptshftfval  44336  fzsscn  45309  dvnprodlem2  45942  elaa2lem  46228  oddibas  48171  2zrngbas  48240  2zrng0  48242