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	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
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	syl5eq	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) ↑ 𝑁 ) ) = ( 𝑡 ∈ 𝐴 ↦ ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
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→ ℂ ) )