Theorem zsscn 12590

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

Syntax hints:   ⊆ wss 3907  ℂcc 11086  ℤcz 12582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-resscn 11145

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403  df-neg 11432  df-z 12583

This theorem is referenced by:  zex  12591  elq  12965  zexpcl  14103  fsumzcl  15776  fprodzcl  15998  zrisefaccl  16064  zfallfaccl  16065  4sqlem11  17005  cygabl  19952  zringbas  21563  zring0  21568  fermltlchr  21639  lmbrf  23378  lmres  23418  sszcld  24936  lmmbrf  25382  iscauf  25400  caucfil  25403  lmclimf  25424  elqaalem3  26443  iaa  26447  aareccl  26448  wilthlem2  27191  wilthlem3  27192  lgsfcl2  27425  2sqlem6  27545  gsumzrsum  33298  znfermltl  33596  zringnm  34265  fsum2dsub  34911  reprsuc  34919  caures  38271  mzpexpmpt  43338  uzmptshftfval  44920  fzsscn  45888  dvnprodlem2  46519  elaa2lem  46805  nthrucw  47460  oddibas  48793  2zrngbas  48862  2zrng0  48864