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 ffvelrnd ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑘 ∈ ( ℤ ‘ ( 𝑗 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑘 − 1 ) ) ∈ ℂ )
42 1 uztrn2 ( ( ( 𝑗 + 1 ) ∈ 𝑍𝑘 ∈ ( ℤ ‘ ( 𝑗 + 1 ) ) ) → 𝑘𝑍 )
43 12 42 sylan ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑘 ∈ ( ℤ ‘ ( 𝑗 + 1 ) ) ) → 𝑘𝑍 )
44 38 43 ffvelrnd ( ( ( 𝜑𝑗𝑍 ) ∧ 𝑘 ∈ ( ℤ ‘ ( 𝑗 + 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 )