Metamath Proof Explorer

Theorem iseraltlem3

Description: Lemma for iseralt . From iseraltlem2 , we have ( -u 1 ^ n ) x. S ( n + 2 k ) <_ ( -u 1 ^ n ) x. S ( n ) and ( -u 1 ^ n ) x. S ( n + 1 ) <_ ( -u 1 ^ n ) x. S ( n + 2 k + 1 ) , and we also have ( -u 1 ^ n ) x. S ( n + 1 ) = ( -u 1 ^ n ) x. S ( n ) - G ( n + 1 ) for each n by the definition of the partial sum S , so combining the inequalities we get ( -u 1 ^ n ) x. S ( n ) - G ( n + 1 ) = ( -u 1 ^ n ) x. S ( n + 1 ) <_ ( -u 1 ^ n ) x. S ( n + 2 k + 1 ) = ( -u 1 ^ n ) x. S ( n + 2 k ) - G ( n + 2 k + 1 ) <_ ( -u 1 ^ n ) x. S ( n + 2 k ) <_ ( -u 1 ^ n ) x. S ( n ) <_ ( -u 1 ^ n ) x. S ( n ) + G ( n + 1 ) , so | ( -u 1 ^ n ) x. S ( n + 2 k + 1 ) - ( -u 1 ^ n ) x. S ( n ) | = | S ( n + 2 k + 1 ) - S ( n ) | <_ G ( n + 1 ) and | ( -u 1 ^ n ) x. S ( n + 2 k ) - ( -u 1 ^ n ) x. S ( n ) | = | S ( n + 2 k ) - S ( n ) | <_ G ( n + 1 ) . Thus, both even and odd partial sums are Cauchy if G converges to 0 . (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypotheses iseralt.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
iseralt.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
iseralt.3 ⊢ ( 𝜑 → 𝐺 : 𝑍 ⟶ ℝ )
iseralt.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐺 ‘ 𝑘 ) )
iseralt.5 ⊢ ( 𝜑 → 𝐺 ⇝ 0 )
iseralt.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( ( - 1 ↑ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
Assertion iseraltlem3 ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ≤ ( 𝐺 ‘ ( 𝑁 + 1 ) ) ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ≤ ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 iseralt.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 iseralt.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 iseralt.3 ⊢ ( 𝜑 → 𝐺 : 𝑍 ⟶ ℝ )
4 iseralt.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐺 ‘ 𝑘 ) )
5 iseralt.5 ⊢ ( 𝜑 → 𝐺 ⇝ 0 )
6 iseralt.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( ( - 1 ↑ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
7 neg1rr ⊢ - 1 ∈ ℝ
8 7 a1i ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → - 1 ∈ ℝ )
9 neg1ne0 ⊢ - 1 ≠ 0
10 9 a1i ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → - 1 ≠ 0 )
11 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
12 1 11 eqsstri ⊢ 𝑍 ⊆ ℤ
13 simp2 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → 𝑁 ∈ 𝑍 )
14 12 13 sseldi ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
15 8 10 14 reexpclzd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - 1 ↑ 𝑁 ) ∈ ℝ )
16 15 recnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - 1 ↑ 𝑁 ) ∈ ℂ )
17 7 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → - 1 ∈ ℝ )
18 9 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → - 1 ≠ 0 )
19 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝑍 )
20 12 19 sseldi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ℤ )
21 17 18 20 reexpclzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( - 1 ↑ 𝑘 ) ∈ ℝ )
22 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
23 21 22 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( - 1 ↑ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ )
24 6 23 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
25 1 2 24 serfre ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ )
26 25 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ )
27 13 1 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
28 2nn0 ⊢ 2 ∈ ℕ0
29 simp3 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℕ0 )
30 nn0mulcl ⊢ ( ( 2 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 2 · 𝐾 ) ∈ ℕ0 )
31 28 29 30 sylancr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 2 · 𝐾 ) ∈ ℕ0 )
32 uzaddcl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 2 · 𝐾 ) ∈ ℕ0 ) → ( 𝑁 + ( 2 · 𝐾 ) ) ∈ ( ℤ≥ ‘ 𝑀 ) )
33 27 31 32 syl2anc ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑁 + ( 2 · 𝐾 ) ) ∈ ( ℤ≥ ‘ 𝑀 ) )
34 33 1 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑁 + ( 2 · 𝐾 ) ) ∈ 𝑍 )
35 26 34 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ∈ ℝ )
36 35 recnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ∈ ℂ )
37 26 13 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ ℝ )
38 37 recnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ ℂ )
39 16 36 38 subdid ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) = ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) − ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
40 39 fveq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( - 1 ↑ 𝑁 ) · ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) = ( abs ‘ ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) − ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) )
41 35 37 resubcld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ∈ ℝ )
42 41 recnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ∈ ℂ )
43 16 42 absmuld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( - 1 ↑ 𝑁 ) · ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) = ( ( abs ‘ ( - 1 ↑ 𝑁 ) ) · ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) )
44 40 43 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) − ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) = ( ( abs ‘ ( - 1 ↑ 𝑁 ) ) · ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) )
45 8 recnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → - 1 ∈ ℂ )
46 absexpz ⊢ ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( abs ‘ ( - 1 ↑ 𝑁 ) ) = ( ( abs ‘ - 1 ) ↑ 𝑁 ) )
47 45 10 14 46 syl3anc ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( - 1 ↑ 𝑁 ) ) = ( ( abs ‘ - 1 ) ↑ 𝑁 ) )
48 ax-1cn ⊢ 1 ∈ ℂ
49 48 absnegi ⊢ ( abs ‘ - 1 ) = ( abs ‘ 1 )
50 abs1 ⊢ ( abs ‘ 1 ) = 1
51 49 50 eqtri ⊢ ( abs ‘ - 1 ) = 1
52 51 oveq1i ⊢ ( ( abs ‘ - 1 ) ↑ 𝑁 ) = ( 1 ↑ 𝑁 )
53 1exp ⊢ ( 𝑁 ∈ ℤ → ( 1 ↑ 𝑁 ) = 1 )
54 14 53 syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 1 ↑ 𝑁 ) = 1 )
55 52 54 syl5eq ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( abs ‘ - 1 ) ↑ 𝑁 ) = 1 )
56 47 55 eqtrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( - 1 ↑ 𝑁 ) ) = 1 )
57 56 oveq1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( abs ‘ ( - 1 ↑ 𝑁 ) ) · ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) = ( 1 · ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) )
58 42 abscld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ∈ ℝ )
59 58 recnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ∈ ℂ )
60 59 mulid2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 1 · ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) = ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
61 44 57 60 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) − ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) = ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
62 15 37 remulcld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ∈ ℝ )
63 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → 𝐺 : 𝑍 ⟶ ℝ )
64 1 peano2uzs ⊢ ( 𝑁 ∈ 𝑍 → ( 𝑁 + 1 ) ∈ 𝑍 )
65 64 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ 𝑍 )
66 63 65 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 𝐺 ‘ ( 𝑁 + 1 ) ) ∈ ℝ )
67 62 66 resubcld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) − ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ∈ ℝ )
68 1 peano2uzs ⊢ ( ( 𝑁 + ( 2 · 𝐾 ) ) ∈ 𝑍 → ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ∈ 𝑍 )
69 34 68 syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ∈ 𝑍 )
70 26 69 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ∈ ℝ )
71 15 70 remulcld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ∈ ℝ )
72 15 35 remulcld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) ∈ ℝ )
73 seqp1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )
74 27 73 syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )
75 fveq2 ⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑁 + 1 ) ) )
76 oveq2 ⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( - 1 ↑ 𝑘 ) = ( - 1 ↑ ( 𝑁 + 1 ) ) )
77 fveq2 ⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝑁 + 1 ) ) )
78 76 77 oveq12d ⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( ( - 1 ↑ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) = ( ( - 1 ↑ ( 𝑁 + 1 ) ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
79 75 78 eqeq12d ⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) = ( ( - 1 ↑ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) ↔ ( 𝐹 ‘ ( 𝑁 + 1 ) ) = ( ( - 1 ↑ ( 𝑁 + 1 ) ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ) )
80 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) = ( ( - 1 ↑ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
81 80 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) = ( ( - 1 ↑ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
82 79 81 65 rspcdva ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑁 + 1 ) ) = ( ( - 1 ↑ ( 𝑁 + 1 ) ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
83 82 oveq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( ( - 1 ↑ ( 𝑁 + 1 ) ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ) )
84 45 10 14 expp1zd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - 1 ↑ ( 𝑁 + 1 ) ) = ( ( - 1 ↑ 𝑁 ) · - 1 ) )
85 neg1cn ⊢ - 1 ∈ ℂ
86 mulcom ⊢ ( ( ( - 1 ↑ 𝑁 ) ∈ ℂ ∧ - 1 ∈ ℂ ) → ( ( - 1 ↑ 𝑁 ) · - 1 ) = ( - 1 · ( - 1 ↑ 𝑁 ) ) )
87 16 85 86 sylancl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · - 1 ) = ( - 1 · ( - 1 ↑ 𝑁 ) ) )
88 16 mulm1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - 1 · ( - 1 ↑ 𝑁 ) ) = - ( - 1 ↑ 𝑁 ) )
89 84 87 88 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - 1 ↑ ( 𝑁 + 1 ) ) = - ( - 1 ↑ 𝑁 ) )
90 89 oveq1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ ( 𝑁 + 1 ) ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) = ( - ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
91 66 recnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 𝐺 ‘ ( 𝑁 + 1 ) ) ∈ ℂ )
92 16 91 mulneg1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) = - ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
93 90 92 eqtrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ ( 𝑁 + 1 ) ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) = - ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
94 93 oveq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( ( - 1 ↑ ( 𝑁 + 1 ) ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + - ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ) )
95 74 83 94 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + - ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ) )
96 15 66 remulcld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ∈ ℝ )
97 96 recnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ∈ ℂ )
98 38 97 negsubd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + - ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) − ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ) )
99 95 98 eqtrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) − ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ) )
100 99 oveq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) − ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ) ) )
101 16 38 97 subdid ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) − ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ) ) = ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) − ( ( - 1 ↑ 𝑁 ) · ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ) ) )
102 14 zcnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
103 102 2timesd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) )
104 103 oveq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - 1 ↑ ( 2 · 𝑁 ) ) = ( - 1 ↑ ( 𝑁 + 𝑁 ) ) )
105 2z ⊢ 2 ∈ ℤ
106 105 a1i ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → 2 ∈ ℤ )
107 expmulz ⊢ ( ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) ∧ ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( - 1 ↑ ( 2 · 𝑁 ) ) = ( ( - 1 ↑ 2 ) ↑ 𝑁 ) )
108 45 10 106 14 107 syl22anc ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - 1 ↑ ( 2 · 𝑁 ) ) = ( ( - 1 ↑ 2 ) ↑ 𝑁 ) )
109 104 108 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - 1 ↑ ( 𝑁 + 𝑁 ) ) = ( ( - 1 ↑ 2 ) ↑ 𝑁 ) )
110 neg1sqe1 ⊢ ( - 1 ↑ 2 ) = 1
111 110 oveq1i ⊢ ( ( - 1 ↑ 2 ) ↑ 𝑁 ) = ( 1 ↑ 𝑁 )
112 109 111 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - 1 ↑ ( 𝑁 + 𝑁 ) ) = ( 1 ↑ 𝑁 ) )
113 expaddz ⊢ ( ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( - 1 ↑ ( 𝑁 + 𝑁 ) ) = ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) )
114 45 10 14 14 113 syl22anc ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - 1 ↑ ( 𝑁 + 𝑁 ) ) = ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) )
115 112 114 54 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = 1 )
116 115 oveq1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) = ( 1 · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
117 16 16 91 mulassd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ) )
118 91 mulid2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 1 · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) = ( 𝐺 ‘ ( 𝑁 + 1 ) ) )
119 116 117 118 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ) = ( 𝐺 ‘ ( 𝑁 + 1 ) ) )
120 119 oveq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) − ( ( - 1 ↑ 𝑁 ) · ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ) ) = ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) − ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
121 100 101 120 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ) = ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) − ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
122 1 2 3 4 5 6 iseraltlem2 ⊢ ( ( 𝜑 ∧ ( 𝑁 + 1 ) ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ ( 𝑁 + 1 ) ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + 1 ) + ( 2 · 𝐾 ) ) ) ) ≤ ( ( - 1 ↑ ( 𝑁 + 1 ) ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ) )
123 64 122 syl3an2 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ ( 𝑁 + 1 ) ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + 1 ) + ( 2 · 𝐾 ) ) ) ) ≤ ( ( - 1 ↑ ( 𝑁 + 1 ) ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ) )
124 1cnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → 1 ∈ ℂ )
125 31 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 2 · 𝐾 ) ∈ ℂ )
126 102 124 125 add32d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝑁 + 1 ) + ( 2 · 𝐾 ) ) = ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) )
127 126 fveq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + 1 ) + ( 2 · 𝐾 ) ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) )
128 89 127 oveq12d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ ( 𝑁 + 1 ) ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + 1 ) + ( 2 · 𝐾 ) ) ) ) = ( - ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) )
129 89 oveq1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ ( 𝑁 + 1 ) ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ) = ( - ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ) )
130 123 128 129 3brtr3d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ≤ ( - ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ) )
131 70 recnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ∈ ℂ )
132 16 131 mulneg1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) = - ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) )
133 26 65 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ∈ ℝ )
134 133 recnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ∈ ℂ )
135 16 134 mulneg1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ) = - ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ) )
136 130 132 135 3brtr3d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → - ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ≤ - ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ) )
137 15 133 remulcld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ) ∈ ℝ )
138 137 71 lenegd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ↔ - ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ≤ - ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ) ) )
139 136 138 mpbird ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) )
140 121 139 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) − ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) )
141 seqp1 ⊢ ( ( 𝑁 + ( 2 · 𝐾 ) ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) + ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) )
142 33 141 syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) + ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) )
143 fveq2 ⊢ ( 𝑘 = ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) )
144 oveq2 ⊢ ( 𝑘 = ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) → ( - 1 ↑ 𝑘 ) = ( - 1 ↑ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) )
145 fveq2 ⊢ ( 𝑘 = ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) )
146 144 145 oveq12d ⊢ ( 𝑘 = ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) → ( ( - 1 ↑ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) = ( ( - 1 ↑ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) )
147 143 146 eqeq12d ⊢ ( 𝑘 = ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) → ( ( 𝐹 ‘ 𝑘 ) = ( ( - 1 ↑ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) ↔ ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) = ( ( - 1 ↑ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ) )
148 147 81 69 rspcdva ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) = ( ( - 1 ↑ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) )
149 12 65 sseldi ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ℤ )
150 31 nn0zd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 2 · 𝐾 ) ∈ ℤ )
151 expaddz ⊢ ( ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) ∧ ( ( 𝑁 + 1 ) ∈ ℤ ∧ ( 2 · 𝐾 ) ∈ ℤ ) ) → ( - 1 ↑ ( ( 𝑁 + 1 ) + ( 2 · 𝐾 ) ) ) = ( ( - 1 ↑ ( 𝑁 + 1 ) ) · ( - 1 ↑ ( 2 · 𝐾 ) ) ) )
152 45 10 149 150 151 syl22anc ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - 1 ↑ ( ( 𝑁 + 1 ) + ( 2 · 𝐾 ) ) ) = ( ( - 1 ↑ ( 𝑁 + 1 ) ) · ( - 1 ↑ ( 2 · 𝐾 ) ) ) )
153 29 nn0zd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℤ )
154 expmulz ⊢ ( ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) ∧ ( 2 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( - 1 ↑ ( 2 · 𝐾 ) ) = ( ( - 1 ↑ 2 ) ↑ 𝐾 ) )
155 45 10 106 153 154 syl22anc ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - 1 ↑ ( 2 · 𝐾 ) ) = ( ( - 1 ↑ 2 ) ↑ 𝐾 ) )
156 110 oveq1i ⊢ ( ( - 1 ↑ 2 ) ↑ 𝐾 ) = ( 1 ↑ 𝐾 )
157 1exp ⊢ ( 𝐾 ∈ ℤ → ( 1 ↑ 𝐾 ) = 1 )
158 153 157 syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 1 ↑ 𝐾 ) = 1 )
159 156 158 syl5eq ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 2 ) ↑ 𝐾 ) = 1 )
160 155 159 eqtrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - 1 ↑ ( 2 · 𝐾 ) ) = 1 )
161 89 160 oveq12d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ ( 𝑁 + 1 ) ) · ( - 1 ↑ ( 2 · 𝐾 ) ) ) = ( - ( - 1 ↑ 𝑁 ) · 1 ) )
162 152 161 eqtrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - 1 ↑ ( ( 𝑁 + 1 ) + ( 2 · 𝐾 ) ) ) = ( - ( - 1 ↑ 𝑁 ) · 1 ) )
163 126 oveq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - 1 ↑ ( ( 𝑁 + 1 ) + ( 2 · 𝐾 ) ) ) = ( - 1 ↑ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) )
164 16 negcld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → - ( - 1 ↑ 𝑁 ) ∈ ℂ )
165 164 mulid1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - ( - 1 ↑ 𝑁 ) · 1 ) = - ( - 1 ↑ 𝑁 ) )
166 162 163 165 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - 1 ↑ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) = - ( - 1 ↑ 𝑁 ) )
167 166 oveq1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) = ( - ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) )
168 63 69 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ∈ ℝ )
169 168 recnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ∈ ℂ )
170 16 169 mulneg1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( - ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) = - ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) )
171 148 167 170 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) = - ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) )
172 171 oveq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) + ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) + - ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ) )
173 15 168 remulcld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ∈ ℝ )
174 173 recnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ∈ ℂ )
175 36 174 negsubd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) + - ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ) )
176 142 172 175 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ) )
177 176 oveq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ) ) )
178 16 36 174 subdid ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ) ) = ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) − ( ( - 1 ↑ 𝑁 ) · ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ) ) )
179 115 oveq1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) = ( 1 · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) )
180 16 16 169 mulassd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ) )
181 169 mulid2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 1 · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) = ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) )
182 179 180 181 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ) = ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) )
183 182 oveq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) − ( ( - 1 ↑ 𝑁 ) · ( ( - 1 ↑ 𝑁 ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ) ) = ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) − ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) )
184 177 178 183 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) = ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) − ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) )
185 simp1 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → 𝜑 )
186 1 2 3 4 5 iseraltlem1 ⊢ ( ( 𝜑 ∧ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ∈ 𝑍 ) → 0 ≤ ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) )
187 185 69 186 syl2anc ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → 0 ≤ ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) )
188 72 168 subge02d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 0 ≤ ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ↔ ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) − ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) ) )
189 187 188 mpbid ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) − ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) )
190 184 189 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) )
191 67 71 72 140 190 letrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) − ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) )
192 62 66 readdcld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ∈ ℝ )
193 1 2 3 4 5 6 iseraltlem2 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
194 1 2 3 4 5 iseraltlem1 ⊢ ( ( 𝜑 ∧ ( 𝑁 + 1 ) ∈ 𝑍 ) → 0 ≤ ( 𝐺 ‘ ( 𝑁 + 1 ) ) )
195 185 65 194 syl2anc ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → 0 ≤ ( 𝐺 ‘ ( 𝑁 + 1 ) ) )
196 62 66 addge01d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 0 ≤ ( 𝐺 ‘ ( 𝑁 + 1 ) ) ↔ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ≤ ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ) )
197 195 196 mpbid ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ≤ ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
198 72 62 192 193 197 letrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) ≤ ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
199 72 62 66 absdifled ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( abs ‘ ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) − ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) ≤ ( 𝐺 ‘ ( 𝑁 + 1 ) ) ↔ ( ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) − ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) ∧ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) ≤ ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ) ) )
200 191 198 199 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) − ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) ≤ ( 𝐺 ‘ ( 𝑁 + 1 ) ) )
201 61 200 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ≤ ( 𝐺 ‘ ( 𝑁 + 1 ) ) )
202 16 131 38 subdid ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) = ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) − ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
203 202 fveq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( - 1 ↑ 𝑁 ) · ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) = ( abs ‘ ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) − ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) )
204 70 37 resubcld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ∈ ℝ )
205 204 recnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ∈ ℂ )
206 16 205 absmuld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( - 1 ↑ 𝑁 ) · ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) = ( ( abs ‘ ( - 1 ↑ 𝑁 ) ) · ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) )
207 203 206 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) − ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) = ( ( abs ‘ ( - 1 ↑ 𝑁 ) ) · ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) )
208 56 oveq1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( abs ‘ ( - 1 ↑ 𝑁 ) ) · ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) = ( 1 · ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) )
209 205 abscld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ∈ ℝ )
210 209 recnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ∈ ℂ )
211 210 mulid2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( 1 · ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) = ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
212 207 208 211 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) − ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) = ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
213 71 72 192 190 198 letrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ≤ ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )
214 71 62 66 absdifled ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( abs ‘ ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) − ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) ≤ ( 𝐺 ‘ ( 𝑁 + 1 ) ) ↔ ( ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) − ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ∧ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) ≤ ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) + ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) ) ) )
215 140 213 214 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) ) − ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) ≤ ( 𝐺 ‘ ( 𝑁 + 1 ) ) )
216 212 215 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ≤ ( 𝐺 ‘ ( 𝑁 + 1 ) ) )
217 201 216 jca ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ≤ ( 𝐺 ‘ ( 𝑁 + 1 ) ) ∧ ( abs ‘ ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝐾 ) ) + 1 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ≤ ( 𝐺 ‘ ( 𝑁 + 1 ) ) ) )