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

Theorem iseraltlem3 15036
Description: Lemma for iseralt 15037. From iseraltlem2 15035, 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 11744 . . . . . . . . . 10 -1 ∈ ℝ
21a1i 11 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -1 ∈ ℝ)
3 neg1ne0 11745 . . . . . . . . . 10 -1 ≠ 0
43a1i 11 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -1 ≠ 0)
5 iseralt.1 . . . . . . . . . . 11 𝑍 = (ℤ𝑀)
6 uzssz 12256 . . . . . . . . . . 11 (ℤ𝑀) ⊆ ℤ
75, 6eqsstri 3952 . . . . . . . . . 10 𝑍 ⊆ ℤ
8 simp2 1134 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝑁𝑍)
97, 8sseldi 3916 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝑁 ∈ ℤ)
102, 4, 9reexpclzd 13610 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑𝑁) ∈ ℝ)
1110recnd 10662 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑𝑁) ∈ ℂ)
12 iseralt.2 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℤ)
13 iseralt.6 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
141a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → -1 ∈ ℝ)
153a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → -1 ≠ 0)
16 simpr 488 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑍) → 𝑘𝑍)
177, 16sseldi 3916 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → 𝑘 ∈ ℤ)
1814, 15, 17reexpclzd 13610 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → (-1↑𝑘) ∈ ℝ)
19 iseralt.3 . . . . . . . . . . . . . 14 (𝜑𝐺:𝑍⟶ℝ)
2019ffvelrnda 6832 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)
2118, 20remulcld 10664 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → ((-1↑𝑘) · (𝐺𝑘)) ∈ ℝ)
2213, 21eqeltrd 2893 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
235, 12, 22serfre 13399 . . . . . . . . . 10 (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
24233ad2ant1 1130 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → seq𝑀( + , 𝐹):𝑍⟶ℝ)
258, 5eleqtrdi 2903 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝑁 ∈ (ℤ𝑀))
26 2nn0 11906 . . . . . . . . . . . 12 2 ∈ ℕ0
27 simp3 1135 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝐾 ∈ ℕ0)
28 nn0mulcl 11925 . . . . . . . . . . . 12 ((2 ∈ ℕ0𝐾 ∈ ℕ0) → (2 · 𝐾) ∈ ℕ0)
2926, 27, 28sylancr 590 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (2 · 𝐾) ∈ ℕ0)
30 uzaddcl 12296 . . . . . . . . . . 11 ((𝑁 ∈ (ℤ𝑀) ∧ (2 · 𝐾) ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈ (ℤ𝑀))
3125, 29, 30syl2anc 587 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈ (ℤ𝑀))
3231, 5eleqtrrdi 2904 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈ 𝑍)
3324, 32ffvelrnd 6833 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) ∈ ℝ)
3433recnd 10662 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) ∈ ℂ)
3524, 8ffvelrnd 6833 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℝ)
3635recnd 10662 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℂ)
3711, 34, 36subdid 11089 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
3837fveq2d 6653 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
3933, 35resubcld 11061 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
4039recnd 10662 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℂ)
4111, 40absmuld 14810 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))))
4238, 41eqtr3d 2838 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))))
432recnd 10662 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -1 ∈ ℂ)
44 absexpz 14661 . . . . . . 7 ((-1 ∈ ℂ ∧ -1 ≠ 0 ∧ 𝑁 ∈ ℤ) → (abs‘(-1↑𝑁)) = ((abs‘-1)↑𝑁))
4543, 4, 9, 44syl3anc 1368 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(-1↑𝑁)) = ((abs‘-1)↑𝑁))
46 ax-1cn 10588 . . . . . . . . . 10 1 ∈ ℂ
4746absnegi 14756 . . . . . . . . 9 (abs‘-1) = (abs‘1)
48 abs1 14653 . . . . . . . . 9 (abs‘1) = 1
4947, 48eqtri 2824 . . . . . . . 8 (abs‘-1) = 1
5049oveq1i 7149 . . . . . . 7 ((abs‘-1)↑𝑁) = (1↑𝑁)
51 1exp 13458 . . . . . . . 8 (𝑁 ∈ ℤ → (1↑𝑁) = 1)
529, 51syl 17 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1↑𝑁) = 1)
5350, 52syl5eq 2848 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘-1)↑𝑁) = 1)
5445, 53eqtrd 2836 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(-1↑𝑁)) = 1)
5554oveq1d 7154 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (1 · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))))
5640abscld 14792 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℝ)
5756recnd 10662 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℂ)
5857mulid2d 10652 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1 · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))))
5942, 55, 583eqtrd 2840 . . 3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))))
6010, 35remulcld 10664 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
61193ad2ant1 1130 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝐺:𝑍⟶ℝ)
625peano2uzs 12294 . . . . . . . 8 (𝑁𝑍 → (𝑁 + 1) ∈ 𝑍)
63623ad2ant2 1131 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝑁 + 1) ∈ 𝑍)
6461, 63ffvelrnd 6833 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐺‘(𝑁 + 1)) ∈ ℝ)
6560, 64resubcld 11061 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ∈ ℝ)
665peano2uzs 12294 . . . . . . . 8 ((𝑁 + (2 · 𝐾)) ∈ 𝑍 → ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍)
6732, 66syl 17 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍)
6824, 67ffvelrnd 6833 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℝ)
6910, 68remulcld 10664 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℝ)
7010, 33remulcld 10664 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ∈ ℝ)
71 seqp1 13383 . . . . . . . . . . 11 (𝑁 ∈ (ℤ𝑀) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1))))
7225, 71syl 17 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1))))
73 fveq2 6649 . . . . . . . . . . . . 13 (𝑘 = (𝑁 + 1) → (𝐹𝑘) = (𝐹‘(𝑁 + 1)))
74 oveq2 7147 . . . . . . . . . . . . . 14 (𝑘 = (𝑁 + 1) → (-1↑𝑘) = (-1↑(𝑁 + 1)))
75 fveq2 6649 . . . . . . . . . . . . . 14 (𝑘 = (𝑁 + 1) → (𝐺𝑘) = (𝐺‘(𝑁 + 1)))
7674, 75oveq12d 7157 . . . . . . . . . . . . 13 (𝑘 = (𝑁 + 1) → ((-1↑𝑘) · (𝐺𝑘)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))))
7773, 76eqeq12d 2817 . . . . . . . . . . . 12 (𝑘 = (𝑁 + 1) → ((𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) ↔ (𝐹‘(𝑁 + 1)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))))
7813ralrimiva 3152 . . . . . . . . . . . . 13 (𝜑 → ∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
79783ad2ant1 1130 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
8077, 79, 63rspcdva 3576 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐹‘(𝑁 + 1)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))))
8180oveq2d 7155 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1))) = ((seq𝑀( + , 𝐹)‘𝑁) + ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))))
8243, 4, 9expp1zd 13519 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 1)) = ((-1↑𝑁) · -1))
83 neg1cn 11743 . . . . . . . . . . . . . . 15 -1 ∈ ℂ
84 mulcom 10616 . . . . . . . . . . . . . . 15 (((-1↑𝑁) ∈ ℂ ∧ -1 ∈ ℂ) → ((-1↑𝑁) · -1) = (-1 · (-1↑𝑁)))
8511, 83, 84sylancl 589 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · -1) = (-1 · (-1↑𝑁)))
8611mulm1d 11085 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1 · (-1↑𝑁)) = -(-1↑𝑁))
8782, 85, 863eqtrd 2840 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 1)) = -(-1↑𝑁))
8887oveq1d 7154 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))) = (-(-1↑𝑁) · (𝐺‘(𝑁 + 1))))
8964recnd 10662 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐺‘(𝑁 + 1)) ∈ ℂ)
9011, 89mulneg1d 11086 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (𝐺‘(𝑁 + 1))) = -((-1↑𝑁) · (𝐺‘(𝑁 + 1))))
9188, 90eqtrd 2836 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))) = -((-1↑𝑁) · (𝐺‘(𝑁 + 1))))
9291oveq2d 7155 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘𝑁) + ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))) = ((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
9372, 81, 923eqtrd 2840 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
9410, 64remulcld 10664 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (𝐺‘(𝑁 + 1))) ∈ ℝ)
9594recnd 10662 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (𝐺‘(𝑁 + 1))) ∈ ℂ)
9636, 95negsubd 10996 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))) = ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
9793, 96eqtrd 2836 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
9897oveq2d 7155 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))))
9911, 36, 95subdid 11089 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))))
1009zcnd 12080 . . . . . . . . . . . . . . 15 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝑁 ∈ ℂ)
1011002timesd 11872 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (2 · 𝑁) = (𝑁 + 𝑁))
102101oveq2d 7155 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(2 · 𝑁)) = (-1↑(𝑁 + 𝑁)))
103 2z 12006 . . . . . . . . . . . . . . 15 2 ∈ ℤ
104103a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 2 ∈ ℤ)
105 expmulz 13475 . . . . . . . . . . . . . 14 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (-1↑(2 · 𝑁)) = ((-1↑2)↑𝑁))
10643, 4, 104, 9, 105syl22anc 837 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(2 · 𝑁)) = ((-1↑2)↑𝑁))
107102, 106eqtr3d 2838 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 𝑁)) = ((-1↑2)↑𝑁))
108 neg1sqe1 13559 . . . . . . . . . . . . 13 (-1↑2) = 1
109108oveq1i 7149 . . . . . . . . . . . 12 ((-1↑2)↑𝑁) = (1↑𝑁)
110107, 109eqtrdi 2852 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 𝑁)) = (1↑𝑁))
111 expaddz 13473 . . . . . . . . . . . 12 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (-1↑(𝑁 + 𝑁)) = ((-1↑𝑁) · (-1↑𝑁)))
11243, 4, 9, 9, 111syl22anc 837 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 𝑁)) = ((-1↑𝑁) · (-1↑𝑁)))
113110, 112, 523eqtr3d 2844 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (-1↑𝑁)) = 1)
114113oveq1d 7154 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (-1↑𝑁)) · (𝐺‘(𝑁 + 1))) = (1 · (𝐺‘(𝑁 + 1))))
11511, 11, 89mulassd 10657 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (-1↑𝑁)) · (𝐺‘(𝑁 + 1))) = ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
11689mulid2d 10652 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1 · (𝐺‘(𝑁 + 1))) = (𝐺‘(𝑁 + 1)))
117114, 115, 1163eqtr3d 2844 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))) = (𝐺‘(𝑁 + 1)))
118117oveq2d 7155 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))))
11998, 99, 1183eqtrd 2840 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))))
120 iseralt.4 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
121 iseralt.5 . . . . . . . . . . 11 (𝜑𝐺 ⇝ 0)
1225, 12, 19, 120, 121, 13iseraltlem2 15035 . . . . . . . . . 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 10629 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 1 ∈ ℂ)
12529nn0cnd 11949 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (2 · 𝐾) ∈ ℂ)
126100, 124, 125add32d 10860 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((𝑁 + 1) + (2 · 𝐾)) = ((𝑁 + (2 · 𝐾)) + 1))
127126fveq2d 6653 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾))) = (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)))
12887, 127oveq12d 7157 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾)))) = (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))))
12987oveq1d 7154 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) = (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
130123, 128, 1293brtr3d 5064 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
13168recnd 10662 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℂ)
13211, 131mulneg1d 11086 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))))
13324, 63ffvelrnd 6833 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) ∈ ℝ)
134133recnd 10662 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) ∈ ℂ)
13511, 134mulneg1d 11086 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) = -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
136130, 132, 1353brtr3d 5064 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
13710, 133remulcld 10664 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) ∈ ℝ)
138137, 69lenegd 11212 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ↔ -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1)))))
139136, 138mpbird 260 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))))
140119, 139eqbrtrrd 5057 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))))
141 seqp1 13383 . . . . . . . . . 10 ((𝑁 + (2 · 𝐾)) ∈ (ℤ𝑀) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1))))
14231, 141syl 17 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1))))
143 fveq2 6649 . . . . . . . . . . . . 13 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (𝐹𝑘) = (𝐹‘((𝑁 + (2 · 𝐾)) + 1)))
144 oveq2 7147 . . . . . . . . . . . . . 14 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (-1↑𝑘) = (-1↑((𝑁 + (2 · 𝐾)) + 1)))
145 fveq2 6649 . . . . . . . . . . . . . 14 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (𝐺𝑘) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
146144, 145oveq12d 7157 . . . . . . . . . . . . 13 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → ((-1↑𝑘) · (𝐺𝑘)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
147143, 146eqeq12d 2817 . . . . . . . . . . . 12 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → ((𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) ↔ (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
148147, 79, 67rspcdva 3576 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
1497, 63sseldi 3916 . . . . . . . . . . . . . . 15 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝑁 + 1) ∈ ℤ)
15029nn0zd 12077 . . . . . . . . . . . . . . 15 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (2 · 𝐾) ∈ ℤ)
151 expaddz 13473 . . . . . . . . . . . . . . 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 12077 . . . . . . . . . . . . . . . . 17 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝐾 ∈ ℤ)
154 expmulz 13475 . . . . . . . . . . . . . . . . 17 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (-1↑(2 · 𝐾)) = ((-1↑2)↑𝐾))
15543, 4, 104, 153, 154syl22anc 837 . . . . . . . . . . . . . . . 16 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(2 · 𝐾)) = ((-1↑2)↑𝐾))
156108oveq1i 7149 . . . . . . . . . . . . . . . . 17 ((-1↑2)↑𝐾) = (1↑𝐾)
157 1exp 13458 . . . . . . . . . . . . . . . . . 18 (𝐾 ∈ ℤ → (1↑𝐾) = 1)
158153, 157syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1↑𝐾) = 1)
159156, 158syl5eq 2848 . . . . . . . . . . . . . . . 16 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑2)↑𝐾) = 1)
160155, 159eqtrd 2836 . . . . . . . . . . . . . . 15 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(2 · 𝐾)) = 1)
16187, 160oveq12d 7157 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (-1↑(2 · 𝐾))) = (-(-1↑𝑁) · 1))
162152, 161eqtrd 2836 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑((𝑁 + 1) + (2 · 𝐾))) = (-(-1↑𝑁) · 1))
163126oveq2d 7155 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑((𝑁 + 1) + (2 · 𝐾))) = (-1↑((𝑁 + (2 · 𝐾)) + 1)))
16411negcld 10977 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -(-1↑𝑁) ∈ ℂ)
165164mulid1d 10651 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · 1) = -(-1↑𝑁))
166162, 163, 1653eqtr3d 2844 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑((𝑁 + (2 · 𝐾)) + 1)) = -(-1↑𝑁))
167166oveq1d 7154 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (-(-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
16861, 67ffvelrnd 6833 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℝ)
169168recnd 10662 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℂ)
17011, 169mulneg1d 11086 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
171148, 167, 1703eqtrd 2840 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
172171oveq2d 7155 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
17310, 168remulcld 10664 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℝ)
174173recnd 10662 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℂ)
17534, 174negsubd 10996 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
176142, 172, 1753eqtrd 2840 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
177176oveq2d 7155 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))))
17811, 34, 174subdid 11089 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))))
179113oveq1d 7154 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (-1↑𝑁)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (1 · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
18011, 11, 169mulassd 10657 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (-1↑𝑁)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
181169mulid2d 10652 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1 · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
182179, 180, 1813eqtr3d 2844 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
183182oveq2d 7155 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
184177, 178, 1833eqtrd 2840 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
185 simp1 1133 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝜑)
1865, 12, 19, 120, 121iseraltlem1 15034 . . . . . . . 8 ((𝜑 ∧ ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍) → 0 ≤ (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
187185, 67, 186syl2anc 587 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 0 ≤ (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
18870, 168subge02d 11225 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (0 ≤ (𝐺‘((𝑁 + (2 · 𝐾)) + 1)) ↔ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))))))
189187, 188mpbid 235 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
190184, 189eqbrtrd 5055 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
19165, 69, 70, 140, 190letrd 10790 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
19260, 64readdcld 10663 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))) ∈ ℝ)
1935, 12, 19, 120, 121, 13iseraltlem2 15035 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
1945, 12, 19, 120, 121iseraltlem1 15034 . . . . . . 7 ((𝜑 ∧ (𝑁 + 1) ∈ 𝑍) → 0 ≤ (𝐺‘(𝑁 + 1)))
195185, 63, 194syl2anc 587 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 0 ≤ (𝐺‘(𝑁 + 1)))
19660, 64addge01d 11221 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (0 ≤ (𝐺‘(𝑁 + 1)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1)))))
197195, 196mpbid 235 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))
19870, 60, 192, 193, 197letrd 10790 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))
19970, 60, 64absdifled 14790 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)) ↔ ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))))
200191, 198, 199mpbir2and 712 . . 3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)))
20159, 200eqbrtrrd 5057 . 2 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)))
20211, 131, 36subdid 11089 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
203202fveq2d 6653 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
20468, 35resubcld 11061 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
205204recnd 10662 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℂ)
20611, 205absmuld 14810 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))))
207203, 206eqtr3d 2838 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))))
20854oveq1d 7154 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (1 · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))))
209205abscld 14792 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℝ)
210209recnd 10662 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℂ)
211210mulid2d 10652 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1 · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))))
212207, 208, 2113eqtrd 2840 . . 3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))))
21369, 70, 192, 190, 198letrd 10790 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))
21469, 60, 64absdifled 14790 . . . 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 712 . . 3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)))
216212, 215eqbrtrrd 5057 . 2 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)))
217201, 216jca 515 1 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084   = wceq 1538  wcel 2112  wne 2990  wral 3109   class class class wbr 5033  wf 6324  cfv 6328  (class class class)co 7139  cc 10528  cr 10529  0cc0 10530  1c1 10531   + caddc 10533   · cmul 10535  cle 10669  cmin 10863  -cneg 10864  2c2 11684  0cn0 11889  cz 11973  cuz 12235  seqcseq 13368  cexp 13429  abscabs 14589  cli 14837
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-er 8276  df-pm 8396  df-en 8497  df-dom 8498  df-sdom 8499  df-sup 8894  df-inf 8895  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-n0 11890  df-z 11974  df-uz 12236  df-rp 12382  df-fz 12890  df-fl 13161  df-seq 13369  df-exp 13430  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-clim 14841  df-rlim 14842
This theorem is referenced by:  iseralt  15037
  Copyright terms: Public domain W3C validator