Metamath Proof Explorer

Theorem iseralt

Description: The alternating series test. If G ( k ) is a decreasing sequence that converges to 0 , then sum_ k e. Z ( -u 1 ^ k ) x. G ( k ) is a convergent series. (Note that the first term is positive if M is even, and negative if M is odd. If the parity of your series does not match up with this, you will need to post-compose the series with multiplication by -u 1 using isermulc2 .) (Contributed by Mario Carneiro, 7-Apr-2015) (Proof shortened by AV, 9-Jul-2022)

Ref Expression
Hypotheses iseralt.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
iseralt.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
iseralt.3 ⊢ ( 𝜑 → 𝐺 : 𝑍 ⟶ ℝ )
iseralt.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐺 ‘ 𝑘 ) )
iseralt.5 ⊢ ( 𝜑 → 𝐺 ⇝ 0 )
iseralt.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( ( - 1 ↑ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
Assertion iseralt ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )

Proof

Step Hyp Ref Expression
1 iseralt.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 iseralt.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 iseralt.3 ⊢ ( 𝜑 → 𝐺 : 𝑍 ⟶ ℝ )
4 iseralt.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐺 ‘ 𝑘 ) )
5 iseralt.5 ⊢ ( 𝜑 → 𝐺 ⇝ 0 )
6 iseralt.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( ( - 1 ↑ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
7 seqex ⊢ seq 𝑀 ( + , 𝐹 ) ∈ V
8 7 a1i ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ V )
9 climrel ⊢ Rel ⇝
10 9 brrelex1i ⊢ ( 𝐺 ⇝ 0 → 𝐺 ∈ V )
11 5 10 syl ⊢ ( 𝜑 → 𝐺 ∈ V )
12 eqidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) )
13 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑛 ) ∈ ℝ )
14 13 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑛 ) ∈ ℂ )
15 1 2 11 12 14 clim0c ⊢ ( 𝜑 → ( 𝐺 ⇝ 0 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑥 ) )
16 5 15 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑥 )
17 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝑍 )
18 17 1 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
19 eluzelz ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑗 ∈ ℤ )
20 uzid ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
21 18 19 20 3syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
22 peano2uz ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) → ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) )
23 2fveq3 ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( abs ‘ ( 𝐺 ‘ 𝑛 ) ) = ( abs ‘ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) )
24 23 breq1d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( ( abs ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑥 ↔ ( abs ‘ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) < 𝑥 ) )
25 24 rspcv ⊢ ( ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑥 → ( abs ‘ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) < 𝑥 ) )
26 21 22 25 3syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑥 → ( abs ‘ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) < 𝑥 ) )
27 eluzelz ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) → 𝑛 ∈ ℤ )
28 27 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑛 ∈ ℤ )
29 28 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑛 ∈ ℂ )
30 19 1 eleq2s ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ )
31 30 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑗 ∈ ℤ )
32 31 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑗 ∈ ℂ )
33 29 32 subcld ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑛 − 𝑗 ) ∈ ℂ )
34 2cnd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 2 ∈ ℂ )
35 2ne0 ⊢ 2 ≠ 0
36 35 a1i ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 2 ≠ 0 )
37 33 34 36 divcan2d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 2 · ( ( 𝑛 − 𝑗 ) / 2 ) ) = ( 𝑛 − 𝑗 ) )
38 37 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑗 + ( 2 · ( ( 𝑛 − 𝑗 ) / 2 ) ) ) = ( 𝑗 + ( 𝑛 − 𝑗 ) ) )
39 32 29 pncan3d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑗 + ( 𝑛 − 𝑗 ) ) = 𝑛 )
40 38 39 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑛 = ( 𝑗 + ( 2 · ( ( 𝑛 − 𝑗 ) / 2 ) ) ) )
41 40 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( 𝑛 − 𝑗 ) / 2 ) ∈ ℤ ) → 𝑛 = ( 𝑗 + ( 2 · ( ( 𝑛 − 𝑗 ) / 2 ) ) ) )
42 41 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( 𝑛 − 𝑗 ) / 2 ) ∈ ℤ ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑗 + ( 2 · ( ( 𝑛 − 𝑗 ) / 2 ) ) ) ) )
43 42 fvoveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( 𝑛 − 𝑗 ) / 2 ) ∈ ℤ ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) = ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑗 + ( 2 · ( ( 𝑛 − 𝑗 ) / 2 ) ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) )
44 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( 𝑛 − 𝑗 ) / 2 ) ∈ ℤ ) → 𝜑 )
45 simpl ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑗 ∈ 𝑍 )
46 45 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( 𝑛 − 𝑗 ) / 2 ) ∈ ℤ ) → 𝑗 ∈ 𝑍 )
47 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( 𝑛 − 𝑗 ) / 2 ) ∈ ℤ ) → ( ( 𝑛 − 𝑗 ) / 2 ) ∈ ℤ )
48 28 31 zsubcld ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑛 − 𝑗 ) ∈ ℤ )
49 48 zred ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑛 − 𝑗 ) ∈ ℝ )
50 2rp ⊢ 2 ∈ ℝ+
51 50 a1i ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 2 ∈ ℝ+ )
52 eluzle ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) → 𝑗 ≤ 𝑛 )
53 52 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑗 ≤ 𝑛 )
54 28 zred ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑛 ∈ ℝ )
55 31 zred ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑗 ∈ ℝ )
56 54 55 subge0d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 0 ≤ ( 𝑛 − 𝑗 ) ↔ 𝑗 ≤ 𝑛 ) )
57 53 56 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 0 ≤ ( 𝑛 − 𝑗 ) )
58 49 51 57 divge0d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 0 ≤ ( ( 𝑛 − 𝑗 ) / 2 ) )
59 58 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( 𝑛 − 𝑗 ) / 2 ) ∈ ℤ ) → 0 ≤ ( ( 𝑛 − 𝑗 ) / 2 ) )
60 elnn0z ⊢ ( ( ( 𝑛 − 𝑗 ) / 2 ) ∈ ℕ0 ↔ ( ( ( 𝑛 − 𝑗 ) / 2 ) ∈ ℤ ∧ 0 ≤ ( ( 𝑛 − 𝑗 ) / 2 ) ) )
61 47 59 60 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( 𝑛 − 𝑗 ) / 2 ) ∈ ℤ ) → ( ( 𝑛 − 𝑗 ) / 2 ) ∈ ℕ0 )
62 1 2 3 4 5 6 iseraltlem3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ( ( 𝑛 − 𝑗 ) / 2 ) ∈ ℕ0 ) → ( ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑗 + ( 2 · ( ( 𝑛 − 𝑗 ) / 2 ) ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ≤ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑗 + ( 2 · ( ( 𝑛 − 𝑗 ) / 2 ) ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ≤ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) )
63 62 simpld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ( ( 𝑛 − 𝑗 ) / 2 ) ∈ ℕ0 ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑗 + ( 2 · ( ( 𝑛 − 𝑗 ) / 2 ) ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ≤ ( 𝐺 ‘ ( 𝑗 + 1 ) ) )
64 44 46 61 63 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( 𝑛 − 𝑗 ) / 2 ) ∈ ℤ ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑗 + ( 2 · ( ( 𝑛 − 𝑗 ) / 2 ) ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ≤ ( 𝐺 ‘ ( 𝑗 + 1 ) ) )
65 43 64 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( 𝑛 − 𝑗 ) / 2 ) ∈ ℤ ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ≤ ( 𝐺 ‘ ( 𝑗 + 1 ) ) )
66 2div2e1 ⊢ ( 2 / 2 ) = 1
67 66 oveq2i ⊢ ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − ( 2 / 2 ) ) = ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − 1 )
68 peano2cn ⊢ ( ( 𝑛 − 𝑗 ) ∈ ℂ → ( ( 𝑛 − 𝑗 ) + 1 ) ∈ ℂ )
69 33 68 syl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝑛 − 𝑗 ) + 1 ) ∈ ℂ )
70 69 34 34 36 divsubdird ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( ( 𝑛 − 𝑗 ) + 1 ) − 2 ) / 2 ) = ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − ( 2 / 2 ) ) )
71 df-2 ⊢ 2 = ( 1 + 1 )
72 71 oveq2i ⊢ ( ( ( 𝑛 − 𝑗 ) + 1 ) − 2 ) = ( ( ( 𝑛 − 𝑗 ) + 1 ) − ( 1 + 1 ) )
73 ax-1cn ⊢ 1 ∈ ℂ
74 73 a1i ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 1 ∈ ℂ )
75 33 74 74 pnpcan2d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( 𝑛 − 𝑗 ) + 1 ) − ( 1 + 1 ) ) = ( ( 𝑛 − 𝑗 ) − 1 ) )
76 72 75 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( 𝑛 − 𝑗 ) + 1 ) − 2 ) = ( ( 𝑛 − 𝑗 ) − 1 ) )
77 76 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( ( 𝑛 − 𝑗 ) + 1 ) − 2 ) / 2 ) = ( ( ( 𝑛 − 𝑗 ) − 1 ) / 2 ) )
78 70 77 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − ( 2 / 2 ) ) = ( ( ( 𝑛 − 𝑗 ) − 1 ) / 2 ) )
79 67 78 eqtr3id ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − 1 ) = ( ( ( 𝑛 − 𝑗 ) − 1 ) / 2 ) )
80 79 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 2 · ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − 1 ) ) = ( 2 · ( ( ( 𝑛 − 𝑗 ) − 1 ) / 2 ) ) )
81 subcl ⊢ ( ( ( 𝑛 − 𝑗 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 − 𝑗 ) − 1 ) ∈ ℂ )
82 33 73 81 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝑛 − 𝑗 ) − 1 ) ∈ ℂ )
83 82 34 36 divcan2d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 2 · ( ( ( 𝑛 − 𝑗 ) − 1 ) / 2 ) ) = ( ( 𝑛 − 𝑗 ) − 1 ) )
84 29 32 74 sub32d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝑛 − 𝑗 ) − 1 ) = ( ( 𝑛 − 1 ) − 𝑗 ) )
85 80 83 84 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 2 · ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − 1 ) ) = ( ( 𝑛 − 1 ) − 𝑗 ) )
86 85 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑗 + ( 2 · ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − 1 ) ) ) = ( 𝑗 + ( ( 𝑛 − 1 ) − 𝑗 ) ) )
87 subcl ⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑛 − 1 ) ∈ ℂ )
88 29 73 87 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑛 − 1 ) ∈ ℂ )
89 32 88 pncan3d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑗 + ( ( 𝑛 − 1 ) − 𝑗 ) ) = ( 𝑛 − 1 ) )
90 86 89 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑗 + ( 2 · ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − 1 ) ) ) = ( 𝑛 − 1 ) )
91 90 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝑗 + ( 2 · ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − 1 ) ) ) + 1 ) = ( ( 𝑛 − 1 ) + 1 ) )
92 npcan ⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
93 29 73 92 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
94 91 93 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑛 = ( ( 𝑗 + ( 2 · ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − 1 ) ) ) + 1 ) )
95 94 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) ∈ ℤ ) → 𝑛 = ( ( 𝑗 + ( 2 · ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − 1 ) ) ) + 1 ) )
96 95 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) ∈ ℤ ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑗 + ( 2 · ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − 1 ) ) ) + 1 ) ) )
97 96 fvoveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) ∈ ℤ ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) = ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑗 + ( 2 · ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − 1 ) ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) )
98 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) ∈ ℤ ) → 𝜑 )
99 45 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) ∈ ℤ ) → 𝑗 ∈ 𝑍 )
100 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) ∈ ℤ ) → ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) ∈ ℤ )
101 uznn0sub ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) → ( 𝑛 − 𝑗 ) ∈ ℕ0 )
102 101 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑛 − 𝑗 ) ∈ ℕ0 )
103 nn0p1nn ⊢ ( ( 𝑛 − 𝑗 ) ∈ ℕ0 → ( ( 𝑛 − 𝑗 ) + 1 ) ∈ ℕ )
104 102 103 syl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝑛 − 𝑗 ) + 1 ) ∈ ℕ )
105 104 nnrpd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝑛 − 𝑗 ) + 1 ) ∈ ℝ+ )
106 105 rphalfcld ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) ∈ ℝ+ )
107 106 rpgt0d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 0 < ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) )
108 107 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) ∈ ℤ ) → 0 < ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) )
109 elnnz ⊢ ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) ∈ ℕ ↔ ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) ∈ ℤ ∧ 0 < ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) ) )
110 100 108 109 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) ∈ ℤ ) → ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) ∈ ℕ )
111 nnm1nn0 ⊢ ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) ∈ ℕ → ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − 1 ) ∈ ℕ0 )
112 110 111 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) ∈ ℤ ) → ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − 1 ) ∈ ℕ0 )
113 1 2 3 4 5 6 iseraltlem3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − 1 ) ∈ ℕ0 ) → ( ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑗 + ( 2 · ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − 1 ) ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ≤ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑗 + ( 2 · ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − 1 ) ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ≤ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) )
114 113 simprd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − 1 ) ∈ ℕ0 ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑗 + ( 2 · ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − 1 ) ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ≤ ( 𝐺 ‘ ( 𝑗 + 1 ) ) )
115 98 99 112 114 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) ∈ ℤ ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑗 + ( 2 · ( ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) − 1 ) ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ≤ ( 𝐺 ‘ ( 𝑗 + 1 ) ) )
116 97 115 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) ∧ ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) ∈ ℤ ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ≤ ( 𝐺 ‘ ( 𝑗 + 1 ) ) )
117 zeo ⊢ ( ( 𝑛 − 𝑗 ) ∈ ℤ → ( ( ( 𝑛 − 𝑗 ) / 2 ) ∈ ℤ ∨ ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) ∈ ℤ ) )
118 48 117 syl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( 𝑛 − 𝑗 ) / 2 ) ∈ ℤ ∨ ( ( ( 𝑛 − 𝑗 ) + 1 ) / 2 ) ∈ ℤ ) )
119 65 116 118 mpjaodan ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ≤ ( 𝐺 ‘ ( 𝑗 + 1 ) ) )
120 1 peano2uzs ⊢ ( 𝑗 ∈ 𝑍 → ( 𝑗 + 1 ) ∈ 𝑍 )
121 120 adantr ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑗 + 1 ) ∈ 𝑍 )
122 ffvelrn ⊢ ( ( 𝐺 : 𝑍 ⟶ ℝ ∧ ( 𝑗 + 1 ) ∈ 𝑍 ) → ( 𝐺 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
123 3 121 122 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐺 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
124 1 2 3 4 5 iseraltlem1 ⊢ ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ 𝑍 ) → 0 ≤ ( 𝐺 ‘ ( 𝑗 + 1 ) ) )
125 121 124 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 0 ≤ ( 𝐺 ‘ ( 𝑗 + 1 ) ) )
126 123 125 absidd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( abs ‘ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) = ( 𝐺 ‘ ( 𝑗 + 1 ) ) )
127 119 126 breqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ≤ ( abs ‘ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) )
128 127 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ≤ ( abs ‘ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) )
129 neg1rr ⊢ - 1 ∈ ℝ
130 129 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → - 1 ∈ ℝ )
131 neg1ne0 ⊢ - 1 ≠ 0
132 131 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → - 1 ≠ 0 )
133 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℤ )
134 133 1 eleq2s ⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ )
135 134 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ℤ )
136 130 132 135 reexpclzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( - 1 ↑ 𝑘 ) ∈ ℝ )
137 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
138 136 137 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( - 1 ↑ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ )
139 6 138 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
140 1 2 139 serfre ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ )
141 1 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑛 ∈ 𝑍 )
142 ffvelrn ⊢ ( ( seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ ∧ 𝑛 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℝ )
143 140 141 142 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℝ )
144 ffvelrn ⊢ ( ( seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ∈ ℝ )
145 140 45 144 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ∈ ℝ )
146 143 145 resubcld ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ∈ ℝ )
147 146 recnd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ∈ ℂ )
148 147 abscld ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ∈ ℝ )
149 148 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ∈ ℝ )
150 126 123 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( abs ‘ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ )
151 150 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( abs ‘ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ )
152 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
153 152 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑥 ∈ ℝ )
154 lelttr ⊢ ( ( ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ≤ ( abs ‘ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∧ ( abs ‘ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) < 𝑥 ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) )
155 149 151 153 154 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) ≤ ( abs ‘ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∧ ( abs ‘ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) < 𝑥 ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) )
156 128 155 mpand ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( abs ‘ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) < 𝑥 → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) )
157 140 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ )
158 157 141 142 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℝ )
159 156 158 jctild ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( abs ‘ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) < 𝑥 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℝ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) ) )
160 159 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( abs ‘ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) < 𝑥 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℝ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) ) )
161 160 ralrimdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ( abs ‘ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) < 𝑥 → ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℝ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) ) )
162 26 161 syld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑥 → ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℝ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) ) )
163 162 reximdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑥 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℝ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) ) )
164 163 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( 𝐺 ‘ 𝑛 ) ) < 𝑥 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℝ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) ) )
165 16 164 mpd ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) ∈ ℝ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑛 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) )
166 1 8 165 caurcvg2 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )