Metamath Proof Explorer

Theorem cvgcmpce

Description: A comparison test for convergence of a complex infinite series. (Contributed by NM, 25-Apr-2005) (Revised by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses cvgcmpce.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
cvgcmpce.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
cvgcmpce.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
cvgcmpce.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
cvgcmpce.5 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
cvgcmpce.6 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
cvgcmpce.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 𝐶 · ( 𝐹 ‘ 𝑘 ) ) )
Assertion cvgcmpce ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ∈ dom ⇝ )

Proof

Step Hyp Ref Expression
1 cvgcmpce.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 cvgcmpce.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
3 cvgcmpce.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
4 cvgcmpce.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
5 cvgcmpce.5 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
6 cvgcmpce.6 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
7 cvgcmpce.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) ≤ ( 𝐶 · ( 𝐹 ‘ 𝑘 ) ) )
8 2 1 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
9 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
10 8 9 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
11 1 10 4 serf ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) : 𝑍 ⟶ ℂ )
12 11 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ )
13 fveq2 ⊢ ( 𝑚 = 𝑘 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑘 ) )
14 13 oveq2d ⊢ ( 𝑚 = 𝑘 → ( 𝐶 · ( 𝐹 ‘ 𝑚 ) ) = ( 𝐶 · ( 𝐹 ‘ 𝑘 ) ) )
15 eqid ⊢ ( 𝑚 ∈ 𝑍 ↦ ( 𝐶 · ( 𝐹 ‘ 𝑚 ) ) ) = ( 𝑚 ∈ 𝑍 ↦ ( 𝐶 · ( 𝐹 ‘ 𝑚 ) ) )
16 ovex ⊢ ( 𝐶 · ( 𝐹 ‘ 𝑘 ) ) ∈ V
17 14 15 16 fvmpt ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝑚 ∈ 𝑍 ↦ ( 𝐶 · ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑘 ) = ( 𝐶 · ( 𝐹 ‘ 𝑘 ) ) )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( 𝐶 · ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑘 ) = ( 𝐶 · ( 𝐹 ‘ 𝑘 ) ) )
19 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐶 ∈ ℝ )
20 19 3 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐶 · ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
21 18 20 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( 𝐶 · ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑘 ) ∈ ℝ )
22 2fveq3 ⊢ ( 𝑚 = 𝑘 → ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) = ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) )
23 eqid ⊢ ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) = ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) )
24 fvex ⊢ ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ V
25 22 23 24 fvmpt ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ‘ 𝑘 ) = ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) )
26 25 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ‘ 𝑘 ) = ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) )
27 4 abscld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ )
28 26 27 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ‘ 𝑘 ) ∈ ℝ )
29 6 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
30 climdm ⊢ ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑀 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )
31 5 30 sylib ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )
32 3 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
33 1 10 29 31 32 18 isermulc2 ⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( 𝐶 · ( 𝐹 ‘ 𝑚 ) ) ) ) ⇝ ( 𝐶 · ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) ) )
34 climrel ⊢ Rel ⇝
35 34 releldmi ⊢ ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( 𝐶 · ( 𝐹 ‘ 𝑚 ) ) ) ) ⇝ ( 𝐶 · ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) ) → seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( 𝐶 · ( 𝐹 ‘ 𝑚 ) ) ) ) ∈ dom ⇝ )
36 33 35 syl ⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( 𝐶 · ( 𝐹 ‘ 𝑚 ) ) ) ) ∈ dom ⇝ )
37 1 uztrn2 ⊢ ( ( 𝑁 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ 𝑍 )
38 2 37 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ 𝑍 )
39 4 absge0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) )
40 39 26 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ ( ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ‘ 𝑘 ) )
41 38 40 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 ≤ ( ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ‘ 𝑘 ) )
42 38 25 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ‘ 𝑘 ) = ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) )
43 38 17 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( 𝐶 · ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑘 ) = ( 𝐶 · ( 𝐹 ‘ 𝑘 ) ) )
44 7 42 43 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ‘ 𝑘 ) ≤ ( ( 𝑚 ∈ 𝑍 ↦ ( 𝐶 · ( 𝐹 ‘ 𝑚 ) ) ) ‘ 𝑘 ) )
45 1 2 21 28 36 41 44 cvgcmp ⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ∈ dom ⇝ )
46 1 climcau ⊢ ( ( 𝑀 ∈ ℤ ∧ seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ∈ dom ⇝ ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) ) < 𝑥 )
47 10 45 46 syl2anc ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) ) < 𝑥 )
48 1 10 28 serfre ⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) : 𝑍 ⟶ ℝ )
49 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) : 𝑍 ⟶ ℝ )
50 1 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑛 ∈ 𝑍 )
51 50 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑛 ∈ 𝑍 )
52 49 51 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) ∈ ℝ )
53 simprl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑗 ∈ 𝑍 )
54 49 53 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ∈ ℝ )
55 52 54 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) ∈ ℝ )
56 0red ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 0 ∈ ℝ )
57 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → seq 𝑀 ( + , 𝐺 ) : 𝑍 ⟶ ℂ )
58 57 51 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) ∈ ℂ )
59 57 53 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ∈ ℂ )
60 58 59 subcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ) ∈ ℂ )
61 60 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ) ) ∈ ℝ )
62 60 absge0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 0 ≤ ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ) ) )
63 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑀 ... 𝑛 ) ∈ Fin )
64 difss ⊢ ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ⊆ ( 𝑀 ... 𝑛 )
65 ssfi ⊢ ( ( ( 𝑀 ... 𝑛 ) ∈ Fin ∧ ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ⊆ ( 𝑀 ... 𝑛 ) ) → ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ∈ Fin )
66 63 64 65 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ∈ Fin )
67 eldifi ⊢ ( 𝑘 ∈ ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) → 𝑘 ∈ ( 𝑀 ... 𝑛 ) )
68 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝜑 )
69 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑛 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
70 69 1 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑛 ) → 𝑘 ∈ 𝑍 )
71 68 70 4 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
72 67 71 sylan2 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
73 66 72 fsumabs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( abs ‘ Σ 𝑘 ∈ ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ( 𝐺 ‘ 𝑘 ) ) ≤ Σ 𝑘 ∈ ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) )
74 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
75 51 1 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
76 74 75 71 fsumser ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( 𝐺 ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) )
77 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) )
78 53 1 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
79 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
80 79 1 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ 𝑍 )
81 68 80 4 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
82 77 78 81 fsumser ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ( 𝐺 ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) )
83 76 82 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( 𝐺 ‘ 𝑘 ) − Σ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ( 𝐺 ‘ 𝑘 ) ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ) )
84 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑀 ... 𝑗 ) ∈ Fin )
85 84 81 fsumcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
86 66 72 fsumcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → Σ 𝑘 ∈ ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
87 disjdif ⊢ ( ( 𝑀 ... 𝑗 ) ∩ ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ) = ∅
88 87 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝑀 ... 𝑗 ) ∩ ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ) = ∅ )
89 undif2 ⊢ ( ( 𝑀 ... 𝑗 ) ∪ ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ) = ( ( 𝑀 ... 𝑗 ) ∪ ( 𝑀 ... 𝑛 ) )
90 fzss2 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) → ( 𝑀 ... 𝑗 ) ⊆ ( 𝑀 ... 𝑛 ) )
91 90 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑀 ... 𝑗 ) ⊆ ( 𝑀 ... 𝑛 ) )
92 ssequn1 ⊢ ( ( 𝑀 ... 𝑗 ) ⊆ ( 𝑀 ... 𝑛 ) ↔ ( ( 𝑀 ... 𝑗 ) ∪ ( 𝑀 ... 𝑛 ) ) = ( 𝑀 ... 𝑛 ) )
93 91 92 sylib ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝑀 ... 𝑗 ) ∪ ( 𝑀 ... 𝑛 ) ) = ( 𝑀 ... 𝑛 ) )
94 89 93 eqtr2id ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑀 ... 𝑛 ) = ( ( 𝑀 ... 𝑗 ) ∪ ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ) )
95 88 94 63 71 fsumsplit ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( 𝐺 ‘ 𝑘 ) = ( Σ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ( 𝐺 ‘ 𝑘 ) + Σ 𝑘 ∈ ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ( 𝐺 ‘ 𝑘 ) ) )
96 85 86 95 mvrladdd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( 𝐺 ‘ 𝑘 ) − Σ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ( 𝐺 ‘ 𝑘 ) ) = Σ 𝑘 ∈ ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ( 𝐺 ‘ 𝑘 ) )
97 83 96 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ) = Σ 𝑘 ∈ ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ( 𝐺 ‘ 𝑘 ) )
98 97 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ) ) = ( abs ‘ Σ 𝑘 ∈ ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ( 𝐺 ‘ 𝑘 ) ) )
99 70 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → 𝑘 ∈ 𝑍 )
100 99 25 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ‘ 𝑘 ) = ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) )
101 abscl ⊢ ( ( 𝐺 ‘ 𝑘 ) ∈ ℂ → ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ )
102 101 recnd ⊢ ( ( 𝐺 ‘ 𝑘 ) ∈ ℂ → ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ )
103 71 102 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ) → ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ )
104 100 75 103 fsumser ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) = ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) )
105 80 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → 𝑘 ∈ 𝑍 )
106 105 25 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ‘ 𝑘 ) = ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) )
107 81 102 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ )
108 106 78 107 fsumser ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) = ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) )
109 104 108 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) − Σ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) ) = ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) )
110 84 107 fsumcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ )
111 72 102 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ 𝑘 ∈ ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ) → ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ )
112 66 111 fsumcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → Σ 𝑘 ∈ ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) ∈ ℂ )
113 88 94 63 103 fsumsplit ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) = ( Σ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) + Σ 𝑘 ∈ ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) ) )
114 110 112 113 mvrladdd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( Σ 𝑘 ∈ ( 𝑀 ... 𝑛 ) ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) − Σ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) ) = Σ 𝑘 ∈ ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) )
115 109 114 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) = Σ 𝑘 ∈ ( ( 𝑀 ... 𝑛 ) ∖ ( 𝑀 ... 𝑗 ) ) ( abs ‘ ( 𝐺 ‘ 𝑘 ) ) )
116 73 98 115 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ) ) ≤ ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) )
117 56 61 55 62 116 letrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 0 ≤ ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) )
118 55 117 absidd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( abs ‘ ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) ) = ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) )
119 118 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( abs ‘ ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) ) < 𝑥 ↔ ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) < 𝑥 ) )
120 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
121 120 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑥 ∈ ℝ )
122 lelttr ⊢ ( ( ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ) ) ∈ ℝ ∧ ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ) ) ≤ ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) ∧ ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) < 𝑥 ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ) ) < 𝑥 ) )
123 61 55 121 122 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ) ) ≤ ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) ∧ ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) < 𝑥 ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ) ) < 𝑥 ) )
124 116 123 mpand ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) < 𝑥 → ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ) ) < 𝑥 ) )
125 119 124 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( abs ‘ ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) ) < 𝑥 → ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ) ) < 𝑥 ) )
126 125 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) ) < 𝑥 → ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ) ) < 𝑥 ) )
127 126 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) ) < 𝑥 → ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ) ) < 𝑥 ) )
128 127 reximdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) ) < 𝑥 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ) ) < 𝑥 ) )
129 128 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑛 ) − ( seq 𝑀 ( + , ( 𝑚 ∈ 𝑍 ↦ ( abs ‘ ( 𝐺 ‘ 𝑚 ) ) ) ) ‘ 𝑗 ) ) ) < 𝑥 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ) ) < 𝑥 ) )
130 47 129 mpd ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑗 ) ) ) < 𝑥 )
131 seqex ⊢ seq 𝑀 ( + , 𝐺 ) ∈ V
132 131 a1i ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ∈ V )
133 1 12 130 132 caucvg ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ∈ dom ⇝ )