Theorem zsscn 12530

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

Syntax hints:   ⊆ wss 3890  ℂcc 11034  ℤcz 12522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-resscn 11093

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-neg 11378  df-z 12523

This theorem is referenced by:  zex  12531  elq  12898  zexpcl  14036  fsumzcl  15695  fprodzcl  15917  zrisefaccl  15983  zfallfaccl  15984  4sqlem11  16924  cygabl  19864  zringbas  21435  zring0  21440  fermltlchr  21511  lmbrf  23250  lmres  23290  sszcld  24808  lmmbrf  25254  iscauf  25272  caucfil  25275  lmclimf  25296  elqaalem3  26312  iaa  26316  aareccl  26317  wilthlem2  27057  wilthlem3  27058  lgsfcl2  27291  2sqlem6  27411  gsumzrsum  33153  znfermltl  33456  zringnm  34149  fsum2dsub  34798  reprsuc  34806  caures  38134  mzpexpmpt  43201  uzmptshftfval  44797  fzsscn  45766  dvnprodlem2  46397  elaa2lem  46683  nthrucw  47338  oddibas  48671  2zrngbas  48740  2zrng0  48742