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 11382 | . 2 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℂ) | |
2 | 1 | ssriv 3607 | 1 ⊢ ℤ ⊆ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ⊆ wss 3574 ℂcc 9934 ℤcz 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 |
Copyright terms: Public domain | W3C validator |