![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > zsscn | Structured version Visualization version GIF version |
Description: The integers are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.) |
Ref | Expression |
---|---|
zsscn | ⊢ ℤ ⊆ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zcn 12545 | . 2 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℂ) | |
2 | 1 | ssriv 3982 | 1 ⊢ ℤ ⊆ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ⊆ wss 3944 ℂcc 11090 ℤcz 12540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 ax-resscn 11149 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 df-v 3475 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4523 df-sn 4623 df-pr 4625 df-op 4629 df-uni 4902 df-br 5142 df-iota 6484 df-fv 6540 df-ov 7396 df-neg 11429 df-z 12541 |
This theorem is referenced by: zex 12549 elq 12916 zexpcl 14024 fsumzcl 15663 fprodzcl 15880 zrisefaccl 15946 zfallfaccl 15947 4sqlem11 16870 cygabl 19718 zringbas 20957 zring0 20961 lmbrf 22693 lmres 22733 sszcld 24262 lmmbrf 24708 iscauf 24726 caucfil 24729 lmclimf 24750 elqaalem3 25763 iaa 25767 aareccl 25768 wilthlem2 26500 wilthlem3 26501 lgsfcl2 26733 2sqlem6 26853 fermltlchr 32340 znfermltl 32341 zringnm 32769 fsum2dsub 33450 reprsuc 33458 caures 36433 mzpexpmpt 41254 uzmptshftfval 42876 fzsscn 43794 dvnprodlem1 44435 dvnprodlem2 44436 elaa2lem 44722 oddibas 46355 2zrngbas 46482 2zrng0 46484 |
Copyright terms: Public domain | W3C validator |