Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐹 )