Metamath Proof Explorer

Theorem dvgrat

Description: Ratio test for divergence of a complex infinite series. See e.g. remark "if ( abs( ( a( n + 1 ) ) / ( an ) ) ) >_ 1 for all large n..." in https://en.wikipedia.org/wiki/Ratio_test#The_test . (Contributed by Steve Rodriguez, 28-Feb-2020)

Ref Expression
Hypotheses dvgrat.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
dvgrat.w ⊢ 𝑊 = ( ℤ≥ ‘ 𝑁 )
dvgrat.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
dvgrat.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
dvgrat.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
dvgrat.n0 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( 𝐹 ‘ 𝑘 ) ≠ 0 )
dvgrat.le ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
Assertion dvgrat ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∉ dom ⇝ )

Proof

Step Hyp Ref Expression
1 dvgrat.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 dvgrat.w ⊢ 𝑊 = ( ℤ≥ ‘ 𝑁 )
3 dvgrat.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
4 dvgrat.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
5 dvgrat.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
6 dvgrat.n0 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( 𝐹 ‘ 𝑘 ) ≠ 0 )
7 dvgrat.le ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
8 3 1 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
9 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
10 8 9 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
11 uzid ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
12 11 2 eleqtrrdi ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ 𝑊 )
13 10 12 syl ⊢ ( 𝜑 → 𝑁 ∈ 𝑊 )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑁 ) → 𝑘 = 𝑁 )
15 14 eleq1d ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑁 ) → ( 𝑘 ∈ 𝑊 ↔ 𝑁 ∈ 𝑊 ) )
16 14 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑁 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑁 ) )
17 16 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑁 ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) )
18 17 breq2d ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑁 ) → ( 0 < ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ↔ 0 < ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
19 15 18 imbi12d ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑁 ) → ( ( 𝑘 ∈ 𝑊 → 0 < ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ↔ ( 𝑁 ∈ 𝑊 → 0 < ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ) ) )
20 2 eleq2i ⊢ ( 𝑘 ∈ 𝑊 ↔ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) )
21 1 uztrn2 ⊢ ( ( 𝑁 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ 𝑍 )
22 20 21 sylan2b ⊢ ( ( 𝑁 ∈ 𝑍 ∧ 𝑘 ∈ 𝑊 ) → 𝑘 ∈ 𝑍 )
23 3 22 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → 𝑘 ∈ 𝑍 )
24 23 5 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
25 absgt0 ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ → ( ( 𝐹 ‘ 𝑘 ) ≠ 0 ↔ 0 < ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
26 24 25 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( ( 𝐹 ‘ 𝑘 ) ≠ 0 ↔ 0 < ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
27 6 26 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → 0 < ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
28 27 ex ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑊 → 0 < ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
29 3 19 28 vtocld ⊢ ( 𝜑 → ( 𝑁 ∈ 𝑊 → 0 < ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
30 13 29 mpd ⊢ ( 𝜑 → 0 < ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) )
31 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
32 14 eleq1d ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑁 ) → ( 𝑘 ∈ 𝑍 ↔ 𝑁 ∈ 𝑍 ) )
33 16 eleq1d ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑁 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑁 ) ∈ ℂ ) )
34 32 33 imbi12d ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑁 ) → ( ( 𝑘 ∈ 𝑍 → ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ↔ ( 𝑁 ∈ 𝑍 → ( 𝐹 ‘ 𝑁 ) ∈ ℂ ) ) )
35 5 ex ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 → ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) )
36 3 34 35 vtocld ⊢ ( 𝜑 → ( 𝑁 ∈ 𝑍 → ( 𝐹 ‘ 𝑁 ) ∈ ℂ ) )
37 3 36 mpd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℂ )
38 37 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ )
39 31 38 ltnled ⊢ ( 𝜑 → ( 0 < ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ↔ ¬ ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ 0 ) )
40 30 39 mpbid ⊢ ( 𝜑 → ¬ ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ 0 )
41 10 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 0 ) → 𝑁 ∈ ℤ )
42 38 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 0 ) → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ )
43 simpr ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 0 ) → 𝐹 ⇝ 0 )
44 2 fvexi ⊢ 𝑊 ∈ V
45 44 mptex ⊢ ( 𝑖 ∈ 𝑊 ↦ ( abs ‘ ( 𝐹 ‘ 𝑖 ) ) ) ∈ V
46 45 a1i ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 0 ) → ( 𝑖 ∈ 𝑊 ↦ ( abs ‘ ( 𝐹 ‘ 𝑖 ) ) ) ∈ V )
47 24 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝ 0 ) ∧ 𝑘 ∈ 𝑊 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
48 eqidd ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝ 0 ) ∧ 𝑘 ∈ 𝑊 ) → ( 𝑖 ∈ 𝑊 ↦ ( abs ‘ ( 𝐹 ‘ 𝑖 ) ) ) = ( 𝑖 ∈ 𝑊 ↦ ( abs ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
49 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ⇝ 0 ) ∧ 𝑘 ∈ 𝑊 ) ∧ 𝑖 = 𝑘 ) → 𝑖 = 𝑘 )
50 49 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ⇝ 0 ) ∧ 𝑘 ∈ 𝑊 ) ∧ 𝑖 = 𝑘 ) → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑘 ) )
51 50 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ⇝ 0 ) ∧ 𝑘 ∈ 𝑊 ) ∧ 𝑖 = 𝑘 ) → ( abs ‘ ( 𝐹 ‘ 𝑖 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
52 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝ 0 ) ∧ 𝑘 ∈ 𝑊 ) → 𝑘 ∈ 𝑊 )
53 fvex ⊢ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ V
54 53 a1i ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝ 0 ) ∧ 𝑘 ∈ 𝑊 ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ V )
55 48 51 52 54 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝ 0 ) ∧ 𝑘 ∈ 𝑊 ) → ( ( 𝑖 ∈ 𝑊 ↦ ( abs ‘ ( 𝐹 ‘ 𝑖 ) ) ) ‘ 𝑘 ) = ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
56 2 43 46 41 47 55 climabs ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 0 ) → ( 𝑖 ∈ 𝑊 ↦ ( abs ‘ ( 𝐹 ‘ 𝑖 ) ) ) ⇝ ( abs ‘ 0 ) )
57 abs0 ⊢ ( abs ‘ 0 ) = 0
58 56 57 breqtrdi ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 0 ) → ( 𝑖 ∈ 𝑊 ↦ ( abs ‘ ( 𝐹 ‘ 𝑖 ) ) ) ⇝ 0 )
59 47 abscld ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝ 0 ) ∧ 𝑘 ∈ 𝑊 ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
60 55 59 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝ 0 ) ∧ 𝑘 ∈ 𝑊 ) → ( ( 𝑖 ∈ 𝑊 ↦ ( abs ‘ ( 𝐹 ‘ 𝑖 ) ) ) ‘ 𝑘 ) ∈ ℝ )
61 2fveq3 ⊢ ( 𝑖 = 𝑁 → ( abs ‘ ( 𝐹 ‘ 𝑖 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) )
62 61 breq2d ⊢ ( 𝑖 = 𝑁 → ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑖 ) ) ↔ ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
63 62 imbi2d ⊢ ( 𝑖 = 𝑁 → ( ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑖 ) ) ) ↔ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ) ) )
64 2fveq3 ⊢ ( 𝑖 = 𝑘 → ( abs ‘ ( 𝐹 ‘ 𝑖 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
65 64 breq2d ⊢ ( 𝑖 = 𝑘 → ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑖 ) ) ↔ ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
66 65 imbi2d ⊢ ( 𝑖 = 𝑘 → ( ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑖 ) ) ) ↔ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
67 2fveq3 ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( abs ‘ ( 𝐹 ‘ 𝑖 ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
68 67 breq2d ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑖 ) ) ↔ ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
69 68 imbi2d ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑖 ) ) ) ↔ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
70 38 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℤ ) → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ )
71 70 leidd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℤ ) → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) )
72 71 expcom ⊢ ( 𝑁 ∈ ℤ → ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
73 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ )
74 24 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
75 74 abscld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
76 2 peano2uzs ⊢ ( 𝑘 ∈ 𝑊 → ( 𝑘 + 1 ) ∈ 𝑊 )
77 ovex ⊢ ( 𝑘 + 1 ) ∈ V
78 eleq1 ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( 𝑖 ∈ 𝑊 ↔ ( 𝑘 + 1 ) ∈ 𝑊 ) )
79 78 anbi2d ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( ( 𝜑 ∧ 𝑖 ∈ 𝑊 ) ↔ ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ 𝑊 ) ) )
80 fveq2 ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
81 80 eleq1d ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( ( 𝐹 ‘ 𝑖 ) ∈ ℂ ↔ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℂ ) )
82 79 81 imbi12d ⊢ ( 𝑖 = ( 𝑘 + 1 ) → ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑊 ) → ( 𝐹 ‘ 𝑖 ) ∈ ℂ ) ↔ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ 𝑊 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℂ ) ) )
83 eleq1 ⊢ ( 𝑘 = 𝑖 → ( 𝑘 ∈ 𝑊 ↔ 𝑖 ∈ 𝑊 ) )
84 83 anbi2d ⊢ ( 𝑘 = 𝑖 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) ↔ ( 𝜑 ∧ 𝑖 ∈ 𝑊 ) ) )
85 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑖 ) )
86 85 eleq1d ⊢ ( 𝑘 = 𝑖 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑖 ) ∈ ℂ ) )
87 84 86 imbi12d ⊢ ( 𝑘 = 𝑖 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ 𝑊 ) → ( 𝐹 ‘ 𝑖 ) ∈ ℂ ) ) )
88 87 24 chvarvv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑊 ) → ( 𝐹 ‘ 𝑖 ) ∈ ℂ )
89 77 82 88 vtocl ⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ 𝑊 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
90 76 89 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
91 90 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
92 91 abscld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ )
93 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
94 7 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
95 73 75 92 93 94 letrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
96 95 ex ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
97 20 96 sylan2br ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
98 97 expcom ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝜑 → ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
99 98 a2d ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → ( ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) ) )
100 63 66 69 66 72 99 uzind4 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
101 100 impcom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
102 20 101 sylan2b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
103 102 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝ 0 ) ∧ 𝑘 ∈ 𝑊 ) → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
104 103 55 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝ 0 ) ∧ 𝑘 ∈ 𝑊 ) → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( ( 𝑖 ∈ 𝑊 ↦ ( abs ‘ ( 𝐹 ‘ 𝑖 ) ) ) ‘ 𝑘 ) )
105 2 41 42 58 60 104 climlec2 ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 0 ) → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ 0 )
106 40 105 mtand ⊢ ( 𝜑 → ¬ 𝐹 ⇝ 0 )
107 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
108 8 107 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
109 108 adantr ⊢ ( ( 𝜑 ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) → 𝑀 ∈ ℤ )
110 4 adantr ⊢ ( ( 𝜑 ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) → 𝐹 ∈ 𝑉 )
111 simpr ⊢ ( ( 𝜑 ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
112 5 adantlr ⊢ ( ( ( 𝜑 ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
113 1 109 110 111 112 serf0 ⊢ ( ( 𝜑 ∧ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) → 𝐹 ⇝ 0 )
114 106 113 mtand ⊢ ( 𝜑 → ¬ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
115 df-nel ⊢ ( seq 𝑀 ( + , 𝐹 ) ∉ dom ⇝ ↔ ¬ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
116 114 115 sylibr ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∉ dom ⇝ )