Proof of Theorem iseraltlem3
Step | Hyp | Ref
| Expression |
1 | | neg1rr 11125 |
. . . . . . . . . 10
⊢ -1 ∈
ℝ |
2 | 1 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → -1
∈ ℝ) |
3 | | neg1ne0 11126 |
. . . . . . . . . 10
⊢ -1 ≠
0 |
4 | 3 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → -1 ≠
0) |
5 | | iseralt.1 |
. . . . . . . . . . 11
⊢ 𝑍 =
(ℤ≥‘𝑀) |
6 | | uzssz 11707 |
. . . . . . . . . . 11
⊢
(ℤ≥‘𝑀) ⊆ ℤ |
7 | 5, 6 | eqsstri 3635 |
. . . . . . . . . 10
⊢ 𝑍 ⊆
ℤ |
8 | | simp2 1062 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 𝑁 ∈ 𝑍) |
9 | 7, 8 | sseldi 3601 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 𝑁 ∈
ℤ) |
10 | 2, 4, 9 | reexpclzd 13034 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑𝑁) ∈
ℝ) |
11 | 10 | recnd 10068 |
. . . . . . 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 477 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ 𝑍) |
17 | 7, 16 | sseldi 3601 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℤ) |
18 | 14, 15, 17 | reexpclzd 13034 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (-1↑𝑘) ∈ ℝ) |
19 | | iseralt.3 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:𝑍⟶ℝ) |
20 | 19 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ) |
21 | 18, 20 | remulcld 10070 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((-1↑𝑘) · (𝐺‘𝑘)) ∈ ℝ) |
22 | 13, 21 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) |
23 | 5, 12, 22 | serfre 12830 |
. . . . . . . . . 10
⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ) |
24 | 23 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → seq𝑀( + , 𝐹):𝑍⟶ℝ) |
25 | 8, 5 | syl6eleq 2711 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 𝑁 ∈
(ℤ≥‘𝑀)) |
26 | | 2nn0 11309 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ0 |
27 | | simp3 1063 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 𝐾 ∈
ℕ0) |
28 | | nn0mulcl 11329 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℕ0 ∧ 𝐾 ∈ ℕ0) → (2
· 𝐾) ∈
ℕ0) |
29 | 26, 27, 28 | sylancr 695 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (2
· 𝐾) ∈
ℕ0) |
30 | | uzaddcl 11744 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (2 · 𝐾) ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈
(ℤ≥‘𝑀)) |
31 | 25, 29, 30 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈
(ℤ≥‘𝑀)) |
32 | 31, 5 | syl6eleqr 2712 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝑁 + (2 · 𝐾)) ∈ 𝑍) |
33 | 24, 32 | ffvelrnd 6360 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) ∈ ℝ) |
34 | 33 | recnd 10068 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) ∈ ℂ) |
35 | 24, 8 | ffvelrnd 6360 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘𝑁) ∈ ℝ) |
36 | 35 | recnd 10068 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘𝑁) ∈ ℂ) |
37 | 11, 34, 36 | subdid 10486 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) |
38 | 37 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘((-1↑𝑁)
· ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))) |
39 | 33, 35 | resubcld 10458 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ) |
40 | 39 | recnd 10068 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℂ) |
41 | 11, 40 | absmuld 14193 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘((-1↑𝑁)
· ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) ·
(abs‘((seq𝑀( + ,
𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))))) |
42 | 38, 41 | eqtr3d 2658 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘(((-1↑𝑁)
· (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) ·
(abs‘((seq𝑀( + ,
𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))))) |
43 | 2 | recnd 10068 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → -1
∈ ℂ) |
44 | | absexpz 14045 |
. . . . . . 7
⊢ ((-1
∈ ℂ ∧ -1 ≠ 0 ∧ 𝑁 ∈ ℤ) →
(abs‘(-1↑𝑁)) =
((abs‘-1)↑𝑁)) |
45 | 43, 4, 9, 44 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘(-1↑𝑁)) =
((abs‘-1)↑𝑁)) |
46 | | ax-1cn 9994 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
47 | 46 | absnegi 14139 |
. . . . . . . . 9
⊢
(abs‘-1) = (abs‘1) |
48 | | abs1 14037 |
. . . . . . . . 9
⊢
(abs‘1) = 1 |
49 | 47, 48 | eqtri 2644 |
. . . . . . . 8
⊢
(abs‘-1) = 1 |
50 | 49 | oveq1i 6660 |
. . . . . . 7
⊢
((abs‘-1)↑𝑁) = (1↑𝑁) |
51 | | 1exp 12889 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ →
(1↑𝑁) =
1) |
52 | 9, 51 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(1↑𝑁) =
1) |
53 | 50, 52 | syl5eq 2668 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((abs‘-1)↑𝑁) =
1) |
54 | 45, 53 | eqtrd 2656 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘(-1↑𝑁)) =
1) |
55 | 54 | oveq1d 6665 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((abs‘(-1↑𝑁))
· (abs‘((seq𝑀(
+ , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (1 · (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))))) |
56 | 40 | abscld 14175 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘((seq𝑀( + ,
𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℝ) |
57 | 56 | recnd 10068 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘((seq𝑀( + ,
𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℂ) |
58 | 57 | mulid2d 10058 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (1
· (abs‘((seq𝑀(
+ , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) |
59 | 42, 55, 58 | 3eqtrd 2660 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘(((-1↑𝑁)
· (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁)))) |
60 | 10, 35 | remulcld 10070 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ) |
61 | 19 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 𝐺:𝑍⟶ℝ) |
62 | 5 | peano2uzs 11742 |
. . . . . . . 8
⊢ (𝑁 ∈ 𝑍 → (𝑁 + 1) ∈ 𝑍) |
63 | 62 | 3ad2ant2 1083 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝑁 + 1) ∈ 𝑍) |
64 | 61, 63 | ffvelrnd 6360 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝐺‘(𝑁 + 1)) ∈ ℝ) |
65 | 60, 64 | resubcld 10458 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ∈ ℝ) |
66 | 5 | peano2uzs 11742 |
. . . . . . . 8
⊢ ((𝑁 + (2 · 𝐾)) ∈ 𝑍 → ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍) |
67 | 32, 66 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍) |
68 | 24, 67 | ffvelrnd 6360 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℝ) |
69 | 10, 68 | remulcld 10070 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℝ) |
70 | 10, 33 | remulcld 10070 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ∈ ℝ) |
71 | | seqp1 12816 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1)))) |
72 | 25, 71 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1)))) |
73 | 13 | ralrimiva 2966 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘))) |
74 | 73 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘))) |
75 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑁 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑁 + 1))) |
76 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑁 + 1) → (-1↑𝑘) = (-1↑(𝑁 + 1))) |
77 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑁 + 1) → (𝐺‘𝑘) = (𝐺‘(𝑁 + 1))) |
78 | 76, 77 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑁 + 1) → ((-1↑𝑘) · (𝐺‘𝑘)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))) |
79 | 75, 78 | eqeq12d 2637 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑁 + 1) → ((𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)) ↔ (𝐹‘(𝑁 + 1)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))))) |
80 | 79 | rspcv 3305 |
. . . . . . . . . . . 12
⊢ ((𝑁 + 1) ∈ 𝑍 → (∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)) → (𝐹‘(𝑁 + 1)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))))) |
81 | 63, 74, 80 | sylc 65 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝐹‘(𝑁 + 1)) = ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))) |
82 | 81 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1))) = ((seq𝑀( + , 𝐹)‘𝑁) + ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1))))) |
83 | 43, 4, 9 | expp1zd 13017 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑(𝑁 + 1)) =
((-1↑𝑁) ·
-1)) |
84 | | neg1cn 11124 |
. . . . . . . . . . . . . . 15
⊢ -1 ∈
ℂ |
85 | | mulcom 10022 |
. . . . . . . . . . . . . . 15
⊢
(((-1↑𝑁) ∈
ℂ ∧ -1 ∈ ℂ) → ((-1↑𝑁) · -1) = (-1 · (-1↑𝑁))) |
86 | 11, 84, 85 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) · -1) =
(-1 · (-1↑𝑁))) |
87 | 11 | mulm1d 10482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (-1
· (-1↑𝑁)) =
-(-1↑𝑁)) |
88 | 83, 86, 87 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑(𝑁 + 1)) =
-(-1↑𝑁)) |
89 | 88 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑(𝑁 + 1)) ·
(𝐺‘(𝑁 + 1))) = (-(-1↑𝑁) · (𝐺‘(𝑁 + 1)))) |
90 | 64 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝐺‘(𝑁 + 1)) ∈ ℂ) |
91 | 11, 90 | mulneg1d 10483 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-(-1↑𝑁) ·
(𝐺‘(𝑁 + 1))) = -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))) |
92 | 89, 91 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑(𝑁 + 1)) ·
(𝐺‘(𝑁 + 1))) = -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))) |
93 | 92 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((seq𝑀( + , 𝐹)‘𝑁) + ((-1↑(𝑁 + 1)) · (𝐺‘(𝑁 + 1)))) = ((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) |
94 | 72, 82, 93 | 3eqtrd 2660 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) |
95 | 10, 64 | remulcld 10070 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(𝐺‘(𝑁 + 1))) ∈ ℝ) |
96 | 95 | recnd 10068 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(𝐺‘(𝑁 + 1))) ∈ ℂ) |
97 | 36, 96 | negsubd 10398 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((seq𝑀( + , 𝐹)‘𝑁) + -((-1↑𝑁) · (𝐺‘(𝑁 + 1)))) = ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) |
98 | 94, 97 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) |
99 | 98 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + 1))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))) |
100 | 11, 36, 96 | subdid 10486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
((seq𝑀( + , 𝐹)‘𝑁) − ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1)))))) |
101 | 9 | zcnd 11483 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 𝑁 ∈
ℂ) |
102 | 101 | 2timesd 11275 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (2
· 𝑁) = (𝑁 + 𝑁)) |
103 | 102 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑(2 · 𝑁)) =
(-1↑(𝑁 + 𝑁))) |
104 | | 2z 11409 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
105 | 104 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 2 ∈
ℤ) |
106 | | expmulz 12906 |
. . . . . . . . . . . . . 14
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (-1↑(2
· 𝑁)) =
((-1↑2)↑𝑁)) |
107 | 43, 4, 105, 9, 106 | syl22anc 1327 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑(2 · 𝑁)) =
((-1↑2)↑𝑁)) |
108 | 103, 107 | eqtr3d 2658 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑(𝑁 + 𝑁)) = ((-1↑2)↑𝑁)) |
109 | | neg1sqe1 12959 |
. . . . . . . . . . . . 13
⊢
(-1↑2) = 1 |
110 | 109 | oveq1i 6660 |
. . . . . . . . . . . 12
⊢
((-1↑2)↑𝑁)
= (1↑𝑁) |
111 | 108, 110 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑(𝑁 + 𝑁)) = (1↑𝑁)) |
112 | | expaddz 12904 |
. . . . . . . . . . . 12
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (-1↑(𝑁 + 𝑁)) = ((-1↑𝑁) · (-1↑𝑁))) |
113 | 43, 4, 9, 9, 112 | syl22anc 1327 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑(𝑁 + 𝑁)) = ((-1↑𝑁) · (-1↑𝑁))) |
114 | 111, 113,
52 | 3eqtr3d 2664 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(-1↑𝑁)) =
1) |
115 | 114 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(-1↑𝑁)) ·
(𝐺‘(𝑁 + 1))) = (1 · (𝐺‘(𝑁 + 1)))) |
116 | 11, 11, 90 | mulassd 10063 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(-1↑𝑁)) ·
(𝐺‘(𝑁 + 1))) = ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) |
117 | 90 | mulid2d 10058 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (1
· (𝐺‘(𝑁 + 1))) = (𝐺‘(𝑁 + 1))) |
118 | 115, 116,
117 | 3eqtr3d 2664 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
((-1↑𝑁) ·
(𝐺‘(𝑁 + 1)))) = (𝐺‘(𝑁 + 1))) |
119 | 118 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘𝑁)) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘(𝑁 + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1)))) |
120 | 99, 100, 119 | 3eqtrd 2660 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + 1))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1)))) |
121 | | iseralt.4 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘)) |
122 | | iseralt.5 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ⇝ 0) |
123 | 5, 12, 19, 121, 122, 13 | iseraltlem2 14413 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑁 + 1) ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑(𝑁 + 1)) ·
(seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾)))) ≤ ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘(𝑁 + 1)))) |
124 | 62, 123 | syl3an2 1360 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑(𝑁 + 1)) ·
(seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾)))) ≤ ((-1↑(𝑁 + 1)) · (seq𝑀( + , 𝐹)‘(𝑁 + 1)))) |
125 | | 1cnd 10056 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 1 ∈
ℂ) |
126 | 29 | nn0cnd 11353 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (2
· 𝐾) ∈
ℂ) |
127 | 101, 125,
126 | add32d 10263 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → ((𝑁 + 1) + (2 · 𝐾)) = ((𝑁 + (2 · 𝐾)) + 1)) |
128 | 127 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾))) = (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) |
129 | 88, 128 | oveq12d 6668 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑(𝑁 + 1)) ·
(seq𝑀( + , 𝐹)‘((𝑁 + 1) + (2 · 𝐾)))) = (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)))) |
130 | 88 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑(𝑁 + 1)) ·
(seq𝑀( + , 𝐹)‘(𝑁 + 1))) = (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1)))) |
131 | 124, 129,
130 | 3brtr3d 4684 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-(-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ (-(-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1)))) |
132 | 68 | recnd 10068 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℂ) |
133 | 11, 132 | mulneg1d 10483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-(-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)))) |
134 | 24, 63 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘(𝑁 + 1)) ∈ ℝ) |
135 | 134 | recnd 10068 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘(𝑁 + 1)) ∈ ℂ) |
136 | 11, 135 | mulneg1d 10483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-(-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + 1))) = -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1)))) |
137 | 131, 133,
136 | 3brtr3d 4684 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
-((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1)))) |
138 | 10, 134 | remulcld 10070 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + 1))) ∈ ℝ) |
139 | 138, 69 | lenegd 10606 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ↔ -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ -((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + 1))))) |
140 | 137, 139 | mpbird 247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)))) |
141 | 120, 140 | eqbrtrrd 4677 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)))) |
142 | | seqp1 12816 |
. . . . . . . . . 10
⊢ ((𝑁 + (2 · 𝐾)) ∈
(ℤ≥‘𝑀) → (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1)))) |
143 | 31, 142 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1)))) |
144 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (𝐹‘𝑘) = (𝐹‘((𝑁 + (2 · 𝐾)) + 1))) |
145 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (-1↑𝑘) = (-1↑((𝑁 + (2 · 𝐾)) + 1))) |
146 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → (𝐺‘𝑘) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) |
147 | 145, 146 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → ((-1↑𝑘) · (𝐺‘𝑘)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) |
148 | 144, 147 | eqeq12d 2637 |
. . . . . . . . . . . . 13
⊢ (𝑘 = ((𝑁 + (2 · 𝐾)) + 1) → ((𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)) ↔ (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) |
149 | 148 | rspcv 3305 |
. . . . . . . . . . . 12
⊢ (((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍 → (∀𝑘 ∈ 𝑍 (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘)) → (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) |
150 | 67, 74, 149 | sylc 65 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = ((-1↑((𝑁 + (2 · 𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) |
151 | 7, 63 | sseldi 3601 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝑁 + 1) ∈
ℤ) |
152 | 29 | nn0zd 11480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (2
· 𝐾) ∈
ℤ) |
153 | | expaddz 12904 |
. . . . . . . . . . . . . . 15
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ ((𝑁 + 1) ∈ ℤ ∧ (2 · 𝐾) ∈ ℤ)) →
(-1↑((𝑁 + 1) + (2
· 𝐾))) =
((-1↑(𝑁 + 1)) ·
(-1↑(2 · 𝐾)))) |
154 | 43, 4, 151, 152, 153 | syl22anc 1327 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑((𝑁 + 1) + (2
· 𝐾))) =
((-1↑(𝑁 + 1)) ·
(-1↑(2 · 𝐾)))) |
155 | 27 | nn0zd 11480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 𝐾 ∈
ℤ) |
156 | | expmulz 12906 |
. . . . . . . . . . . . . . . . 17
⊢ (((-1
∈ ℂ ∧ -1 ≠ 0) ∧ (2 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (-1↑(2
· 𝐾)) =
((-1↑2)↑𝐾)) |
157 | 43, 4, 105, 155, 156 | syl22anc 1327 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑(2 · 𝐾)) =
((-1↑2)↑𝐾)) |
158 | 109 | oveq1i 6660 |
. . . . . . . . . . . . . . . . 17
⊢
((-1↑2)↑𝐾)
= (1↑𝐾) |
159 | | 1exp 12889 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐾 ∈ ℤ →
(1↑𝐾) =
1) |
160 | 155, 159 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(1↑𝐾) =
1) |
161 | 158, 160 | syl5eq 2668 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑2)↑𝐾) =
1) |
162 | 157, 161 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑(2 · 𝐾)) =
1) |
163 | 88, 162 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑(𝑁 + 1)) ·
(-1↑(2 · 𝐾))) =
(-(-1↑𝑁) ·
1)) |
164 | 154, 163 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑((𝑁 + 1) + (2
· 𝐾))) =
(-(-1↑𝑁) ·
1)) |
165 | 127 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑((𝑁 + 1) + (2
· 𝐾))) =
(-1↑((𝑁 + (2 ·
𝐾)) + 1))) |
166 | 11 | negcld 10379 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
-(-1↑𝑁) ∈
ℂ) |
167 | 166 | mulid1d 10057 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-(-1↑𝑁) · 1) =
-(-1↑𝑁)) |
168 | 164, 165,
167 | 3eqtr3d 2664 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-1↑((𝑁 + (2 ·
𝐾)) + 1)) = -(-1↑𝑁)) |
169 | 168 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑((𝑁 + (2 ·
𝐾)) + 1)) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (-(-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) |
170 | 61, 67 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℝ) |
171 | 170 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝐺‘((𝑁 + (2 · 𝐾)) + 1)) ∈ ℂ) |
172 | 11, 171 | mulneg1d 10483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(-(-1↑𝑁) ·
(𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) |
173 | 150, 169,
172 | 3eqtrd 2660 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (𝐹‘((𝑁 + (2 · 𝐾)) + 1)) = -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) |
174 | 173 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + (𝐹‘((𝑁 + (2 · 𝐾)) + 1))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) |
175 | 10, 170 | remulcld 10070 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℝ) |
176 | 175 | recnd 10068 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ∈ ℂ) |
177 | 34, 176 | negsubd 10398 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) + -((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) |
178 | 143, 174,
177 | 3eqtrd 2660 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) = ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) |
179 | 178 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = ((-1↑𝑁) · ((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))) |
180 | 11, 34, 176 | subdid 10486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
((seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))) − ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))))) |
181 | 114 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(-1↑𝑁)) ·
(𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (1 · (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) |
182 | 11, 11, 171 | mulassd 10063 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(-1↑𝑁)) ·
(𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) |
183 | 171 | mulid2d 10058 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (1
· (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) |
184 | 181, 182,
183 | 3eqtr3d 2664 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
((-1↑𝑁) ·
(𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) = (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) |
185 | 184 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · ((-1↑𝑁) · (𝐺‘((𝑁 + (2 · 𝐾)) + 1))))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) |
186 | 179, 180,
185 | 3eqtrd 2660 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1)))) |
187 | | simp1 1061 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 𝜑) |
188 | 5, 12, 19, 121, 122 | iseraltlem1 14412 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑁 + (2 · 𝐾)) + 1) ∈ 𝑍) → 0 ≤ (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) |
189 | 187, 67, 188 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 0 ≤
(𝐺‘((𝑁 + (2 · 𝐾)) + 1))) |
190 | 70, 170 | subge02d 10619 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (0 ≤
(𝐺‘((𝑁 + (2 · 𝐾)) + 1)) ↔ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))))) |
191 | 189, 190 | mpbid 222 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − (𝐺‘((𝑁 + (2 · 𝐾)) + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))))) |
192 | 186, 191 | eqbrtrd 4675 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))))) |
193 | 65, 69, 70, 141, 192 | letrd 10194 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾))))) |
194 | 60, 64 | readdcld 10069 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))) ∈ ℝ) |
195 | 5, 12, 19, 121, 122, 13 | iseraltlem2 14413 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))) |
196 | 5, 12, 19, 121, 122 | iseraltlem1 14412 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑁 + 1) ∈ 𝑍) → 0 ≤ (𝐺‘(𝑁 + 1))) |
197 | 187, 63, 196 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → 0 ≤
(𝐺‘(𝑁 + 1))) |
198 | 60, 64 | addge01d 10615 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (0 ≤
(𝐺‘(𝑁 + 1)) ↔ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1))))) |
199 | 197, 198 | mpbid 222 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘𝑁)) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1)))) |
200 | 70, 60, 194, 195, 199 | letrd 10194 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1)))) |
201 | 70, 60, 64 | absdifled 14173 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((abs‘(((-1↑𝑁)
· (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)) ↔ ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1)))))) |
202 | 193, 200,
201 | mpbir2and 957 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘(((-1↑𝑁)
· (seq𝑀( + , 𝐹)‘(𝑁 + (2 · 𝐾)))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1))) |
203 | 59, 202 | eqbrtrrd 4677 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘((seq𝑀( + ,
𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1))) |
204 | 11, 132, 36 | subdid 10486 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) = (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) |
205 | 204 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘((-1↑𝑁)
· ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘(((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁))))) |
206 | 68, 35 | resubcld 10458 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℝ) |
207 | 206 | recnd 10068 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)) ∈ ℂ) |
208 | 11, 207 | absmuld 14193 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘((-1↑𝑁)
· ((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) ·
(abs‘((seq𝑀( + ,
𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))))) |
209 | 205, 208 | eqtr3d 2658 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘(((-1↑𝑁)
· (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = ((abs‘(-1↑𝑁)) ·
(abs‘((seq𝑀( + ,
𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))))) |
210 | 54 | oveq1d 6665 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((abs‘(-1↑𝑁))
· (abs‘((seq𝑀(
+ , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (1 · (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))))) |
211 | 207 | abscld 14175 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘((seq𝑀( + ,
𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℝ) |
212 | 211 | recnd 10068 |
. . . . 5
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘((seq𝑀( + ,
𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ∈ ℂ) |
213 | 212 | mulid2d 10058 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) → (1
· (abs‘((seq𝑀(
+ , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) |
214 | 209, 210,
213 | 3eqtrd 2660 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘(((-1↑𝑁)
· (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) = (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁)))) |
215 | 69, 70, 194, 192, 200 | letrd 10194 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((-1↑𝑁) ·
(seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1)))) |
216 | 69, 60, 64 | absdifled 14173 |
. . . 4
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((abs‘(((-1↑𝑁)
· (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1)) ↔ ((((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) − (𝐺‘(𝑁 + 1))) ≤ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ∧ ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) ≤ (((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)) + (𝐺‘(𝑁 + 1)))))) |
217 | 141, 215,
216 | mpbir2and 957 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘(((-1↑𝑁)
· (seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1))) − ((-1↑𝑁) · (seq𝑀( + , 𝐹)‘𝑁)))) ≤ (𝐺‘(𝑁 + 1))) |
218 | 214, 217 | eqbrtrrd 4677 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
(abs‘((seq𝑀( + ,
𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1))) |
219 | 203, 218 | jca 554 |
1
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑍 ∧ 𝐾 ∈ ℕ0) →
((abs‘((seq𝑀( + ,
𝐹)‘(𝑁 + (2 · 𝐾))) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑁 + (2 · 𝐾)) + 1)) − (seq𝑀( + , 𝐹)‘𝑁))) ≤ (𝐺‘(𝑁 + 1)))) |