Metamath Proof Explorer

Theorem cvgrat

Description: Ratio test for convergence of a complex infinite series. If the ratio A of the absolute values of successive terms in an infinite sequence F is less than 1 for all terms beyond some index B , then the infinite sum of the terms of F converges to a complex number. Equivalent to first part of Exercise 4 of Gleason p. 182. (Contributed by NM, 26-Apr-2005) (Proof shortened by Mario Carneiro, 27-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 cvgrat.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 cvgrat.2 ⊢ 𝑊 = ( ℤ≥ ‘ 𝑁 )
3 cvgrat.3 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4 cvgrat.4 ⊢ ( 𝜑 → 𝐴 < 1 )
5 cvgrat.5 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
6 cvgrat.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
7 cvgrat.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( 𝐴 · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
8 5 1 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
9 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
10 8 9 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
11 uzid ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
12 10 11 syl ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
13 12 2 eleqtrrdi ⊢ ( 𝜑 → 𝑁 ∈ 𝑊 )
14 oveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 − 𝑁 ) = ( 𝑘 − 𝑁 ) )
15 14 oveq2d ⊢ ( 𝑛 = 𝑘 → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) = ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) )
16 eqid ⊢ ( 𝑛 ∈ 𝑊 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) ) = ( 𝑛 ∈ 𝑊 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) )
17 ovex ⊢ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ∈ V
18 15 16 17 fvmpt ⊢ ( 𝑘 ∈ 𝑊 → ( ( 𝑛 ∈ 𝑊 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) ) ‘ 𝑘 ) = ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( ( 𝑛 ∈ 𝑊 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) ) ‘ 𝑘 ) = ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) )
20 0re ⊢ 0 ∈ ℝ
21 ifcl ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ∈ ℝ )
22 20 3 21 sylancr ⊢ ( 𝜑 → if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ∈ ℝ )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ∈ ℝ )
24 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → 𝑘 ∈ 𝑊 )
25 24 2 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) )
26 uznn0sub ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑘 − 𝑁 ) ∈ ℕ0 )
27 25 26 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( 𝑘 − 𝑁 ) ∈ ℕ0 )
28 23 27 reexpcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ∈ ℝ )
29 19 28 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( ( 𝑛 ∈ 𝑊 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) ) ‘ 𝑘 ) ∈ ℝ )
30 uzss ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
31 8 30 syl ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
32 31 2 1 3sstr4g ⊢ ( 𝜑 → 𝑊 ⊆ 𝑍 )
33 32 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → 𝑘 ∈ 𝑍 )
34 33 6 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
35 26 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑘 − 𝑁 ) ∈ ℕ0 )
36 oveq2 ⊢ ( 𝑛 = ( 𝑘 − 𝑁 ) → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) = ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) )
37 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) )
38 36 37 17 fvmpt ⊢ ( ( 𝑘 − 𝑁 ) ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ‘ ( 𝑘 − 𝑁 ) ) = ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) )
39 35 38 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ‘ ( 𝑘 − 𝑁 ) ) = ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) )
40 10 zcnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
41 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑘 ∈ ℤ )
42 41 zcnd ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑘 ∈ ℂ )
43 nn0ex ⊢ ℕ0 ∈ V
44 43 mptex ⊢ ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ∈ V
45 44 shftval ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) shift 𝑁 ) ‘ 𝑘 ) = ( ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ‘ ( 𝑘 − 𝑁 ) ) )
46 40 42 45 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) shift 𝑁 ) ‘ 𝑘 ) = ( ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ‘ ( 𝑘 − 𝑁 ) ) )
47 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) )
48 47 2 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ 𝑊 )
49 48 18 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑛 ∈ 𝑊 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) ) ‘ 𝑘 ) = ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) )
50 39 46 49 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑛 ∈ 𝑊 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) ) ‘ 𝑘 ) = ( ( ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) shift 𝑁 ) ‘ 𝑘 ) )
51 10 50 seqfeq ⊢ ( 𝜑 → seq 𝑁 ( + , ( 𝑛 ∈ 𝑊 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) ) ) = seq 𝑁 ( + , ( ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) shift 𝑁 ) ) )
52 44 seqshft ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → seq 𝑁 ( + , ( ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) shift 𝑁 ) ) = ( seq ( 𝑁 − 𝑁 ) ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ) shift 𝑁 ) )
53 10 10 52 syl2anc ⊢ ( 𝜑 → seq 𝑁 ( + , ( ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) shift 𝑁 ) ) = ( seq ( 𝑁 − 𝑁 ) ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ) shift 𝑁 ) )
54 40 subidd ⊢ ( 𝜑 → ( 𝑁 − 𝑁 ) = 0 )
55 54 seqeq1d ⊢ ( 𝜑 → seq ( 𝑁 − 𝑁 ) ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ) = seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ) )
56 55 oveq1d ⊢ ( 𝜑 → ( seq ( 𝑁 − 𝑁 ) ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ) shift 𝑁 ) = ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ) shift 𝑁 ) )
57 51 53 56 3eqtrd ⊢ ( 𝜑 → seq 𝑁 ( + , ( 𝑛 ∈ 𝑊 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) ) ) = ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ) shift 𝑁 ) )
58 22 recnd ⊢ ( 𝜑 → if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ∈ ℂ )
59 max2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → 0 ≤ if ( 𝐴 ≤ 0 , 0 , 𝐴 ) )
60 3 20 59 sylancl ⊢ ( 𝜑 → 0 ≤ if ( 𝐴 ≤ 0 , 0 , 𝐴 ) )
61 22 60 absidd ⊢ ( 𝜑 → ( abs ‘ if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ) = if ( 𝐴 ≤ 0 , 0 , 𝐴 ) )
62 0lt1 ⊢ 0 < 1
63 breq1 ⊢ ( 0 = if ( 𝐴 ≤ 0 , 0 , 𝐴 ) → ( 0 < 1 ↔ if ( 𝐴 ≤ 0 , 0 , 𝐴 ) < 1 ) )
64 breq1 ⊢ ( 𝐴 = if ( 𝐴 ≤ 0 , 0 , 𝐴 ) → ( 𝐴 < 1 ↔ if ( 𝐴 ≤ 0 , 0 , 𝐴 ) < 1 ) )
65 63 64 ifboth ⊢ ( ( 0 < 1 ∧ 𝐴 < 1 ) → if ( 𝐴 ≤ 0 , 0 , 𝐴 ) < 1 )
66 62 4 65 sylancr ⊢ ( 𝜑 → if ( 𝐴 ≤ 0 , 0 , 𝐴 ) < 1 )
67 61 66 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ) < 1 )
68 oveq2 ⊢ ( 𝑛 = 𝑘 → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) = ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑘 ) )
69 ovex ⊢ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑘 ) ∈ V
70 68 37 69 fvmpt ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) = ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑘 ) )
71 70 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ‘ 𝑘 ) = ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑘 ) )
72 58 67 71 geolim ⊢ ( 𝜑 → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ) ⇝ ( 1 / ( 1 − if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ) ) )
73 seqex ⊢ seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ) ∈ V
74 climshft ⊢ ( ( 𝑁 ∈ ℤ ∧ seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ) ∈ V ) → ( ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ) shift 𝑁 ) ⇝ ( 1 / ( 1 − if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ) ) ↔ seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ) ⇝ ( 1 / ( 1 − if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ) ) ) )
75 10 73 74 sylancl ⊢ ( 𝜑 → ( ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ) shift 𝑁 ) ⇝ ( 1 / ( 1 − if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ) ) ↔ seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ) ⇝ ( 1 / ( 1 − if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ) ) ) )
76 72 75 mpbird ⊢ ( 𝜑 → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ) shift 𝑁 ) ⇝ ( 1 / ( 1 − if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ) ) )
77 ovex ⊢ ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ) shift 𝑁 ) ∈ V
78 ovex ⊢ ( 1 / ( 1 − if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ) ) ∈ V
79 77 78 breldm ⊢ ( ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ) shift 𝑁 ) ⇝ ( 1 / ( 1 − if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ) ) → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ) shift 𝑁 ) ∈ dom ⇝ )
80 76 79 syl ⊢ ( 𝜑 → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 𝑛 ) ) ) shift 𝑁 ) ∈ dom ⇝ )
81 57 80 eqeltrd ⊢ ( 𝜑 → seq 𝑁 ( + , ( 𝑛 ∈ 𝑊 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) ) ) ∈ dom ⇝ )
82 fveq2 ⊢ ( 𝑘 = 𝑁 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑁 ) )
83 82 eleq1d ⊢ ( 𝑘 = 𝑁 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑁 ) ∈ ℂ ) )
84 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
85 83 84 5 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ∈ ℂ )
86 85 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ )
87 2fveq3 ⊢ ( 𝑛 = 𝑁 → ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) )
88 oveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 − 𝑁 ) = ( 𝑁 − 𝑁 ) )
89 88 oveq2d ⊢ ( 𝑛 = 𝑁 → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) = ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑁 − 𝑁 ) ) )
90 89 oveq2d ⊢ ( 𝑛 = 𝑁 → ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑁 − 𝑁 ) ) ) )
91 87 90 breq12d ⊢ ( 𝑛 = 𝑁 → ( ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) ) ↔ ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑁 − 𝑁 ) ) ) ) )
92 91 imbi2d ⊢ ( 𝑛 = 𝑁 → ( ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) ) ) ↔ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑁 − 𝑁 ) ) ) ) ) )
93 2fveq3 ⊢ ( 𝑛 = 𝑘 → ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
94 15 oveq2d ⊢ ( 𝑛 = 𝑘 → ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) )
95 93 94 breq12d ⊢ ( 𝑛 = 𝑘 → ( ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) ) ↔ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) ) )
96 95 imbi2d ⊢ ( 𝑛 = 𝑘 → ( ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) ) ) ↔ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) ) ) )
97 2fveq3 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
98 oveq1 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑛 − 𝑁 ) = ( ( 𝑘 + 1 ) − 𝑁 ) )
99 98 oveq2d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) = ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) )
100 99 oveq2d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) ) )
101 97 100 breq12d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) ) ↔ ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) ) ) )
102 101 imbi2d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) ) ) ↔ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) ) ) ) )
103 86 leidd ⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) )
104 54 oveq2d ⊢ ( 𝜑 → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑁 − 𝑁 ) ) = ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 0 ) )
105 58 exp0d ⊢ ( 𝜑 → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ 0 ) = 1 )
106 104 105 eqtrd ⊢ ( 𝜑 → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑁 − 𝑁 ) ) = 1 )
107 106 oveq2d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑁 − 𝑁 ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · 1 ) )
108 86 recnd ⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℂ )
109 108 mulid1d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · 1 ) = ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) )
110 107 109 eqtrd ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑁 − 𝑁 ) ) ) = ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) )
111 103 110 breqtrrd ⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑁 − 𝑁 ) ) ) )
112 34 abscld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
113 86 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℝ )
114 113 28 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) ∈ ℝ )
115 60 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → 0 ≤ if ( 𝐴 ≤ 0 , 0 , 𝐴 ) )
116 lemul2a ⊢ ( ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) ∈ ℝ ∧ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ∈ ℝ ∧ 0 ≤ if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ) ) ∧ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) ) → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ≤ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) ) )
117 116 ex ⊢ ( ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ ∧ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) ∈ ℝ ∧ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ∈ ℝ ∧ 0 ≤ if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ≤ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) ) ) )
118 112 114 23 115 117 syl112anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ≤ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) ) ) )
119 58 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ∈ ℂ )
120 108 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) ∈ ℂ )
121 28 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ∈ ℂ )
122 119 120 121 mul12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) ) )
123 119 27 expp1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 − 𝑁 ) + 1 ) ) = ( ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) · if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ) )
124 42 2 eleq2s ⊢ ( 𝑘 ∈ 𝑊 → 𝑘 ∈ ℂ )
125 ax-1cn ⊢ 1 ∈ ℂ
126 addsub ⊢ ( ( 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑘 + 1 ) − 𝑁 ) = ( ( 𝑘 − 𝑁 ) + 1 ) )
127 125 126 mp3an2 ⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑘 + 1 ) − 𝑁 ) = ( ( 𝑘 − 𝑁 ) + 1 ) )
128 124 40 127 syl2anr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( ( 𝑘 + 1 ) − 𝑁 ) = ( ( 𝑘 − 𝑁 ) + 1 ) )
129 128 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) = ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 − 𝑁 ) + 1 ) ) )
130 119 121 mulcomd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) = ( ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) · if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ) )
131 123 129 130 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) = ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) )
132 131 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) ) )
133 122 132 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) ) )
134 133 breq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ≤ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) ) ↔ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) ) ) )
135 118 134 sylibd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) ) ) )
136 fveq2 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
137 136 eleq1d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ( 𝐹 ‘ 𝑛 ) ∈ ℂ ↔ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℂ ) )
138 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
139 138 eleq1d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑛 ) ∈ ℂ ) )
140 139 cbvralvw ⊢ ( ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ∀ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
141 84 140 sylib ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
142 141 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ∀ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
143 2 peano2uzs ⊢ ( 𝑘 ∈ 𝑊 → ( 𝑘 + 1 ) ∈ 𝑊 )
144 32 sselda ⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ 𝑊 ) → ( 𝑘 + 1 ) ∈ 𝑍 )
145 143 144 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( 𝑘 + 1 ) ∈ 𝑍 )
146 137 142 145 rspcdva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
147 146 abscld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ )
148 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → 𝐴 ∈ ℝ )
149 148 112 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( 𝐴 · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ )
150 23 112 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ )
151 34 absge0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) )
152 max1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → 𝐴 ≤ if ( 𝐴 ≤ 0 , 0 , 𝐴 ) )
153 3 20 152 sylancl ⊢ ( 𝜑 → 𝐴 ≤ if ( 𝐴 ≤ 0 , 0 , 𝐴 ) )
154 153 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → 𝐴 ≤ if ( 𝐴 ≤ 0 , 0 , 𝐴 ) )
155 148 23 112 151 154 lemul1ad ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( 𝐴 · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ≤ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
156 147 149 150 7 155 letrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
157 peano2uz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
158 25 157 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
159 uznn0sub ⊢ ( ( 𝑘 + 1 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( ( 𝑘 + 1 ) − 𝑁 ) ∈ ℕ0 )
160 158 159 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( ( 𝑘 + 1 ) − 𝑁 ) ∈ ℕ0 )
161 23 160 reexpcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) ∈ ℝ )
162 113 161 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) ) ∈ ℝ )
163 letr ⊢ ( ( ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ ∧ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ ∧ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) ) ∈ ℝ ) → ( ( ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ∧ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) ) ) )
164 147 150 162 163 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( ( ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ∧ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) ) ) )
165 156 164 mpand ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) · ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) ) ) )
166 135 165 syld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) ) ) )
167 48 166 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) ) ) )
168 167 expcom ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝜑 → ( ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) ) ) ) )
169 168 a2d ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → ( ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) ) → ( 𝜑 → ( abs ‘ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( ( 𝑘 + 1 ) − 𝑁 ) ) ) ) ) )
170 92 96 102 96 111 169 uzind4i ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) ) )
171 170 impcom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) )
172 49 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( ( 𝑛 ∈ 𝑊 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) ) ‘ 𝑘 ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑘 − 𝑁 ) ) ) )
173 171 172 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑘 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ 𝑁 ) ) · ( ( 𝑛 ∈ 𝑊 ↦ ( if ( 𝐴 ≤ 0 , 0 , 𝐴 ) ↑ ( 𝑛 − 𝑁 ) ) ) ‘ 𝑘 ) ) )
174 2 13 29 34 81 86 173 cvgcmpce ⊢ ( 𝜑 → seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
175 1 5 6 iserex ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) )
176 174 175 mpbird ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )