This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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→ ℂ ) )