Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  iseraltlem3 Structured version   Visualization version   GIF version

Theorem iseraltlem3 14262
 Description: Lemma for iseralt 14263. From iseraltlem2 14261, we have (-1↑𝑛) · 𝑆(𝑛 + 2𝑘) ≤ (-1↑𝑛) · 𝑆(𝑛) and (-1↑𝑛) · 𝑆(𝑛 + 1) ≤ (-1↑𝑛) · 𝑆(𝑛 + 2𝑘 + 1), and we also have (-1↑𝑛) · 𝑆(𝑛 + 1) = (-1↑𝑛) · 𝑆(𝑛) − 𝐺(𝑛 + 1) for each 𝑛 by the definition of the partial sum 𝑆, so combining the inequalities we get (-1↑𝑛) · 𝑆(𝑛) − 𝐺(𝑛 + 1) = (-1↑𝑛) · 𝑆(𝑛 + 1) ≤ (-1↑𝑛) · 𝑆(𝑛 + 2𝑘 + 1) = (-1↑𝑛) · 𝑆(𝑛 + 2𝑘) − 𝐺(𝑛 + 2𝑘 + 1) ≤ (-1↑𝑛) · 𝑆(𝑛 + 2𝑘) ≤ (-1↑𝑛) · 𝑆(𝑛) ≤ (-1↑𝑛) · 𝑆(𝑛) + 𝐺(𝑛 + 1), so ∣ (-1↑𝑛) · 𝑆(𝑛 + 2𝑘 + 1) − (-1↑𝑛) · 𝑆(𝑛) ∣ = ∣ 𝑆(𝑛 + 2𝑘 + 1) − 𝑆(𝑛) ∣ ≤ 𝐺(𝑛 + 1) and ∣ (-1↑𝑛) · 𝑆(𝑛 + 2𝑘) − (-1↑𝑛) · 𝑆(𝑛) ∣ = ∣ 𝑆(𝑛 + 2𝑘) − 𝑆(𝑛) ∣ ≤ 𝐺(𝑛 + 1). Thus, both even and odd partial sums are Cauchy if 𝐺 converges to 0. (Contributed by Mario Carneiro, 6-Apr-2015.)
Hypotheses
Ref Expression
iseralt.1 𝑍 = (ℤ𝑀)
iseralt.2 (𝜑𝑀 ∈ ℤ)
iseralt.3 (𝜑𝐺:𝑍⟶ℝ)
iseralt.4 ((𝜑𝑘𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
iseralt.5 (𝜑𝐺 ⇝ 0)
iseralt.6 ((𝜑𝑘𝑍) → (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
Assertion
Ref Expression
iseraltlem3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1))))
Distinct variable groups:   𝑘,𝐹   𝑘,𝐺   𝑘,𝑀   𝜑,𝑘   𝑘,𝐾   𝑘,𝑁   𝑘,𝑍

Proof of Theorem iseraltlem3
StepHypRef Expression
1 neg1rr 11002 . . . . . . . . . 10 -1 ∈ ℝ
21a1i 11 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -1 ∈ ℝ)
3 neg1ne0 11003 . . . . . . . . . 10 -1 ≠ 0
43a1i 11 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -1 ≠ 0)
5 iseralt.1 . . . . . . . . . . 11 𝑍 = (ℤ𝑀)
6 uzssz 11583 . . . . . . . . . . 11 (ℤ𝑀) ⊆ ℤ
75, 6eqsstri 3598 . . . . . . . . . 10 𝑍 ⊆ ℤ
8 simp2 1055 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝑁𝑍)
97, 8sseldi 3566 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝑁 ∈ ℤ)
102, 4, 9reexpclzd 12896 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑𝑁) ∈ ℝ)
1110recnd 9947 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑𝑁) ∈ ℂ)
12 iseralt.2 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℤ)
13 iseralt.6 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
141a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → -1 ∈ ℝ)
153a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → -1 ≠ 0)
16 simpr 476 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑍) → 𝑘𝑍)
177, 16sseldi 3566 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → 𝑘 ∈ ℤ)
1814, 15, 17reexpclzd 12896 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → (-1↑𝑘) ∈ ℝ)
19 iseralt.3 . . . . . . . . . . . . . 14 (𝜑𝐺:𝑍⟶ℝ)
2019ffvelrnda 6267 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)
2118, 20remulcld 9949 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → ((-1↑𝑘) · (𝐺𝑘)) ∈ ℝ)
2213, 21eqeltrd 2688 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
235, 12, 22serfre 12692 . . . . . . . . . 10 (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
24233ad2ant1 1075 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → seq𝑀( + , 𝐹):𝑍⟶ℝ)
258, 5syl6eleq 2698 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝑁 ∈ (ℤ𝑀))
26 2nn0 11186 . . . . . . . . . . . 12 2 ∈ ℕ0
27 simp3 1056 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝐾 ∈ ℕ0)
28 nn0mulcl 11206 . . . . . . . . . . . 12 ((2 ∈ ℕ0𝐾 ∈ ℕ0) → (2 · 𝐾) ∈ ℕ0)
2926, 27, 28sylancr 694 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (2 · 𝐾) ∈ ℕ0)
30 uzaddcl 11620 . . . . . . . . . . 11 ((𝑁 ∈ (ℤ𝑀) ∧ (2 · 𝐾) ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈ (ℤ𝑀))
3125, 29, 30syl2anc 691 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈ (ℤ𝑀))
3231, 5syl6eleqr 2699 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈ 𝑍)
3324, 32ffvelrnd 6268 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) ∈ ℝ)
3433recnd 9947 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) ∈ ℂ)
3524, 8ffvelrnd 6268 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℝ)
3635recnd 9947 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℂ)
3711, 34, 36subdid 10365 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
3837fveq2d 6107 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
3933, 35resubcld 10337 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
4039recnd 9947 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℂ)
4111, 40absmuld 14041 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))))
4238, 41eqtr3d 2646 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))))
432recnd 9947 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -1 ∈ ℂ)
44 absexpz 13893 . . . . . . 7 ((-1 ∈ ℂ ∧ -1 ≠ 0 ∧ 𝑁 ∈ ℤ) → (abs‘(-1↑𝑁)) = ((abs‘-1)↑𝑁))
4543, 4, 9, 44syl3anc 1318 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(-1↑𝑁)) = ((abs‘-1)↑𝑁))
46 ax-1cn 9873 . . . . . . . . . 10 1 ∈ ℂ
4746absnegi 13987 . . . . . . . . 9 (abs‘-1) = (abs‘1)
48 abs1 13885 . . . . . . . . 9 (abs‘1) = 1
4947, 48eqtri 2632 . . . . . . . 8 (abs‘-1) = 1
5049oveq1i 6559 . . . . . . 7 ((abs‘-1)↑𝑁) = (1↑𝑁)
51 1exp 12751 . . . . . . . 8 (𝑁 ∈ ℤ → (1↑𝑁) = 1)
529, 51syl 17 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1↑𝑁) = 1)
5350, 52syl5eq 2656 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘-1)↑𝑁) = 1)
5445, 53eqtrd 2644 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(-1↑𝑁)) = 1)
5554oveq1d 6564 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (1 · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))))
5640abscld 14023 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℝ)
5756recnd 9947 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℂ)
5857mulid2d 9937 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1 · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))))
5942, 55, 583eqtrd 2648 . . 3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))))
6010, 35remulcld 9949 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
61193ad2ant1 1075 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝐺:𝑍⟶ℝ)
625peano2uzs 11618 . . . . . . . 8 (𝑁𝑍 → (𝑁 + 1) ∈ 𝑍)
63623ad2ant2 1076 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝑁 + 1) ∈ 𝑍)
6461, 63ffvelrnd 6268 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐺‘(𝑁 + 1)) ∈ ℝ)
6560, 64resubcld 10337 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ∈ ℝ)
665peano2uzs 11618 . . . . . . . 8 ((𝑁 + (2 · 𝐾)) ∈ 𝑍 → ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍)
6732, 66syl 17 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍)
6824, 67ffvelrnd 6268 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℝ)
6910, 68remulcld 9949 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℝ)
7010, 33remulcld 9949 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ∈ ℝ)
71 seqp1 12678 . . . . . . . . . . 11 (𝑁 ∈ (ℤ𝑀) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1))))
7225, 71syl 17 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1))))
7313ralrimiva 2949 . . . . . . . . . . . . 13 (𝜑 → ∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
74733ad2ant1 1075 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
75 fveq2 6103 . . . . . . . . . . . . . 14 (𝑘 = (𝑁 + 1) → (𝐹𝑘) = (𝐹‘(𝑁 + 1)))
76 oveq2 6557 . . . . . . . . . . . . . . 15 (𝑘 = (𝑁 + 1) → (-1↑𝑘) = (-1↑(𝑁 + 1)))
77 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑘 = (𝑁 + 1) → (𝐺𝑘) = (𝐺‘(𝑁 + 1)))
7876, 77oveq12d 6567 . . . . . . . . . . . . . 14 (𝑘 = (𝑁 + 1) → ((-1↑𝑘) · (𝐺𝑘)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))))
7975, 78eqeq12d 2625 . . . . . . . . . . . . 13 (𝑘 = (𝑁 + 1) → ((𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) ↔ (𝐹‘(𝑁 + 1)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))))
8079rspcv 3278 . . . . . . . . . . . 12 ((𝑁 + 1) ∈ 𝑍 → (∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) → (𝐹‘(𝑁 + 1)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))))
8163, 74, 80sylc 63 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐹‘(𝑁 + 1)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))))
8281oveq2d 6565 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1))) = ((seq𝑀( + , 𝐹)‘𝑁) + ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))))
8343, 4, 9expp1zd 12879 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 1)) = ((-1↑𝑁) · -1))
84 neg1cn 11001 . . . . . . . . . . . . . . 15 -1 ∈ ℂ
85 mulcom 9901 . . . . . . . . . . . . . . 15 (((-1↑𝑁) ∈ ℂ ∧ -1 ∈ ℂ) → ((-1↑𝑁) · -1) = (-1 · (-1↑𝑁)))
8611, 84, 85sylancl 693 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · -1) = (-1 · (-1↑𝑁)))
8711mulm1d 10361 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1 · (-1↑𝑁)) = -(-1↑𝑁))
8883, 86, 873eqtrd 2648 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 1)) = -(-1↑𝑁))
8988oveq1d 6564 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))) = (-(-1↑𝑁) · (𝐺‘(𝑁 + 1))))
9064recnd 9947 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐺‘(𝑁 + 1)) ∈ ℂ)
9111, 90mulneg1d 10362 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (𝐺‘(𝑁 + 1))) = -((-1↑𝑁) · (𝐺‘(𝑁 + 1))))
9289, 91eqtrd 2644 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))) = -((-1↑𝑁) · (𝐺‘(𝑁 + 1))))
9392oveq2d 6565 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘𝑁) + ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))) = ((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
9472, 82, 933eqtrd 2648 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
9510, 64remulcld 9949 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (𝐺‘(𝑁 + 1))) ∈ ℝ)
9695recnd 9947 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (𝐺‘(𝑁 + 1))) ∈ ℂ)
9736, 96negsubd 10277 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))) = ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
9894, 97eqtrd 2644 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
9998oveq2d 6565 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))))
10011, 36, 96subdid 10365 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))))
1019zcnd 11359 . . . . . . . . . . . . . . 15 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝑁 ∈ ℂ)
1021012timesd 11152 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (2 · 𝑁) = (𝑁 + 𝑁))
103102oveq2d 6565 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(2 · 𝑁)) = (-1↑(𝑁 + 𝑁)))
104 2z 11286 . . . . . . . . . . . . . . 15 2 ∈ ℤ
105104a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 2 ∈ ℤ)
106 expmulz 12768 . . . . . . . . . . . . . 14 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (-1↑(2 · 𝑁)) = ((-1↑2)↑𝑁))
10743, 4, 105, 9, 106syl22anc 1319 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(2 · 𝑁)) = ((-1↑2)↑𝑁))
108103, 107eqtr3d 2646 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 𝑁)) = ((-1↑2)↑𝑁))
109 neg1sqe1 12821 . . . . . . . . . . . . 13 (-1↑2) = 1
110109oveq1i 6559 . . . . . . . . . . . 12 ((-1↑2)↑𝑁) = (1↑𝑁)
111108, 110syl6eq 2660 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 𝑁)) = (1↑𝑁))
112 expaddz 12766 . . . . . . . . . . . 12 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (-1↑(𝑁 + 𝑁)) = ((-1↑𝑁) · (-1↑𝑁)))
11343, 4, 9, 9, 112syl22anc 1319 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 𝑁)) = ((-1↑𝑁) · (-1↑𝑁)))
114111, 113, 523eqtr3d 2652 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (-1↑𝑁)) = 1)
115114oveq1d 6564 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (-1↑𝑁)) · (𝐺‘(𝑁 + 1))) = (1 · (𝐺‘(𝑁 + 1))))
11611, 11, 90mulassd 9942 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (-1↑𝑁)) · (𝐺‘(𝑁 + 1))) = ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
11790mulid2d 9937 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1 · (𝐺‘(𝑁 + 1))) = (𝐺‘(𝑁 + 1)))
118115, 116, 1173eqtr3d 2652 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))) = (𝐺‘(𝑁 + 1)))
119118oveq2d 6565 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))))
12099, 100, 1193eqtrd 2648 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))))
121 iseralt.4 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
122 iseralt.5 . . . . . . . . . . 11 (𝜑𝐺 ⇝ 0)
1235, 12, 19, 121, 122, 13iseraltlem2 14261 . . . . . . . . . 10 ((𝜑 ∧ (𝑁 + 1) ∈ 𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾)))) ≤ ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
12462, 123syl3an2 1352 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾)))) ≤ ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
125 1cnd 9935 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 1 ∈ ℂ)
12629nn0cnd 11230 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (2 · 𝐾) ∈ ℂ)
127101, 125, 126add32d 10142 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((𝑁 + 1) + (2 · 𝐾)) = ((𝑁 + (2 · 𝐾)) + 1))
128127fveq2d 6107 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾))) = (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)))
12988, 128oveq12d 6567 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾)))) = (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))))
13088oveq1d 6564 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) = (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
131124, 129, 1303brtr3d 4614 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
13268recnd 9947 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℂ)
13311, 132mulneg1d 10362 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))))
13424, 63ffvelrnd 6268 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) ∈ ℝ)
135134recnd 9947 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) ∈ ℂ)
13611, 135mulneg1d 10362 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) = -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
137131, 133, 1363brtr3d 4614 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
13810, 134remulcld 9949 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) ∈ ℝ)
139138, 69lenegd 10485 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ↔ -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1)))))
140137, 139mpbird 246 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))))
141120, 140eqbrtrrd 4607 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))))
142 seqp1 12678 . . . . . . . . . 10 ((𝑁 + (2 · 𝐾)) ∈ (ℤ𝑀) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1))))
14331, 142syl 17 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1))))
144 fveq2 6103 . . . . . . . . . . . . . 14 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (𝐹𝑘) = (𝐹‘((𝑁 + (2 · 𝐾)) + 1)))
145 oveq2 6557 . . . . . . . . . . . . . . 15 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (-1↑𝑘) = (-1↑((𝑁 + (2 · 𝐾)) + 1)))
146 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (𝐺𝑘) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
147145, 146oveq12d 6567 . . . . . . . . . . . . . 14 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → ((-1↑𝑘) · (𝐺𝑘)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
148144, 147eqeq12d 2625 . . . . . . . . . . . . 13 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → ((𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) ↔ (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
149148rspcv 3278 . . . . . . . . . . . 12 (((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍 → (∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) → (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
15067, 74, 149sylc 63 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
1517, 63sseldi 3566 . . . . . . . . . . . . . . 15 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝑁 + 1) ∈ ℤ)
15229nn0zd 11356 . . . . . . . . . . . . . . 15 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (2 · 𝐾) ∈ ℤ)
153 expaddz 12766 . . . . . . . . . . . . . . 15 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ ((𝑁 + 1) ∈ ℤ ∧ (2 · 𝐾) ∈ ℤ)) → (-1↑((𝑁 + 1) + (2 · 𝐾))) = ((-1↑(𝑁 + 1)) · (-1↑(2 · 𝐾))))
15443, 4, 151, 152, 153syl22anc 1319 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑((𝑁 + 1) + (2 · 𝐾))) = ((-1↑(𝑁 + 1)) · (-1↑(2 · 𝐾))))
15527nn0zd 11356 . . . . . . . . . . . . . . . . 17 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝐾 ∈ ℤ)
156 expmulz 12768 . . . . . . . . . . . . . . . . 17 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (-1↑(2 · 𝐾)) = ((-1↑2)↑𝐾))
15743, 4, 105, 155, 156syl22anc 1319 . . . . . . . . . . . . . . . 16 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(2 · 𝐾)) = ((-1↑2)↑𝐾))
158109oveq1i 6559 . . . . . . . . . . . . . . . . 17 ((-1↑2)↑𝐾) = (1↑𝐾)
159 1exp 12751 . . . . . . . . . . . . . . . . . 18 (𝐾 ∈ ℤ → (1↑𝐾) = 1)
160155, 159syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1↑𝐾) = 1)
161158, 160syl5eq 2656 . . . . . . . . . . . . . . . 16 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑2)↑𝐾) = 1)
162157, 161eqtrd 2644 . . . . . . . . . . . . . . 15 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(2 · 𝐾)) = 1)
16388, 162oveq12d 6567 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (-1↑(2 · 𝐾))) = (-(-1↑𝑁) · 1))
164154, 163eqtrd 2644 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑((𝑁 + 1) + (2 · 𝐾))) = (-(-1↑𝑁) · 1))
165127oveq2d 6565 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑((𝑁 + 1) + (2 · 𝐾))) = (-1↑((𝑁 + (2 · 𝐾)) + 1)))
16611negcld 10258 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -(-1↑𝑁) ∈ ℂ)
167166mulid1d 9936 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · 1) = -(-1↑𝑁))
168164, 165, 1673eqtr3d 2652 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑((𝑁 + (2 · 𝐾)) + 1)) = -(-1↑𝑁))
169168oveq1d 6564 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (-(-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
17061, 67ffvelrnd 6268 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℝ)
171170recnd 9947 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℂ)
17211, 171mulneg1d 10362 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
173150, 169, 1723eqtrd 2648 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
174173oveq2d 6565 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
17510, 170remulcld 9949 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℝ)
176175recnd 9947 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℂ)
17734, 176negsubd 10277 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
178143, 174, 1773eqtrd 2648 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
179178oveq2d 6565 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))))
18011, 34, 176subdid 10365 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))))
181114oveq1d 6564 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (-1↑𝑁)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (1 · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
18211, 11, 171mulassd 9942 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (-1↑𝑁)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
183171mulid2d 9937 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1 · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
184181, 182, 1833eqtr3d 2652 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
185184oveq2d 6565 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
186179, 180, 1853eqtrd 2648 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
187 simp1 1054 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝜑)
1885, 12, 19, 121, 122iseraltlem1 14260 . . . . . . . 8 ((𝜑 ∧ ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍) → 0 ≤ (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
189187, 67, 188syl2anc 691 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 0 ≤ (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
19070, 170subge02d 10498 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (0 ≤ (𝐺‘((𝑁 + (2 · 𝐾)) + 1)) ↔ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))))))
191189, 190mpbid 221 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
192186, 191eqbrtrd 4605 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
19365, 69, 70, 141, 192letrd 10073 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
19460, 64readdcld 9948 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))) ∈ ℝ)
1955, 12, 19, 121, 122, 13iseraltlem2 14261 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
1965, 12, 19, 121, 122iseraltlem1 14260 . . . . . . 7 ((𝜑 ∧ (𝑁 + 1) ∈ 𝑍) → 0 ≤ (𝐺‘(𝑁 + 1)))
197187, 63, 196syl2anc 691 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 0 ≤ (𝐺‘(𝑁 + 1)))
19860, 64addge01d 10494 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (0 ≤ (𝐺‘(𝑁 + 1)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1)))))
199197, 198mpbid 221 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))
20070, 60, 194, 195, 199letrd 10073 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))
20170, 60, 64absdifled 14021 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)) ↔ ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))))
202193, 200, 201mpbir2and 959 . . 3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)))
20359, 202eqbrtrrd 4607 . 2 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)))
20411, 132, 36subdid 10365 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
205204fveq2d 6107 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
20668, 35resubcld 10337 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
207206recnd 9947 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℂ)
20811, 207absmuld 14041 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))))
209205, 208eqtr3d 2646 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))))
21054oveq1d 6564 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (1 · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))))
211207abscld 14023 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℝ)
212211recnd 9947 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℂ)
213212mulid2d 9937 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1 · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))))
214209, 210, 2133eqtrd 2648 . . 3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))))
21569, 70, 194, 192, 200letrd 10073 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))
21669, 60, 64absdifled 14021 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)) ↔ ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))))
217141, 215, 216mpbir2and 959 . . 3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)))
218214, 217eqbrtrrd 4607 . 2 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)))
219203, 218jca 553 1 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896   class class class wbr 4583  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820   ≤ cle 9954   − cmin 10145  -cneg 10146  2c2 10947  ℕ0cn0 11169  ℤcz 11254  ℤ≥cuz 11563  seqcseq 12663  ↑cexp 12722  abscabs 13822   ⇝ cli 14063 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-fz 12198  df-fl 12455  df-seq 12664  df-exp 12723  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-rlim 14068 This theorem is referenced by:  iseralt  14263
 Copyright terms: Public domain W3C validator