![]() |
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 12224 | . 2 ⊢ 9 = (8 + 1) | |
2 | 8cn 12251 | . . 3 ⊢ 8 ∈ ℂ | |
3 | ax-1cn 11110 | . . 3 ⊢ 1 ∈ ℂ | |
4 | 2, 3 | addcli 11162 | . 2 ⊢ (8 + 1) ∈ ℂ |
5 | 1, 4 | eqeltri 2834 | 1 ⊢ 9 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 (class class class)co 7358 ℂcc 11050 1c1 11053 + caddc 11055 8c8 12215 9c9 12216 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 ax-1cn 11110 ax-addcl 11112 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-cleq 2729 df-clel 2815 df-2 12217 df-3 12218 df-4 12219 df-5 12220 df-6 12221 df-7 12222 df-8 12223 df-9 12224 |
This theorem is referenced by: 10m1e9 12715 9t2e18 12741 9t8e72 12747 9t9e81 12748 9t11e99 12749 0.999... 15767 cos2bnd 16071 3dvds 16214 3dvdsdec 16215 3dvds2dec 16216 2exp8 16962 139prm 16997 163prm 16998 317prm 16999 631prm 17000 1259lem1 17004 1259lem2 17005 1259lem3 17006 1259lem4 17007 1259lem5 17008 2503lem1 17010 2503lem2 17011 2503lem3 17012 2503prm 17013 4001lem1 17014 4001lem2 17015 4001lem3 17016 4001lem4 17017 sqrt2cxp2logb9e3 26152 mcubic 26200 cubic2 26201 cubic 26202 quartlem1 26210 log2tlbnd 26298 log2ublem3 26301 log2ub 26302 bposlem8 26642 ex-lcm 29405 9p10ne21 29417 1mhdrd 31775 hgt750lem2 33268 60gcd7e1 40465 3lexlogpow5ineq1 40514 3lexlogpow2ineq2 40519 3lexlogpow5ineq5 40520 fmtno5lem4 45755 257prm 45760 fmtno4nprmfac193 45773 139prmALT 45795 127prm 45798 8exp8mod9 45935 nfermltl8rev 45941 evengpop3 45997 |
Copyright terms: Public domain | W3C validator |