![]() |
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 complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
9cn | ⊢ 9 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 9re 11308 | . 2 ⊢ 9 ∈ ℝ | |
2 | 1 | recni 10253 | 1 ⊢ 9 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2144 ℂcc 10135 9c9 11278 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-9 2153 ax-10 2173 ax-11 2189 ax-12 2202 ax-13 2407 ax-ext 2750 ax-resscn 10194 ax-1cn 10195 ax-icn 10196 ax-addcl 10197 ax-addrcl 10198 ax-mulcl 10199 ax-mulrcl 10200 ax-i2m1 10205 ax-1ne0 10206 ax-rrecex 10209 ax-cnre 10210 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-3an 1072 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2049 df-clab 2757 df-cleq 2763 df-clel 2766 df-nfc 2901 df-ne 2943 df-ral 3065 df-rex 3066 df-rab 3069 df-v 3351 df-dif 3724 df-un 3726 df-in 3728 df-ss 3735 df-nul 4062 df-if 4224 df-sn 4315 df-pr 4317 df-op 4321 df-uni 4573 df-br 4785 df-iota 5994 df-fv 6039 df-ov 6795 df-2 11280 df-3 11281 df-4 11282 df-5 11283 df-6 11284 df-7 11285 df-8 11286 df-9 11287 |
This theorem is referenced by: 10m1e9 11830 9t2e18 11863 9t8e72 11869 9t9e81 11870 9t11e99 11871 9t11e99OLD 11872 0.999... 14818 0.999...OLD 14819 cos2bnd 15123 3dvds 15260 3dvdsOLD 15261 3dvdsdec 15262 3dvdsdecOLD 15263 3dvds2dec 15264 2exp8 16002 139prm 16037 163prm 16038 317prm 16039 631prm 16040 1259lem1 16044 1259lem2 16045 1259lem3 16046 1259lem4 16047 1259lem5 16048 2503lem1 16050 2503lem2 16051 2503lem3 16052 2503prm 16053 4001lem1 16054 4001lem2 16055 4001lem3 16056 4001lem4 16057 mcubic 24794 cubic2 24795 cubic 24796 quartlem1 24804 log2tlbnd 24892 log2ublem3 24895 log2ub 24896 bposlem8 25236 ex-lcm 27651 1mhdrd 29958 hgt750lem2 31064 fmtno5lem4 41986 257prm 41991 fmtno4nprmfac193 42004 139prmALT 42029 127prm 42033 evengpop3 42204 |
Copyright terms: Public domain | W3C validator |