Proof of Theorem iseraltlem3
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | neg1rr 12381 | . . . . . . . . . 10
⊢ -1 ∈
ℝ | 
| 2 | 1 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → -1
∈ ℝ) | 
| 3 |  | neg1ne0 12382 | . . . . . . . . . 10
⊢ -1 ≠
0 | 
| 4 | 3 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → -1 ≠
0) | 
| 5 |  | iseralt.1 | . . . . . . . . . . 11
⊢ 𝑍 =
(ℤ≥‘𝑀) | 
| 6 |  | uzssz 12899 | . . . . . . . . . . 11
⊢
(ℤ≥‘𝑀) ⊆ ℤ | 
| 7 | 5, 6 | eqsstri 4030 | . . . . . . . . . 10
⊢ 𝑍 ⊆
ℤ | 
| 8 |  | simp2 1138 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 𝑁 ∈ 𝑍) | 
| 9 | 7, 8 | sselid 3981 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 𝑁 ∈
ℤ) | 
| 10 | 2, 4, 9 | reexpclzd 14288 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑𝑁) ∈
ℝ) | 
| 11 | 10 | recnd 11289 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑𝑁) ∈
ℂ) | 
| 12 |  | iseralt.2 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 13 |  | iseralt.6 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘))) | 
| 14 | 1 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → -1 ∈ ℝ) | 
| 15 | 3 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → -1 ≠ 0) | 
| 16 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ 𝑍) | 
| 17 | 7, 16 | sselid 3981 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℤ) | 
| 18 | 14, 15, 17 | reexpclzd 14288 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (-1↑𝑘) ∈ ℝ) | 
| 19 |  | iseralt.3 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:𝑍⟶ℝ) | 
| 20 | 19 | ffvelcdmda 7104 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ) | 
| 21 | 18, 20 | remulcld 11291 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((-1↑𝑘) · (𝐺‘𝑘)) ∈ ℝ) | 
| 22 | 13, 21 | eqeltrd 2841 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) | 
| 23 | 5, 12, 22 | serfre 14072 | . . . . . . . . . 10
⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ) | 
| 24 | 23 | 3ad2ant1 1134 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → seq𝑀( + , 𝐹):𝑍⟶ℝ) | 
| 25 | 8, 5 | eleqtrdi 2851 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 𝑁 ∈
(ℤ≥‘𝑀)) | 
| 26 |  | 2nn0 12543 | . . . . . . . . . . . 12
⊢ 2 ∈
ℕ0 | 
| 27 |  | simp3 1139 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 𝐾 ∈
ℕ0) | 
| 28 |  | nn0mulcl 12562 | . . . . . . . . . . . 12
⊢ ((2
∈ ℕ0 ∧ 𝐾 ∈ ℕ0) → (2
· 𝐾) ∈
ℕ0) | 
| 29 | 26, 27, 28 | sylancr 587 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (2
· 𝐾) ∈
ℕ0) | 
| 30 |  | uzaddcl 12946 | . . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (2 · 𝐾) ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈
(ℤ≥‘𝑀)) | 
| 31 | 25, 29, 30 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈
(ℤ≥‘𝑀)) | 
| 32 | 31, 5 | eleqtrrdi 2852 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈ 𝑍) | 
| 33 | 24, 32 | ffvelcdmd 7105 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) ∈ ℝ) | 
| 34 | 33 | recnd 11289 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) ∈ ℂ) | 
| 35 | 24, 8 | ffvelcdmd 7105 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘𝑁) ∈ ℝ) | 
| 36 | 35 | recnd 11289 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘𝑁) ∈ ℂ) | 
| 37 | 11, 34, 36 | subdid 11719 | . . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) | 
| 38 | 37 | fveq2d 6910 | . . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘((-1↑𝑁)
· ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))) | 
| 39 | 33, 35 | resubcld 11691 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ) | 
| 40 | 39 | recnd 11289 | . . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℂ) | 
| 41 | 11, 40 | absmuld 15493 | . . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘((-1↑𝑁)
· ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) ·
(abs‘((seq𝑀( + ,
𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))))) | 
| 42 | 38, 41 | eqtr3d 2779 | . . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘(((-1↑𝑁)
· (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) ·
(abs‘((seq𝑀( + ,
𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))))) | 
| 43 | 2 | recnd 11289 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → -1
∈ ℂ) | 
| 44 |  | absexpz 15344 | . . . . . . 7
⊢ ((-1
∈ ℂ ∧ -1 ≠ 0 ∧ 𝑁 ∈ ℤ) →
(abs‘(-1↑𝑁)) =
((abs‘-1)↑𝑁)) | 
| 45 | 43, 4, 9, 44 | syl3anc 1373 | . . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘(-1↑𝑁)) =
((abs‘-1)↑𝑁)) | 
| 46 |  | ax-1cn 11213 | . . . . . . . . . 10
⊢ 1 ∈
ℂ | 
| 47 | 46 | absnegi 15439 | . . . . . . . . 9
⊢
(abs‘-1) = (abs‘1) | 
| 48 |  | abs1 15336 | . . . . . . . . 9
⊢
(abs‘1) = 1 | 
| 49 | 47, 48 | eqtri 2765 | . . . . . . . 8
⊢
(abs‘-1) = 1 | 
| 50 | 49 | oveq1i 7441 | . . . . . . 7
⊢
((abs‘-1)↑𝑁) = (1↑𝑁) | 
| 51 |  | 1exp 14132 | . . . . . . . 8
⊢ (𝑁 ∈ ℤ →
(1↑𝑁) =
1) | 
| 52 | 9, 51 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(1↑𝑁) =
1) | 
| 53 | 50, 52 | eqtrid 2789 | . . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((abs‘-1)↑𝑁) =
1) | 
| 54 | 45, 53 | eqtrd 2777 | . . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘(-1↑𝑁)) =
1) | 
| 55 | 54 | oveq1d 7446 | . . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((abs‘(-1↑𝑁))
· (abs‘((seq𝑀(
+ , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (1 · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))))) | 
| 56 | 40 | abscld 15475 | . . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘((seq𝑀( + ,
𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℝ) | 
| 57 | 56 | recnd 11289 | . . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘((seq𝑀( + ,
𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℂ) | 
| 58 | 57 | mullidd 11279 | . . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (1
· (abs‘((seq𝑀(
+ , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) | 
| 59 | 42, 55, 58 | 3eqtrd 2781 | . . 3
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘(((-1↑𝑁)
· (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) | 
| 60 | 10, 35 | remulcld 11291 | . . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ) | 
| 61 | 19 | 3ad2ant1 1134 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 𝐺:𝑍⟶ℝ) | 
| 62 | 5 | peano2uzs 12944 | . . . . . . . 8
⊢ (𝑁 ∈ 𝑍 → (𝑁 + 1) ∈ 𝑍) | 
| 63 | 62 | 3ad2ant2 1135 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝑁 + 1) ∈ 𝑍) | 
| 64 | 61, 63 | ffvelcdmd 7105 | . . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝐺‘(𝑁 + 1)) ∈ ℝ) | 
| 65 | 60, 64 | resubcld 11691 | . . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ∈ ℝ) | 
| 66 | 5 | peano2uzs 12944 | . . . . . . . 8
⊢ ((𝑁 + (2 · 𝐾)) ∈ 𝑍 → ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍) | 
| 67 | 32, 66 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍) | 
| 68 | 24, 67 | ffvelcdmd 7105 | . . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℝ) | 
| 69 | 10, 68 | remulcld 11291 | . . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℝ) | 
| 70 | 10, 33 | remulcld 11291 | . . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ∈ ℝ) | 
| 71 |  | seqp1 14057 | . . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1)))) | 
| 72 | 25, 71 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1)))) | 
| 73 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑘 = (𝑁 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑁 + 1))) | 
| 74 |  | oveq2 7439 | . . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑁 + 1) → (-1↑𝑘) = (-1↑(𝑁 + 1))) | 
| 75 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑁 + 1) → (𝐺‘𝑘) = (𝐺‘(𝑁 + 1))) | 
| 76 | 74, 75 | oveq12d 7449 | . . . . . . . . . . . . 13
⊢ (𝑘 = (𝑁 + 1) → ((-1↑𝑘) · (𝐺‘𝑘)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))) | 
| 77 | 73, 76 | eqeq12d 2753 | . . . . . . . . . . . 12
⊢ (𝑘 = (𝑁 + 1) → ((𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)) ↔ (𝐹‘(𝑁 + 1)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))))) | 
| 78 | 13 | ralrimiva 3146 | . . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘))) | 
| 79 | 78 | 3ad2ant1 1134 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘))) | 
| 80 | 77, 79, 63 | rspcdva 3623 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝐹‘(𝑁 + 1)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))) | 
| 81 | 80 | oveq2d 7447 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1))) = ((seq𝑀( + , 𝐹)‘𝑁) + ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))))) | 
| 82 | 43, 4, 9 | expp1zd 14195 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑(𝑁 + 1)) =
((-1↑𝑁) ·
-1)) | 
| 83 |  | neg1cn 12380 | . . . . . . . . . . . . . . 15
⊢ -1 ∈
ℂ | 
| 84 |  | mulcom 11241 | . . . . . . . . . . . . . . 15
⊢
(((-1↑𝑁) ∈
ℂ ∧ -1 ∈ ℂ) → ((-1↑𝑁) · -1) = (-1 · (-1↑𝑁))) | 
| 85 | 11, 83, 84 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) · -1) =
(-1 · (-1↑𝑁))) | 
| 86 | 11 | mulm1d 11715 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (-1
· (-1↑𝑁)) =
-(-1↑𝑁)) | 
| 87 | 82, 85, 86 | 3eqtrd 2781 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑(𝑁 + 1)) =
-(-1↑𝑁)) | 
| 88 | 87 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑(𝑁 + 1)) ·
(𝐺‘(𝑁 + 1))) = (-(-1↑𝑁) · (𝐺‘(𝑁 + 1)))) | 
| 89 | 64 | recnd 11289 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝐺‘(𝑁 + 1)) ∈ ℂ) | 
| 90 | 11, 89 | mulneg1d 11716 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-(-1↑𝑁) ·
(𝐺‘(𝑁 + 1))) = -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))) | 
| 91 | 88, 90 | eqtrd 2777 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑(𝑁 + 1)) ·
(𝐺‘(𝑁 + 1))) = -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))) | 
| 92 | 91 | oveq2d 7447 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((seq𝑀( + , 𝐹)‘𝑁) + ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))) = ((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) | 
| 93 | 72, 81, 92 | 3eqtrd 2781 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) | 
| 94 | 10, 64 | remulcld 11291 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(𝐺‘(𝑁 + 1))) ∈ ℝ) | 
| 95 | 94 | recnd 11289 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(𝐺‘(𝑁 + 1))) ∈ ℂ) | 
| 96 | 36, 95 | negsubd 11626 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))) = ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) | 
| 97 | 93, 96 | eqtrd 2777 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) | 
| 98 | 97 | oveq2d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + 1))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))) | 
| 99 | 11, 36, 95 | subdid 11719 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))) | 
| 100 | 9 | zcnd 12723 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 𝑁 ∈
ℂ) | 
| 101 | 100 | 2timesd 12509 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (2
· 𝑁) = (𝑁 + 𝑁)) | 
| 102 | 101 | oveq2d 7447 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑(2 · 𝑁)) =
(-1↑(𝑁 + 𝑁))) | 
| 103 |  | 2z 12649 | . . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ | 
| 104 | 103 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 2 ∈
ℤ) | 
| 105 |  | expmulz 14149 | . . . . . . . . . . . . . 14
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (-1↑(2
· 𝑁)) =
((-1↑2)↑𝑁)) | 
| 106 | 43, 4, 104, 9, 105 | syl22anc 839 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑(2 · 𝑁)) =
((-1↑2)↑𝑁)) | 
| 107 | 102, 106 | eqtr3d 2779 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑(𝑁 + 𝑁)) = ((-1↑2)↑𝑁)) | 
| 108 |  | neg1sqe1 14235 | . . . . . . . . . . . . 13
⊢
(-1↑2) = 1 | 
| 109 | 108 | oveq1i 7441 | . . . . . . . . . . . 12
⊢
((-1↑2)↑𝑁)
= (1↑𝑁) | 
| 110 | 107, 109 | eqtrdi 2793 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑(𝑁 + 𝑁)) = (1↑𝑁)) | 
| 111 |  | expaddz 14147 | . . . . . . . . . . . 12
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (-1↑(𝑁 + 𝑁)) = ((-1↑𝑁) · (-1↑𝑁))) | 
| 112 | 43, 4, 9, 9, 111 | syl22anc 839 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑(𝑁 + 𝑁)) = ((-1↑𝑁) · (-1↑𝑁))) | 
| 113 | 110, 112,
52 | 3eqtr3d 2785 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(-1↑𝑁)) =
1) | 
| 114 | 113 | oveq1d 7446 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(-1↑𝑁)) ·
(𝐺‘(𝑁 + 1))) = (1 · (𝐺‘(𝑁 + 1)))) | 
| 115 | 11, 11, 89 | mulassd 11284 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(-1↑𝑁)) ·
(𝐺‘(𝑁 + 1))) = ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) | 
| 116 | 89 | mullidd 11279 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (1
· (𝐺‘(𝑁 + 1))) = (𝐺‘(𝑁 + 1))) | 
| 117 | 114, 115,
116 | 3eqtr3d 2785 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
((-1↑𝑁) ·
(𝐺‘(𝑁 + 1)))) = (𝐺‘(𝑁 + 1))) | 
| 118 | 117 | oveq2d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘𝑁)) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1)))) | 
| 119 | 98, 99, 118 | 3eqtrd 2781 | . . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + 1))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1)))) | 
| 120 |  | iseralt.4 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘)) | 
| 121 |  | iseralt.5 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ⇝ 0) | 
| 122 | 5, 12, 19, 120, 121, 13 | iseraltlem2 15719 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑁 + 1) ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑(𝑁 + 1)) ·
(seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾)))) ≤ ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘(𝑁 + 1)))) | 
| 123 | 62, 122 | syl3an2 1165 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑(𝑁 + 1)) ·
(seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾)))) ≤ ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘(𝑁 + 1)))) | 
| 124 |  | 1cnd 11256 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 1 ∈
ℂ) | 
| 125 | 29 | nn0cnd 12589 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (2
· 𝐾) ∈
ℂ) | 
| 126 | 100, 124,
125 | add32d 11489 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → ((𝑁 + 1) + (2 · 𝐾)) = ((𝑁 + (2 · 𝐾)) + 1)) | 
| 127 | 126 | fveq2d 6910 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾))) = (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) | 
| 128 | 87, 127 | oveq12d 7449 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑(𝑁 + 1)) ·
(seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾)))) = (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)))) | 
| 129 | 87 | oveq1d 7446 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑(𝑁 + 1)) ·
(seq𝑀( + , 𝐹)‘(𝑁 + 1))) = (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1)))) | 
| 130 | 123, 128,
129 | 3brtr3d 5174 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-(-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1)))) | 
| 131 | 68 | recnd 11289 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℂ) | 
| 132 | 11, 131 | mulneg1d 11716 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-(-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)))) | 
| 133 | 24, 63 | ffvelcdmd 7105 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘(𝑁 + 1)) ∈ ℝ) | 
| 134 | 133 | recnd 11289 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘(𝑁 + 1)) ∈ ℂ) | 
| 135 | 11, 134 | mulneg1d 11716 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-(-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + 1))) = -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1)))) | 
| 136 | 130, 132,
135 | 3brtr3d 5174 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
-((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1)))) | 
| 137 | 10, 133 | remulcld 11291 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + 1))) ∈ ℝ) | 
| 138 | 137, 69 | lenegd 11842 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ↔ -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))) | 
| 139 | 136, 138 | mpbird 257 | . . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)))) | 
| 140 | 119, 139 | eqbrtrrd 5167 | . . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)))) | 
| 141 |  | seqp1 14057 | . . . . . . . . . 10
⊢ ((𝑁 + (2 · 𝐾)) ∈
(ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1)))) | 
| 142 | 31, 141 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1)))) | 
| 143 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (𝐹‘𝑘) = (𝐹‘((𝑁 + (2 · 𝐾)) + 1))) | 
| 144 |  | oveq2 7439 | . . . . . . . . . . . . . 14
⊢ (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (-1↑𝑘) = (-1↑((𝑁 + (2 · 𝐾)) + 1))) | 
| 145 |  | fveq2 6906 | . . . . . . . . . . . . . 14
⊢ (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (𝐺‘𝑘) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) | 
| 146 | 144, 145 | oveq12d 7449 | . . . . . . . . . . . . 13
⊢ (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → ((-1↑𝑘) · (𝐺‘𝑘)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) | 
| 147 | 143, 146 | eqeq12d 2753 | . . . . . . . . . . . 12
⊢ (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → ((𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)) ↔ (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) | 
| 148 | 147, 79, 67 | rspcdva 3623 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) | 
| 149 | 7, 63 | sselid 3981 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝑁 + 1) ∈
ℤ) | 
| 150 | 29 | nn0zd 12639 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (2
· 𝐾) ∈
ℤ) | 
| 151 |  | expaddz 14147 | . . . . . . . . . . . . . . 15
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ ((𝑁 + 1) ∈ ℤ ∧ (2 · 𝐾) ∈ ℤ)) →
(-1↑((𝑁 + 1) + (2
· 𝐾))) =
((-1↑(𝑁 + 1)) ·
(-1↑(2 · 𝐾)))) | 
| 152 | 43, 4, 149, 150, 151 | syl22anc 839 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑((𝑁 + 1) + (2
· 𝐾))) =
((-1↑(𝑁 + 1)) ·
(-1↑(2 · 𝐾)))) | 
| 153 | 27 | nn0zd 12639 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 𝐾 ∈
ℤ) | 
| 154 |  | expmulz 14149 | . . . . . . . . . . . . . . . . 17
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (-1↑(2
· 𝐾)) =
((-1↑2)↑𝐾)) | 
| 155 | 43, 4, 104, 153, 154 | syl22anc 839 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑(2 · 𝐾)) =
((-1↑2)↑𝐾)) | 
| 156 | 108 | oveq1i 7441 | . . . . . . . . . . . . . . . . 17
⊢
((-1↑2)↑𝐾)
= (1↑𝐾) | 
| 157 |  | 1exp 14132 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐾 ∈ ℤ →
(1↑𝐾) =
1) | 
| 158 | 153, 157 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(1↑𝐾) =
1) | 
| 159 | 156, 158 | eqtrid 2789 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑2)↑𝐾) =
1) | 
| 160 | 155, 159 | eqtrd 2777 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑(2 · 𝐾)) =
1) | 
| 161 | 87, 160 | oveq12d 7449 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑(𝑁 + 1)) ·
(-1↑(2 · 𝐾))) =
(-(-1↑𝑁) ·
1)) | 
| 162 | 152, 161 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑((𝑁 + 1) + (2
· 𝐾))) =
(-(-1↑𝑁) ·
1)) | 
| 163 | 126 | oveq2d 7447 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑((𝑁 + 1) + (2
· 𝐾))) =
(-1↑((𝑁 + (2 ·
𝐾)) + 1))) | 
| 164 | 11 | negcld 11607 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
-(-1↑𝑁) ∈
ℂ) | 
| 165 | 164 | mulridd 11278 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-(-1↑𝑁) · 1) =
-(-1↑𝑁)) | 
| 166 | 162, 163,
165 | 3eqtr3d 2785 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑((𝑁 + (2 ·
𝐾)) + 1)) = -(-1↑𝑁)) | 
| 167 | 166 | oveq1d 7446 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑((𝑁 + (2 ·
𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (-(-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) | 
| 168 | 61, 67 | ffvelcdmd 7105 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℝ) | 
| 169 | 168 | recnd 11289 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℂ) | 
| 170 | 11, 169 | mulneg1d 11716 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-(-1↑𝑁) ·
(𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) | 
| 171 | 148, 167,
170 | 3eqtrd 2781 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) | 
| 172 | 171 | oveq2d 7447 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) | 
| 173 | 10, 168 | remulcld 11291 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℝ) | 
| 174 | 173 | recnd 11289 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℂ) | 
| 175 | 34, 174 | negsubd 11626 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) | 
| 176 | 142, 172,
175 | 3eqtrd 2781 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) | 
| 177 | 176 | oveq2d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))) | 
| 178 | 11, 34, 174 | subdid 11719 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))) | 
| 179 | 113 | oveq1d 7446 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(-1↑𝑁)) ·
(𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (1 · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) | 
| 180 | 11, 11, 169 | mulassd 11284 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(-1↑𝑁)) ·
(𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) | 
| 181 | 169 | mullidd 11279 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (1
· (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) | 
| 182 | 179, 180,
181 | 3eqtr3d 2785 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
((-1↑𝑁) ·
(𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) | 
| 183 | 182 | oveq2d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) | 
| 184 | 177, 178,
183 | 3eqtrd 2781 | . . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) | 
| 185 |  | simp1 1137 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 𝜑) | 
| 186 | 5, 12, 19, 120, 121 | iseraltlem1 15718 | . . . . . . . 8
⊢ ((𝜑 ∧ ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍) → 0 ≤ (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) | 
| 187 | 185, 67, 186 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 0 ≤
(𝐺‘((𝑁 + (2 · 𝐾)) + 1))) | 
| 188 | 70, 168 | subge02d 11855 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (0 ≤
(𝐺‘((𝑁 + (2 · 𝐾)) + 1)) ↔ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))) | 
| 189 | 187, 188 | mpbid 232 | . . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))))) | 
| 190 | 184, 189 | eqbrtrd 5165 | . . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))))) | 
| 191 | 65, 69, 70, 140, 190 | letrd 11418 | . . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))))) | 
| 192 | 60, 64 | readdcld 11290 | . . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))) ∈ ℝ) | 
| 193 | 5, 12, 19, 120, 121, 13 | iseraltlem2 15719 | . . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) | 
| 194 | 5, 12, 19, 120, 121 | iseraltlem1 15718 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑁 + 1) ∈ 𝑍) → 0 ≤ (𝐺‘(𝑁 + 1))) | 
| 195 | 185, 63, 194 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 0 ≤
(𝐺‘(𝑁 + 1))) | 
| 196 | 60, 64 | addge01d 11851 | . . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (0 ≤
(𝐺‘(𝑁 + 1)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))) | 
| 197 | 195, 196 | mpbid 232 | . . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘𝑁)) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1)))) | 
| 198 | 70, 60, 192, 193, 197 | letrd 11418 | . . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1)))) | 
| 199 | 70, 60, 64 | absdifled 15473 | . . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((abs‘(((-1↑𝑁)
· (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)) ↔ ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1)))))) | 
| 200 | 191, 198,
199 | mpbir2and 713 | . . 3
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘(((-1↑𝑁)
· (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1))) | 
| 201 | 59, 200 | eqbrtrrd 5167 | . 2
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘((seq𝑀( + ,
𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1))) | 
| 202 | 11, 131, 36 | subdid 11719 | . . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) | 
| 203 | 202 | fveq2d 6910 | . . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘((-1↑𝑁)
· ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))) | 
| 204 | 68, 35 | resubcld 11691 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ) | 
| 205 | 204 | recnd 11289 | . . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℂ) | 
| 206 | 11, 205 | absmuld 15493 | . . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘((-1↑𝑁)
· ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) ·
(abs‘((seq𝑀( + ,
𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))))) | 
| 207 | 203, 206 | eqtr3d 2779 | . . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘(((-1↑𝑁)
· (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) ·
(abs‘((seq𝑀( + ,
𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))))) | 
| 208 | 54 | oveq1d 7446 | . . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((abs‘(-1↑𝑁))
· (abs‘((seq𝑀(
+ , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (1 · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))))) | 
| 209 | 205 | abscld 15475 | . . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘((seq𝑀( + ,
𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℝ) | 
| 210 | 209 | recnd 11289 | . . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘((seq𝑀( + ,
𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℂ) | 
| 211 | 210 | mullidd 11279 | . . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (1
· (abs‘((seq𝑀(
+ , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) | 
| 212 | 207, 208,
211 | 3eqtrd 2781 | . . 3
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘(((-1↑𝑁)
· (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) | 
| 213 | 69, 70, 192, 190, 198 | letrd 11418 | . . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1)))) | 
| 214 | 69, 60, 64 | absdifled 15473 | . . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((abs‘(((-1↑𝑁)
· (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)) ↔ ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1)))))) | 
| 215 | 140, 213,
214 | mpbir2and 713 | . . 3
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘(((-1↑𝑁)
· (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1))) | 
| 216 | 212, 215 | eqbrtrrd 5167 | . 2
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘((seq𝑀( + ,
𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1))) | 
| 217 | 201, 216 | jca 511 | 1
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((abs‘((seq𝑀( + ,
𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)))) |