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

Theorem iseraltlem3 14699
Description: Lemma for iseralt 14700. From iseraltlem2 14698, 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 11394 . . . . . . . . . 10 -1 ∈ ℝ
21a1i 11 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -1 ∈ ℝ)
3 neg1ne0 11395 . . . . . . . . . 10 -1 ≠ 0
43a1i 11 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -1 ≠ 0)
5 iseralt.1 . . . . . . . . . . 11 𝑍 = (ℤ𝑀)
6 uzssz 11906 . . . . . . . . . . 11 (ℤ𝑀) ⊆ ℤ
75, 6eqsstri 3795 . . . . . . . . . 10 𝑍 ⊆ ℤ
8 simp2 1167 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝑁𝑍)
97, 8sseldi 3759 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝑁 ∈ ℤ)
102, 4, 9reexpclzd 13241 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑𝑁) ∈ ℝ)
1110recnd 10322 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑𝑁) ∈ ℂ)
12 iseralt.2 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℤ)
13 iseralt.6 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
141a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → -1 ∈ ℝ)
153a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → -1 ≠ 0)
16 simpr 477 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑍) → 𝑘𝑍)
177, 16sseldi 3759 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → 𝑘 ∈ ℤ)
1814, 15, 17reexpclzd 13241 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → (-1↑𝑘) ∈ ℝ)
19 iseralt.3 . . . . . . . . . . . . . 14 (𝜑𝐺:𝑍⟶ℝ)
2019ffvelrnda 6549 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)
2118, 20remulcld 10324 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → ((-1↑𝑘) · (𝐺𝑘)) ∈ ℝ)
2213, 21eqeltrd 2844 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
235, 12, 22serfre 13037 . . . . . . . . . 10 (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
24233ad2ant1 1163 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → seq𝑀( + , 𝐹):𝑍⟶ℝ)
258, 5syl6eleq 2854 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝑁 ∈ (ℤ𝑀))
26 2nn0 11557 . . . . . . . . . . . 12 2 ∈ ℕ0
27 simp3 1168 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝐾 ∈ ℕ0)
28 nn0mulcl 11576 . . . . . . . . . . . 12 ((2 ∈ ℕ0𝐾 ∈ ℕ0) → (2 · 𝐾) ∈ ℕ0)
2926, 27, 28sylancr 581 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (2 · 𝐾) ∈ ℕ0)
30 uzaddcl 11944 . . . . . . . . . . 11 ((𝑁 ∈ (ℤ𝑀) ∧ (2 · 𝐾) ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈ (ℤ𝑀))
3125, 29, 30syl2anc 579 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈ (ℤ𝑀))
3231, 5syl6eleqr 2855 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈ 𝑍)
3324, 32ffvelrnd 6550 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) ∈ ℝ)
3433recnd 10322 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) ∈ ℂ)
3524, 8ffvelrnd 6550 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℝ)
3635recnd 10322 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℂ)
3711, 34, 36subdid 10740 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
3837fveq2d 6379 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
3933, 35resubcld 10712 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
4039recnd 10322 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℂ)
4111, 40absmuld 14478 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))))
4238, 41eqtr3d 2801 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))))
432recnd 10322 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -1 ∈ ℂ)
44 absexpz 14330 . . . . . . 7 ((-1 ∈ ℂ ∧ -1 ≠ 0 ∧ 𝑁 ∈ ℤ) → (abs‘(-1↑𝑁)) = ((abs‘-1)↑𝑁))
4543, 4, 9, 44syl3anc 1490 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(-1↑𝑁)) = ((abs‘-1)↑𝑁))
46 ax-1cn 10247 . . . . . . . . . 10 1 ∈ ℂ
4746absnegi 14424 . . . . . . . . 9 (abs‘-1) = (abs‘1)
48 abs1 14322 . . . . . . . . 9 (abs‘1) = 1
4947, 48eqtri 2787 . . . . . . . 8 (abs‘-1) = 1
5049oveq1i 6852 . . . . . . 7 ((abs‘-1)↑𝑁) = (1↑𝑁)
51 1exp 13096 . . . . . . . 8 (𝑁 ∈ ℤ → (1↑𝑁) = 1)
529, 51syl 17 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1↑𝑁) = 1)
5350, 52syl5eq 2811 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘-1)↑𝑁) = 1)
5445, 53eqtrd 2799 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(-1↑𝑁)) = 1)
5554oveq1d 6857 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (1 · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))))
5640abscld 14460 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℝ)
5756recnd 10322 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℂ)
5857mulid2d 10312 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1 · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))))
5942, 55, 583eqtrd 2803 . . 3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))))
6010, 35remulcld 10324 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
61193ad2ant1 1163 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝐺:𝑍⟶ℝ)
625peano2uzs 11942 . . . . . . . 8 (𝑁𝑍 → (𝑁 + 1) ∈ 𝑍)
63623ad2ant2 1164 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝑁 + 1) ∈ 𝑍)
6461, 63ffvelrnd 6550 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐺‘(𝑁 + 1)) ∈ ℝ)
6560, 64resubcld 10712 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ∈ ℝ)
665peano2uzs 11942 . . . . . . . 8 ((𝑁 + (2 · 𝐾)) ∈ 𝑍 → ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍)
6732, 66syl 17 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍)
6824, 67ffvelrnd 6550 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℝ)
6910, 68remulcld 10324 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℝ)
7010, 33remulcld 10324 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ∈ ℝ)
71 seqp1 13023 . . . . . . . . . . 11 (𝑁 ∈ (ℤ𝑀) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1))))
7225, 71syl 17 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1))))
73 fveq2 6375 . . . . . . . . . . . . 13 (𝑘 = (𝑁 + 1) → (𝐹𝑘) = (𝐹‘(𝑁 + 1)))
74 oveq2 6850 . . . . . . . . . . . . . 14 (𝑘 = (𝑁 + 1) → (-1↑𝑘) = (-1↑(𝑁 + 1)))
75 fveq2 6375 . . . . . . . . . . . . . 14 (𝑘 = (𝑁 + 1) → (𝐺𝑘) = (𝐺‘(𝑁 + 1)))
7674, 75oveq12d 6860 . . . . . . . . . . . . 13 (𝑘 = (𝑁 + 1) → ((-1↑𝑘) · (𝐺𝑘)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))))
7773, 76eqeq12d 2780 . . . . . . . . . . . 12 (𝑘 = (𝑁 + 1) → ((𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) ↔ (𝐹‘(𝑁 + 1)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))))
7813ralrimiva 3113 . . . . . . . . . . . . 13 (𝜑 → ∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
79783ad2ant1 1163 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
8077, 79, 63rspcdva 3467 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐹‘(𝑁 + 1)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))))
8180oveq2d 6858 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1))) = ((seq𝑀( + , 𝐹)‘𝑁) + ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))))
8243, 4, 9expp1zd 13224 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 1)) = ((-1↑𝑁) · -1))
83 neg1cn 11393 . . . . . . . . . . . . . . 15 -1 ∈ ℂ
84 mulcom 10275 . . . . . . . . . . . . . . 15 (((-1↑𝑁) ∈ ℂ ∧ -1 ∈ ℂ) → ((-1↑𝑁) · -1) = (-1 · (-1↑𝑁)))
8511, 83, 84sylancl 580 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · -1) = (-1 · (-1↑𝑁)))
8611mulm1d 10736 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1 · (-1↑𝑁)) = -(-1↑𝑁))
8782, 85, 863eqtrd 2803 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 1)) = -(-1↑𝑁))
8887oveq1d 6857 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))) = (-(-1↑𝑁) · (𝐺‘(𝑁 + 1))))
8964recnd 10322 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐺‘(𝑁 + 1)) ∈ ℂ)
9011, 89mulneg1d 10737 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (𝐺‘(𝑁 + 1))) = -((-1↑𝑁) · (𝐺‘(𝑁 + 1))))
9188, 90eqtrd 2799 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))) = -((-1↑𝑁) · (𝐺‘(𝑁 + 1))))
9291oveq2d 6858 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘𝑁) + ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))) = ((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
9372, 81, 923eqtrd 2803 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
9410, 64remulcld 10324 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (𝐺‘(𝑁 + 1))) ∈ ℝ)
9594recnd 10322 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (𝐺‘(𝑁 + 1))) ∈ ℂ)
9636, 95negsubd 10652 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))) = ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
9793, 96eqtrd 2799 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
9897oveq2d 6858 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))))
9911, 36, 95subdid 10740 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))))
1009zcnd 11730 . . . . . . . . . . . . . . 15 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝑁 ∈ ℂ)
1011002timesd 11521 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (2 · 𝑁) = (𝑁 + 𝑁))
102101oveq2d 6858 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(2 · 𝑁)) = (-1↑(𝑁 + 𝑁)))
103 2z 11656 . . . . . . . . . . . . . . 15 2 ∈ ℤ
104103a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 2 ∈ ℤ)
105 expmulz 13113 . . . . . . . . . . . . . 14 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (-1↑(2 · 𝑁)) = ((-1↑2)↑𝑁))
10643, 4, 104, 9, 105syl22anc 867 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(2 · 𝑁)) = ((-1↑2)↑𝑁))
107102, 106eqtr3d 2801 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 𝑁)) = ((-1↑2)↑𝑁))
108 neg1sqe1 13166 . . . . . . . . . . . . 13 (-1↑2) = 1
109108oveq1i 6852 . . . . . . . . . . . 12 ((-1↑2)↑𝑁) = (1↑𝑁)
110107, 109syl6eq 2815 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 𝑁)) = (1↑𝑁))
111 expaddz 13111 . . . . . . . . . . . 12 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (-1↑(𝑁 + 𝑁)) = ((-1↑𝑁) · (-1↑𝑁)))
11243, 4, 9, 9, 111syl22anc 867 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 𝑁)) = ((-1↑𝑁) · (-1↑𝑁)))
113110, 112, 523eqtr3d 2807 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (-1↑𝑁)) = 1)
114113oveq1d 6857 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (-1↑𝑁)) · (𝐺‘(𝑁 + 1))) = (1 · (𝐺‘(𝑁 + 1))))
11511, 11, 89mulassd 10317 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (-1↑𝑁)) · (𝐺‘(𝑁 + 1))) = ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
11689mulid2d 10312 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1 · (𝐺‘(𝑁 + 1))) = (𝐺‘(𝑁 + 1)))
117114, 115, 1163eqtr3d 2807 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))) = (𝐺‘(𝑁 + 1)))
118117oveq2d 6858 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))))
11998, 99, 1183eqtrd 2803 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))))
120 iseralt.4 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
121 iseralt.5 . . . . . . . . . . 11 (𝜑𝐺 ⇝ 0)
1225, 12, 19, 120, 121, 13iseraltlem2 14698 . . . . . . . . . 10 ((𝜑 ∧ (𝑁 + 1) ∈ 𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾)))) ≤ ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
12362, 122syl3an2 1203 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾)))) ≤ ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
124 1cnd 10288 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 1 ∈ ℂ)
12529nn0cnd 11600 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (2 · 𝐾) ∈ ℂ)
126100, 124, 125add32d 10517 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((𝑁 + 1) + (2 · 𝐾)) = ((𝑁 + (2 · 𝐾)) + 1))
127126fveq2d 6379 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾))) = (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)))
12887, 127oveq12d 6860 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾)))) = (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))))
12987oveq1d 6857 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) = (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
130123, 128, 1293brtr3d 4840 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
13168recnd 10322 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℂ)
13211, 131mulneg1d 10737 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))))
13324, 63ffvelrnd 6550 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) ∈ ℝ)
134133recnd 10322 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) ∈ ℂ)
13511, 134mulneg1d 10737 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) = -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
136130, 132, 1353brtr3d 4840 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
13710, 133remulcld 10324 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) ∈ ℝ)
138137, 69lenegd 10860 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ↔ -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1)))))
139136, 138mpbird 248 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))))
140119, 139eqbrtrrd 4833 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))))
141 seqp1 13023 . . . . . . . . . 10 ((𝑁 + (2 · 𝐾)) ∈ (ℤ𝑀) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1))))
14231, 141syl 17 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1))))
143 fveq2 6375 . . . . . . . . . . . . 13 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (𝐹𝑘) = (𝐹‘((𝑁 + (2 · 𝐾)) + 1)))
144 oveq2 6850 . . . . . . . . . . . . . 14 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (-1↑𝑘) = (-1↑((𝑁 + (2 · 𝐾)) + 1)))
145 fveq2 6375 . . . . . . . . . . . . . 14 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (𝐺𝑘) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
146144, 145oveq12d 6860 . . . . . . . . . . . . 13 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → ((-1↑𝑘) · (𝐺𝑘)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
147143, 146eqeq12d 2780 . . . . . . . . . . . 12 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → ((𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) ↔ (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
148147, 79, 67rspcdva 3467 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
1497, 63sseldi 3759 . . . . . . . . . . . . . . 15 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝑁 + 1) ∈ ℤ)
15029nn0zd 11727 . . . . . . . . . . . . . . 15 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (2 · 𝐾) ∈ ℤ)
151 expaddz 13111 . . . . . . . . . . . . . . 15 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ ((𝑁 + 1) ∈ ℤ ∧ (2 · 𝐾) ∈ ℤ)) → (-1↑((𝑁 + 1) + (2 · 𝐾))) = ((-1↑(𝑁 + 1)) · (-1↑(2 · 𝐾))))
15243, 4, 149, 150, 151syl22anc 867 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑((𝑁 + 1) + (2 · 𝐾))) = ((-1↑(𝑁 + 1)) · (-1↑(2 · 𝐾))))
15327nn0zd 11727 . . . . . . . . . . . . . . . . 17 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝐾 ∈ ℤ)
154 expmulz 13113 . . . . . . . . . . . . . . . . 17 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (-1↑(2 · 𝐾)) = ((-1↑2)↑𝐾))
15543, 4, 104, 153, 154syl22anc 867 . . . . . . . . . . . . . . . 16 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(2 · 𝐾)) = ((-1↑2)↑𝐾))
156108oveq1i 6852 . . . . . . . . . . . . . . . . 17 ((-1↑2)↑𝐾) = (1↑𝐾)
157 1exp 13096 . . . . . . . . . . . . . . . . . 18 (𝐾 ∈ ℤ → (1↑𝐾) = 1)
158153, 157syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1↑𝐾) = 1)
159156, 158syl5eq 2811 . . . . . . . . . . . . . . . 16 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑2)↑𝐾) = 1)
160155, 159eqtrd 2799 . . . . . . . . . . . . . . 15 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(2 · 𝐾)) = 1)
16187, 160oveq12d 6860 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (-1↑(2 · 𝐾))) = (-(-1↑𝑁) · 1))
162152, 161eqtrd 2799 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑((𝑁 + 1) + (2 · 𝐾))) = (-(-1↑𝑁) · 1))
163126oveq2d 6858 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑((𝑁 + 1) + (2 · 𝐾))) = (-1↑((𝑁 + (2 · 𝐾)) + 1)))
16411negcld 10633 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -(-1↑𝑁) ∈ ℂ)
165164mulid1d 10311 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · 1) = -(-1↑𝑁))
166162, 163, 1653eqtr3d 2807 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑((𝑁 + (2 · 𝐾)) + 1)) = -(-1↑𝑁))
167166oveq1d 6857 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (-(-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
16861, 67ffvelrnd 6550 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℝ)
169168recnd 10322 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℂ)
17011, 169mulneg1d 10737 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
171148, 167, 1703eqtrd 2803 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
172171oveq2d 6858 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
17310, 168remulcld 10324 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℝ)
174173recnd 10322 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℂ)
17534, 174negsubd 10652 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
176142, 172, 1753eqtrd 2803 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
177176oveq2d 6858 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))))
17811, 34, 174subdid 10740 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))))
179113oveq1d 6857 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (-1↑𝑁)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (1 · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
18011, 11, 169mulassd 10317 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (-1↑𝑁)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
181169mulid2d 10312 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1 · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
182179, 180, 1813eqtr3d 2807 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
183182oveq2d 6858 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
184177, 178, 1833eqtrd 2803 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
185 simp1 1166 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝜑)
1865, 12, 19, 120, 121iseraltlem1 14697 . . . . . . . 8 ((𝜑 ∧ ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍) → 0 ≤ (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
187185, 67, 186syl2anc 579 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 0 ≤ (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
18870, 168subge02d 10873 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (0 ≤ (𝐺‘((𝑁 + (2 · 𝐾)) + 1)) ↔ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))))))
189187, 188mpbid 223 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
190184, 189eqbrtrd 4831 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
19165, 69, 70, 140, 190letrd 10448 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
19260, 64readdcld 10323 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))) ∈ ℝ)
1935, 12, 19, 120, 121, 13iseraltlem2 14698 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
1945, 12, 19, 120, 121iseraltlem1 14697 . . . . . . 7 ((𝜑 ∧ (𝑁 + 1) ∈ 𝑍) → 0 ≤ (𝐺‘(𝑁 + 1)))
195185, 63, 194syl2anc 579 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 0 ≤ (𝐺‘(𝑁 + 1)))
19660, 64addge01d 10869 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (0 ≤ (𝐺‘(𝑁 + 1)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1)))))
197195, 196mpbid 223 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))
19870, 60, 192, 193, 197letrd 10448 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))
19970, 60, 64absdifled 14458 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)) ↔ ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))))
200191, 198, 199mpbir2and 704 . . 3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)))
20159, 200eqbrtrrd 4833 . 2 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)))
20211, 131, 36subdid 10740 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
203202fveq2d 6379 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
20468, 35resubcld 10712 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
205204recnd 10322 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℂ)
20611, 205absmuld 14478 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))))
207203, 206eqtr3d 2801 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))))
20854oveq1d 6857 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (1 · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))))
209205abscld 14460 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℝ)
210209recnd 10322 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℂ)
211210mulid2d 10312 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1 · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))))
212207, 208, 2113eqtrd 2803 . . 3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))))
21369, 70, 192, 190, 198letrd 10448 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))
21469, 60, 64absdifled 14458 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)) ↔ ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))))
215140, 213, 214mpbir2and 704 . . 3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)))
216212, 215eqbrtrrd 4833 . 2 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)))
217201, 216jca 507 1 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055   class class class wbr 4809  wf 6064  cfv 6068  (class class class)co 6842  cc 10187  cr 10188  0cc0 10189  1c1 10190   + caddc 10192   · cmul 10194  cle 10329  cmin 10520  -cneg 10521  2c2 11327  0cn0 11538  cz 11624  cuz 11886  seqcseq 13008  cexp 13067  abscabs 14259  cli 14500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-er 7947  df-pm 8063  df-en 8161  df-dom 8162  df-sdom 8163  df-sup 8555  df-inf 8556  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-n0 11539  df-z 11625  df-uz 11887  df-rp 12029  df-fz 12534  df-fl 12801  df-seq 13009  df-exp 13068  df-cj 14124  df-re 14125  df-im 14126  df-sqrt 14260  df-abs 14261  df-clim 14504  df-rlim 14505
This theorem is referenced by:  iseralt  14700
  Copyright terms: Public domain W3C validator