Metamath Proof Explorer

Theorem iseraltlem2

Description: Lemma for iseralt . The terms of an alternating series form a chain of inequalities in alternate terms, so that for example S ( 1 ) <_ S ( 3 ) <_ S ( 5 ) <_ ... and ... <_ S ( 4 ) <_ S ( 2 ) <_ S ( 0 ) (assuming M = 0 so that these terms are defined). (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 iseraltlem2 ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )

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 oveq2 ⊢ ( 𝑥 = 0 → ( 2 · 𝑥 ) = ( 2 · 0 ) )
8 2t0e0 ⊢ ( 2 · 0 ) = 0
9 7 8 eqtrdi ⊢ ( 𝑥 = 0 → ( 2 · 𝑥 ) = 0 )
10 9 oveq2d ⊢ ( 𝑥 = 0 → ( 𝑁 + ( 2 · 𝑥 ) ) = ( 𝑁 + 0 ) )
11 10 fveq2d ⊢ ( 𝑥 = 0 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑥 ) ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 0 ) ) )
12 11 oveq2d ⊢ ( 𝑥 = 0 → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑥 ) ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 0 ) ) ) )
13 12 breq1d ⊢ ( 𝑥 = 0 → ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑥 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ↔ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 0 ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
14 13 imbi2d ⊢ ( 𝑥 = 0 → ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑥 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ↔ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 0 ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) )
15 oveq2 ⊢ ( 𝑥 = 𝑛 → ( 2 · 𝑥 ) = ( 2 · 𝑛 ) )
16 15 oveq2d ⊢ ( 𝑥 = 𝑛 → ( 𝑁 + ( 2 · 𝑥 ) ) = ( 𝑁 + ( 2 · 𝑛 ) ) )
17 16 fveq2d ⊢ ( 𝑥 = 𝑛 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑥 ) ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) )
18 17 oveq2d ⊢ ( 𝑥 = 𝑛 → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑥 ) ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) )
19 18 breq1d ⊢ ( 𝑥 = 𝑛 → ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑥 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ↔ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
20 19 imbi2d ⊢ ( 𝑥 = 𝑛 → ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑥 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ↔ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) )
21 oveq2 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 2 · 𝑥 ) = ( 2 · ( 𝑛 + 1 ) ) )
22 21 oveq2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑁 + ( 2 · 𝑥 ) ) = ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) )
23 22 fveq2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑥 ) ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ) )
24 23 oveq2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑥 ) ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ) ) )
25 24 breq1d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑥 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ↔ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
26 25 imbi2d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑥 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ↔ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) )
27 oveq2 ⊢ ( 𝑥 = 𝐾 → ( 2 · 𝑥 ) = ( 2 · 𝐾 ) )
28 27 oveq2d ⊢ ( 𝑥 = 𝐾 → ( 𝑁 + ( 2 · 𝑥 ) ) = ( 𝑁 + ( 2 · 𝐾 ) ) )
29 28 fveq2d ⊢ ( 𝑥 = 𝐾 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑥 ) ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) )
30 29 oveq2d ⊢ ( 𝑥 = 𝐾 → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑥 ) ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) )
31 30 breq1d ⊢ ( 𝑥 = 𝐾 → ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑥 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ↔ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
32 31 imbi2d ⊢ ( 𝑥 = 𝐾 → ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑥 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ↔ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) )
33 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
34 1 33 eqsstri ⊢ 𝑍 ⊆ ℤ
35 34 a1i ⊢ ( 𝜑 → 𝑍 ⊆ ℤ )
36 35 sselda ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → 𝑁 ∈ ℤ )
37 36 zcnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → 𝑁 ∈ ℂ )
38 37 addid1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( 𝑁 + 0 ) = 𝑁 )
39 38 fveq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 0 ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
40 39 oveq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 0 ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
41 neg1rr ⊢ - 1 ∈ ℝ
42 neg1ne0 ⊢ - 1 ≠ 0
43 reexpclz ⊢ ( ( - 1 ∈ ℝ ∧ - 1 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( - 1 ↑ 𝑁 ) ∈ ℝ )
44 41 42 36 43 mp3an12i ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( - 1 ↑ 𝑁 ) ∈ ℝ )
45 35 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ℤ )
46 reexpclz ⊢ ( ( - 1 ∈ ℝ ∧ - 1 ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( - 1 ↑ 𝑘 ) ∈ ℝ )
47 41 42 45 46 mp3an12i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( - 1 ↑ 𝑘 ) ∈ ℝ )
48 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
49 47 48 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( - 1 ↑ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) ∈ ℝ )
50 6 49 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
51 1 2 50 serfre ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ )
52 51 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ ℝ )
53 44 52 remulcld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ∈ ℝ )
54 53 leidd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
55 40 54 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 0 ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
56 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → 𝐺 : 𝑍 ⟶ ℝ )
57 ax-1cn ⊢ 1 ∈ ℂ
58 57 2timesi ⊢ ( 2 · 1 ) = ( 1 + 1 )
59 58 oveq2i ⊢ ( ( 𝑁 + ( 2 · 𝑛 ) ) + ( 2 · 1 ) ) = ( ( 𝑁 + ( 2 · 𝑛 ) ) + ( 1 + 1 ) )
60 simpr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → 𝑁 ∈ 𝑍 )
61 60 1 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
62 61 adantr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
63 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
64 62 63 syl ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
65 64 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
66 2cn ⊢ 2 ∈ ℂ
67 nn0cn ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℂ )
68 67 adantl ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℂ )
69 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( 2 · 𝑛 ) ∈ ℂ )
70 66 68 69 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 2 · 𝑛 ) ∈ ℂ )
71 66 57 mulcli ⊢ ( 2 · 1 ) ∈ ℂ
72 71 a1i ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 2 · 1 ) ∈ ℂ )
73 65 70 72 addassd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑁 + ( 2 · 𝑛 ) ) + ( 2 · 1 ) ) = ( 𝑁 + ( ( 2 · 𝑛 ) + ( 2 · 1 ) ) ) )
74 59 73 eqtr3id ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑁 + ( 2 · 𝑛 ) ) + ( 1 + 1 ) ) = ( 𝑁 + ( ( 2 · 𝑛 ) + ( 2 · 1 ) ) ) )
75 2nn0 ⊢ 2 ∈ ℕ0
76 simpr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
77 nn0mulcl ⊢ ( ( 2 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 · 𝑛 ) ∈ ℕ0 )
78 75 76 77 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 2 · 𝑛 ) ∈ ℕ0 )
79 uzaddcl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 2 · 𝑛 ) ∈ ℕ0 ) → ( 𝑁 + ( 2 · 𝑛 ) ) ∈ ( ℤ≥ ‘ 𝑀 ) )
80 62 78 79 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑁 + ( 2 · 𝑛 ) ) ∈ ( ℤ≥ ‘ 𝑀 ) )
81 33 80 sselid ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑁 + ( 2 · 𝑛 ) ) ∈ ℤ )
82 81 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑁 + ( 2 · 𝑛 ) ) ∈ ℂ )
83 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → 1 ∈ ℂ )
84 82 83 83 addassd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) = ( ( 𝑁 + ( 2 · 𝑛 ) ) + ( 1 + 1 ) ) )
85 2cnd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → 2 ∈ ℂ )
86 85 68 83 adddid ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 2 · ( 𝑛 + 1 ) ) = ( ( 2 · 𝑛 ) + ( 2 · 1 ) ) )
87 86 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) = ( 𝑁 + ( ( 2 · 𝑛 ) + ( 2 · 1 ) ) ) )
88 74 84 87 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) = ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) )
89 peano2nn0 ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 1 ) ∈ ℕ0 )
90 89 adantl ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 + 1 ) ∈ ℕ0 )
91 nn0mulcl ⊢ ( ( 2 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ℕ0 ) → ( 2 · ( 𝑛 + 1 ) ) ∈ ℕ0 )
92 75 90 91 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 2 · ( 𝑛 + 1 ) ) ∈ ℕ0 )
93 uzaddcl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 2 · ( 𝑛 + 1 ) ) ∈ ℕ0 ) → ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ∈ ( ℤ≥ ‘ 𝑀 ) )
94 62 92 93 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ∈ ( ℤ≥ ‘ 𝑀 ) )
95 94 1 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ∈ 𝑍 )
96 88 95 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ∈ 𝑍 )
97 56 96 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ∈ ℝ )
98 peano2uz ⊢ ( ( 𝑁 + ( 2 · 𝑛 ) ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
99 80 98 syl ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
100 99 1 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ∈ 𝑍 )
101 56 100 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ∈ ℝ )
102 97 101 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) − ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) ∈ ℝ )
103 0red ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → 0 ∈ ℝ )
104 44 adantr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( - 1 ↑ 𝑁 ) ∈ ℝ )
105 51 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ )
106 80 1 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑁 + ( 2 · 𝑛 ) ) ∈ 𝑍 )
107 105 106 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ∈ ℝ )
108 104 107 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) ∈ ℝ )
109 fvoveq1 ⊢ ( 𝑘 = ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) → ( 𝐺 ‘ ( 𝑘 + 1 ) ) = ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) )
110 fveq2 ⊢ ( 𝑘 = ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) )
111 109 110 breq12d ⊢ ( 𝑘 = ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) → ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐺 ‘ 𝑘 ) ↔ ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ≤ ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) )
112 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐺 ‘ 𝑘 ) )
113 112 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ∀ 𝑘 ∈ 𝑍 ( 𝐺 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐺 ‘ 𝑘 ) )
114 111 113 100 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ≤ ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) )
115 97 101 suble0d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) − ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) ≤ 0 ↔ ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ≤ ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) )
116 114 115 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) − ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) ≤ 0 )
117 102 103 108 116 leadd2dd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) + ( ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) − ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) ) ≤ ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) + 0 ) )
118 seqp1 ⊢ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) + ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) )
119 99 118 syl ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) + ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) )
120 seqp1 ⊢ ( ( 𝑁 + ( 2 · 𝑛 ) ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) + ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) )
121 80 120 syl ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) + ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) )
122 121 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) + ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) = ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) + ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) + ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) )
123 119 122 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) = ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) + ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) + ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) )
124 88 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ) )
125 107 recnd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ∈ ℂ )
126 fveq2 ⊢ ( 𝑘 = ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) )
127 oveq2 ⊢ ( 𝑘 = ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) → ( - 1 ↑ 𝑘 ) = ( - 1 ↑ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) )
128 127 110 oveq12d ⊢ ( 𝑘 = ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) → ( ( - 1 ↑ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) = ( ( - 1 ↑ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) )
129 126 128 eqeq12d ⊢ ( 𝑘 = ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) → ( ( 𝐹 ‘ 𝑘 ) = ( ( - 1 ↑ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) ↔ ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) = ( ( - 1 ↑ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) ) )
130 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) = ( ( - 1 ↑ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
131 130 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) = ( ( - 1 ↑ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) )
132 129 131 100 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) = ( ( - 1 ↑ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) )
133 neg1cn ⊢ - 1 ∈ ℂ
134 133 a1i ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → - 1 ∈ ℂ )
135 42 a1i ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → - 1 ≠ 0 )
136 134 135 81 expp1zd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( - 1 ↑ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) = ( ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · - 1 ) )
137 41 a1i ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → - 1 ∈ ℝ )
138 137 135 81 reexpclzd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) ∈ ℝ )
139 138 recnd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) ∈ ℂ )
140 mulcom ⊢ ( ( ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) ∈ ℂ ∧ - 1 ∈ ℂ ) → ( ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · - 1 ) = ( - 1 · ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) )
141 139 133 140 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · - 1 ) = ( - 1 · ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) )
142 139 mulm1d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( - 1 · ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) = - ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) )
143 136 141 142 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( - 1 ↑ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) = - ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) )
144 143 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) = ( - ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) )
145 101 recnd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ∈ ℂ )
146 mulneg12 ⊢ ( ( ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) ∈ ℂ ∧ ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ∈ ℂ ) → ( - ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) = ( ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) )
147 139 145 146 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( - ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) = ( ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) )
148 132 144 147 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) = ( ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) )
149 101 renegcld ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ∈ ℝ )
150 138 149 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) ∈ ℝ )
151 148 150 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ∈ ℝ )
152 151 recnd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ∈ ℂ )
153 fveq2 ⊢ ( 𝑘 = ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) )
154 oveq2 ⊢ ( 𝑘 = ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) → ( - 1 ↑ 𝑘 ) = ( - 1 ↑ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) )
155 fveq2 ⊢ ( 𝑘 = ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) )
156 154 155 oveq12d ⊢ ( 𝑘 = ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) → ( ( - 1 ↑ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) = ( ( - 1 ↑ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) · ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) )
157 153 156 eqeq12d ⊢ ( 𝑘 = ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) → ( ( 𝐹 ‘ 𝑘 ) = ( ( - 1 ↑ 𝑘 ) · ( 𝐺 ‘ 𝑘 ) ) ↔ ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) = ( ( - 1 ↑ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) · ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) ) )
158 157 131 96 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) = ( ( - 1 ↑ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) · ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) )
159 81 peano2zd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ∈ ℤ )
160 134 135 159 expp1zd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( - 1 ↑ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) = ( ( - 1 ↑ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) · - 1 ) )
161 143 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) · - 1 ) = ( - ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · - 1 ) )
162 mul2neg ⊢ ( ( ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( - ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · - 1 ) = ( ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · 1 ) )
163 139 57 162 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( - ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · - 1 ) = ( ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · 1 ) )
164 139 mulid1d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · 1 ) = ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) )
165 163 164 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( - ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · - 1 ) = ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) )
166 160 161 165 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( - 1 ↑ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) = ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) )
167 166 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) · ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) = ( ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) )
168 158 167 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) = ( ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) )
169 138 97 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) ∈ ℝ )
170 168 169 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ∈ ℝ )
171 170 recnd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ∈ ℂ )
172 125 152 171 addassd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) + ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) + ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) + ( ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) + ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) ) )
173 123 124 172 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) + ( ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) + ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) ) )
174 173 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) + ( ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) + ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) ) ) )
175 104 recnd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( - 1 ↑ 𝑁 ) ∈ ℂ )
176 151 170 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) + ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) ∈ ℝ )
177 176 recnd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) + ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) ∈ ℂ )
178 175 125 177 adddid ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) + ( ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) + ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) ) ) = ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) + ( ( - 1 ↑ 𝑁 ) · ( ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) + ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) ) ) )
179 175 152 171 adddid ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) + ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) ) = ( ( ( - 1 ↑ 𝑁 ) · ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) + ( ( - 1 ↑ 𝑁 ) · ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) ) )
180 148 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) ) )
181 149 recnd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ∈ ℂ )
182 175 139 181 mulassd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) · - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) ) )
183 180 182 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) = ( ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) · - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) )
184 85 65 68 adddid ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 2 · ( 𝑁 + 𝑛 ) ) = ( ( 2 · 𝑁 ) + ( 2 · 𝑛 ) ) )
185 65 2timesd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) )
186 185 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 · 𝑁 ) + ( 2 · 𝑛 ) ) = ( ( 𝑁 + 𝑁 ) + ( 2 · 𝑛 ) ) )
187 65 65 70 addassd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑁 + 𝑁 ) + ( 2 · 𝑛 ) ) = ( 𝑁 + ( 𝑁 + ( 2 · 𝑛 ) ) ) )
188 184 186 187 3eqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑁 + ( 𝑁 + ( 2 · 𝑛 ) ) ) = ( 2 · ( 𝑁 + 𝑛 ) ) )
189 188 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( - 1 ↑ ( 𝑁 + ( 𝑁 + ( 2 · 𝑛 ) ) ) ) = ( - 1 ↑ ( 2 · ( 𝑁 + 𝑛 ) ) ) )
190 expaddz ⊢ ( ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) ∧ ( 𝑁 ∈ ℤ ∧ ( 𝑁 + ( 2 · 𝑛 ) ) ∈ ℤ ) ) → ( - 1 ↑ ( 𝑁 + ( 𝑁 + ( 2 · 𝑛 ) ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) )
191 134 135 64 81 190 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( - 1 ↑ ( 𝑁 + ( 𝑁 + ( 2 · 𝑛 ) ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) )
192 2z ⊢ 2 ∈ ℤ
193 192 a1i ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → 2 ∈ ℤ )
194 nn0z ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ )
195 zaddcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑁 + 𝑛 ) ∈ ℤ )
196 36 194 195 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑁 + 𝑛 ) ∈ ℤ )
197 expmulz ⊢ ( ( ( - 1 ∈ ℂ ∧ - 1 ≠ 0 ) ∧ ( 2 ∈ ℤ ∧ ( 𝑁 + 𝑛 ) ∈ ℤ ) ) → ( - 1 ↑ ( 2 · ( 𝑁 + 𝑛 ) ) ) = ( ( - 1 ↑ 2 ) ↑ ( 𝑁 + 𝑛 ) ) )
198 134 135 193 196 197 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( - 1 ↑ ( 2 · ( 𝑁 + 𝑛 ) ) ) = ( ( - 1 ↑ 2 ) ↑ ( 𝑁 + 𝑛 ) ) )
199 neg1sqe1 ⊢ ( - 1 ↑ 2 ) = 1
200 199 oveq1i ⊢ ( ( - 1 ↑ 2 ) ↑ ( 𝑁 + 𝑛 ) ) = ( 1 ↑ ( 𝑁 + 𝑛 ) )
201 1exp ⊢ ( ( 𝑁 + 𝑛 ) ∈ ℤ → ( 1 ↑ ( 𝑁 + 𝑛 ) ) = 1 )
202 196 201 syl ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 1 ↑ ( 𝑁 + 𝑛 ) ) = 1 )
203 200 202 eqtrid ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ 2 ) ↑ ( 𝑁 + 𝑛 ) ) = 1 )
204 198 203 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( - 1 ↑ ( 2 · ( 𝑁 + 𝑛 ) ) ) = 1 )
205 189 191 204 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) = 1 )
206 205 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) · - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) = ( 1 · - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) )
207 181 mulid2d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 1 · - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) = - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) )
208 183 206 207 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) = - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) )
209 168 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) ) )
210 97 recnd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ∈ ℂ )
211 175 139 210 mulassd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) · ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) · ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) ) )
212 209 211 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) = ( ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) · ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) )
213 205 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) · ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) = ( 1 · ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) )
214 210 mulid2d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( 1 · ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) = ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) )
215 212 213 214 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) = ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) )
216 208 215 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) + ( ( - 1 ↑ 𝑁 ) · ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) ) = ( - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) + ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) )
217 145 negcld ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ∈ ℂ )
218 217 210 addcomd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) + ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) = ( ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) + - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) )
219 210 145 negsubd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) + - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) = ( ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) − ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) )
220 218 219 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( - ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) + ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) = ( ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) − ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) )
221 179 216 220 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) + ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) ) = ( ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) − ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) )
222 221 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) + ( ( - 1 ↑ 𝑁 ) · ( ( 𝐹 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) + ( 𝐹 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) ) ) ) = ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) + ( ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) − ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) ) )
223 174 178 222 3eqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) + ( ( 𝐺 ‘ ( ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) + 1 ) ) − ( 𝐺 ‘ ( ( 𝑁 + ( 2 · 𝑛 ) ) + 1 ) ) ) ) = ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ) ) )
224 108 recnd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) ∈ ℂ )
225 224 addid1d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) + 0 ) = ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) )
226 117 223 225 3brtr3d ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) )
227 105 95 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ) ∈ ℝ )
228 104 227 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ) ) ∈ ℝ )
229 53 adantr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ∈ ℝ )
230 letr ⊢ ( ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ) ) ∈ ℝ ∧ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) ∈ ℝ ∧ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ∈ ℝ ) → ( ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) ∧ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
231 228 108 229 230 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) ∧ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
232 226 231 mpand ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
233 232 expcom ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) )
234 233 a2d ⊢ ( 𝑛 ∈ ℕ0 → ( ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝑛 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) → ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · ( 𝑛 + 1 ) ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) ) )
235 14 20 26 32 55 234 nn0ind ⊢ ( 𝐾 ∈ ℕ0 → ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
236 235 com12 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( 𝐾 ∈ ℕ0 → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ) )
237 236 3impia ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + ( 2 · 𝐾 ) ) ) ) ≤ ( ( - 1 ↑ 𝑁 ) · ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )