Theorem 2mulicn 11863

Description: (2 · i) ∈ ℂ. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
2mulicn	⊢ (2 · i) ∈ ℂ

Proof of Theorem 2mulicn

Step	Hyp	Ref	Expression
1		2cn 11715	. 2 ⊢ 2 ∈ ℂ
2		ax-icn 10598	. 2 ⊢ i ∈ ℂ
3	1, 2	mulcli 10650	1 ⊢ (2 · i) ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7158  ℂcc 10537  ici 10541   · cmul 10544  2c2 11695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-mulcl 10601

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-clel 2895  df-2 11703

This theorem is referenced by:  imval2  14512  sinf  15479  sinneg  15501  efival  15507  sinadd  15519  dvmptim  24569  sincn  25034  sineq0  25111  sinasin  25469  efiatan2  25497  2efiatan  25498  tanatan  25499  sineq0ALT  41278