![]() |
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 a complex number. (Contributed by David A. Wheeler, 8-Dec-2018.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.) |
Ref | Expression |
---|---|
8cn | ⊢ 8 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-8 11515 | . 2 ⊢ 8 = (7 + 1) | |
2 | 7cn 11544 | . . 3 ⊢ 7 ∈ ℂ | |
3 | ax-1cn 10399 | . . 3 ⊢ 1 ∈ ℂ | |
4 | 2, 3 | addcli 10452 | . 2 ⊢ (7 + 1) ∈ ℂ |
5 | 1, 4 | eqeltri 2864 | 1 ⊢ 8 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2051 (class class class)co 6982 ℂcc 10339 1c1 10342 + caddc 10344 7c7 11506 8c8 11507 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-ext 2752 ax-1cn 10399 ax-addcl 10401 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1744 df-cleq 2773 df-clel 2848 df-2 11509 df-3 11510 df-4 11511 df-5 11512 df-6 11513 df-7 11514 df-8 11515 |
This theorem is referenced by: 9cn 11552 9m1e8 11587 8p2e10 11999 8t2e16 12034 8t5e40 12037 cos2bnd 15407 2exp16 16286 139prm 16319 163prm 16320 317prm 16321 631prm 16322 1259lem2 16327 1259lem3 16328 1259lem4 16329 1259lem5 16330 2503lem2 16333 2503lem3 16334 2503prm 16335 4001lem1 16336 4001lem2 16337 4001prm 16340 quart1cl 25148 quart1lem 25149 quart1 25150 quartlem1 25151 log2tlbnd 25240 log2ublem3 25243 log2ub 25244 bposlem8 25584 lgsdir2lem1 25618 lgsdir2lem5 25622 2lgslem3a 25689 2lgslem3b 25690 2lgslem3c 25691 2lgslem3d 25692 2lgslem3a1 25693 2lgslem3b1 25694 2lgslem3c1 25695 2lgslem3d1 25696 2lgsoddprmlem1 25701 2lgsoddprmlem2 25702 2lgsoddprmlem3a 25703 2lgsoddprmlem3b 25704 2lgsoddprmlem3c 25705 2lgsoddprmlem3d 25706 ex-exp 28022 hgt750lem2 31603 ex-decpmul 38651 fmtno5lem4 43121 257prm 43126 fmtnoprmfac2lem1 43131 fmtno4prmfac 43137 fmtno4nprmfac193 43139 fmtno5faclem3 43146 m3prm 43157 139prmALT 43162 127prm 43166 m7prm 43167 2exp11 43168 5tcu2e40 43183 2exp340mod341 43301 8exp8mod9 43304 nfermltl8rev 43310 evengpop3 43366 tgoldbachlt 43384 |
Copyright terms: Public domain | W3C validator |