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 ⇝ )