Theorem zsscn 12566

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

Syntax hints:   ⊆ wss 3949  ℂcc 11108  ℤcz 12558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-resscn 11167

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-neg 11447  df-z 12559

This theorem is referenced by:  zex  12567  elq  12934  zexpcl  14042  fsumzcl  15681  fprodzcl  15898  zrisefaccl  15964  zfallfaccl  15965  4sqlem11  16888  cygabl  19759  zringbas  21023  zring0  21028  lmbrf  22764  lmres  22804  sszcld  24333  lmmbrf  24779  iscauf  24797  caucfil  24800  lmclimf  24821  elqaalem3  25834  iaa  25838  aareccl  25839  wilthlem2  26573  wilthlem3  26574  lgsfcl2  26806  2sqlem6  26926  fermltlchr  32478  znfermltl  32479  zringnm  32938  fsum2dsub  33619  reprsuc  33627  caures  36628  mzpexpmpt  41483  uzmptshftfval  43105  fzsscn  44021  dvnprodlem1  44662  dvnprodlem2  44663  elaa2lem  44949  oddibas  46583  2zrngbas  46834  2zrng0  46836