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	$$⊢\underset{\_}{Ⅎ}xF$$
	expcnfg.2	$$⊢\phi \to F:A\underset{cn}{⟶}ℂ$$
	expcnfg.3	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	expcnfg	$$⊢\phi \to \left(x\in A⟼{F\left(x\right)}^N\right):A\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		expcnfg.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		expcnfg.2	$$⊢\phi \to F:A\underset{cn}{⟶}ℂ$$
3		expcnfg.3	$$⊢\phi \to N\in {\mathbb{N}}_0$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}t{F\left(x\right)}^N$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xt$$
6	1 5	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(t\right)$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}x^$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}xN$$
9	6 7 8	nfov	$$⊢\underset{\_}{Ⅎ}x{F\left(t\right)}^N$$
10		fveq2	$$⊢x=t\to F\left(x\right)=F\left(t\right)$$
11	10	oveq1d	$$⊢x=t\to {F\left(x\right)}^N={F\left(t\right)}^N$$
12	4 9 11	cbvmpt	$$⊢\left(x\in A⟼{F\left(x\right)}^N\right)=\left(t\in A⟼{F\left(t\right)}^N\right)$$
13		cncff	$$⊢F:A\underset{cn}{⟶}ℂ\to F:A⟶ℂ$$
14	2 13	syl	$$⊢\phi \to F:A⟶ℂ$$
15	14	ffvelrnda	$$⊢\left(\phi \wedge t\in A\right)\to F\left(t\right)\in ℂ$$
16	3	adantr	$$⊢\left(\phi \wedge t\in A\right)\to N\in {\mathbb{N}}_0$$
17	15 16	expcld	$$⊢\left(\phi \wedge t\in A\right)\to {F\left(t\right)}^N\in ℂ$$
18		oveq1	$$⊢x=F\left(t\right)\to x^N={F\left(t\right)}^N$$
19		eqid	$$⊢\left(x\in ℂ⟼x^N\right)=\left(x\in ℂ⟼x^N\right)$$
20	6 9 18 19	fvmptf	$$⊢\left(F\left(t\right)\in ℂ\wedge {F\left(t\right)}^N\in ℂ\right)\to \left(x\in ℂ⟼x^N\right)\left(F\left(t\right)\right)={F\left(t\right)}^N$$
21	15 17 20	syl2anc	$$⊢\left(\phi \wedge t\in A\right)\to \left(x\in ℂ⟼x^N\right)\left(F\left(t\right)\right)={F\left(t\right)}^N$$
22	21	eqcomd	$$⊢\left(\phi \wedge t\in A\right)\to {F\left(t\right)}^N=\left(x\in ℂ⟼x^N\right)\left(F\left(t\right)\right)$$
23	22	mpteq2dva	$$⊢\phi \to \left(t\in A⟼{F\left(t\right)}^N\right)=\left(t\in A⟼\left(x\in ℂ⟼x^N\right)\left(F\left(t\right)\right)\right)$$
24	12 23	syl5eq	$$⊢\phi \to \left(x\in A⟼{F\left(x\right)}^N\right)=\left(t\in A⟼\left(x\in ℂ⟼x^N\right)\left(F\left(t\right)\right)\right)$$
25		simpr	$$⊢\left(\phi \wedge x\in ℂ\right)\to x\in ℂ$$
26	3	adantr	$$⊢\left(\phi \wedge x\in ℂ\right)\to N\in {\mathbb{N}}_0$$
27	25 26	expcld	$$⊢\left(\phi \wedge x\in ℂ\right)\to x^N\in ℂ$$
28	27	fmpttd	$$⊢\phi \to \left(x\in ℂ⟼x^N\right):ℂ⟶ℂ$$
29		fcompt	$$⊢\left(\left(x\in ℂ⟼x^N\right):ℂ⟶ℂ\wedge F:A⟶ℂ\right)\to \left(x\in ℂ⟼x^N\right)\circ F=\left(t\in A⟼\left(x\in ℂ⟼x^N\right)\left(F\left(t\right)\right)\right)$$
30	28 14 29	syl2anc	$$⊢\phi \to \left(x\in ℂ⟼x^N\right)\circ F=\left(t\in A⟼\left(x\in ℂ⟼x^N\right)\left(F\left(t\right)\right)\right)$$
31	24 30	eqtr4d	$$⊢\phi \to \left(x\in A⟼{F\left(x\right)}^N\right)=\left(x\in ℂ⟼x^N\right)\circ F$$
32		expcncf	$$⊢N\in {\mathbb{N}}_0\to \left(x\in ℂ⟼x^N\right):ℂ\underset{cn}{⟶}ℂ$$
33	3 32	syl	$$⊢\phi \to \left(x\in ℂ⟼x^N\right):ℂ\underset{cn}{⟶}ℂ$$
34	2 33	cncfco	$$⊢\phi \to \left(\left(x\in ℂ⟼x^N\right)\circ F\right):A\underset{cn}{⟶}ℂ$$
35	31 34	eqeltrd	$$⊢\phi \to \left(x\in A⟼{F\left(x\right)}^N\right):A\underset{cn}{⟶}ℂ$$