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

Theorem iseraltlem3 15683
Description: Lemma for iseralt 15684. From iseraltlem2 15682, 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 12374 . . . . . . . . . 10 -1 ∈ ℝ
21a1i 11 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -1 ∈ ℝ)
3 neg1ne0 12375 . . . . . . . . . 10 -1 ≠ 0
43a1i 11 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -1 ≠ 0)
5 iseralt.1 . . . . . . . . . . 11 𝑍 = (ℤ𝑀)
6 uzssz 12890 . . . . . . . . . . 11 (ℤ𝑀) ⊆ ℤ
75, 6eqsstri 4013 . . . . . . . . . 10 𝑍 ⊆ ℤ
8 simp2 1134 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝑁𝑍)
97, 8sselid 3976 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝑁 ∈ ℤ)
102, 4, 9reexpclzd 14261 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑𝑁) ∈ ℝ)
1110recnd 11288 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑𝑁) ∈ ℂ)
12 iseralt.2 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℤ)
13 iseralt.6 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
141a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → -1 ∈ ℝ)
153a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → -1 ≠ 0)
16 simpr 483 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑍) → 𝑘𝑍)
177, 16sselid 3976 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → 𝑘 ∈ ℤ)
1814, 15, 17reexpclzd 14261 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → (-1↑𝑘) ∈ ℝ)
19 iseralt.3 . . . . . . . . . . . . . 14 (𝜑𝐺:𝑍⟶ℝ)
2019ffvelcdmda 7097 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)
2118, 20remulcld 11290 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → ((-1↑𝑘) · (𝐺𝑘)) ∈ ℝ)
2213, 21eqeltrd 2825 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
235, 12, 22serfre 14046 . . . . . . . . . 10 (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
24233ad2ant1 1130 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → seq𝑀( + , 𝐹):𝑍⟶ℝ)
258, 5eleqtrdi 2835 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝑁 ∈ (ℤ𝑀))
26 2nn0 12536 . . . . . . . . . . . 12 2 ∈ ℕ0
27 simp3 1135 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝐾 ∈ ℕ0)
28 nn0mulcl 12555 . . . . . . . . . . . 12 ((2 ∈ ℕ0𝐾 ∈ ℕ0) → (2 · 𝐾) ∈ ℕ0)
2926, 27, 28sylancr 585 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (2 · 𝐾) ∈ ℕ0)
30 uzaddcl 12935 . . . . . . . . . . 11 ((𝑁 ∈ (ℤ𝑀) ∧ (2 · 𝐾) ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈ (ℤ𝑀))
3125, 29, 30syl2anc 582 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈ (ℤ𝑀))
3231, 5eleqtrrdi 2836 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈ 𝑍)
3324, 32ffvelcdmd 7098 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) ∈ ℝ)
3433recnd 11288 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) ∈ ℂ)
3524, 8ffvelcdmd 7098 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℝ)
3635recnd 11288 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℂ)
3711, 34, 36subdid 11716 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
3837fveq2d 6904 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
3933, 35resubcld 11688 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
4039recnd 11288 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℂ)
4111, 40absmuld 15454 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))))
4238, 41eqtr3d 2767 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))))
432recnd 11288 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -1 ∈ ℂ)
44 absexpz 15305 . . . . . . 7 ((-1 ∈ ℂ ∧ -1 ≠ 0 ∧ 𝑁 ∈ ℤ) → (abs‘(-1↑𝑁)) = ((abs‘-1)↑𝑁))
4543, 4, 9, 44syl3anc 1368 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(-1↑𝑁)) = ((abs‘-1)↑𝑁))
46 ax-1cn 11212 . . . . . . . . . 10 1 ∈ ℂ
4746absnegi 15400 . . . . . . . . 9 (abs‘-1) = (abs‘1)
48 abs1 15297 . . . . . . . . 9 (abs‘1) = 1
4947, 48eqtri 2753 . . . . . . . 8 (abs‘-1) = 1
5049oveq1i 7433 . . . . . . 7 ((abs‘-1)↑𝑁) = (1↑𝑁)
51 1exp 14106 . . . . . . . 8 (𝑁 ∈ ℤ → (1↑𝑁) = 1)
529, 51syl 17 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1↑𝑁) = 1)
5350, 52eqtrid 2777 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘-1)↑𝑁) = 1)
5445, 53eqtrd 2765 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(-1↑𝑁)) = 1)
5554oveq1d 7438 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (1 · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))))
5640abscld 15436 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℝ)
5756recnd 11288 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℂ)
5857mullidd 11278 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1 · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))))
5942, 55, 583eqtrd 2769 . . 3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))))
6010, 35remulcld 11290 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
61193ad2ant1 1130 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝐺:𝑍⟶ℝ)
625peano2uzs 12933 . . . . . . . 8 (𝑁𝑍 → (𝑁 + 1) ∈ 𝑍)
63623ad2ant2 1131 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝑁 + 1) ∈ 𝑍)
6461, 63ffvelcdmd 7098 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐺‘(𝑁 + 1)) ∈ ℝ)
6560, 64resubcld 11688 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ∈ ℝ)
665peano2uzs 12933 . . . . . . . 8 ((𝑁 + (2 · 𝐾)) ∈ 𝑍 → ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍)
6732, 66syl 17 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍)
6824, 67ffvelcdmd 7098 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℝ)
6910, 68remulcld 11290 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℝ)
7010, 33remulcld 11290 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ∈ ℝ)
71 seqp1 14031 . . . . . . . . . . 11 (𝑁 ∈ (ℤ𝑀) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1))))
7225, 71syl 17 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1))))
73 fveq2 6900 . . . . . . . . . . . . 13 (𝑘 = (𝑁 + 1) → (𝐹𝑘) = (𝐹‘(𝑁 + 1)))
74 oveq2 7431 . . . . . . . . . . . . . 14 (𝑘 = (𝑁 + 1) → (-1↑𝑘) = (-1↑(𝑁 + 1)))
75 fveq2 6900 . . . . . . . . . . . . . 14 (𝑘 = (𝑁 + 1) → (𝐺𝑘) = (𝐺‘(𝑁 + 1)))
7674, 75oveq12d 7441 . . . . . . . . . . . . 13 (𝑘 = (𝑁 + 1) → ((-1↑𝑘) · (𝐺𝑘)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))))
7773, 76eqeq12d 2741 . . . . . . . . . . . 12 (𝑘 = (𝑁 + 1) → ((𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) ↔ (𝐹‘(𝑁 + 1)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))))
7813ralrimiva 3135 . . . . . . . . . . . . 13 (𝜑 → ∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
79783ad2ant1 1130 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
8077, 79, 63rspcdva 3608 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐹‘(𝑁 + 1)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))))
8180oveq2d 7439 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1))) = ((seq𝑀( + , 𝐹)‘𝑁) + ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))))
8243, 4, 9expp1zd 14169 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 1)) = ((-1↑𝑁) · -1))
83 neg1cn 12373 . . . . . . . . . . . . . . 15 -1 ∈ ℂ
84 mulcom 11240 . . . . . . . . . . . . . . 15 (((-1↑𝑁) ∈ ℂ ∧ -1 ∈ ℂ) → ((-1↑𝑁) · -1) = (-1 · (-1↑𝑁)))
8511, 83, 84sylancl 584 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · -1) = (-1 · (-1↑𝑁)))
8611mulm1d 11712 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1 · (-1↑𝑁)) = -(-1↑𝑁))
8782, 85, 863eqtrd 2769 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 1)) = -(-1↑𝑁))
8887oveq1d 7438 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))) = (-(-1↑𝑁) · (𝐺‘(𝑁 + 1))))
8964recnd 11288 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐺‘(𝑁 + 1)) ∈ ℂ)
9011, 89mulneg1d 11713 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (𝐺‘(𝑁 + 1))) = -((-1↑𝑁) · (𝐺‘(𝑁 + 1))))
9188, 90eqtrd 2765 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))) = -((-1↑𝑁) · (𝐺‘(𝑁 + 1))))
9291oveq2d 7439 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘𝑁) + ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))) = ((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
9372, 81, 923eqtrd 2769 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
9410, 64remulcld 11290 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (𝐺‘(𝑁 + 1))) ∈ ℝ)
9594recnd 11288 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (𝐺‘(𝑁 + 1))) ∈ ℂ)
9636, 95negsubd 11623 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))) = ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
9793, 96eqtrd 2765 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
9897oveq2d 7439 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))))
9911, 36, 95subdid 11716 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))))
1009zcnd 12714 . . . . . . . . . . . . . . 15 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝑁 ∈ ℂ)
1011002timesd 12502 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (2 · 𝑁) = (𝑁 + 𝑁))
102101oveq2d 7439 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(2 · 𝑁)) = (-1↑(𝑁 + 𝑁)))
103 2z 12641 . . . . . . . . . . . . . . 15 2 ∈ ℤ
104103a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 2 ∈ ℤ)
105 expmulz 14123 . . . . . . . . . . . . . 14 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (-1↑(2 · 𝑁)) = ((-1↑2)↑𝑁))
10643, 4, 104, 9, 105syl22anc 837 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(2 · 𝑁)) = ((-1↑2)↑𝑁))
107102, 106eqtr3d 2767 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 𝑁)) = ((-1↑2)↑𝑁))
108 neg1sqe1 14209 . . . . . . . . . . . . 13 (-1↑2) = 1
109108oveq1i 7433 . . . . . . . . . . . 12 ((-1↑2)↑𝑁) = (1↑𝑁)
110107, 109eqtrdi 2781 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 𝑁)) = (1↑𝑁))
111 expaddz 14121 . . . . . . . . . . . 12 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (-1↑(𝑁 + 𝑁)) = ((-1↑𝑁) · (-1↑𝑁)))
11243, 4, 9, 9, 111syl22anc 837 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 𝑁)) = ((-1↑𝑁) · (-1↑𝑁)))
113110, 112, 523eqtr3d 2773 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (-1↑𝑁)) = 1)
114113oveq1d 7438 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (-1↑𝑁)) · (𝐺‘(𝑁 + 1))) = (1 · (𝐺‘(𝑁 + 1))))
11511, 11, 89mulassd 11283 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (-1↑𝑁)) · (𝐺‘(𝑁 + 1))) = ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
11689mullidd 11278 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1 · (𝐺‘(𝑁 + 1))) = (𝐺‘(𝑁 + 1)))
117114, 115, 1163eqtr3d 2773 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))) = (𝐺‘(𝑁 + 1)))
118117oveq2d 7439 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))))
11998, 99, 1183eqtrd 2769 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))))
120 iseralt.4 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
121 iseralt.5 . . . . . . . . . . 11 (𝜑𝐺 ⇝ 0)
1225, 12, 19, 120, 121, 13iseraltlem2 15682 . . . . . . . . . 10 ((𝜑 ∧ (𝑁 + 1) ∈ 𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾)))) ≤ ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
12362, 122syl3an2 1161 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾)))) ≤ ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
124 1cnd 11255 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 1 ∈ ℂ)
12529nn0cnd 12581 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (2 · 𝐾) ∈ ℂ)
126100, 124, 125add32d 11487 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((𝑁 + 1) + (2 · 𝐾)) = ((𝑁 + (2 · 𝐾)) + 1))
127126fveq2d 6904 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾))) = (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)))
12887, 127oveq12d 7441 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾)))) = (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))))
12987oveq1d 7438 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) = (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
130123, 128, 1293brtr3d 5183 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
13168recnd 11288 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℂ)
13211, 131mulneg1d 11713 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))))
13324, 63ffvelcdmd 7098 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) ∈ ℝ)
134133recnd 11288 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) ∈ ℂ)
13511, 134mulneg1d 11713 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) = -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
136130, 132, 1353brtr3d 5183 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
13710, 133remulcld 11290 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) ∈ ℝ)
138137, 69lenegd 11839 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ↔ -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1)))))
139136, 138mpbird 256 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))))
140119, 139eqbrtrrd 5176 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))))
141 seqp1 14031 . . . . . . . . . 10 ((𝑁 + (2 · 𝐾)) ∈ (ℤ𝑀) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1))))
14231, 141syl 17 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1))))
143 fveq2 6900 . . . . . . . . . . . . 13 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (𝐹𝑘) = (𝐹‘((𝑁 + (2 · 𝐾)) + 1)))
144 oveq2 7431 . . . . . . . . . . . . . 14 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (-1↑𝑘) = (-1↑((𝑁 + (2 · 𝐾)) + 1)))
145 fveq2 6900 . . . . . . . . . . . . . 14 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (𝐺𝑘) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
146144, 145oveq12d 7441 . . . . . . . . . . . . 13 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → ((-1↑𝑘) · (𝐺𝑘)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
147143, 146eqeq12d 2741 . . . . . . . . . . . 12 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → ((𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) ↔ (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
148147, 79, 67rspcdva 3608 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
1497, 63sselid 3976 . . . . . . . . . . . . . . 15 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝑁 + 1) ∈ ℤ)
15029nn0zd 12631 . . . . . . . . . . . . . . 15 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (2 · 𝐾) ∈ ℤ)
151 expaddz 14121 . . . . . . . . . . . . . . 15 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ ((𝑁 + 1) ∈ ℤ ∧ (2 · 𝐾) ∈ ℤ)) → (-1↑((𝑁 + 1) + (2 · 𝐾))) = ((-1↑(𝑁 + 1)) · (-1↑(2 · 𝐾))))
15243, 4, 149, 150, 151syl22anc 837 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑((𝑁 + 1) + (2 · 𝐾))) = ((-1↑(𝑁 + 1)) · (-1↑(2 · 𝐾))))
15327nn0zd 12631 . . . . . . . . . . . . . . . . 17 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝐾 ∈ ℤ)
154 expmulz 14123 . . . . . . . . . . . . . . . . 17 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (-1↑(2 · 𝐾)) = ((-1↑2)↑𝐾))
15543, 4, 104, 153, 154syl22anc 837 . . . . . . . . . . . . . . . 16 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(2 · 𝐾)) = ((-1↑2)↑𝐾))
156108oveq1i 7433 . . . . . . . . . . . . . . . . 17 ((-1↑2)↑𝐾) = (1↑𝐾)
157 1exp 14106 . . . . . . . . . . . . . . . . . 18 (𝐾 ∈ ℤ → (1↑𝐾) = 1)
158153, 157syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1↑𝐾) = 1)
159156, 158eqtrid 2777 . . . . . . . . . . . . . . . 16 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑2)↑𝐾) = 1)
160155, 159eqtrd 2765 . . . . . . . . . . . . . . 15 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(2 · 𝐾)) = 1)
16187, 160oveq12d 7441 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (-1↑(2 · 𝐾))) = (-(-1↑𝑁) · 1))
162152, 161eqtrd 2765 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑((𝑁 + 1) + (2 · 𝐾))) = (-(-1↑𝑁) · 1))
163126oveq2d 7439 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑((𝑁 + 1) + (2 · 𝐾))) = (-1↑((𝑁 + (2 · 𝐾)) + 1)))
16411negcld 11604 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -(-1↑𝑁) ∈ ℂ)
165164mulridd 11277 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · 1) = -(-1↑𝑁))
166162, 163, 1653eqtr3d 2773 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑((𝑁 + (2 · 𝐾)) + 1)) = -(-1↑𝑁))
167166oveq1d 7438 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (-(-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
16861, 67ffvelcdmd 7098 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℝ)
169168recnd 11288 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℂ)
17011, 169mulneg1d 11713 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
171148, 167, 1703eqtrd 2769 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
172171oveq2d 7439 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
17310, 168remulcld 11290 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℝ)
174173recnd 11288 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℂ)
17534, 174negsubd 11623 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
176142, 172, 1753eqtrd 2769 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
177176oveq2d 7439 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))))
17811, 34, 174subdid 11716 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))))
179113oveq1d 7438 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (-1↑𝑁)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (1 · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
18011, 11, 169mulassd 11283 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (-1↑𝑁)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
181169mullidd 11278 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1 · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
182179, 180, 1813eqtr3d 2773 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
183182oveq2d 7439 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
184177, 178, 1833eqtrd 2769 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
185 simp1 1133 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝜑)
1865, 12, 19, 120, 121iseraltlem1 15681 . . . . . . . 8 ((𝜑 ∧ ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍) → 0 ≤ (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
187185, 67, 186syl2anc 582 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 0 ≤ (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
18870, 168subge02d 11852 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (0 ≤ (𝐺‘((𝑁 + (2 · 𝐾)) + 1)) ↔ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))))))
189187, 188mpbid 231 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
190184, 189eqbrtrd 5174 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
19165, 69, 70, 140, 190letrd 11417 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
19260, 64readdcld 11289 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))) ∈ ℝ)
1935, 12, 19, 120, 121, 13iseraltlem2 15682 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
1945, 12, 19, 120, 121iseraltlem1 15681 . . . . . . 7 ((𝜑 ∧ (𝑁 + 1) ∈ 𝑍) → 0 ≤ (𝐺‘(𝑁 + 1)))
195185, 63, 194syl2anc 582 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 0 ≤ (𝐺‘(𝑁 + 1)))
19660, 64addge01d 11848 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (0 ≤ (𝐺‘(𝑁 + 1)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1)))))
197195, 196mpbid 231 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))
19870, 60, 192, 193, 197letrd 11417 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))
19970, 60, 64absdifled 15434 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)) ↔ ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))))
200191, 198, 199mpbir2and 711 . . 3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)))
20159, 200eqbrtrrd 5176 . 2 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)))
20211, 131, 36subdid 11716 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
203202fveq2d 6904 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
20468, 35resubcld 11688 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
205204recnd 11288 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℂ)
20611, 205absmuld 15454 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))))
207203, 206eqtr3d 2767 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))))
20854oveq1d 7438 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (1 · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))))
209205abscld 15436 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℝ)
210209recnd 11288 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℂ)
211210mullidd 11278 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1 · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))))
212207, 208, 2113eqtrd 2769 . . 3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))))
21369, 70, 192, 190, 198letrd 11417 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))
21469, 60, 64absdifled 15434 . . . 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 711 . . 3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)))
216212, 215eqbrtrrd 5176 . 2 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)))
217201, 216jca 510 1 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084   = wceq 1533  wcel 2098  wne 2929  wral 3050   class class class wbr 5152  wf 6549  cfv 6553  (class class class)co 7423  cc 11152  cr 11153  0cc0 11154  1c1 11155   + caddc 11157   · cmul 11159  cle 11295  cmin 11490  -cneg 11491  2c2 12314  0cn0 12519  cz 12605  cuz 12869  seqcseq 14016  cexp 14076  abscabs 15234  cli 15481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5368  ax-pr 5432  ax-un 7745  ax-cnex 11210  ax-resscn 11211  ax-1cn 11212  ax-icn 11213  ax-addcl 11214  ax-addrcl 11215  ax-mulcl 11216  ax-mulrcl 11217  ax-mulcom 11218  ax-addass 11219  ax-mulass 11220  ax-distr 11221  ax-i2m1 11222  ax-1ne0 11223  ax-1rid 11224  ax-rnegex 11225  ax-rrecex 11226  ax-cnre 11227  ax-pre-lttri 11228  ax-pre-lttrn 11229  ax-pre-ltadd 11230  ax-pre-mulgt0 11231  ax-pre-sup 11232
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5579  df-eprel 5585  df-po 5593  df-so 5594  df-fr 5636  df-we 5638  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-pred 6311  df-ord 6378  df-on 6379  df-lim 6380  df-suc 6381  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7379  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7876  df-1st 8002  df-2nd 8003  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-er 8733  df-pm 8857  df-en 8974  df-dom 8975  df-sdom 8976  df-sup 9481  df-inf 9482  df-pnf 11296  df-mnf 11297  df-xr 11298  df-ltxr 11299  df-le 11300  df-sub 11492  df-neg 11493  df-div 11918  df-nn 12260  df-2 12322  df-3 12323  df-n0 12520  df-z 12606  df-uz 12870  df-rp 13024  df-fz 13534  df-fl 13807  df-seq 14017  df-exp 14077  df-cj 15099  df-re 15100  df-im 15101  df-sqrt 15235  df-abs 15236  df-clim 15485  df-rlim 15486
This theorem is referenced by:  iseralt  15684
  Copyright terms: Public domain W3C validator