Theorem efmul2picn

Description: Multiplying by (i x. ( 2 x. pi ) ) and taking the exponential preserves continuity. (Contributed by Thierry Arnoux, 13-Dec-2021)

	Ref	Expression
Hypothesis	efmul2picn.1	$$⊢\phi \to \left(x\in A⟼B\right):A\underset{cn}{⟶}ℂ$$
Assertion	efmul2picn	$$⊢\phi \to \left(x\in A⟼{\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }B}\right):A\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		efmul2picn.1	$$⊢\phi \to \left(x\in A⟼B\right):A\underset{cn}{⟶}ℂ$$
2		efcn	$$⊢\exp :ℂ\underset{cn}{⟶}ℂ$$
3	2	a1i	$$⊢\phi \to \exp :ℂ\underset{cn}{⟶}ℂ$$
4		ax-icn	$$⊢\mathrm{i}\in ℂ$$
5		2cn	$$⊢2\in ℂ$$
6		picn	$$⊢\mathrm{\pi }\in ℂ$$
7	5 6	mulcli	$$⊢2\mathrm{\pi }\in ℂ$$
8	4 7	mulcli	$$⊢\mathrm{i}2\mathrm{\pi }\in ℂ$$
9	8	a1i	$$⊢\phi \to \mathrm{i}2\mathrm{\pi }\in ℂ$$
10		cncfrss	$$⊢\left(x\in A⟼B\right):A\underset{cn}{⟶}ℂ\to A\subseteq ℂ$$
11	1 10	syl	$$⊢\phi \to A\subseteq ℂ$$
12		ssidd	$$⊢\phi \to ℂ\subseteq ℂ$$
13		cncfmptc	$$⊢\left(\mathrm{i}2\mathrm{\pi }\in ℂ\wedge A\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left(x\in A⟼\mathrm{i}2\mathrm{\pi }\right):A\underset{cn}{⟶}ℂ$$
14	9 11 12 13	syl3anc	$$⊢\phi \to \left(x\in A⟼\mathrm{i}2\mathrm{\pi }\right):A\underset{cn}{⟶}ℂ$$
15	14 1	mulcncf	$$⊢\phi \to \left(x\in A⟼\mathrm{i}2\mathrm{\pi }B\right):A\underset{cn}{⟶}ℂ$$
16	3 15	cncfmpt1f	$$⊢\phi \to \left(x\in A⟼{\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }B}\right):A\underset{cn}{⟶}ℂ$$