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 φ$
	climexp.2	$⊢ \underline{Ⅎ} k F$
	climexp.3	$⊢ \underline{Ⅎ} k H$
	climexp.4	$⊢ Z = ℤ_{\geq M}$
	climexp.5	$⊢ φ \to M \in ℤ$
	climexp.6	$⊢ φ \to F : Z ⟶ ℂ$
	climexp.7	$⊢ φ \to F ⇝ A$
	climexp.8	$⊢ φ \to N \in ℕ_{0}$
	climexp.9	$⊢ φ \to H \in V$
	climexp.10	$⊢ (φ \land k \in Z) \to H (k) = {F (k)}^{N}$
Assertion	climexp	$⊢ φ \to H ⇝ A^{N}$

Proof

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

Metamath Proof Explorer

Theorem climexp

Proof