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 11694 | . 2 ⊢ 8 = (7 + 1) | |
2 | 7cn 11719 | . . 3 ⊢ 7 ∈ ℂ | |
3 | ax-1cn 10583 | . . 3 ⊢ 1 ∈ ℂ | |
4 | 2, 3 | addcli 10635 | . 2 ⊢ (7 + 1) ∈ ℂ |
5 | 1, 4 | eqeltri 2906 | 1 ⊢ 8 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 (class class class)co 7145 ℂcc 10523 1c1 10526 + caddc 10528 7c7 11685 8c8 11686 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 ax-1cn 10583 ax-addcl 10585 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 df-clel 2890 df-2 11688 df-3 11689 df-4 11690 df-5 11691 df-6 11692 df-7 11693 df-8 11694 |
This theorem is referenced by: 9cn 11725 9m1e8 11759 8p2e10 12166 8t2e16 12201 8t5e40 12204 cos2bnd 15529 2exp16 16412 139prm 16445 163prm 16446 317prm 16447 631prm 16448 1259lem2 16453 1259lem3 16454 1259lem4 16455 1259lem5 16456 2503lem2 16459 2503lem3 16460 2503prm 16461 4001lem1 16462 4001lem2 16463 4001prm 16466 quart1cl 25359 quart1lem 25360 quart1 25361 quartlem1 25362 log2tlbnd 25450 log2ublem3 25453 log2ub 25454 bposlem8 25794 lgsdir2lem1 25828 lgsdir2lem5 25832 2lgslem3a 25899 2lgslem3b 25900 2lgslem3c 25901 2lgslem3d 25902 2lgslem3a1 25903 2lgslem3b1 25904 2lgslem3c1 25905 2lgslem3d1 25906 2lgsoddprmlem1 25911 2lgsoddprmlem2 25912 2lgsoddprmlem3a 25913 2lgsoddprmlem3b 25914 2lgsoddprmlem3c 25915 2lgsoddprmlem3d 25916 ex-exp 28156 hgt750lem2 31822 ex-decpmul 39056 fmtno5lem4 43595 257prm 43600 fmtnoprmfac2lem1 43605 fmtno4prmfac 43611 fmtno4nprmfac193 43613 fmtno5faclem3 43620 m3prm 43631 139prmALT 43636 127prm 43640 m7prm 43641 2exp11 43642 5tcu2e40 43657 2exp340mod341 43775 8exp8mod9 43778 nfermltl8rev 43784 evengpop3 43840 tgoldbachlt 43858 |
Copyright terms: Public domain | W3C validator |