Theorem zsscn 11983

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

Syntax hints:   ⊆ wss 3935  ℂcc 10529  ℤcz 11975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-resscn 10588

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7153  df-neg 10867  df-z 11976

This theorem is referenced by:  zex  11984  elq  12344  zexpcl  13438  fsumzcl  15086  fprodzcl  15302  zrisefaccl  15368  zfallfaccl  15369  4sqlem11  16285  cygabl  19004  zringbas  20617  zring0  20621  lmbrf  21862  lmres  21902  sszcld  23419  lmmbrf  23859  iscauf  23877  caucfil  23880  lmclimf  23901  elqaalem3  24904  iaa  24908  aareccl  24909  wilthlem2  25640  wilthlem3  25641  lgsfcl2  25873  2sqlem6  25993  zringnm  31196  fsum2dsub  31873  reprsuc  31881  caures  35029  mzpexpmpt  39335  uzmptshftfval  40671  fzsscn  41571  dvnprodlem1  42224  dvnprodlem2  42225  elaa2lem  42512  oddibas  44074  2zrngbas  44201  2zrng0  44203