Theorem zsscn 12647

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

Syntax hints:   ⊆ wss 3976  ℂcc 11182  ℤcz 12639

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 2110  ax-9 2118  ax-ext 2711  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-neg 11523  df-z 12640

This theorem is referenced by:  zex  12648  elq  13015  zexpcl  14127  fsumzcl  15783  fprodzcl  16002  zrisefaccl  16068  zfallfaccl  16069  4sqlem11  17002  cygabl  19933  zringbas  21487  zring0  21492  fermltlchr  21567  lmbrf  23289  lmres  23329  sszcld  24858  lmmbrf  25315  iscauf  25333  caucfil  25336  lmclimf  25357  elqaalem3  26381  iaa  26385  aareccl  26386  wilthlem2  27130  wilthlem3  27131  lgsfcl2  27365  2sqlem6  27485  znfermltl  33359  zringnm  33904  fsum2dsub  34584  reprsuc  34592  caures  37720  mzpexpmpt  42701  uzmptshftfval  44315  fzsscn  45226  dvnprodlem1  45867  dvnprodlem2  45868  elaa2lem  46154  oddibas  47896  2zrngbas  47965  2zrng0  47967