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

Theorem iseraltlem3 15486
Description: Lemma for iseralt 15487. From iseraltlem2 15485, 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 12181 . . . . . . . . . 10 -1 ∈ ℝ
21a1i 11 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -1 ∈ ℝ)
3 neg1ne0 12182 . . . . . . . . . 10 -1 ≠ 0
43a1i 11 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -1 ≠ 0)
5 iseralt.1 . . . . . . . . . . 11 𝑍 = (ℤ𝑀)
6 uzssz 12696 . . . . . . . . . . 11 (ℤ𝑀) ⊆ ℤ
75, 6eqsstri 3965 . . . . . . . . . 10 𝑍 ⊆ ℤ
8 simp2 1136 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝑁𝑍)
97, 8sselid 3929 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝑁 ∈ ℤ)
102, 4, 9reexpclzd 14057 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑𝑁) ∈ ℝ)
1110recnd 11096 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑𝑁) ∈ ℂ)
12 iseralt.2 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℤ)
13 iseralt.6 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
141a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → -1 ∈ ℝ)
153a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → -1 ≠ 0)
16 simpr 485 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑍) → 𝑘𝑍)
177, 16sselid 3929 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑍) → 𝑘 ∈ ℤ)
1814, 15, 17reexpclzd 14057 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → (-1↑𝑘) ∈ ℝ)
19 iseralt.3 . . . . . . . . . . . . . 14 (𝜑𝐺:𝑍⟶ℝ)
2019ffvelcdmda 7011 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ ℝ)
2118, 20remulcld 11098 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → ((-1↑𝑘) · (𝐺𝑘)) ∈ ℝ)
2213, 21eqeltrd 2837 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℝ)
235, 12, 22serfre 13845 . . . . . . . . . 10 (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ)
24233ad2ant1 1132 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → seq𝑀( + , 𝐹):𝑍⟶ℝ)
258, 5eleqtrdi 2847 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝑁 ∈ (ℤ𝑀))
26 2nn0 12343 . . . . . . . . . . . 12 2 ∈ ℕ0
27 simp3 1137 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝐾 ∈ ℕ0)
28 nn0mulcl 12362 . . . . . . . . . . . 12 ((2 ∈ ℕ0𝐾 ∈ ℕ0) → (2 · 𝐾) ∈ ℕ0)
2926, 27, 28sylancr 587 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (2 · 𝐾) ∈ ℕ0)
30 uzaddcl 12737 . . . . . . . . . . 11 ((𝑁 ∈ (ℤ𝑀) ∧ (2 · 𝐾) ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈ (ℤ𝑀))
3125, 29, 30syl2anc 584 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈ (ℤ𝑀))
3231, 5eleqtrrdi 2848 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈ 𝑍)
3324, 32ffvelcdmd 7012 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) ∈ ℝ)
3433recnd 11096 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) ∈ ℂ)
3524, 8ffvelcdmd 7012 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℝ)
3635recnd 11096 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘𝑁) ∈ ℂ)
3711, 34, 36subdid 11524 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
3837fveq2d 6823 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
3933, 35resubcld 11496 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
4039recnd 11096 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℂ)
4111, 40absmuld 15257 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))))
4238, 41eqtr3d 2778 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))))
432recnd 11096 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -1 ∈ ℂ)
44 absexpz 15108 . . . . . . 7 ((-1 ∈ ℂ ∧ -1 ≠ 0 ∧ 𝑁 ∈ ℤ) → (abs‘(-1↑𝑁)) = ((abs‘-1)↑𝑁))
4543, 4, 9, 44syl3anc 1370 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(-1↑𝑁)) = ((abs‘-1)↑𝑁))
46 ax-1cn 11022 . . . . . . . . . 10 1 ∈ ℂ
4746absnegi 15203 . . . . . . . . 9 (abs‘-1) = (abs‘1)
48 abs1 15100 . . . . . . . . 9 (abs‘1) = 1
4947, 48eqtri 2764 . . . . . . . 8 (abs‘-1) = 1
5049oveq1i 7339 . . . . . . 7 ((abs‘-1)↑𝑁) = (1↑𝑁)
51 1exp 13905 . . . . . . . 8 (𝑁 ∈ ℤ → (1↑𝑁) = 1)
529, 51syl 17 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1↑𝑁) = 1)
5350, 52eqtrid 2788 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘-1)↑𝑁) = 1)
5445, 53eqtrd 2776 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(-1↑𝑁)) = 1)
5554oveq1d 7344 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (1 · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))))
5640abscld 15239 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℝ)
5756recnd 11096 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℂ)
5857mulid2d 11086 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1 · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))))
5942, 55, 583eqtrd 2780 . . 3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))))
6010, 35remulcld 11098 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
61193ad2ant1 1132 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝐺:𝑍⟶ℝ)
625peano2uzs 12735 . . . . . . . 8 (𝑁𝑍 → (𝑁 + 1) ∈ 𝑍)
63623ad2ant2 1133 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝑁 + 1) ∈ 𝑍)
6461, 63ffvelcdmd 7012 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐺‘(𝑁 + 1)) ∈ ℝ)
6560, 64resubcld 11496 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ∈ ℝ)
665peano2uzs 12735 . . . . . . . 8 ((𝑁 + (2 · 𝐾)) ∈ 𝑍 → ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍)
6732, 66syl 17 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍)
6824, 67ffvelcdmd 7012 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℝ)
6910, 68remulcld 11098 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℝ)
7010, 33remulcld 11098 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ∈ ℝ)
71 seqp1 13829 . . . . . . . . . . 11 (𝑁 ∈ (ℤ𝑀) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1))))
7225, 71syl 17 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1))))
73 fveq2 6819 . . . . . . . . . . . . 13 (𝑘 = (𝑁 + 1) → (𝐹𝑘) = (𝐹‘(𝑁 + 1)))
74 oveq2 7337 . . . . . . . . . . . . . 14 (𝑘 = (𝑁 + 1) → (-1↑𝑘) = (-1↑(𝑁 + 1)))
75 fveq2 6819 . . . . . . . . . . . . . 14 (𝑘 = (𝑁 + 1) → (𝐺𝑘) = (𝐺‘(𝑁 + 1)))
7674, 75oveq12d 7347 . . . . . . . . . . . . 13 (𝑘 = (𝑁 + 1) → ((-1↑𝑘) · (𝐺𝑘)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))))
7773, 76eqeq12d 2752 . . . . . . . . . . . 12 (𝑘 = (𝑁 + 1) → ((𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) ↔ (𝐹‘(𝑁 + 1)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))))
7813ralrimiva 3139 . . . . . . . . . . . . 13 (𝜑 → ∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
79783ad2ant1 1132 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ∀𝑘𝑍 (𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)))
8077, 79, 63rspcdva 3571 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐹‘(𝑁 + 1)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))))
8180oveq2d 7345 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1))) = ((seq𝑀( + , 𝐹)‘𝑁) + ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))))
8243, 4, 9expp1zd 13966 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 1)) = ((-1↑𝑁) · -1))
83 neg1cn 12180 . . . . . . . . . . . . . . 15 -1 ∈ ℂ
84 mulcom 11050 . . . . . . . . . . . . . . 15 (((-1↑𝑁) ∈ ℂ ∧ -1 ∈ ℂ) → ((-1↑𝑁) · -1) = (-1 · (-1↑𝑁)))
8511, 83, 84sylancl 586 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · -1) = (-1 · (-1↑𝑁)))
8611mulm1d 11520 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1 · (-1↑𝑁)) = -(-1↑𝑁))
8782, 85, 863eqtrd 2780 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 1)) = -(-1↑𝑁))
8887oveq1d 7344 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))) = (-(-1↑𝑁) · (𝐺‘(𝑁 + 1))))
8964recnd 11096 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐺‘(𝑁 + 1)) ∈ ℂ)
9011, 89mulneg1d 11521 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (𝐺‘(𝑁 + 1))) = -((-1↑𝑁) · (𝐺‘(𝑁 + 1))))
9188, 90eqtrd 2776 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))) = -((-1↑𝑁) · (𝐺‘(𝑁 + 1))))
9291oveq2d 7345 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘𝑁) + ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))) = ((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
9372, 81, 923eqtrd 2780 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
9410, 64remulcld 11098 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (𝐺‘(𝑁 + 1))) ∈ ℝ)
9594recnd 11096 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (𝐺‘(𝑁 + 1))) ∈ ℂ)
9636, 95negsubd 11431 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))) = ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
9793, 96eqtrd 2776 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
9897oveq2d 7345 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))))
9911, 36, 95subdid 11524 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))))
1009zcnd 12520 . . . . . . . . . . . . . . 15 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝑁 ∈ ℂ)
1011002timesd 12309 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (2 · 𝑁) = (𝑁 + 𝑁))
102101oveq2d 7345 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(2 · 𝑁)) = (-1↑(𝑁 + 𝑁)))
103 2z 12445 . . . . . . . . . . . . . . 15 2 ∈ ℤ
104103a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 2 ∈ ℤ)
105 expmulz 13922 . . . . . . . . . . . . . 14 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (-1↑(2 · 𝑁)) = ((-1↑2)↑𝑁))
10643, 4, 104, 9, 105syl22anc 836 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(2 · 𝑁)) = ((-1↑2)↑𝑁))
107102, 106eqtr3d 2778 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 𝑁)) = ((-1↑2)↑𝑁))
108 neg1sqe1 14006 . . . . . . . . . . . . 13 (-1↑2) = 1
109108oveq1i 7339 . . . . . . . . . . . 12 ((-1↑2)↑𝑁) = (1↑𝑁)
110107, 109eqtrdi 2792 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 𝑁)) = (1↑𝑁))
111 expaddz 13920 . . . . . . . . . . . 12 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (-1↑(𝑁 + 𝑁)) = ((-1↑𝑁) · (-1↑𝑁)))
11243, 4, 9, 9, 111syl22anc 836 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(𝑁 + 𝑁)) = ((-1↑𝑁) · (-1↑𝑁)))
113110, 112, 523eqtr3d 2784 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (-1↑𝑁)) = 1)
114113oveq1d 7344 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (-1↑𝑁)) · (𝐺‘(𝑁 + 1))) = (1 · (𝐺‘(𝑁 + 1))))
11511, 11, 89mulassd 11091 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (-1↑𝑁)) · (𝐺‘(𝑁 + 1))) = ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))
11689mulid2d 11086 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1 · (𝐺‘(𝑁 + 1))) = (𝐺‘(𝑁 + 1)))
117114, 115, 1163eqtr3d 2784 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))) = (𝐺‘(𝑁 + 1)))
118117oveq2d 7345 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))))
11998, 99, 1183eqtrd 2780 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))))
120 iseralt.4 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺𝑘))
121 iseralt.5 . . . . . . . . . . 11 (𝜑𝐺 ⇝ 0)
1225, 12, 19, 120, 121, 13iseraltlem2 15485 . . . . . . . . . 10 ((𝜑 ∧ (𝑁 + 1) ∈ 𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾)))) ≤ ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
12362, 122syl3an2 1163 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾)))) ≤ ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
124 1cnd 11063 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 1 ∈ ℂ)
12529nn0cnd 12388 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (2 · 𝐾) ∈ ℂ)
126100, 124, 125add32d 11295 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((𝑁 + 1) + (2 · 𝐾)) = ((𝑁 + (2 · 𝐾)) + 1))
127126fveq2d 6823 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾))) = (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)))
12887, 127oveq12d 7347 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾)))) = (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))))
12987oveq1d 7344 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) = (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
130123, 128, 1293brtr3d 5120 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
13168recnd 11096 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℂ)
13211, 131mulneg1d 11521 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))))
13324, 63ffvelcdmd 7012 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) ∈ ℝ)
134133recnd 11096 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) ∈ ℂ)
13511, 134mulneg1d 11521 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) = -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
136130, 132, 1353brtr3d 5120 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))
13710, 133remulcld 11098 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))) ∈ ℝ)
138137, 69lenegd 11647 . . . . . . 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 5113 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))))
141 seqp1 13829 . . . . . . . . . 10 ((𝑁 + (2 · 𝐾)) ∈ (ℤ𝑀) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1))))
14231, 141syl 17 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1))))
143 fveq2 6819 . . . . . . . . . . . . 13 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (𝐹𝑘) = (𝐹‘((𝑁 + (2 · 𝐾)) + 1)))
144 oveq2 7337 . . . . . . . . . . . . . 14 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (-1↑𝑘) = (-1↑((𝑁 + (2 · 𝐾)) + 1)))
145 fveq2 6819 . . . . . . . . . . . . . 14 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (𝐺𝑘) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
146144, 145oveq12d 7347 . . . . . . . . . . . . 13 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → ((-1↑𝑘) · (𝐺𝑘)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
147143, 146eqeq12d 2752 . . . . . . . . . . . 12 (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → ((𝐹𝑘) = ((-1↑𝑘) · (𝐺𝑘)) ↔ (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
148147, 79, 67rspcdva 3571 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
1497, 63sselid 3929 . . . . . . . . . . . . . . 15 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝑁 + 1) ∈ ℤ)
15029nn0zd 12517 . . . . . . . . . . . . . . 15 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (2 · 𝐾) ∈ ℤ)
151 expaddz 13920 . . . . . . . . . . . . . . 15 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ ((𝑁 + 1) ∈ ℤ ∧ (2 · 𝐾) ∈ ℤ)) → (-1↑((𝑁 + 1) + (2 · 𝐾))) = ((-1↑(𝑁 + 1)) · (-1↑(2 · 𝐾))))
15243, 4, 149, 150, 151syl22anc 836 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑((𝑁 + 1) + (2 · 𝐾))) = ((-1↑(𝑁 + 1)) · (-1↑(2 · 𝐾))))
15327nn0zd 12517 . . . . . . . . . . . . . . . . 17 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝐾 ∈ ℤ)
154 expmulz 13922 . . . . . . . . . . . . . . . . 17 (((-1 ∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (-1↑(2 · 𝐾)) = ((-1↑2)↑𝐾))
15543, 4, 104, 153, 154syl22anc 836 . . . . . . . . . . . . . . . 16 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(2 · 𝐾)) = ((-1↑2)↑𝐾))
156108oveq1i 7339 . . . . . . . . . . . . . . . . 17 ((-1↑2)↑𝐾) = (1↑𝐾)
157 1exp 13905 . . . . . . . . . . . . . . . . . 18 (𝐾 ∈ ℤ → (1↑𝐾) = 1)
158153, 157syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1↑𝐾) = 1)
159156, 158eqtrid 2788 . . . . . . . . . . . . . . . 16 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑2)↑𝐾) = 1)
160155, 159eqtrd 2776 . . . . . . . . . . . . . . 15 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑(2 · 𝐾)) = 1)
16187, 160oveq12d 7347 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑(𝑁 + 1)) · (-1↑(2 · 𝐾))) = (-(-1↑𝑁) · 1))
162152, 161eqtrd 2776 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑((𝑁 + 1) + (2 · 𝐾))) = (-(-1↑𝑁) · 1))
163126oveq2d 7345 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑((𝑁 + 1) + (2 · 𝐾))) = (-1↑((𝑁 + (2 · 𝐾)) + 1)))
16411negcld 11412 . . . . . . . . . . . . . 14 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → -(-1↑𝑁) ∈ ℂ)
165164mulid1d 11085 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · 1) = -(-1↑𝑁))
166162, 163, 1653eqtr3d 2784 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-1↑((𝑁 + (2 · 𝐾)) + 1)) = -(-1↑𝑁))
167166oveq1d 7344 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (-(-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
16861, 67ffvelcdmd 7012 . . . . . . . . . . . . 13 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℝ)
169168recnd 11096 . . . . . . . . . . . 12 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℂ)
17011, 169mulneg1d 11521 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (-(-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
171148, 167, 1703eqtrd 2780 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
172171oveq2d 7345 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
17310, 168remulcld 11098 . . . . . . . . . . 11 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℝ)
174173recnd 11096 . . . . . . . . . 10 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℂ)
17534, 174negsubd 11431 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
176142, 172, 1753eqtrd 2780 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
177176oveq2d 7345 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))))
17811, 34, 174subdid 11524 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))))
179113oveq1d 7344 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (-1↑𝑁)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (1 · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
18011, 11, 169mulassd 11091 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (-1↑𝑁)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))
181169mulid2d 11086 . . . . . . . . 9 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1 · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
182179, 180, 1813eqtr3d 2784 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
183182oveq2d 7345 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
184177, 178, 1833eqtrd 2780 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))
185 simp1 1135 . . . . . . . 8 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 𝜑)
1865, 12, 19, 120, 121iseraltlem1 15484 . . . . . . . 8 ((𝜑 ∧ ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍) → 0 ≤ (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
187185, 67, 186syl2anc 584 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 0 ≤ (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))
18870, 168subge02d 11660 . . . . . . 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 5111 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
19165, 69, 70, 140, 190letrd 11225 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))
19260, 64readdcld 11097 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))) ∈ ℝ)
1935, 12, 19, 120, 121, 13iseraltlem2 15485 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))
1945, 12, 19, 120, 121iseraltlem1 15484 . . . . . . 7 ((𝜑 ∧ (𝑁 + 1) ∈ 𝑍) → 0 ≤ (𝐺‘(𝑁 + 1)))
195185, 63, 194syl2anc 584 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → 0 ≤ (𝐺‘(𝑁 + 1)))
19660, 64addge01d 11656 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (0 ≤ (𝐺‘(𝑁 + 1)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1)))))
197195, 196mpbid 231 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))
19870, 60, 192, 193, 197letrd 11225 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))
19970, 60, 64absdifled 15237 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)) ↔ ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))))
200191, 198, 199mpbir2and 710 . . 3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)))
20159, 200eqbrtrrd 5113 . 2 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)))
20211, 131, 36subdid 11524 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))
203202fveq2d 6823 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))))
20468, 35resubcld 11496 . . . . . . 7 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ)
205204recnd 11096 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℂ)
20611, 205absmuld 15257 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))))
207203, 206eqtr3d 2778 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))))
20854oveq1d 7344 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘(-1↑𝑁)) · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (1 · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))))
209205abscld 15239 . . . . . 6 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℝ)
210209recnd 11096 . . . . 5 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℂ)
211210mulid2d 11086 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (1 · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))))
212207, 208, 2113eqtrd 2780 . . 3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))))
21369, 70, 192, 190, 198letrd 11225 . . . 4 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))
21469, 60, 64absdifled 15237 . . . 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 710 . . 3 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)))
216212, 215eqbrtrrd 5113 . 2 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)))
217201, 216jca 512 1 ((𝜑𝑁𝑍𝐾 ∈ ℕ0) → ((abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1086   = wceq 1540  wcel 2105  wne 2940  wral 3061   class class class wbr 5089  wf 6469  cfv 6473  (class class class)co 7329  cc 10962  cr 10963  0cc0 10964  1c1 10965   + caddc 10967   · cmul 10969  cle 11103  cmin 11298  -cneg 11299  2c2 12121  0cn0 12326  cz 12412  cuz 12675  seqcseq 13814  cexp 13875  abscabs 15036  cli 15284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5226  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642  ax-cnex 11020  ax-resscn 11021  ax-1cn 11022  ax-icn 11023  ax-addcl 11024  ax-addrcl 11025  ax-mulcl 11026  ax-mulrcl 11027  ax-mulcom 11028  ax-addass 11029  ax-mulass 11030  ax-distr 11031  ax-i2m1 11032  ax-1ne0 11033  ax-1rid 11034  ax-rnegex 11035  ax-rrecex 11036  ax-cnre 11037  ax-pre-lttri 11038  ax-pre-lttrn 11039  ax-pre-ltadd 11040  ax-pre-mulgt0 11041  ax-pre-sup 11042
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-iun 4940  df-br 5090  df-opab 5152  df-mpt 5173  df-tr 5207  df-id 5512  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5569  df-we 5571  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6232  df-ord 6299  df-on 6300  df-lim 6301  df-suc 6302  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-fv 6481  df-riota 7286  df-ov 7332  df-oprab 7333  df-mpo 7334  df-om 7773  df-1st 7891  df-2nd 7892  df-frecs 8159  df-wrecs 8190  df-recs 8264  df-rdg 8303  df-er 8561  df-pm 8681  df-en 8797  df-dom 8798  df-sdom 8799  df-sup 9291  df-inf 9292  df-pnf 11104  df-mnf 11105  df-xr 11106  df-ltxr 11107  df-le 11108  df-sub 11300  df-neg 11301  df-div 11726  df-nn 12067  df-2 12129  df-3 12130  df-n0 12327  df-z 12413  df-uz 12676  df-rp 12824  df-fz 13333  df-fl 13605  df-seq 13815  df-exp 13876  df-cj 14901  df-re 14902  df-im 14903  df-sqrt 15037  df-abs 15038  df-clim 15288  df-rlim 15289
This theorem is referenced by:  iseralt  15487
  Copyright terms: Public domain W3C validator