![]() |
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 12219 | . 2 ⊢ 9 = (8 + 1) | |
2 | 8cn 12246 | . . 3 ⊢ 8 ∈ ℂ | |
3 | ax-1cn 11105 | . . 3 ⊢ 1 ∈ ℂ | |
4 | 2, 3 | addcli 11157 | . 2 ⊢ (8 + 1) ∈ ℂ |
5 | 1, 4 | eqeltri 2834 | 1 ⊢ 9 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 (class class class)co 7353 ℂcc 11045 1c1 11048 + caddc 11050 8c8 12210 9c9 12211 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 ax-1cn 11105 ax-addcl 11107 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2728 df-clel 2814 df-2 12212 df-3 12213 df-4 12214 df-5 12215 df-6 12216 df-7 12217 df-8 12218 df-9 12219 |
This theorem is referenced by: 10m1e9 12710 9t2e18 12736 9t8e72 12742 9t9e81 12743 9t11e99 12744 0.999... 15758 cos2bnd 16062 3dvds 16205 3dvdsdec 16206 3dvds2dec 16207 2exp8 16953 139prm 16988 163prm 16989 317prm 16990 631prm 16991 1259lem1 16995 1259lem2 16996 1259lem3 16997 1259lem4 16998 1259lem5 16999 2503lem1 17001 2503lem2 17002 2503lem3 17003 2503prm 17004 4001lem1 17005 4001lem2 17006 4001lem3 17007 4001lem4 17008 sqrt2cxp2logb9e3 26133 mcubic 26181 cubic2 26182 cubic 26183 quartlem1 26191 log2tlbnd 26279 log2ublem3 26282 log2ub 26283 bposlem8 26623 ex-lcm 29288 9p10ne21 29300 1mhdrd 31655 hgt750lem2 33134 60gcd7e1 40429 3lexlogpow5ineq1 40478 3lexlogpow2ineq2 40483 3lexlogpow5ineq5 40484 fmtno5lem4 45680 257prm 45685 fmtno4nprmfac193 45698 139prmALT 45720 127prm 45723 8exp8mod9 45860 nfermltl8rev 45866 evengpop3 45922 |
Copyright terms: Public domain | W3C validator |