![]() |
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 12314 | . 2 ⊢ 8 = (7 + 1) | |
2 | 7cn 12339 | . . 3 ⊢ 7 ∈ ℂ | |
3 | ax-1cn 11198 | . . 3 ⊢ 1 ∈ ℂ | |
4 | 2, 3 | addcli 11252 | . 2 ⊢ (7 + 1) ∈ ℂ |
5 | 1, 4 | eqeltri 2821 | 1 ⊢ 8 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2098 (class class class)co 7419 ℂcc 11138 1c1 11141 + caddc 11143 7c7 12305 8c8 12306 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-1cn 11198 ax-addcl 11200 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-cleq 2717 df-clel 2802 df-2 12308 df-3 12309 df-4 12310 df-5 12311 df-6 12312 df-7 12313 df-8 12314 |
This theorem is referenced by: 9cn 12345 9m1e8 12379 8p2e10 12790 8t2e16 12825 8t5e40 12828 cos2bnd 16168 2exp11 17062 2exp16 17063 139prm 17096 163prm 17097 317prm 17098 631prm 17099 1259lem2 17104 1259lem3 17105 1259lem4 17106 1259lem5 17107 2503lem2 17110 2503lem3 17111 2503prm 17112 4001lem1 17113 4001lem2 17114 4001prm 17117 quart1cl 26831 quart1lem 26832 quart1 26833 quartlem1 26834 log2tlbnd 26922 log2ublem3 26925 log2ub 26926 bposlem8 27269 lgsdir2lem1 27303 lgsdir2lem5 27307 2lgslem3a 27374 2lgslem3b 27375 2lgslem3c 27376 2lgslem3d 27377 2lgslem3a1 27378 2lgslem3b1 27379 2lgslem3c1 27380 2lgslem3d1 27381 2lgsoddprmlem1 27386 2lgsoddprmlem2 27387 2lgsoddprmlem3a 27388 2lgsoddprmlem3b 27389 2lgsoddprmlem3c 27390 2lgsoddprmlem3d 27391 ex-exp 30332 hgt750lem2 34415 420lcm8e840 41614 3exp7 41656 3lexlogpow5ineq1 41657 3lexlogpow5ineq5 41663 aks4d1p1 41679 ex-decpmul 42003 resqrtvalex 43217 imsqrtvalex 43218 fmtno5lem4 47033 257prm 47038 fmtnoprmfac2lem1 47043 fmtno4prmfac 47049 fmtno4nprmfac193 47051 fmtno5faclem3 47058 m3prm 47069 139prmALT 47073 127prm 47076 m7prm 47077 5tcu2e40 47092 2exp340mod341 47210 8exp8mod9 47213 nfermltl8rev 47219 evengpop3 47275 tgoldbachlt 47293 |
Copyright terms: Public domain | W3C validator |