Theorem zsscn 12544

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

Syntax hints:   ⊆ wss 3917  ℂcc 11073  ℤcz 12536

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 2702  ax-resscn 11132

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-neg 11415  df-z 12537

This theorem is referenced by:  zex  12545  elq  12916  zexpcl  14048  fsumzcl  15708  fprodzcl  15927  zrisefaccl  15993  zfallfaccl  15994  4sqlem11  16933  cygabl  19828  zringbas  21370  zring0  21375  fermltlchr  21446  lmbrf  23154  lmres  23194  sszcld  24713  lmmbrf  25169  iscauf  25187  caucfil  25190  lmclimf  25211  elqaalem3  26236  iaa  26240  aareccl  26241  wilthlem2  26986  wilthlem3  26987  lgsfcl2  27221  2sqlem6  27341  gsumzrsum  33006  znfermltl  33344  zringnm  33955  fsum2dsub  34605  reprsuc  34613  caures  37761  mzpexpmpt  42740  uzmptshftfval  44342  fzsscn  45316  dvnprodlem2  45952  elaa2lem  46238  oddibas  48165  2zrngbas  48234  2zrng0  48236