Theorem zsscn 11385

Description: The integers are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)

Assertion

Ref	Expression
zsscn	|- ZZ C_ CC

Proof of Theorem zsscn

Step	Hyp	Ref	Expression
1		zcn 11382	. 2 |- ( x e. ZZ -> x e. CC )
2	1	ssriv 3607	1 |- ZZ C_ CC

Syntax hints:   C_ wss 3574   CCcc 9934   ZZcz 11377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-neg 10269  df-z 11378

This theorem is referenced by:  zex  11386  elq  11790  zexpcl  12875  fsumzcl  14466  fprodzcl  14684  zrisefaccl  14751  zfallfaccl  14752  4sqlem11  15659  zringbas  19824  zring0  19828  lmbrf  21064  lmres  21104  sszcld  22620  lmmbrf  23060  iscauf  23078  caucfil  23081  lmclimf  23102  elqaalem3  24076  iaa  24080  aareccl  24081  wilthlem2  24795  wilthlem3  24796  lgsfcl2  25028  2sqlem6  25148  zringnm  30004  fsum2dsub  30685  reprsuc  30693  caures  33556  mzpexpmpt  37308  uzmptshftfval  38545  fzsscn  39526  dvnprodlem1  40161  dvnprodlem2  40162  elaa2lem  40450  oddibas  41813  2zrngbas  41936  2zrng0  41938