Theorem climexp

Description: The limit of natural powers, is the natural power of the limit. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	climexp.1	$$⊢Ⅎk\phi$$
	climexp.2	$$⊢\underset{\_}{Ⅎ}kF$$
	climexp.3	$$⊢\underset{\_}{Ⅎ}kH$$
	climexp.4	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climexp.5	$$⊢\phi \to M\in \mathbb{Z}$$
	climexp.6	$$⊢\phi \to F:Z⟶ℂ$$
	climexp.7	$$⊢\phi \to F⇝A$$
	climexp.8	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	climexp.9	$$⊢\phi \to H\in V$$
	climexp.10	$$⊢\left(\phi \wedge k\in Z\right)\to H\left(k\right)={F\left(k\right)}^N$$
Assertion	climexp	$$⊢\phi \to H⇝A^N$$

Proof

Step	Hyp	Ref	Expression
1		climexp.1	$$⊢Ⅎk\phi$$
2		climexp.2	$$⊢\underset{\_}{Ⅎ}kF$$
3		climexp.3	$$⊢\underset{\_}{Ⅎ}kH$$
4		climexp.4	$$⊢Z={\mathbb{Z}}_{\ge M}$$
5		climexp.5	$$⊢\phi \to M\in \mathbb{Z}$$
6		climexp.6	$$⊢\phi \to F:Z⟶ℂ$$
7		climexp.7	$$⊢\phi \to F⇝A$$
8		climexp.8	$$⊢\phi \to N\in {\mathbb{N}}_0$$
9		climexp.9	$$⊢\phi \to H\in V$$
10		climexp.10	$$⊢\left(\phi \wedge k\in Z\right)\to H\left(k\right)={F\left(k\right)}^N$$
11		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
12	11	expcn	$$⊢N\in {\mathbb{N}}_0\to \left(x\in ℂ⟼x^N\right)\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
13	8 12	syl	$$⊢\phi \to \left(x\in ℂ⟼x^N\right)\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
14	11	cncfcn1	$$⊢ℂ\underset{cn}{⟶}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
15	13 14	eleqtrrdi	$$⊢\phi \to \left(x\in ℂ⟼x^N\right):ℂ\underset{cn}{⟶}ℂ$$
16		climcl	$$⊢F⇝A\to A\in ℂ$$
17	7 16	syl	$$⊢\phi \to A\in ℂ$$
18	4 5 15 6 7 17	climcncf	$$⊢\phi \to \left(\left(x\in ℂ⟼x^N\right)\circ F\right)⇝\left(x\in ℂ⟼x^N\right)\left(A\right)$$
19		eqidd	$$⊢\phi \to \left(x\in ℂ⟼x^N\right)=\left(x\in ℂ⟼x^N\right)$$
20		simpr	$$⊢\left(\phi \wedge x=A\right)\to x=A$$
21	20	oveq1d	$$⊢\left(\phi \wedge x=A\right)\to x^N=A^N$$
22	17 8	expcld	$$⊢\phi \to A^N\in ℂ$$
23	19 21 17 22	fvmptd	$$⊢\phi \to \left(x\in ℂ⟼x^N\right)\left(A\right)=A^N$$
24	18 23	breqtrd	$$⊢\phi \to \left(\left(x\in ℂ⟼x^N\right)\circ F\right)⇝A^N$$
25		cnex	$$⊢ℂ\in \mathrm{V}$$
26	25	mptex	$$⊢\left(x\in ℂ⟼x^N\right)\in \mathrm{V}$$
27	4	fvexi	$$⊢Z\in \mathrm{V}$$
28		fex	$$⊢\left(F:Z⟶ℂ\wedge Z\in \mathrm{V}\right)\to F\in \mathrm{V}$$
29	6 27 28	sylancl	$$⊢\phi \to F\in \mathrm{V}$$
30		coexg	$$⊢\left(\left(x\in ℂ⟼x^N\right)\in \mathrm{V}\wedge F\in \mathrm{V}\right)\to \left(x\in ℂ⟼x^N\right)\circ F\in \mathrm{V}$$
31	26 29 30	sylancr	$$⊢\phi \to \left(x\in ℂ⟼x^N\right)\circ F\in \mathrm{V}$$
32		eqidd	$$⊢\left(\phi \wedge j\in Z\right)\to \left(x\in ℂ⟼x^N\right)=\left(x\in ℂ⟼x^N\right)$$
33		simpr	$$⊢\left(\left(\phi \wedge j\in Z\right)\wedge x=F\left(j\right)\right)\to x=F\left(j\right)$$
34	33	oveq1d	$$⊢\left(\left(\phi \wedge j\in Z\right)\wedge x=F\left(j\right)\right)\to x^N={F\left(j\right)}^N$$
35	6	ffvelrnda	$$⊢\left(\phi \wedge j\in Z\right)\to F\left(j\right)\in ℂ$$
36	8	adantr	$$⊢\left(\phi \wedge j\in Z\right)\to N\in {\mathbb{N}}_0$$
37	35 36	expcld	$$⊢\left(\phi \wedge j\in Z\right)\to {F\left(j\right)}^N\in ℂ$$
38	32 34 35 37	fvmptd	$$⊢\left(\phi \wedge j\in Z\right)\to \left(x\in ℂ⟼x^N\right)\left(F\left(j\right)\right)={F\left(j\right)}^N$$
39		fvco3	$$⊢\left(F:Z⟶ℂ\wedge j\in Z\right)\to \left(\left(x\in ℂ⟼x^N\right)\circ F\right)\left(j\right)=\left(x\in ℂ⟼x^N\right)\left(F\left(j\right)\right)$$
40	6 39	sylan	$$⊢\left(\phi \wedge j\in Z\right)\to \left(\left(x\in ℂ⟼x^N\right)\circ F\right)\left(j\right)=\left(x\in ℂ⟼x^N\right)\left(F\left(j\right)\right)$$
41		nfv	$$⊢Ⅎkj\in Z$$
42	1 41	nfan	$$⊢Ⅎk\left(\phi \wedge j\in Z\right)$$
43		nfcv	$$⊢\underset{\_}{Ⅎ}kj$$
44	3 43	nffv	$$⊢\underset{\_}{Ⅎ}kH\left(j\right)$$
45	2 43	nffv	$$⊢\underset{\_}{Ⅎ}kF\left(j\right)$$
46		nfcv	$$⊢\underset{\_}{Ⅎ}k^$$
47		nfcv	$$⊢\underset{\_}{Ⅎ}kN$$
48	45 46 47	nfov	$$⊢\underset{\_}{Ⅎ}k{F\left(j\right)}^N$$
49	44 48	nfeq	$$⊢ℲkH\left(j\right)={F\left(j\right)}^N$$
50	42 49	nfim	$$⊢Ⅎk\left(\left(\phi \wedge j\in Z\right)\to H\left(j\right)={F\left(j\right)}^N\right)$$
51		eleq1w	$$⊢k=j\to \left(k\in Z\leftrightarrow j\in Z\right)$$
52	51	anbi2d	$$⊢k=j\to \left(\left(\phi \wedge k\in Z\right)\leftrightarrow \left(\phi \wedge j\in Z\right)\right)$$
53		fveq2	$$⊢k=j\to H\left(k\right)=H\left(j\right)$$
54		fveq2	$$⊢k=j\to F\left(k\right)=F\left(j\right)$$
55	54	oveq1d	$$⊢k=j\to {F\left(k\right)}^N={F\left(j\right)}^N$$
56	53 55	eqeq12d	$$⊢k=j\to \left(H\left(k\right)={F\left(k\right)}^N\leftrightarrow H\left(j\right)={F\left(j\right)}^N\right)$$
57	52 56	imbi12d	$$⊢k=j\to \left(\left(\left(\phi \wedge k\in Z\right)\to H\left(k\right)={F\left(k\right)}^N\right)\leftrightarrow \left(\left(\phi \wedge j\in Z\right)\to H\left(j\right)={F\left(j\right)}^N\right)\right)$$
58	50 57 10	chvarfv	$$⊢\left(\phi \wedge j\in Z\right)\to H\left(j\right)={F\left(j\right)}^N$$
59	38 40 58	3eqtr4rd	$$⊢\left(\phi \wedge j\in Z\right)\to H\left(j\right)=\left(\left(x\in ℂ⟼x^N\right)\circ F\right)\left(j\right)$$
60	4 9 31 5 59	climeq	$$⊢\phi \to \left(H⇝A^N\leftrightarrow \left(\left(x\in ℂ⟼x^N\right)\circ F\right)⇝A^N\right)$$
61	24 60	mpbird	$$⊢\phi \to H⇝A^N$$