This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem serf0

Description: If an infinite series converges, its underlying sequence converges to zero. (Contributed by NM, 2-Sep-2005) (Revised by Mario Carneiro, 16-Feb-2014)

Ref Expression
Hypotheses caucvgb.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
serf0.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
serf0.3 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
serf0.4 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
serf0.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
Assertion serf0 ( 𝜑 → 𝐹 ⇝ 0 )

Proof

Step Hyp Ref Expression
1 caucvgb.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 serf0.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 serf0.3 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
4 serf0.4 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
5 serf0.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
6 1 caucvgb ⊢ ( ( 𝑀 ∈ ℤ ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) → ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) ) )
7 2 4 6 syl2anc ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) ) )
8 4 7 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) )
9 1 cau3 ⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ∈ ℂ ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ∈ ℂ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) ) < 𝑥 ) )
10 8 9 sylib ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ∈ ℂ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) ) < 𝑥 ) )
11 1 peano2uzs ⊢ ( 𝑗 ∈ 𝑍 → ( 𝑗 + 1 ) ∈ 𝑍 )
12 11 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝑗 + 1 ) ∈ 𝑍 )
13 eluzelz ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) → 𝑚 ∈ ℤ )
14 uzid ⊢ ( 𝑚 ∈ ℤ → 𝑚 ∈ ( ℤ≥ ‘ 𝑚 ) )
15 peano2uz ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑚 ) → ( 𝑚 + 1 ) ∈ ( ℤ≥ ‘ 𝑚 ) )
16 fveq2 ⊢ ( 𝑘 = ( 𝑚 + 1 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑚 + 1 ) ) )
17 16 oveq2d ⊢ ( 𝑘 = ( 𝑚 + 1 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑚 + 1 ) ) ) )
18 17 fveq2d ⊢ ( 𝑘 = ( 𝑚 + 1 ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) ) = ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑚 + 1 ) ) ) ) )
19 18 breq1d ⊢ ( 𝑘 = ( 𝑚 + 1 ) → ( ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑚 + 1 ) ) ) ) < 𝑥 ) )
20 19 rspcv ⊢ ( ( 𝑚 + 1 ) ∈ ( ℤ≥ ‘ 𝑚 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) ) < 𝑥 → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑚 + 1 ) ) ) ) < 𝑥 ) )
21 13 14 15 20 4syl ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) ) < 𝑥 → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑚 + 1 ) ) ) ) < 𝑥 ) )
22 21 adantld ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ∈ ℂ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) ) < 𝑥 ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑚 + 1 ) ) ) ) < 𝑥 ) )
23 22 ralimia ⊢ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ∈ ℂ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) ) < 𝑥 ) → ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑚 + 1 ) ) ) ) < 𝑥 )
24 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝑍 )
25 24 1 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
26 eluzelz ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑗 ∈ ℤ )
27 25 26 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ ℤ )
28 eluzp1m1 ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( 𝑘 − 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) )
29 27 28 sylan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( 𝑘 − 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) )
30 fveq2 ⊢ ( 𝑚 = ( 𝑘 − 1 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) )
31 fvoveq1 ⊢ ( 𝑚 = ( 𝑘 − 1 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑚 + 1 ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑘 − 1 ) + 1 ) ) )
32 30 31 oveq12d ⊢ ( 𝑚 = ( 𝑘 − 1 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑚 + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑘 − 1 ) + 1 ) ) ) )
33 32 fveq2d ⊢ ( 𝑚 = ( 𝑘 − 1 ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑚 + 1 ) ) ) ) = ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑘 − 1 ) + 1 ) ) ) ) )
34 33 breq1d ⊢ ( 𝑚 = ( 𝑘 − 1 ) → ( ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑚 + 1 ) ) ) ) < 𝑥 ↔ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑘 − 1 ) + 1 ) ) ) ) < 𝑥 ) )
35 34 rspcv ⊢ ( ( 𝑘 − 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑚 + 1 ) ) ) ) < 𝑥 → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑘 − 1 ) + 1 ) ) ) ) < 𝑥 ) )
36 29 35 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑚 + 1 ) ) ) ) < 𝑥 → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑘 − 1 ) + 1 ) ) ) ) < 𝑥 ) )
37 1 2 5 serf ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℂ )
38 37 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℂ )
39 1 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ ( 𝑘 − 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑘 − 1 ) ∈ 𝑍 )
40 24 29 39 syl2an2r ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( 𝑘 − 1 ) ∈ 𝑍 )
41 38 40 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) ∈ ℂ )
42 1 uztrn2 ⊢ ( ( ( 𝑗 + 1 ) ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → 𝑘 ∈ 𝑍 )
43 12 42 sylan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → 𝑘 ∈ 𝑍 )
44 38 43 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ∈ ℂ )
45 41 44 abssubd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) ) = ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) ) ) )
46 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) → 𝑘 ∈ ℤ )
47 46 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → 𝑘 ∈ ℤ )
48 47 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → 𝑘 ∈ ℂ )
49 ax-1cn ⊢ 1 ∈ ℂ
50 npcan ⊢ ( ( 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑘 − 1 ) + 1 ) = 𝑘 )
51 48 49 50 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( ( 𝑘 − 1 ) + 1 ) = 𝑘 )
52 51 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑘 − 1 ) + 1 ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) )
53 52 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑘 − 1 ) + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) )
54 53 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑘 − 1 ) + 1 ) ) ) ) = ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) ) )
55 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → 𝑀 ∈ ℤ )
56 eluzp1p1 ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
57 25 56 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
58 eqid ⊢ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) = ( ℤ≥ ‘ ( 𝑀 + 1 ) )
59 58 uztrn2 ⊢ ( ( ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
60 57 59 sylan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
61 seqm1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) + ( 𝐹 ‘ 𝑘 ) ) )
62 55 60 61 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) + ( 𝐹 ‘ 𝑘 ) ) )
63 62 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) ) = ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) + ( 𝐹 ‘ 𝑘 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) ) )
64 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
65 43 64 syldan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
66 41 65 pncan2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) + ( 𝐹 ‘ 𝑘 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) ) = ( 𝐹 ‘ 𝑘 ) )
67 63 66 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) ) )
68 67 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) = ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) ) ) )
69 45 54 68 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑘 − 1 ) + 1 ) ) ) ) = ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
70 69 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑘 − 1 ) + 1 ) ) ) ) < 𝑥 ↔ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) )
71 36 70 sylibd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑚 + 1 ) ) ) ) < 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) )
72 71 ralrimdva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑚 + 1 ) ) ) ) < 𝑥 → ∀ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) )
73 23 72 syl5 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ∈ ℂ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) ) < 𝑥 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) )
74 fveq2 ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( ℤ≥ ‘ 𝑛 ) = ( ℤ≥ ‘ ( 𝑗 + 1 ) ) )
75 74 raleqdv ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) )
76 75 rspcev ⊢ ( ( ( 𝑗 + 1 ) ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 )
77 12 73 76 syl6an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ∈ ℂ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) ) < 𝑥 ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) )
78 77 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ∈ ℂ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) ) < 𝑥 ) → ∃ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) )
79 78 ralimdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) ∈ ℂ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑚 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑘 ) ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) )
80 10 79 mpd ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 )
81 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
82 1 2 3 81 5 clim0c ⊢ ( 𝜑 → ( 𝐹 ⇝ 0 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑛 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) )
83 80 82 mpbird ⊢ ( 𝜑 → 𝐹 ⇝ 0 )