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

Metamath Proof Explorer

Theorem expcnfg

Description: If F is a complex continuous function and N is a fixed number, then F^N is continuous too. A generalization of expcncf . (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses expcnfg.1 ⊢ Ⅎ 𝑥 𝐹
expcnfg.2 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )
expcnfg.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion expcnfg ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) ↑ 𝑁 ) ) ∈ ( 𝐴 –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 expcnfg.1 ⊢ Ⅎ 𝑥 𝐹
2 expcnfg.2 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )
3 expcnfg.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4 nfcv ⊢ Ⅎ 𝑡 ( ( 𝐹 ‘ 𝑥 ) ↑ 𝑁 )
5 nfcv ⊢ Ⅎ 𝑥 𝑡
6 1 5 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑡 )
7 nfcv ⊢ Ⅎ 𝑥 ↑
8 nfcv ⊢ Ⅎ 𝑥 𝑁
9 6 7 8 nfov ⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑁 )
10 fveq2 ⊢ ( 𝑥 = 𝑡 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑡 ) )
11 10 oveq1d ⊢ ( 𝑥 = 𝑡 → ( ( 𝐹 ‘ 𝑥 ) ↑ 𝑁 ) = ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑁 ) )
12 4 9 11 cbvmpt ⊢ ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) ↑ 𝑁 ) ) = ( 𝑡 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑁 ) )
13 cncff ⊢ ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ )
14 2 13 syl ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
15 14 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
16 3 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) → 𝑁 ∈ ℕ0 )
17 15 16 expcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑁 ) ∈ ℂ )
18 oveq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑡 ) → ( 𝑥 ↑ 𝑁 ) = ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑁 ) )
19 eqid ⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) )
20 6 9 18 19 fvmptf ⊢ ( ( ( 𝐹 ‘ 𝑡 ) ∈ ℂ ∧ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑁 ) ∈ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ‘ ( 𝐹 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑁 ) )
21 15 17 20 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ‘ ( 𝐹 ‘ 𝑡 ) ) = ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑁 ) )
22 21 eqcomd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑁 ) = ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ‘ ( 𝐹 ‘ 𝑡 ) ) )
23 22 mpteq2dva ⊢ ( 𝜑 → ( 𝑡 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑡 ) ↑ 𝑁 ) ) = ( 𝑡 ∈ 𝐴 ↦ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
24 12 23 eqtrid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) ↑ 𝑁 ) ) = ( 𝑡 ∈ 𝐴 ↦ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
25 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
26 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑁 ∈ ℕ0 )
27 25 26 expcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ↑ 𝑁 ) ∈ ℂ )
28 27 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) : ℂ ⟶ ℂ )
29 fcompt ⊢ ( ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) : ℂ ⟶ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∘ 𝐹 ) = ( 𝑡 ∈ 𝐴 ↦ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
30 28 14 29 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∘ 𝐹 ) = ( 𝑡 ∈ 𝐴 ↦ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
31 24 30 eqtr4d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) ↑ 𝑁 ) ) = ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∘ 𝐹 ) )
32 expcncf ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ ( ℂ –cn→ ℂ ) )
33 3 32 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ ( ℂ –cn→ ℂ ) )
34 2 33 cncfco ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∘ 𝐹 ) ∈ ( 𝐴 –cn→ ℂ ) )
35 31 34 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) ↑ 𝑁 ) ) ∈ ( 𝐴 –cn→ ℂ ) )