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	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ ℂ ) )
Assertion	efmul2picn	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( exp ‘ ( ( i · ( 2 · π ) ) · 𝐵 ) ) ) ∈ ( 𝐴 –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		efmul2picn.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ ℂ ) )
2		efcn	⊢ exp ∈ ( ℂ –cn→ ℂ )
3	2	a1i	⊢ ( 𝜑 → exp ∈ ( ℂ –cn→ ℂ ) )
4		ax-icn	⊢ i ∈ ℂ
5		2cn	⊢ 2 ∈ ℂ
6		picn	⊢ π ∈ ℂ
7	5 6	mulcli	⊢ ( 2 · π ) ∈ ℂ
8	4 7	mulcli	⊢ ( i · ( 2 · π ) ) ∈ ℂ
9	8	a1i	⊢ ( 𝜑 → ( i · ( 2 · π ) ) ∈ ℂ )
10		cncfrss	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ ℂ ) → 𝐴 ⊆ ℂ )
11	1 10	syl	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
12		ssidd	⊢ ( 𝜑 → ℂ ⊆ ℂ )
13		cncfmptc	⊢ ( ( ( i · ( 2 · π ) ) ∈ ℂ ∧ 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ ( i · ( 2 · π ) ) ) ∈ ( 𝐴 –cn→ ℂ ) )
14	9 11 12 13	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( i · ( 2 · π ) ) ) ∈ ( 𝐴 –cn→ ℂ ) )
15	14 1	mulcncf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( i · ( 2 · π ) ) · 𝐵 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
16	3 15	cncfmpt1f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( exp ‘ ( ( i · ( 2 · π ) ) · 𝐵 ) ) ) ∈ ( 𝐴 –cn→ ℂ ) )