Theorem zsscn 12682

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

This proof depends on syntax axioms:   ⊆ wss 3899  ℂcc 11179  ℤcz 12674

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-resscn 11238

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-ov 7415  df-neg 11525  df-z 12675

This theorem is used by:  zex  12683  elq  13058  zexpcl  14199  fsumzcl  15881  fprodzcl  16101  zrisefaccl  16167  zfallfaccl  16168  4sqlem11  17113  cygabl  20085  zringbas  21739  zring0  21744  fermltlchr  21815  lmbrf  23558  lmres  23598  sszcld  25117  lmmbrf  25563  iscauf  25581  caucfil  25584  lmclimf  25605  elqaalem3  26626  iaaOLD  26634  aareccl  26635  wilthlem2  27378  wilthlem3  27379  lgsfcl2  27612  2sqlem6  27732  gsumzrsum  33608  znfermltl  33904  zringnm  34572  fsum2dsub  35219  reprsuc  35227  caures  38662  mzpexpmpt  43709  uzmptshftfval  45289  fzsscn  46270  dvnprodlem2  46901  elaa2lem  47187  sqrtnnaa  47857  oddibas  49214  2zrngbas  49283  2zrng0  49285