Theorem pserulm

Description: If S is a region contained in a circle of radius M < R , then the sequence of partial sums of the infinite series converges uniformly on S . (Contributed by Mario Carneiro, 26-Feb-2015)

	Ref	Expression
Hypotheses	pserf.g	⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
	pserf.f	⊢ 𝐹 = ( 𝑦 ∈ 𝑆 ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) )
	pserf.a	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
	pserf.r	⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
	pserulm.h	⊢ 𝐻 = ( 𝑖 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) )
	pserulm.m	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
	pserulm.l	⊢ ( 𝜑 → 𝑀 < 𝑅 )
	pserulm.y	⊢ ( 𝜑 → 𝑆 ⊆ ( ◡ abs “ ( 0 [,] 𝑀 ) ) )
Assertion	pserulm	⊢ ( 𝜑 → 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		pserf.g	⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
2		pserf.f	⊢ 𝐹 = ( 𝑦 ∈ 𝑆 ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) )
3		pserf.a	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
4		pserf.r	⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
5		pserulm.h	⊢ 𝐻 = ( 𝑖 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) )
6		pserulm.m	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
7		pserulm.l	⊢ ( 𝜑 → 𝑀 < 𝑅 )
8		pserulm.y	⊢ ( 𝜑 → 𝑆 ⊆ ( ◡ abs “ ( 0 [,] 𝑀 ) ) )
9	8	adantr	⊢ ( ( 𝜑 ∧ 𝑀 < 0 ) → 𝑆 ⊆ ( ◡ abs “ ( 0 [,] 𝑀 ) ) )
10		0xr	⊢ 0 ∈ ℝ*
11	6	rexrd	⊢ ( 𝜑 → 𝑀 ∈ ℝ* )
12		icc0	⊢ ( ( 0 ∈ ℝ* ∧ 𝑀 ∈ ℝ* ) → ( ( 0 [,] 𝑀 ) = ∅ ↔ 𝑀 < 0 ) )
13	10 11 12	sylancr	⊢ ( 𝜑 → ( ( 0 [,] 𝑀 ) = ∅ ↔ 𝑀 < 0 ) )
14	13	biimpar	⊢ ( ( 𝜑 ∧ 𝑀 < 0 ) → ( 0 [,] 𝑀 ) = ∅ )
15	14	imaeq2d	⊢ ( ( 𝜑 ∧ 𝑀 < 0 ) → ( ◡ abs “ ( 0 [,] 𝑀 ) ) = ( ◡ abs “ ∅ ) )
16		ima0	⊢ ( ◡ abs “ ∅ ) = ∅
17	15 16	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑀 < 0 ) → ( ◡ abs “ ( 0 [,] 𝑀 ) ) = ∅ )
18	9 17	sseqtrd	⊢ ( ( 𝜑 ∧ 𝑀 < 0 ) → 𝑆 ⊆ ∅ )
19		ss0	⊢ ( 𝑆 ⊆ ∅ → 𝑆 = ∅ )
20	18 19	syl	⊢ ( ( 𝜑 ∧ 𝑀 < 0 ) → 𝑆 = ∅ )
21		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
22		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
23		0zd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 0 ∈ ℤ )
24	3	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
25		cnvimass	⊢ ( ◡ abs “ ( 0 [,] 𝑀 ) ) ⊆ dom abs
26		absf	⊢ abs : ℂ ⟶ ℝ
27	26	fdmi	⊢ dom abs = ℂ
28	25 27	sseqtri	⊢ ( ◡ abs “ ( 0 [,] 𝑀 ) ) ⊆ ℂ
29	8 28	sstrdi	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
30	29	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ ℂ )
31	1 24 30	psergf	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑦 ) : ℕ0 ⟶ ℂ )
32	31	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) ∈ ℂ )
33	21 23 32	serf	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) : ℕ0 ⟶ ℂ )
34	33	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ∈ ℂ )
35	34	an32s	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝑆 ) → ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ∈ ℂ )
36	35	fmpttd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) : 𝑆 ⟶ ℂ )
37		cnex	⊢ ℂ ∈ V
38		ssexg	⊢ ( ( 𝑆 ⊆ ℂ ∧ ℂ ∈ V ) → 𝑆 ∈ V )
39	29 37 38	sylancl	⊢ ( 𝜑 → 𝑆 ∈ V )
40	39	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑆 ∈ V )
41		elmapg	⊢ ( ( ℂ ∈ V ∧ 𝑆 ∈ V ) → ( ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ∈ ( ℂ ↑m 𝑆 ) ↔ ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) : 𝑆 ⟶ ℂ ) )
42	37 40 41	sylancr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ∈ ( ℂ ↑m 𝑆 ) ↔ ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) : 𝑆 ⟶ ℂ ) )
43	36 42	mpbird	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ∈ ( ℂ ↑m 𝑆 ) )
44	43 5	fmptd	⊢ ( 𝜑 → 𝐻 : ℕ0 ⟶ ( ℂ ↑m 𝑆 ) )
45		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) = ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) )
46	8	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ ( ◡ abs “ ( 0 [,] 𝑀 ) ) )
47		ffn	⊢ ( abs : ℂ ⟶ ℝ → abs Fn ℂ )
48		elpreima	⊢ ( abs Fn ℂ → ( 𝑦 ∈ ( ◡ abs “ ( 0 [,] 𝑀 ) ) ↔ ( 𝑦 ∈ ℂ ∧ ( abs ‘ 𝑦 ) ∈ ( 0 [,] 𝑀 ) ) ) )
49	26 47 48	mp2b	⊢ ( 𝑦 ∈ ( ◡ abs “ ( 0 [,] 𝑀 ) ) ↔ ( 𝑦 ∈ ℂ ∧ ( abs ‘ 𝑦 ) ∈ ( 0 [,] 𝑀 ) ) )
50	46 49	sylib	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑦 ∈ ℂ ∧ ( abs ‘ 𝑦 ) ∈ ( 0 [,] 𝑀 ) ) )
51	50	simprd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( abs ‘ 𝑦 ) ∈ ( 0 [,] 𝑀 ) )
52		0re	⊢ 0 ∈ ℝ
53	6	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑀 ∈ ℝ )
54		elicc2	⊢ ( ( 0 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ( abs ‘ 𝑦 ) ∈ ( 0 [,] 𝑀 ) ↔ ( ( abs ‘ 𝑦 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑦 ) ∧ ( abs ‘ 𝑦 ) ≤ 𝑀 ) ) )
55	52 53 54	sylancr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( abs ‘ 𝑦 ) ∈ ( 0 [,] 𝑀 ) ↔ ( ( abs ‘ 𝑦 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑦 ) ∧ ( abs ‘ 𝑦 ) ≤ 𝑀 ) ) )
56	51 55	mpbid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( abs ‘ 𝑦 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑦 ) ∧ ( abs ‘ 𝑦 ) ≤ 𝑀 ) )
57	56	simp1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( abs ‘ 𝑦 ) ∈ ℝ )
58	57	rexrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( abs ‘ 𝑦 ) ∈ ℝ* )
59	11	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑀 ∈ ℝ* )
60		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
61	1 3 4	radcnvcl	⊢ ( 𝜑 → 𝑅 ∈ ( 0 [,] +∞ ) )
62	60 61	sselid	⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
63	62	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑅 ∈ ℝ* )
64	56	simp3d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( abs ‘ 𝑦 ) ≤ 𝑀 )
65	7	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑀 < 𝑅 )
66	58 59 63 64 65	xrlelttrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( abs ‘ 𝑦 ) < 𝑅 )
67	1 24 4 30 66	radcnvlt2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ∈ dom ⇝ )
68	21 23 45 32 67	isumcl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) ∈ ℂ )
69	68 2	fmptd	⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ ℂ )
70	21 22 44 69	ulm0	⊢ ( ( 𝜑 ∧ 𝑆 = ∅ ) → 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐹 )
71	20 70	syldan	⊢ ( ( 𝜑 ∧ 𝑀 < 0 ) → 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐹 )
72		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℕ0 )
73	72 21	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ( ℤ≥ ‘ 0 ) )
74		eqid	⊢ ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) )
75		fveq2	⊢ ( 𝑤 = 𝑦 → ( 𝐺 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑦 ) )
76	75	fveq1d	⊢ ( 𝑤 = 𝑦 → ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) = ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑚 ) )
77	76	cbvmptv	⊢ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) = ( 𝑦 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑚 ) )
78		fveq2	⊢ ( 𝑚 = 𝑘 → ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑚 ) = ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑘 ) )
79	78	mpteq2dv	⊢ ( 𝑚 = 𝑘 → ( 𝑦 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑚 ) ) = ( 𝑦 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑘 ) ) )
80	77 79	eqtrid	⊢ ( 𝑚 = 𝑘 → ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) = ( 𝑦 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑘 ) ) )
81		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑖 ) → 𝑘 ∈ ℕ0 )
82	81	adantl	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → 𝑘 ∈ ℕ0 )
83	39	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → 𝑆 ∈ V )
84	83	mptexd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → ( 𝑦 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑘 ) ) ∈ V )
85	74 80 82 84	fvmptd3	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑘 ) ) )
86	40 73 85	seqof	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ) ‘ 𝑖 ) = ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) )
87	86	eqcomd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) = ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ) ‘ 𝑖 ) )
88	87	mpteq2dva	⊢ ( 𝜑 → ( 𝑖 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ) ‘ 𝑖 ) ) )
89		0z	⊢ 0 ∈ ℤ
90		seqfn	⊢ ( 0 ∈ ℤ → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ) Fn ( ℤ≥ ‘ 0 ) )
91	89 90	ax-mp	⊢ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ) Fn ( ℤ≥ ‘ 0 )
92	21	fneq2i	⊢ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ) Fn ℕ0 ↔ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ) Fn ( ℤ≥ ‘ 0 ) )
93	91 92	mpbir	⊢ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ) Fn ℕ0
94		dffn5	⊢ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ) Fn ℕ0 ↔ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ) ‘ 𝑖 ) ) )
95	93 94	mpbi	⊢ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ) ‘ 𝑖 ) )
96	88 5 95	3eqtr4g	⊢ ( 𝜑 → 𝐻 = seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ) )
97	96	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝑀 ) → 𝐻 = seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ) )
98		0zd	⊢ ( ( 𝜑 ∧ 0 ≤ 𝑀 ) → 0 ∈ ℤ )
99	39	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝑀 ) → 𝑆 ∈ V )
100	3	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
101	29	sselda	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑆 ) → 𝑤 ∈ ℂ )
102	1 100 101	psergf	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑤 ) : ℕ0 ⟶ ℂ )
103	102	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ∈ ℂ )
104	103	an32s	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ∈ ℂ )
105	104	fmpttd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) : 𝑆 ⟶ ℂ )
106	39	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝑆 ∈ V )
107		elmapg	⊢ ( ( ℂ ∈ V ∧ 𝑆 ∈ V ) → ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ∈ ( ℂ ↑m 𝑆 ) ↔ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) : 𝑆 ⟶ ℂ ) )
108	37 106 107	sylancr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ∈ ( ℂ ↑m 𝑆 ) ↔ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) : 𝑆 ⟶ ℂ ) )
109	105 108	mpbird	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ∈ ( ℂ ↑m 𝑆 ) )
110	109	fmpttd	⊢ ( 𝜑 → ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) : ℕ0 ⟶ ( ℂ ↑m 𝑆 ) )
111	110	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝑀 ) → ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) : ℕ0 ⟶ ( ℂ ↑m 𝑆 ) )
112		fex	⊢ ( ( abs : ℂ ⟶ ℝ ∧ ℂ ∈ V ) → abs ∈ V )
113	26 37 112	mp2an	⊢ abs ∈ V
114		fvex	⊢ ( 𝐺 ‘ 𝑀 ) ∈ V
115	113 114	coex	⊢ ( abs ∘ ( 𝐺 ‘ 𝑀 ) ) ∈ V
116	115	a1i	⊢ ( ( 𝜑 ∧ 0 ≤ 𝑀 ) → ( abs ∘ ( 𝐺 ‘ 𝑀 ) ) ∈ V )
117	3	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝑀 ) → 𝐴 : ℕ0 ⟶ ℂ )
118	6	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝑀 ) → 𝑀 ∈ ℝ )
119	118	recnd	⊢ ( ( 𝜑 ∧ 0 ≤ 𝑀 ) → 𝑀 ∈ ℂ )
120	1 117 119	psergf	⊢ ( ( 𝜑 ∧ 0 ≤ 𝑀 ) → ( 𝐺 ‘ 𝑀 ) : ℕ0 ⟶ ℂ )
121		fco	⊢ ( ( abs : ℂ ⟶ ℝ ∧ ( 𝐺 ‘ 𝑀 ) : ℕ0 ⟶ ℂ ) → ( abs ∘ ( 𝐺 ‘ 𝑀 ) ) : ℕ0 ⟶ ℝ )
122	26 120 121	sylancr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝑀 ) → ( abs ∘ ( 𝐺 ‘ 𝑀 ) ) : ℕ0 ⟶ ℝ )
123	122	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( abs ∘ ( 𝐺 ‘ 𝑀 ) ) ‘ 𝑘 ) ∈ ℝ )
124	29	ad2antrr	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑆 ⊆ ℂ )
125		simprr	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑧 ∈ 𝑆 )
126	124 125	sseldd	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑧 ∈ ℂ )
127		simprl	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑘 ∈ ℕ0 )
128	126 127	expcld	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
129	128	abscld	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( abs ‘ ( 𝑧 ↑ 𝑘 ) ) ∈ ℝ )
130	119	adantr	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑀 ∈ ℂ )
131	130 127	expcld	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝑀 ↑ 𝑘 ) ∈ ℂ )
132	131	abscld	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( abs ‘ ( 𝑀 ↑ 𝑘 ) ) ∈ ℝ )
133	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → 𝐴 : ℕ0 ⟶ ℂ )
134	133 127	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
135	134	abscld	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ )
136	134	absge0d	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → 0 ≤ ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) )
137	126	abscld	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( abs ‘ 𝑧 ) ∈ ℝ )
138	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑀 ∈ ℝ )
139	126	absge0d	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → 0 ≤ ( abs ‘ 𝑧 ) )
140		fveq2	⊢ ( 𝑦 = 𝑧 → ( abs ‘ 𝑦 ) = ( abs ‘ 𝑧 ) )
141	140	breq1d	⊢ ( 𝑦 = 𝑧 → ( ( abs ‘ 𝑦 ) ≤ 𝑀 ↔ ( abs ‘ 𝑧 ) ≤ 𝑀 ) )
142	64	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑆 ( abs ‘ 𝑦 ) ≤ 𝑀 )
143	142	ad2antrr	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ∀ 𝑦 ∈ 𝑆 ( abs ‘ 𝑦 ) ≤ 𝑀 )
144	141 143 125	rspcdva	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( abs ‘ 𝑧 ) ≤ 𝑀 )
145		leexp1a	⊢ ( ( ( ( abs ‘ 𝑧 ) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) ∧ ( 0 ≤ ( abs ‘ 𝑧 ) ∧ ( abs ‘ 𝑧 ) ≤ 𝑀 ) ) → ( ( abs ‘ 𝑧 ) ↑ 𝑘 ) ≤ ( 𝑀 ↑ 𝑘 ) )
146	137 138 127 139 144 145	syl32anc	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( abs ‘ 𝑧 ) ↑ 𝑘 ) ≤ ( 𝑀 ↑ 𝑘 ) )
147	126 127	absexpd	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( abs ‘ ( 𝑧 ↑ 𝑘 ) ) = ( ( abs ‘ 𝑧 ) ↑ 𝑘 ) )
148	130 127	absexpd	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( abs ‘ ( 𝑀 ↑ 𝑘 ) ) = ( ( abs ‘ 𝑀 ) ↑ 𝑘 ) )
149		absid	⊢ ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) → ( abs ‘ 𝑀 ) = 𝑀 )
150	6 149	sylan	⊢ ( ( 𝜑 ∧ 0 ≤ 𝑀 ) → ( abs ‘ 𝑀 ) = 𝑀 )
151	150	adantr	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( abs ‘ 𝑀 ) = 𝑀 )
152	151	oveq1d	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( abs ‘ 𝑀 ) ↑ 𝑘 ) = ( 𝑀 ↑ 𝑘 ) )
153	148 152	eqtrd	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( abs ‘ ( 𝑀 ↑ 𝑘 ) ) = ( 𝑀 ↑ 𝑘 ) )
154	146 147 153	3brtr4d	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( abs ‘ ( 𝑧 ↑ 𝑘 ) ) ≤ ( abs ‘ ( 𝑀 ↑ 𝑘 ) ) )
155	129 132 135 136 154	lemul2ad	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( abs ‘ ( 𝑧 ↑ 𝑘 ) ) ) ≤ ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( abs ‘ ( 𝑀 ↑ 𝑘 ) ) ) )
156	134 128	absmuld	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( abs ‘ ( 𝑧 ↑ 𝑘 ) ) ) )
157	134 131	absmuld	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑀 ↑ 𝑘 ) ) ) = ( ( abs ‘ ( 𝐴 ‘ 𝑘 ) ) · ( abs ‘ ( 𝑀 ↑ 𝑘 ) ) ) )
158	155 156 157	3brtr4d	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ≤ ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑀 ↑ 𝑘 ) ) ) )
159	39	ad2antrr	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑆 ∈ V )
160	159	mptexd	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝑦 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑘 ) ) ∈ V )
161	74 80 127 160	fvmptd3	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ‘ 𝑘 ) = ( 𝑦 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑘 ) ) )
162	161	fveq1d	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( 𝑦 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑘 ) ) ‘ 𝑧 ) )
163		fveq2	⊢ ( 𝑦 = 𝑧 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) )
164	163	fveq1d	⊢ ( 𝑦 = 𝑧 → ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑘 ) = ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑘 ) )
165		eqid	⊢ ( 𝑦 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑘 ) ) = ( 𝑦 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑘 ) )
166		fvex	⊢ ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑘 ) ∈ V
167	164 165 166	fvmpt	⊢ ( 𝑧 ∈ 𝑆 → ( ( 𝑦 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑘 ) ) ‘ 𝑧 ) = ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑘 ) )
168	167	ad2antll	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑦 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑘 ) ) ‘ 𝑧 ) = ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑘 ) )
169	1	pserval2	⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
170	126 127 169	syl2anc	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝐺 ‘ 𝑧 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
171	162 168 170	3eqtrd	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ‘ 𝑘 ) ‘ 𝑧 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
172	171	fveq2d	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( abs ‘ ( ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ‘ 𝑘 ) ‘ 𝑧 ) ) = ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
173	120	adantr	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝐺 ‘ 𝑀 ) : ℕ0 ⟶ ℂ )
174		fvco3	⊢ ( ( ( 𝐺 ‘ 𝑀 ) : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( abs ∘ ( 𝐺 ‘ 𝑀 ) ) ‘ 𝑘 ) = ( abs ‘ ( ( 𝐺 ‘ 𝑀 ) ‘ 𝑘 ) ) )
175	173 127 174	syl2anc	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( abs ∘ ( 𝐺 ‘ 𝑀 ) ) ‘ 𝑘 ) = ( abs ‘ ( ( 𝐺 ‘ 𝑀 ) ‘ 𝑘 ) ) )
176	1	pserval2	⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑀 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑀 ↑ 𝑘 ) ) )
177	130 127 176	syl2anc	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝐺 ‘ 𝑀 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑀 ↑ 𝑘 ) ) )
178	177	fveq2d	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑀 ) ‘ 𝑘 ) ) = ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑀 ↑ 𝑘 ) ) ) )
179	175 178	eqtrd	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( abs ∘ ( 𝐺 ‘ 𝑀 ) ) ‘ 𝑘 ) = ( abs ‘ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑀 ↑ 𝑘 ) ) ) )
180	158 172 179	3brtr4d	⊢ ( ( ( 𝜑 ∧ 0 ≤ 𝑀 ) ∧ ( 𝑘 ∈ ℕ0 ∧ 𝑧 ∈ 𝑆 ) ) → ( abs ‘ ( ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ ( ( abs ∘ ( 𝐺 ‘ 𝑀 ) ) ‘ 𝑘 ) )
181	7	adantr	⊢ ( ( 𝜑 ∧ 0 ≤ 𝑀 ) → 𝑀 < 𝑅 )
182	150 181	eqbrtrd	⊢ ( ( 𝜑 ∧ 0 ≤ 𝑀 ) → ( abs ‘ 𝑀 ) < 𝑅 )
183		id	⊢ ( 𝑖 = 𝑚 → 𝑖 = 𝑚 )
184		2fveq3	⊢ ( 𝑖 = 𝑚 → ( abs ‘ ( ( 𝐺 ‘ 𝑀 ) ‘ 𝑖 ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑀 ) ‘ 𝑚 ) ) )
185	183 184	oveq12d	⊢ ( 𝑖 = 𝑚 → ( 𝑖 · ( abs ‘ ( ( 𝐺 ‘ 𝑀 ) ‘ 𝑖 ) ) ) = ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑀 ) ‘ 𝑚 ) ) ) )
186	185	cbvmptv	⊢ ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺 ‘ 𝑀 ) ‘ 𝑖 ) ) ) ) = ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑀 ) ‘ 𝑚 ) ) ) )
187	1 117 4 119 182 186	radcnvlt1	⊢ ( ( 𝜑 ∧ 0 ≤ 𝑀 ) → ( seq 0 ( + , ( 𝑖 ∈ ℕ0 ↦ ( 𝑖 · ( abs ‘ ( ( 𝐺 ‘ 𝑀 ) ‘ 𝑖 ) ) ) ) ) ∈ dom ⇝ ∧ seq 0 ( + , ( abs ∘ ( 𝐺 ‘ 𝑀 ) ) ) ∈ dom ⇝ ) )
188	187	simprd	⊢ ( ( 𝜑 ∧ 0 ≤ 𝑀 ) → seq 0 ( + , ( abs ∘ ( 𝐺 ‘ 𝑀 ) ) ) ∈ dom ⇝ )
189	21 98 99 111 116 123 180 188	mtest	⊢ ( ( 𝜑 ∧ 0 ≤ 𝑀 ) → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑤 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑤 ) ‘ 𝑚 ) ) ) ) ∈ dom ( ⇝𝑢 ‘ 𝑆 ) )
190	97 189	eqeltrd	⊢ ( ( 𝜑 ∧ 0 ≤ 𝑀 ) → 𝐻 ∈ dom ( ⇝𝑢 ‘ 𝑆 ) )
191		simpr	⊢ ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) → 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 )
192		ulmcl	⊢ ( 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 → 𝑓 : 𝑆 ⟶ ℂ )
193	192	adantl	⊢ ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) → 𝑓 : 𝑆 ⟶ ℂ )
194	193	feqmptd	⊢ ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) → 𝑓 = ( 𝑦 ∈ 𝑆 ↦ ( 𝑓 ‘ 𝑦 ) ) )
195		0zd	⊢ ( ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) ∧ 𝑦 ∈ 𝑆 ) → 0 ∈ ℤ )
196		eqidd	⊢ ( ( ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) = ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) )
197	31	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑦 ) : ℕ0 ⟶ ℂ )
198	197	ffvelcdmda	⊢ ( ( ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) ∈ ℂ )
199	44	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) ∧ 𝑦 ∈ 𝑆 ) → 𝐻 : ℕ0 ⟶ ( ℂ ↑m 𝑆 ) )
200		simpr	⊢ ( ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝑆 )
201		seqex	⊢ seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ∈ V
202	201	a1i	⊢ ( ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) ∧ 𝑦 ∈ 𝑆 ) → seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ∈ V )
203		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℕ0 )
204	39	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → 𝑆 ∈ V )
205	204	mptexd	⊢ ( ( ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ∈ V )
206	5	fvmpt2	⊢ ( ( 𝑖 ∈ ℕ0 ∧ ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ∈ V ) → ( 𝐻 ‘ 𝑖 ) = ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) )
207	203 205 206	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑖 ) = ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) )
208	207	fveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝐻 ‘ 𝑖 ) ‘ 𝑦 ) = ( ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ‘ 𝑦 ) )
209		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → 𝑦 ∈ 𝑆 )
210		fvex	⊢ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ∈ V
211		eqid	⊢ ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) = ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) )
212	211	fvmpt2	⊢ ( ( 𝑦 ∈ 𝑆 ∧ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ∈ V ) → ( ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ‘ 𝑦 ) = ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) )
213	209 210 212	sylancl	⊢ ( ( ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ‘ 𝑦 ) = ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) )
214	208 213	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝐻 ‘ 𝑖 ) ‘ 𝑦 ) = ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) )
215		simplr	⊢ ( ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) ∧ 𝑦 ∈ 𝑆 ) → 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 )
216	21 195 199 200 202 214 215	ulmclm	⊢ ( ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) ∧ 𝑦 ∈ 𝑆 ) → seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ⇝ ( 𝑓 ‘ 𝑦 ) )
217	21 195 196 198 216	isumclim	⊢ ( ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) ∧ 𝑦 ∈ 𝑆 ) → Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) = ( 𝑓 ‘ 𝑦 ) )
218	217	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) → ( 𝑦 ∈ 𝑆 ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) ) = ( 𝑦 ∈ 𝑆 ↦ ( 𝑓 ‘ 𝑦 ) ) )
219	2 218	eqtrid	⊢ ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) → 𝐹 = ( 𝑦 ∈ 𝑆 ↦ ( 𝑓 ‘ 𝑦 ) ) )
220	194 219	eqtr4d	⊢ ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) → 𝑓 = 𝐹 )
221	191 220	breqtrd	⊢ ( ( 𝜑 ∧ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) → 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐹 )
222	221	ex	⊢ ( 𝜑 → ( 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 → 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐹 ) )
223	222	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑓 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 → 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐹 ) )
224		eldmg	⊢ ( 𝐻 ∈ dom ( ⇝𝑢 ‘ 𝑆 ) → ( 𝐻 ∈ dom ( ⇝𝑢 ‘ 𝑆 ) ↔ ∃ 𝑓 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 ) )
225	224	ibi	⊢ ( 𝐻 ∈ dom ( ⇝𝑢 ‘ 𝑆 ) → ∃ 𝑓 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝑓 )
226	223 225	impel	⊢ ( ( 𝜑 ∧ 𝐻 ∈ dom ( ⇝𝑢 ‘ 𝑆 ) ) → 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐹 )
227	190 226	syldan	⊢ ( ( 𝜑 ∧ 0 ≤ 𝑀 ) → 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐹 )
228		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
229	71 227 6 228	ltlecasei	⊢ ( 𝜑 → 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐹 )