Metamath Proof Explorer

Theorem mtestbdd

Description: Given the hypotheses of the Weierstrass M-test, the convergent function of the sequence is uniformly bounded. (Contributed by Mario Carneiro, 9-Jul-2017)

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

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 mtest.t ⊢ ( 𝜑 → seq 𝑁 ( ∘f + , 𝐹 ) ( ⇝𝑢 ‘ 𝑆 ) 𝑇 )
10 6 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑀 ‘ 𝑘 ) ∈ ℂ )
11 1 2 10 serf ⊢ ( 𝜑 → seq 𝑁 ( + , 𝑀 ) : 𝑍 ⟶ ℂ )
12 11 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ∈ ℂ )
13 12 ralrimiva ⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑍 ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ∈ ℂ )
14 1 climbdd ⊢ ( ( 𝑁 ∈ ℤ ∧ seq 𝑁 ( + , 𝑀 ) ∈ dom ⇝ ∧ ∀ 𝑚 ∈ 𝑍 ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ∈ ℂ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 )
15 2 8 13 14 syl3anc ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 )
16 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) → 𝑁 ∈ ℤ )
17 seqfn ⊢ ( 𝑁 ∈ ℤ → seq 𝑁 ( ∘f + , 𝐹 ) Fn ( ℤ≥ ‘ 𝑁 ) )
18 2 17 syl ⊢ ( 𝜑 → seq 𝑁 ( ∘f + , 𝐹 ) Fn ( ℤ≥ ‘ 𝑁 ) )
19 1 fneq2i ⊢ ( seq 𝑁 ( ∘f + , 𝐹 ) Fn 𝑍 ↔ seq 𝑁 ( ∘f + , 𝐹 ) Fn ( ℤ≥ ‘ 𝑁 ) )
20 18 19 sylibr ⊢ ( 𝜑 → seq 𝑁 ( ∘f + , 𝐹 ) Fn 𝑍 )
21 ulmf2 ⊢ ( ( seq 𝑁 ( ∘f + , 𝐹 ) Fn 𝑍 ∧ seq 𝑁 ( ∘f + , 𝐹 ) ( ⇝𝑢 ‘ 𝑆 ) 𝑇 ) → seq 𝑁 ( ∘f + , 𝐹 ) : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
22 20 9 21 syl2anc ⊢ ( 𝜑 → seq 𝑁 ( ∘f + , 𝐹 ) : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
23 22 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) → seq 𝑁 ( ∘f + , 𝐹 ) : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
24 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) → 𝑦 ∈ ℝ )
25 fveq2 ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) )
26 25 mpteq2dv ⊢ ( 𝑥 = 𝑧 → ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) = ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) )
27 26 seqeq3d ⊢ ( 𝑥 = 𝑧 → seq 𝑁 ( + , ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) ) = seq 𝑁 ( + , ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) )
28 27 fveq1d ⊢ ( 𝑥 = 𝑧 → ( seq 𝑁 ( + , ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) ) ‘ 𝑛 ) = ( seq 𝑁 ( + , ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) ‘ 𝑛 ) )
29 eqid ⊢ ( 𝑥 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) ) ‘ 𝑛 ) ) = ( 𝑥 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) ) ‘ 𝑛 ) )
30 fvex ⊢ ( seq 𝑁 ( + , ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) ‘ 𝑛 ) ∈ V
31 28 29 30 fvmpt ⊢ ( 𝑧 ∈ 𝑆 → ( ( 𝑥 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) ) ‘ 𝑛 ) ) ‘ 𝑧 ) = ( seq 𝑁 ( + , ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) ‘ 𝑛 ) )
32 31 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( 𝑥 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) ) ‘ 𝑛 ) ) ‘ 𝑧 ) = ( seq 𝑁 ( + , ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) ‘ 𝑛 ) )
33 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
34 33 feqmptd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → 𝐹 = ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) )
35 33 ffvelcdmda ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ( ℂ ↑m 𝑆 ) )
36 elmapi ⊢ ( ( 𝐹 ‘ 𝑗 ) ∈ ( ℂ ↑m 𝑆 ) → ( 𝐹 ‘ 𝑗 ) : 𝑆 ⟶ ℂ )
37 35 36 syl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) : 𝑆 ⟶ ℂ )
38 37 feqmptd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) )
39 38 mpteq2dva ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) = ( 𝑗 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) ) )
40 34 39 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → 𝐹 = ( 𝑗 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) ) )
41 40 seqeq3d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → seq 𝑁 ( ∘f + , 𝐹 ) = seq 𝑁 ( ∘f + , ( 𝑗 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) ) ) )
42 41 fveq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑛 ) = ( seq 𝑁 ( ∘f + , ( 𝑗 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) ) ) ‘ 𝑛 ) )
43 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → 𝑆 ∈ 𝑉 )
44 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → 𝑛 ∈ 𝑍 )
45 44 1 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) )
46 elfzuz ⊢ ( 𝑘 ∈ ( 𝑁 ... 𝑛 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) )
47 46 1 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑁 ... 𝑛 ) → 𝑘 ∈ 𝑍 )
48 47 ssriv ⊢ ( 𝑁 ... 𝑛 ) ⊆ 𝑍
49 48 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑁 ... 𝑛 ) ⊆ 𝑍 )
50 37 ffvelcdmda ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ∈ ℂ )
51 50 anasss ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑥 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ∈ ℂ )
52 43 45 49 51 seqof2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( seq 𝑁 ( ∘f + , ( 𝑗 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) ) ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) ) ‘ 𝑛 ) ) )
53 42 52 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) ) ‘ 𝑛 ) ) )
54 53 fveq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑛 ) ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝑆 ↦ ( seq 𝑁 ( + , ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑥 ) ) ) ‘ 𝑛 ) ) ‘ 𝑧 ) )
55 47 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ) → 𝑘 ∈ 𝑍 )
56 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑘 ) )
57 56 fveq1d ⊢ ( 𝑗 = 𝑘 → ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) )
58 eqid ⊢ ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) = ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) )
59 fvex ⊢ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ V
60 57 58 59 fvmpt ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) )
61 55 60 syl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ) → ( ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) )
62 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑗 ∈ 𝑍 ) → 𝑧 ∈ 𝑆 )
63 37 62 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ∈ ℂ )
64 63 fmpttd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) : 𝑍 ⟶ ℂ )
65 64 ffvelcdmda ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ‘ 𝑘 ) ∈ ℂ )
66 47 65 sylan2 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ) → ( ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ‘ 𝑘 ) ∈ ℂ )
67 61 66 eqeltrrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ ℂ )
68 61 45 67 fsumser ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) = ( seq 𝑁 ( + , ( 𝑗 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑗 ) ‘ 𝑧 ) ) ) ‘ 𝑛 ) )
69 32 54 68 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑛 ) ‘ 𝑧 ) = Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) )
70 69 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑛 ) ‘ 𝑧 ) ) = ( abs ‘ Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) )
71 fzfid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝑁 ... 𝑛 ) ∈ Fin )
72 71 67 fsumcl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ∈ ℂ )
73 72 abscld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ∈ ℝ )
74 67 abscld ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ∈ ℝ )
75 71 74 fsumrecl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ∈ ℝ )
76 24 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → 𝑦 ∈ ℝ )
77 71 67 fsumabs ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) )
78 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ) → 𝜑 )
79 78 55 6 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ) → ( 𝑀 ‘ 𝑘 ) ∈ ℝ )
80 71 79 fsumrecl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( 𝑀 ‘ 𝑘 ) ∈ ℝ )
81 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ) → 𝑧 ∈ 𝑆 )
82 78 55 81 7 syl12anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ ( 𝑀 ‘ 𝑘 ) )
83 71 74 79 82 fsumle ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( 𝑀 ‘ 𝑘 ) )
84 80 recnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( 𝑀 ‘ 𝑘 ) ∈ ℂ )
85 84 abscld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( 𝑀 ‘ 𝑘 ) ) ∈ ℝ )
86 80 leabsd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( 𝑀 ‘ 𝑘 ) ≤ ( abs ‘ Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( 𝑀 ‘ 𝑘 ) ) )
87 eqidd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ) → ( 𝑀 ‘ 𝑘 ) = ( 𝑀 ‘ 𝑘 ) )
88 78 55 10 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ) → ( 𝑀 ‘ 𝑘 ) ∈ ℂ )
89 87 45 88 fsumser ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( 𝑀 ‘ 𝑘 ) = ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑛 ) )
90 89 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( 𝑀 ‘ 𝑘 ) ) = ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑛 ) ) )
91 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) → ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 )
92 fveq2 ⊢ ( 𝑚 = 𝑛 → ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) = ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑛 ) )
93 92 fveq2d ⊢ ( 𝑚 = 𝑛 → ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) = ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑛 ) ) )
94 93 breq1d ⊢ ( 𝑚 = 𝑛 → ( ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ↔ ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑛 ) ) ≤ 𝑦 ) )
95 94 rspccva ⊢ ( ( ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ∧ 𝑛 ∈ 𝑍 ) → ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑛 ) ) ≤ 𝑦 )
96 91 95 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) → ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑛 ) ) ≤ 𝑦 )
97 96 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑛 ) ) ≤ 𝑦 )
98 90 97 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( 𝑀 ‘ 𝑘 ) ) ≤ 𝑦 )
99 80 85 76 86 98 letrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( 𝑀 ‘ 𝑘 ) ≤ 𝑦 )
100 75 80 76 83 99 letrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑦 )
101 73 75 76 77 100 letrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ Σ 𝑘 ∈ ( 𝑁 ... 𝑛 ) ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ≤ 𝑦 )
102 70 101 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑧 ∈ 𝑆 ) → ( abs ‘ ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑛 ) ‘ 𝑧 ) ) ≤ 𝑦 )
103 102 ralrimiva ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) → ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑛 ) ‘ 𝑧 ) ) ≤ 𝑦 )
104 brralrspcev ⊢ ( ( 𝑦 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑛 ) ‘ 𝑧 ) ) ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑛 ) ‘ 𝑧 ) ) ≤ 𝑥 )
105 24 103 104 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) ∧ 𝑛 ∈ 𝑍 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( seq 𝑁 ( ∘f + , 𝐹 ) ‘ 𝑛 ) ‘ 𝑧 ) ) ≤ 𝑥 )
106 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) → seq 𝑁 ( ∘f + , 𝐹 ) ( ⇝𝑢 ‘ 𝑆 ) 𝑇 )
107 1 16 23 105 106 ulmbdd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ ∀ 𝑚 ∈ 𝑍 ( abs ‘ ( seq 𝑁 ( + , 𝑀 ) ‘ 𝑚 ) ) ≤ 𝑦 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ 𝑥 )
108 15 107 rexlimddv ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( 𝑇 ‘ 𝑧 ) ) ≤ 𝑥 )