Metamath Proof Explorer

Theorem mtest

Description: The Weierstrass M-test. If F is a sequence of functions which are uniformly bounded by the convergent sequence M ( k ) , then the series generated by the sequence F converges uniformly. (Contributed by Mario Carneiro, 3-Mar-2015)

Ref Expression
Hypotheses mtest.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
mtest.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
mtest.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
mtest.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
mtest.m ⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
mtest.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑀 ‘ 𝑘 ) ∈ ℝ )
mtest.l ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ ( 𝑀 ‘ 𝑘 ) )
mtest.d ⊢ ( 𝜑 → seq 𝑁 ( + , 𝑀 ) ∈ dom ⇝ )
Assertion mtest ( 𝜑 → seq 𝑁 ( ∘f + , 𝐹 ) ∈ dom ( ⇝𝑢 ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 mtest.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
2 mtest.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
3 mtest.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4 mtest.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
5 mtest.m ⊢ ( 𝜑 → 𝑀 ∈ 𝑊 )
6 mtest.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑀 ‘ 𝑘 ) ∈ ℝ )
7 mtest.l ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ ( 𝑀 ‘ 𝑘 ) )
8 mtest.d ⊢ ( 𝜑 → seq 𝑁 ( + , 𝑀 ) ∈ dom ⇝ )
9 1 climcau ⊢ ( ( 𝑁 ∈ ℤ ∧ seq 𝑁 ( + , 𝑀 ) ∈ dom ⇝ ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ) < 𝑟 )
10 2 8 9 syl2anc ⊢ ( 𝜑 → ∀ 𝑟 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ) < 𝑟 )
11 seqfn ⊢ ( 𝑁 ∈ ℤ → seq 𝑁 ( ∘f + , 𝐹 ) Fn ( ℤ≥ ‘ 𝑁 ) )
12 2 11 syl ⊢ ( 𝜑 → seq 𝑁 ( ∘f + , 𝐹 ) Fn ( ℤ≥ ‘ 𝑁 ) )
13 1 fneq2i ⊢ ( seq 𝑁 ( ∘f + , 𝐹 ) Fn 𝑍 ↔ seq 𝑁 ( ∘f + , 𝐹 ) Fn ( ℤ≥ ‘ 𝑁 ) )
14 12 13 sylibr ⊢ ( 𝜑 → seq 𝑁 ( ∘f + , 𝐹 ) Fn 𝑍 )
15 3 elexd ⊢ ( 𝜑 → 𝑆 ∈ V )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝑆 ∈ V )
17 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ 𝑍 )
18 17 1 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑁 ) )
19 4 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
20 elfzuz ⊢ ( 𝑘 ∈ ( 𝑁 ... 𝑖 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) )
21 20 1 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑁 ... 𝑖 ) → 𝑘 ∈ 𝑍 )
22 ffvelrn ⊢ ( ( 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) )
23 19 21 22 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) )
24 elmapi ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) → ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ )
25 23 24 syl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ) → ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ )
26 25 feqmptd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝑧 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) )
27 21 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ) → 𝑘 ∈ 𝑍 )
28 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) )
29 28 fveq1d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) )
30 eqid ⊢ ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) )
31 fvex ⊢ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ V
32 29 30 31 fvmpt ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) )
33 27 32 syl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ) → ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) )
34 33 mpteq2dv ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ) → ( 𝑧 ∈ 𝑆 ↦ ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ‘ 𝑘 ) ) = ( 𝑧 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) )
35 26 34 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝑧 ∈ 𝑆 ↦ ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ‘ 𝑘 ) ) )
36 16 18 35 seqof ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) = ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ) )
37 2 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → 𝑁 ∈ ℤ )
38 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ℂ ↑m 𝑆 ) )
39 elmapi ⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℂ ↑m 𝑆 ) → ( 𝐹 ‘ 𝑛 ) : 𝑆 ⟶ ℂ )
40 38 39 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : 𝑆 ⟶ ℂ )
41 40 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ∈ ℂ )
42 41 an32s ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ∈ ℂ )
43 42 fmpttd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) : 𝑍 ⟶ ℂ )
44 43 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑖 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ‘ 𝑖 ) ∈ ℂ )
45 1 37 44 serf ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) → seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) : 𝑍 ⟶ ℂ )
46 45 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑖 ∈ 𝑍 ) → ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ∈ ℂ )
47 46 an32s ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ∈ ℂ )
48 47 fmpttd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ) : 𝑆 ⟶ ℂ )
49 cnex ⊢ ℂ ∈ V
50 elmapg ⊢ ( ( ℂ ∈ V ∧ 𝑆 ∈ V ) → ( ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ) ∈ ( ℂ ↑m 𝑆 ) ↔ ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ) : 𝑆 ⟶ ℂ ) )
51 49 16 50 sylancr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ) ∈ ( ℂ ↑m 𝑆 ) ↔ ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ) : 𝑆 ⟶ ℂ ) )
52 48 51 mpbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ) ∈ ( ℂ ↑m 𝑆 ) )
53 36 52 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ∈ ( ℂ ↑m 𝑆 ) )
54 53 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑍 ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ∈ ( ℂ ↑m 𝑆 ) )
55 ffnfv ⊢ ( seq 𝑁 ( ∘f + , 𝐹 ) : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) ↔ ( seq 𝑁 ( ∘f + , 𝐹 ) Fn 𝑍 ∧ ∀ 𝑖 ∈ 𝑍 ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ∈ ( ℂ ↑m 𝑆 ) ) )
56 14 54 55 sylanbrc ⊢ ( 𝜑 → seq 𝑁 ( ∘f + , 𝐹 ) : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
57 56 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → seq 𝑁 ( ∘f + , 𝐹 ) : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
58 1 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑖 ∈ 𝑍 )
59 58 adantl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑖 ∈ 𝑍 )
60 57 59 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ∈ ( ℂ ↑m 𝑆 ) )
61 elmapi ⊢ ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ∈ ( ℂ ↑m 𝑆 ) → ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) : 𝑆 ⟶ ℂ )
62 60 61 syl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) : 𝑆 ⟶ ℂ )
63 62 ffvelrnda ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) ∈ ℂ )
64 simprl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑗 ∈ 𝑍 )
65 57 64 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ∈ ( ℂ ↑m 𝑆 ) )
66 elmapi ⊢ ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ∈ ( ℂ ↑m 𝑆 ) → ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) : 𝑆 ⟶ ℂ )
67 65 66 syl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) : 𝑆 ⟶ ℂ )
68 67 ffvelrnda ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ∈ ℂ )
69 63 68 subcld ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) − ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ) ∈ ℂ )
70 69 abscld ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ ( ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) − ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ) ) ∈ ℝ )
71 fzfid ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑗 + 1 ) ... 𝑖 ) ∈ Fin )
72 ssun2 ⊢ ( ( 𝑗 + 1 ) ... 𝑖 ) ⊆ ( ( 𝑁 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑖 ) )
73 64 1 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) )
74 simprr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) )
75 elfzuzb ⊢ ( 𝑗 ∈ ( 𝑁 ... 𝑖 ) ↔ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) )
76 73 74 75 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑗 ∈ ( 𝑁 ... 𝑖 ) )
77 fzsplit ⊢ ( 𝑗 ∈ ( 𝑁 ... 𝑖 ) → ( 𝑁 ... 𝑖 ) = ( ( 𝑁 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑖 ) ) )
78 76 77 syl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑁 ... 𝑖 ) = ( ( 𝑁 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑖 ) ) )
79 72 78 sseqtrrid ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝑗 + 1 ) ... 𝑖 ) ⊆ ( 𝑁 ... 𝑖 ) )
80 79 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ) → 𝑘 ∈ ( 𝑁 ... 𝑖 ) )
81 80 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ) → 𝑘 ∈ ( 𝑁 ... 𝑖 ) )
82 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
83 82 21 22 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) )
84 83 24 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ) → ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ )
85 84 ffvelrnda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ ℂ )
86 85 an32s ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ ℂ )
87 81 86 syldan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ ℂ )
88 87 abscld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ∈ ℝ )
89 71 88 fsumrecl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ∈ ℝ )
90 1 2 6 serfre ⊢ ( 𝜑 → seq 𝑁 ( + , 𝑀 ) : 𝑍 ⟶ ℝ )
91 90 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → seq 𝑁 ( + , 𝑀 ) : 𝑍 ⟶ ℝ )
92 91 59 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) ∈ ℝ )
93 91 64 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ∈ ℝ )
94 92 93 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ∈ ℝ )
95 94 recnd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ∈ ℂ )
96 95 abscld ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( abs ‘ ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ) ∈ ℝ )
97 96 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ) ∈ ℝ )
98 58 36 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) = ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ) )
99 98 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) = ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ) )
100 99 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) = ( ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ) ‘ 𝑧 ) )
101 fvex ⊢ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ∈ V
102 eqid ⊢ ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ) = ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) )
103 102 fvmpt2 ⊢ ( ( 𝑧 ∈ 𝑆 ∧ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ∈ V ) → ( ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ) ‘ 𝑧 ) = ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) )
104 101 103 mpan2 ⊢ ( 𝑧 ∈ 𝑆 → ( ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ) ‘ 𝑧 ) = ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) )
105 100 104 sylan9eq ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) = ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) )
106 fveq2 ⊢ ( 𝑖 = 𝑗 → ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) = ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) )
107 fveq2 ⊢ ( 𝑖 = 𝑗 → ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) = ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑗 ) )
108 107 mpteq2dv ⊢ ( 𝑖 = 𝑗 → ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ) = ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑗 ) ) )
109 106 108 eqeq12d ⊢ ( 𝑖 = 𝑗 → ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) = ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ) ↔ ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) = ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑗 ) ) ) )
110 36 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑍 ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) = ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ) )
111 110 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ∀ 𝑖 ∈ 𝑍 ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) = ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) ) )
112 109 111 64 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) = ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑗 ) ) )
113 112 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) = ( ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑗 ) ) ‘ 𝑧 ) )
114 fvex ⊢ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑗 ) ∈ V
115 eqid ⊢ ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑗 ) ) = ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑗 ) )
116 115 fvmpt2 ⊢ ( ( 𝑧 ∈ 𝑆 ∧ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑗 ) ∈ V ) → ( ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑗 ) ) ‘ 𝑧 ) = ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑗 ) )
117 114 116 mpan2 ⊢ ( 𝑧 ∈ 𝑆 → ( ( 𝑧 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑗 ) ) ‘ 𝑧 ) = ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑗 ) )
118 113 117 sylan9eq ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) = ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑗 ) )
119 105 118 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) − ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ) = ( ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) − ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑗 ) ) )
120 21 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ) → 𝑘 ∈ 𝑍 )
121 120 32 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ) → ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) )
122 59 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → 𝑖 ∈ 𝑍 )
123 122 1 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑁 ) )
124 121 123 86 fsumser ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) )
125 elfzuz ⊢ ( 𝑘 ∈ ( 𝑁 ... 𝑗 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) )
126 125 1 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑁 ... 𝑗 ) → 𝑘 ∈ 𝑍 )
127 126 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ) → 𝑘 ∈ 𝑍 )
128 127 32 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ) → ( ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) )
129 64 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → 𝑗 ∈ 𝑍 )
130 129 1 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) )
131 82 126 22 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℂ ↑m 𝑆 ) )
132 131 24 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) : 𝑆 ⟶ ℂ )
133 132 ffvelrnda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ ℂ )
134 133 an32s ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ ℂ )
135 128 130 134 fsumser ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑗 ) )
136 124 135 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( Σ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − Σ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) = ( ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑖 ) − ( seq 𝑁 ( + , ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) ) ) ‘ 𝑗 ) ) )
137 fzfid ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑁 ... 𝑗 ) ∈ Fin )
138 137 134 fsumcl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ ℂ )
139 71 87 fsumcl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ ℂ )
140 eluzelre ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑗 ∈ ℝ )
141 73 140 syl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑗 ∈ ℝ )
142 141 ltp1d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑗 < ( 𝑗 + 1 ) )
143 fzdisj ⊢ ( 𝑗 < ( 𝑗 + 1 ) → ( ( 𝑁 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑖 ) ) = ∅ )
144 142 143 syl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝑁 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑖 ) ) = ∅ )
145 144 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑁 ... 𝑗 ) ∩ ( ( 𝑗 + 1 ) ... 𝑖 ) ) = ∅ )
146 78 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑁 ... 𝑖 ) = ( ( 𝑁 ... 𝑗 ) ∪ ( ( 𝑗 + 1 ) ... 𝑖 ) ) )
147 fzfid ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑁 ... 𝑖 ) ∈ Fin )
148 145 146 147 86 fsumsplit ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = ( Σ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) + Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) )
149 138 139 148 mvrladdd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( Σ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) − Σ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) = Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) )
150 119 136 149 3eqtr2d ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) − ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ) = Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) )
151 150 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ ( ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) − ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ) ) = ( abs ‘ Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) )
152 71 87 fsumabs ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) )
153 151 152 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ ( ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) − ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ) ) ≤ Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) )
154 simpll ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝜑 )
155 154 21 6 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ) → ( 𝑀 ‘ 𝑘 ) ∈ ℝ )
156 80 155 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ) → ( 𝑀 ‘ 𝑘 ) ∈ ℝ )
157 156 adantlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ) → ( 𝑀 ‘ 𝑘 ) ∈ ℝ )
158 81 21 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ) → 𝑘 ∈ 𝑍 )
159 7 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( 𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ ( 𝑀 ‘ 𝑘 ) )
160 159 anass1rs ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ ( 𝑀 ‘ 𝑘 ) )
161 158 160 syldan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ ( 𝑀 ‘ 𝑘 ) )
162 71 88 157 161 fsumle ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( 𝑀 ‘ 𝑘 ) )
163 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ) → ( 𝑀 ‘ 𝑘 ) = ( 𝑀 ‘ 𝑘 ) )
164 59 1 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑁 ) )
165 155 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ) → ( 𝑀 ‘ 𝑘 ) ∈ ℂ )
166 163 164 165 fsumser ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ 𝑘 ) = ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) )
167 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ) → ( 𝑀 ‘ 𝑘 ) = ( 𝑀 ‘ 𝑘 ) )
168 154 126 6 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ) → ( 𝑀 ‘ 𝑘 ) ∈ ℝ )
169 168 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ) → ( 𝑀 ‘ 𝑘 ) ∈ ℂ )
170 167 73 169 fsumser ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ( 𝑀 ‘ 𝑘 ) = ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) )
171 166 170 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( Σ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ 𝑘 ) − Σ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ( 𝑀 ‘ 𝑘 ) ) = ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) )
172 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑁 ... 𝑗 ) ∈ Fin )
173 172 169 fsumcl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ( 𝑀 ‘ 𝑘 ) ∈ ℂ )
174 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝑗 + 1 ) ... 𝑖 ) ∈ Fin )
175 80 165 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ) → ( 𝑀 ‘ 𝑘 ) ∈ ℂ )
176 174 175 fsumcl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( 𝑀 ‘ 𝑘 ) ∈ ℂ )
177 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑁 ... 𝑖 ) ∈ Fin )
178 144 78 177 165 fsumsplit ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ 𝑘 ) = ( Σ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ( 𝑀 ‘ 𝑘 ) + Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( 𝑀 ‘ 𝑘 ) ) )
179 173 176 178 mvrladdd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( Σ 𝑘 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ 𝑘 ) − Σ 𝑘 ∈ ( 𝑁 ... 𝑗 ) ( 𝑀 ‘ 𝑘 ) ) = Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( 𝑀 ‘ 𝑘 ) )
180 171 179 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) = Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( 𝑀 ‘ 𝑘 ) )
181 180 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( abs ‘ ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ) = ( abs ‘ Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( 𝑀 ‘ 𝑘 ) ) )
182 181 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ) = ( abs ‘ Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( 𝑀 ‘ 𝑘 ) ) )
183 180 94 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( 𝑀 ‘ 𝑘 ) ∈ ℝ )
184 183 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( 𝑀 ‘ 𝑘 ) ∈ ℝ )
185 0red ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ) → 0 ∈ ℝ )
186 87 absge0d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ) → 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) )
187 185 88 157 186 161 letrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ) → 0 ≤ ( 𝑀 ‘ 𝑘 ) )
188 71 157 187 fsumge0 ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → 0 ≤ Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( 𝑀 ‘ 𝑘 ) )
189 184 188 absidd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( 𝑀 ‘ 𝑘 ) ) = Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( 𝑀 ‘ 𝑘 ) )
190 182 189 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ) = Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( 𝑀 ‘ 𝑘 ) )
191 162 190 breqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → Σ 𝑘 ∈ ( ( 𝑗 + 1 ) ... 𝑖 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ ( abs ‘ ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ) )
192 70 89 97 153 191 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ ( ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) − ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ) ) ≤ ( abs ‘ ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ) )
193 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → 𝑟 ∈ ℝ+ )
194 193 rpred ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → 𝑟 ∈ ℝ )
195 lelttr ⊢ ( ( ( abs ‘ ( ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) − ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ) ) ∈ ℝ ∧ ( abs ‘ ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ) ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( ( ( abs ‘ ( ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) − ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ) ) ≤ ( abs ‘ ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ) ∧ ( abs ‘ ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ) < 𝑟 ) → ( abs ‘ ( ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) − ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑟 ) )
196 70 97 194 195 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( ( abs ‘ ( ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) − ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ) ) ≤ ( abs ‘ ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ) ∧ ( abs ‘ ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ) < 𝑟 ) → ( abs ‘ ( ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) − ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑟 ) )
197 192 196 mpand ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑧 ∈ 𝑆 ) → ( ( abs ‘ ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ) < 𝑟 → ( abs ‘ ( ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) − ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑟 ) )
198 197 ralrimdva ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( abs ‘ ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ) < 𝑟 → ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) − ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑟 ) )
199 198 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ) < 𝑟 → ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) − ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑟 ) )
200 199 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ) < 𝑟 → ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) − ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑟 ) )
201 200 reximdva ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ) < 𝑟 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) − ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑟 ) )
202 201 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑖 ) − ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑗 ) ) ) < 𝑟 → ∀ 𝑟 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) − ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑟 ) )
203 10 202 mpd ⊢ ( 𝜑 → ∀ 𝑟 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) − ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑟 )
204 1 2 3 56 ulmcau ⊢ ( 𝜑 → ( seq 𝑁 ( ∘f + , 𝐹 ) ∈ dom ( ⇝𝑢 ‘ 𝑆 ) ↔ ∀ 𝑟 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑖 ) ‘ 𝑧 ) − ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑗 ) ‘ 𝑧 ) ) ) < 𝑟 ) )
205 203 204 mpbird ⊢ ( 𝜑 → seq 𝑁 ( ∘f + , 𝐹 ) ∈ dom ( ⇝𝑢 ‘ 𝑆 ) )