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	sselid	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ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	sselid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ℤ )
21	17 18 20	reexpclzd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( - 1 ↑ 𝑘 ) ∈ ℝ )
22	3	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ∈ ℝ )
36	35	recnd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ∈ ℂ )
37	26 13	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ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	eqtrid	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ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	mullidd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ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	mullidd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ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	sselid	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ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	eqtrid	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ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	mulridd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ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	mullidd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ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	mullidd	⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ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 ) ) ) )