![]() |
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 12334 | . 2 ⊢ 9 = (8 + 1) | |
2 | 8cn 12361 | . . 3 ⊢ 8 ∈ ℂ | |
3 | ax-1cn 11216 | . . 3 ⊢ 1 ∈ ℂ | |
4 | 2, 3 | addcli 11270 | . 2 ⊢ (8 + 1) ∈ ℂ |
5 | 1, 4 | eqeltri 2822 | 1 ⊢ 9 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 (class class class)co 7424 ℂcc 11156 1c1 11159 + caddc 11161 8c8 12325 9c9 12326 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 ax-1cn 11216 ax-addcl 11218 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-cleq 2718 df-clel 2803 df-2 12327 df-3 12328 df-4 12329 df-5 12330 df-6 12331 df-7 12332 df-8 12333 df-9 12334 |
This theorem is referenced by: 10m1e9 12825 9t2e18 12851 9t8e72 12857 9t9e81 12858 9t11e99 12859 0.999... 15885 cos2bnd 16190 3dvds 16333 3dvdsdec 16334 3dvds2dec 16335 2exp8 17091 139prm 17126 163prm 17127 317prm 17128 631prm 17129 1259lem1 17133 1259lem2 17134 1259lem3 17135 1259lem4 17136 1259lem5 17137 2503lem1 17139 2503lem2 17140 2503lem3 17141 2503prm 17142 4001lem1 17143 4001lem2 17144 4001lem3 17145 4001lem4 17146 sqrt2cxp2logb9e3 26827 mcubic 26875 cubic2 26876 cubic 26877 quartlem1 26885 log2tlbnd 26973 log2ublem3 26976 log2ub 26977 bposlem8 27320 ex-lcm 30391 9p10ne21 30403 1mhdrd 32777 hgt750lem2 34498 60gcd7e1 41704 3lexlogpow5ineq1 41753 3lexlogpow2ineq2 41758 3lexlogpow5ineq5 41759 sq9 42105 sum9cubes 42326 fmtno5lem4 47128 257prm 47133 fmtno4nprmfac193 47146 139prmALT 47168 127prm 47171 8exp8mod9 47308 nfermltl8rev 47314 evengpop3 47370 |
Copyright terms: Public domain | W3C validator |