![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 9cn | Structured version Visualization version GIF version |
Description: The number 9 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 |
---|---|
9cn | ⊢ 9 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-9 11508 | . 2 ⊢ 9 = (8 + 1) | |
2 | 8cn 11540 | . . 3 ⊢ 8 ∈ ℂ | |
3 | ax-1cn 10391 | . . 3 ⊢ 1 ∈ ℂ | |
4 | 2, 3 | addcli 10444 | . 2 ⊢ (8 + 1) ∈ ℂ |
5 | 1, 4 | eqeltri 2855 | 1 ⊢ 9 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2051 (class class class)co 6974 ℂcc 10331 1c1 10334 + caddc 10336 8c8 11499 9c9 11500 |
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 2743 ax-1cn 10391 ax-addcl 10393 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1744 df-cleq 2764 df-clel 2839 df-2 11501 df-3 11502 df-4 11503 df-5 11504 df-6 11505 df-7 11506 df-8 11507 df-9 11508 |
This theorem is referenced by: 10m1e9 12007 9t2e18 12033 9t8e72 12039 9t9e81 12040 9t11e99 12041 0.999... 15095 cos2bnd 15399 3dvds 15538 3dvdsdec 15539 3dvds2dec 15540 2exp8 16277 139prm 16311 163prm 16312 317prm 16313 631prm 16314 1259lem1 16318 1259lem2 16319 1259lem3 16320 1259lem4 16321 1259lem5 16322 2503lem1 16324 2503lem2 16325 2503lem3 16326 2503prm 16327 4001lem1 16328 4001lem2 16329 4001lem3 16330 4001lem4 16331 sqrt2cxp2logb9e3 25093 mcubic 25141 cubic2 25142 cubic 25143 quartlem1 25151 log2tlbnd 25240 log2ublem3 25243 log2ub 25244 bposlem8 25584 ex-lcm 28030 9p10ne21 28041 1mhdrd 30362 hgt750lem2 31603 fmtno5lem4 43120 257prm 43125 fmtno4nprmfac193 43138 139prmALT 43161 127prm 43165 8exp8mod9 43303 nfermltl8rev 43309 evengpop3 43365 |
Copyright terms: Public domain | W3C validator |