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 11700 | . 2 ⊢ 2 ∈ ℂ | |
2 | ax-icn 10584 | . 2 ⊢ i ∈ ℂ | |
3 | 1, 2 | mulcli 10636 | 1 ⊢ (2 · i) ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 (class class class)co 7145 ℂcc 10523 ici 10527 · cmul 10530 2c2 11680 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 ax-1cn 10583 ax-icn 10584 ax-addcl 10585 ax-mulcl 10587 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 df-clel 2890 df-2 11688 |
This theorem is referenced by: imval2 14498 sinf 15465 sinneg 15487 efival 15493 sinadd 15505 dvmptim 24494 sincn 24959 sineq0 25036 sinasin 25394 efiatan2 25422 2efiatan 25423 tanatan 25424 sineq0ALT 41148 |
Copyright terms: Public domain | W3C validator |