Theorem zsscn 12704

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

This proof depends on syntax axioms:   ⊆ wss 3895  ℂcc 11201  ℤcz 12696

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-resscn 11260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-neg 11547  df-z 12697

This theorem is used by:  zex  12705  elq  13080  zexpcl  14222  fsumzcl  15906  fprodzcl  16126  zrisefaccl  16192  zfallfaccl  16193  4sqlem11  17138  cygabl  20110  zringbas  21764  zring0  21769  fermltlchr  21840  lmbrf  23583  lmres  23623  sszcld  25142  lmmbrf  25588  iscauf  25606  caucfil  25609  lmclimf  25630  elqaalem3  26649  iaaOLD  26657  aareccl  26658  wilthlem2  27401  wilthlem3  27402  lgsfcl2  27635  2sqlem6  27755  gsumzrsum  33672  znfermltl  33968  zringnm  34636  fsum2dsub  35282  reprsuc  35290  caures  38787  mzpexpmpt  43849  uzmptshftfval  45423  fzsscn  46420  dvnprodlem2  47050  elaa2lem  47336  sqrtnnaa  48006  oddibas  49363  2zrngbas  49432  2zrng0  49434