![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2mulicn | Structured version Visualization version GIF version |
Description: (2 · i) ∈ ℂ. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
2mulicn | ⊢ (2 · i) ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2cn 12339 | . 2 ⊢ 2 ∈ ℂ | |
2 | ax-icn 11212 | . 2 ⊢ i ∈ ℂ | |
3 | 1, 2 | mulcli 11266 | 1 ⊢ (2 · i) ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 (class class class)co 7431 ℂcc 11151 ici 11155 · cmul 11158 2c2 12319 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 ax-1cn 11211 ax-icn 11212 ax-addcl 11213 ax-mulcl 11215 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-cleq 2727 df-clel 2814 df-2 12327 |
This theorem is referenced by: imval2 15187 sinf 16157 sinneg 16179 efival 16185 sinadd 16197 dvmptim 26023 sincn 26503 sineq0 26581 sinasin 26947 efiatan2 26975 2efiatan 26976 tanatan 26977 sineq0ALT 44935 |
Copyright terms: Public domain | W3C validator |