![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 8cn | Structured version Visualization version GIF version |
Description: The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
8cn | ⊢ 8 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 8re 11143 | . 2 ⊢ 8 ∈ ℝ | |
2 | 1 | recni 10090 | 1 ⊢ 8 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2030 ℂcc 9972 8c8 11114 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-resscn 10031 ax-1cn 10032 ax-icn 10033 ax-addcl 10034 ax-addrcl 10035 ax-mulcl 10036 ax-mulrcl 10037 ax-i2m1 10042 ax-1ne0 10043 ax-rrecex 10046 ax-cnre 10047 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ne 2824 df-ral 2946 df-rex 2947 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-uni 4469 df-br 4686 df-iota 5889 df-fv 5934 df-ov 6693 df-2 11117 df-3 11118 df-4 11119 df-5 11120 df-6 11121 df-7 11122 df-8 11123 |
This theorem is referenced by: 9m1e8 11181 8p2e10OLD 11212 8p2e10 11648 8t2e16 11692 8t5e40 11695 8t5e40OLD 11696 cos2bnd 14962 2exp16 15844 139prm 15878 163prm 15879 317prm 15880 631prm 15881 1259lem2 15886 1259lem3 15887 1259lem4 15888 1259lem5 15889 2503lem2 15892 2503lem3 15893 2503prm 15894 4001lem1 15895 4001lem2 15896 4001prm 15899 quart1cl 24626 quart1lem 24627 quart1 24628 quartlem1 24629 log2tlbnd 24717 log2ublem3 24720 log2ub 24721 bposlem8 25061 lgsdir2lem1 25095 lgsdir2lem3 25097 lgsdir2lem5 25099 2lgslem3a 25166 2lgslem3b 25167 2lgslem3c 25168 2lgslem3d 25169 2lgslem3a1 25170 2lgslem3b1 25171 2lgslem3c1 25172 2lgslem3d1 25173 2lgsoddprmlem1 25178 2lgsoddprmlem2 25179 2lgsoddprmlem3a 25180 2lgsoddprmlem3b 25181 2lgsoddprmlem3c 25182 2lgsoddprmlem3d 25183 ex-exp 27437 hgt750lem2 30858 fmtno5lem4 41793 257prm 41798 fmtnoprmfac2lem1 41803 fmtno4prmfac 41809 fmtno4nprmfac193 41811 fmtno5faclem3 41818 m3prm 41831 139prmALT 41836 127prm 41840 m7prm 41841 2exp11 41842 5tcu2e40 41857 evengpop3 42011 tgoldbachlt 42029 tgoldbachltOLD 42035 |
Copyright terms: Public domain | W3C validator |