Proof of Theorem knoppndvlem14
Step | Hyp | Ref
| Expression |
1 | | knoppndvlem14.t |
. . . . . 6
⊢ 𝑇 = (𝑥 ∈ ℝ ↦
(abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) |
2 | | knoppndvlem14.f |
. . . . . 6
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) |
3 | | knoppndvlem14.b |
. . . . . . . 8
⊢ 𝐵 = ((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1)) |
4 | 3 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = ((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1))) |
5 | | knoppndvlem14.n |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
6 | | knoppndvlem14.j |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈
ℕ0) |
7 | 6 | nn0zd 12423 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ ℤ) |
8 | | knoppndvlem14.m |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
9 | 8 | peano2zd 12428 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 + 1) ∈ ℤ) |
10 | 5, 7, 9 | knoppndvlem1 34688 |
. . . . . . 7
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1)) ∈ ℝ) |
11 | 4, 10 | eqeltrd 2841 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℝ) |
12 | | knoppndvlem14.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) |
13 | 12 | knoppndvlem3 34690 |
. . . . . . 7
⊢ (𝜑 → (𝐶 ∈ ℝ ∧ (abs‘𝐶) < 1)) |
14 | 13 | simpld 495 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℝ) |
15 | 1, 2, 11, 14, 5 | knoppndvlem5 34692 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) ∈ ℝ) |
16 | | knoppndvlem14.a |
. . . . . . . 8
⊢ 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀) |
17 | 16 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀)) |
18 | 5, 7, 8 | knoppndvlem1 34688 |
. . . . . . 7
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀) ∈ ℝ) |
19 | 17, 18 | eqeltrd 2841 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) |
20 | 1, 2, 19, 14, 5 | knoppndvlem5 34692 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖) ∈ ℝ) |
21 | 15, 20 | resubcld 11403 |
. . . 4
⊢ (𝜑 → (Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖)) ∈ ℝ) |
22 | 21 | recnd 11004 |
. . 3
⊢ (𝜑 → (Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖)) ∈ ℂ) |
23 | 22 | abscld 15146 |
. 2
⊢ (𝜑 → (abs‘(Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖))) ∈ ℝ) |
24 | 11, 19 | resubcld 11403 |
. . . . 5
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
25 | 24 | recnd 11004 |
. . . 4
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ) |
26 | 25 | abscld 15146 |
. . 3
⊢ (𝜑 → (abs‘(𝐵 − 𝐴)) ∈ ℝ) |
27 | | fzfid 13691 |
. . . 4
⊢ (𝜑 → (0...(𝐽 − 1)) ∈ Fin) |
28 | | 2re 12047 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
29 | 28 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℝ) |
30 | | nnre 11980 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
31 | 5, 30 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℝ) |
32 | 29, 31 | remulcld 11006 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ) |
33 | 14 | recnd 11004 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℂ) |
34 | 33 | abscld 15146 |
. . . . . . 7
⊢ (𝜑 → (abs‘𝐶) ∈
ℝ) |
35 | 32, 34 | remulcld 11006 |
. . . . . 6
⊢ (𝜑 → ((2 · 𝑁) · (abs‘𝐶)) ∈
ℝ) |
36 | 35 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐽 − 1))) → ((2 · 𝑁) · (abs‘𝐶)) ∈
ℝ) |
37 | | elfznn0 13348 |
. . . . . 6
⊢ (𝑖 ∈ (0...(𝐽 − 1)) → 𝑖 ∈ ℕ0) |
38 | 37 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐽 − 1))) → 𝑖 ∈ ℕ0) |
39 | 36, 38 | reexpcld 13879 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐽 − 1))) → (((2 · 𝑁) · (abs‘𝐶))↑𝑖) ∈ ℝ) |
40 | 27, 39 | fsumrecl 15444 |
. . 3
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐽 − 1))(((2 · 𝑁) · (abs‘𝐶))↑𝑖) ∈ ℝ) |
41 | 26, 40 | remulcld 11006 |
. 2
⊢ (𝜑 → ((abs‘(𝐵 − 𝐴)) · Σ𝑖 ∈ (0...(𝐽 − 1))(((2 · 𝑁) · (abs‘𝐶))↑𝑖)) ∈ ℝ) |
42 | 34, 6 | reexpcld 13879 |
. . . 4
⊢ (𝜑 → ((abs‘𝐶)↑𝐽) ∈ ℝ) |
43 | | 2ne0 12077 |
. . . . 5
⊢ 2 ≠
0 |
44 | 43 | a1i 11 |
. . . 4
⊢ (𝜑 → 2 ≠ 0) |
45 | 42, 29, 44 | redivcld 11803 |
. . 3
⊢ (𝜑 → (((abs‘𝐶)↑𝐽) / 2) ∈ ℝ) |
46 | | 1red 10977 |
. . . 4
⊢ (𝜑 → 1 ∈
ℝ) |
47 | 35, 46 | resubcld 11403 |
. . . 4
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶)) − 1) ∈
ℝ) |
48 | | 0red 10979 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℝ) |
49 | | 0lt1 11497 |
. . . . . . . 8
⊢ 0 <
1 |
50 | 49 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 < 1) |
51 | | knoppndvlem14.1 |
. . . . . . . . 9
⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶))) |
52 | 12, 5, 51 | knoppndvlem12 34699 |
. . . . . . . 8
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶)) ≠ 1 ∧ 1 < (((2
· 𝑁) ·
(abs‘𝐶)) −
1))) |
53 | 52 | simprd 496 |
. . . . . . 7
⊢ (𝜑 → 1 < (((2 · 𝑁) · (abs‘𝐶)) − 1)) |
54 | 48, 46, 47, 50, 53 | lttrd 11136 |
. . . . . 6
⊢ (𝜑 → 0 < (((2 · 𝑁) · (abs‘𝐶)) − 1)) |
55 | 48, 54 | jca 512 |
. . . . 5
⊢ (𝜑 → (0 ∈ ℝ ∧ 0
< (((2 · 𝑁)
· (abs‘𝐶))
− 1))) |
56 | | ltne 11072 |
. . . . 5
⊢ ((0
∈ ℝ ∧ 0 < (((2 · 𝑁) · (abs‘𝐶)) − 1)) → (((2 · 𝑁) · (abs‘𝐶)) − 1) ≠
0) |
57 | 55, 56 | syl 17 |
. . . 4
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶)) − 1) ≠
0) |
58 | 46, 47, 57 | redivcld 11803 |
. . 3
⊢ (𝜑 → (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)) ∈
ℝ) |
59 | 45, 58 | remulcld 11006 |
. 2
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1))) ∈
ℝ) |
60 | 1, 2, 19, 11, 12, 6, 5 | knoppndvlem11 34698 |
. 2
⊢ (𝜑 → (abs‘(Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖))) ≤ ((abs‘(𝐵 − 𝐴)) · Σ𝑖 ∈ (0...(𝐽 − 1))(((2 · 𝑁) · (abs‘𝐶))↑𝑖))) |
61 | 4, 17 | oveq12d 7289 |
. . . . . . 7
⊢ (𝜑 → (𝐵 − 𝐴) = (((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1)) − ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀))) |
62 | 29 | recnd 11004 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ∈
ℂ) |
63 | 31 | recnd 11004 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℂ) |
64 | | nnge1 12001 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 1 ≤
𝑁) |
65 | 5, 64 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ≤ 𝑁) |
66 | 48, 46, 31, 50, 65 | ltletrd 11135 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 < 𝑁) |
67 | 48, 66 | jca 512 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (0 ∈ ℝ ∧ 0
< 𝑁)) |
68 | | ltne 11072 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ 0 < 𝑁) → 𝑁 ≠ 0) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ≠ 0) |
70 | 62, 63, 44, 69 | mulne0d 11627 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 · 𝑁) ≠ 0) |
71 | 7 | znegcld 12427 |
. . . . . . . . . . . . 13
⊢ (𝜑 → -𝐽 ∈ ℤ) |
72 | 32, 70, 71 | reexpclzd 13962 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · 𝑁)↑-𝐽) ∈ ℝ) |
73 | 72, 29, 44 | redivcld 11803 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) / 2) ∈ ℝ) |
74 | 73 | recnd 11004 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) / 2) ∈ ℂ) |
75 | 9 | zcnd 12426 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 + 1) ∈ ℂ) |
76 | 8 | zcnd 12426 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℂ) |
77 | 74, 75, 76 | subdid 11431 |
. . . . . . . . 9
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · ((𝑀 + 1) − 𝑀)) = (((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1)) − ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀))) |
78 | 77 | eqcomd 2746 |
. . . . . . . 8
⊢ (𝜑 → (((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1)) − ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀)) = ((((2 · 𝑁)↑-𝐽) / 2) · ((𝑀 + 1) − 𝑀))) |
79 | | 1cnd 10971 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℂ) |
80 | 76, 79 | pncan2d 11334 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑀 + 1) − 𝑀) = 1) |
81 | 80 | oveq2d 7287 |
. . . . . . . 8
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · ((𝑀 + 1) − 𝑀)) = ((((2 · 𝑁)↑-𝐽) / 2) · 1)) |
82 | 74 | mulid1d 10993 |
. . . . . . . 8
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · 1) = (((2 · 𝑁)↑-𝐽) / 2)) |
83 | 78, 81, 82 | 3eqtrd 2784 |
. . . . . . 7
⊢ (𝜑 → (((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1)) − ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀)) = (((2 · 𝑁)↑-𝐽) / 2)) |
84 | 61, 83 | eqtrd 2780 |
. . . . . 6
⊢ (𝜑 → (𝐵 − 𝐴) = (((2 · 𝑁)↑-𝐽) / 2)) |
85 | 84 | fveq2d 6775 |
. . . . 5
⊢ (𝜑 → (abs‘(𝐵 − 𝐴)) = (abs‘(((2 · 𝑁)↑-𝐽) / 2))) |
86 | 72 | recnd 11004 |
. . . . . . 7
⊢ (𝜑 → ((2 · 𝑁)↑-𝐽) ∈ ℂ) |
87 | 86, 62, 44 | absdivd 15165 |
. . . . . 6
⊢ (𝜑 → (abs‘(((2 ·
𝑁)↑-𝐽) / 2)) = ((abs‘((2 · 𝑁)↑-𝐽)) / (abs‘2))) |
88 | 62, 63 | mulcld 10996 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · 𝑁) ∈
ℂ) |
89 | 88, 70, 71 | 3jca 1127 |
. . . . . . . . 9
⊢ (𝜑 → ((2 · 𝑁) ∈ ℂ ∧ (2
· 𝑁) ≠ 0 ∧
-𝐽 ∈
ℤ)) |
90 | | absexpz 15015 |
. . . . . . . . 9
⊢ (((2
· 𝑁) ∈ ℂ
∧ (2 · 𝑁) ≠ 0
∧ -𝐽 ∈ ℤ)
→ (abs‘((2 · 𝑁)↑-𝐽)) = ((abs‘(2 · 𝑁))↑-𝐽)) |
91 | 89, 90 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (abs‘((2 ·
𝑁)↑-𝐽)) = ((abs‘(2 · 𝑁))↑-𝐽)) |
92 | 62, 63 | absmuld 15164 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘(2 ·
𝑁)) = ((abs‘2)
· (abs‘𝑁))) |
93 | | 0le2 12075 |
. . . . . . . . . . . . . 14
⊢ 0 ≤
2 |
94 | 28, 93 | pm3.2i 471 |
. . . . . . . . . . . . 13
⊢ (2 ∈
ℝ ∧ 0 ≤ 2) |
95 | | absid 15006 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2) |
96 | 94, 95 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(abs‘2) = 2 |
97 | 96 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘2) =
2) |
98 | 48, 31, 66 | ltled 11123 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ 𝑁) |
99 | 31, 98 | absidd 15132 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘𝑁) = 𝑁) |
100 | 97, 99 | oveq12d 7289 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs‘2) ·
(abs‘𝑁)) = (2
· 𝑁)) |
101 | 92, 100 | eqtrd 2780 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘(2 ·
𝑁)) = (2 · 𝑁)) |
102 | 101 | oveq1d 7286 |
. . . . . . . 8
⊢ (𝜑 → ((abs‘(2 ·
𝑁))↑-𝐽) = ((2 · 𝑁)↑-𝐽)) |
103 | 91, 102 | eqtrd 2780 |
. . . . . . 7
⊢ (𝜑 → (abs‘((2 ·
𝑁)↑-𝐽)) = ((2 · 𝑁)↑-𝐽)) |
104 | 103, 97 | oveq12d 7289 |
. . . . . 6
⊢ (𝜑 → ((abs‘((2 ·
𝑁)↑-𝐽)) / (abs‘2)) = (((2 · 𝑁)↑-𝐽) / 2)) |
105 | 87, 104 | eqtrd 2780 |
. . . . 5
⊢ (𝜑 → (abs‘(((2 ·
𝑁)↑-𝐽) / 2)) = (((2 · 𝑁)↑-𝐽) / 2)) |
106 | 85, 105 | eqtrd 2780 |
. . . 4
⊢ (𝜑 → (abs‘(𝐵 − 𝐴)) = (((2 · 𝑁)↑-𝐽) / 2)) |
107 | 35 | recnd 11004 |
. . . . . 6
⊢ (𝜑 → ((2 · 𝑁) · (abs‘𝐶)) ∈
ℂ) |
108 | 52 | simpld 495 |
. . . . . 6
⊢ (𝜑 → ((2 · 𝑁) · (abs‘𝐶)) ≠ 1) |
109 | 107, 108,
6 | geoser 15577 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐽 − 1))(((2 · 𝑁) · (abs‘𝐶))↑𝑖) = ((1 − (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) / (1 − ((2 · 𝑁) · (abs‘𝐶))))) |
110 | 107, 6 | expcld 13862 |
. . . . . 6
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶))↑𝐽) ∈ ℂ) |
111 | 108 | necomd 3001 |
. . . . . 6
⊢ (𝜑 → 1 ≠ ((2 · 𝑁) · (abs‘𝐶))) |
112 | 79, 110, 79, 107, 111 | div2subd 11801 |
. . . . 5
⊢ (𝜑 → ((1 − (((2 ·
𝑁) ·
(abs‘𝐶))↑𝐽)) / (1 − ((2 ·
𝑁) ·
(abs‘𝐶)))) = (((((2
· 𝑁) ·
(abs‘𝐶))↑𝐽) − 1) / (((2 ·
𝑁) ·
(abs‘𝐶)) −
1))) |
113 | 109, 112 | eqtrd 2780 |
. . . 4
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐽 − 1))(((2 · 𝑁) · (abs‘𝐶))↑𝑖) = (((((2 · 𝑁) · (abs‘𝐶))↑𝐽) − 1) / (((2 · 𝑁) · (abs‘𝐶)) − 1))) |
114 | 106, 113 | oveq12d 7289 |
. . 3
⊢ (𝜑 → ((abs‘(𝐵 − 𝐴)) · Σ𝑖 ∈ (0...(𝐽 − 1))(((2 · 𝑁) · (abs‘𝐶))↑𝑖)) = ((((2 · 𝑁)↑-𝐽) / 2) · (((((2 · 𝑁) · (abs‘𝐶))↑𝐽) − 1) / (((2 · 𝑁) · (abs‘𝐶)) −
1)))) |
115 | 113, 40 | eqeltrrd 2842 |
. . . . 5
⊢ (𝜑 → (((((2 · 𝑁) · (abs‘𝐶))↑𝐽) − 1) / (((2 · 𝑁) · (abs‘𝐶)) − 1)) ∈
ℝ) |
116 | 35, 6 | reexpcld 13879 |
. . . . . 6
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶))↑𝐽) ∈ ℝ) |
117 | 116, 47, 57 | redivcld 11803 |
. . . . 5
⊢ (𝜑 → ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) / (((2 · 𝑁) · (abs‘𝐶)) − 1)) ∈
ℝ) |
118 | | 2rp 12734 |
. . . . . . 7
⊢ 2 ∈
ℝ+ |
119 | 118 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 2 ∈
ℝ+) |
120 | 119 | rpgt0d 12774 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < 2) |
121 | 29, 31, 120, 66 | mulgt0d 11130 |
. . . . . . . . 9
⊢ (𝜑 → 0 < (2 · 𝑁)) |
122 | 32, 71, 121 | 3jca 1127 |
. . . . . . . 8
⊢ (𝜑 → ((2 · 𝑁) ∈ ℝ ∧ -𝐽 ∈ ℤ ∧ 0 < (2
· 𝑁))) |
123 | | expgt0 13814 |
. . . . . . . 8
⊢ (((2
· 𝑁) ∈ ℝ
∧ -𝐽 ∈ ℤ
∧ 0 < (2 · 𝑁)) → 0 < ((2 · 𝑁)↑-𝐽)) |
124 | 122, 123 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 0 < ((2 · 𝑁)↑-𝐽)) |
125 | 48, 72, 124 | ltled 11123 |
. . . . . 6
⊢ (𝜑 → 0 ≤ ((2 · 𝑁)↑-𝐽)) |
126 | 72, 119, 125 | divge0d 12811 |
. . . . 5
⊢ (𝜑 → 0 ≤ (((2 · 𝑁)↑-𝐽) / 2)) |
127 | 116, 46 | resubcld 11403 |
. . . . . 6
⊢ (𝜑 → ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) − 1) ∈
ℝ) |
128 | 47, 54 | elrpd 12768 |
. . . . . 6
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶)) − 1) ∈
ℝ+) |
129 | 116 | lem1d 11908 |
. . . . . 6
⊢ (𝜑 → ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) − 1) ≤ (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) |
130 | 127, 116,
128, 129 | lediv1dd 12829 |
. . . . 5
⊢ (𝜑 → (((((2 · 𝑁) · (abs‘𝐶))↑𝐽) − 1) / (((2 · 𝑁) · (abs‘𝐶)) − 1)) ≤ ((((2
· 𝑁) ·
(abs‘𝐶))↑𝐽) / (((2 · 𝑁) · (abs‘𝐶)) − 1))) |
131 | 115, 117,
73, 126, 130 | lemul2ad 11915 |
. . . 4
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · (((((2 · 𝑁) · (abs‘𝐶))↑𝐽) − 1) / (((2 · 𝑁) · (abs‘𝐶)) − 1))) ≤ ((((2
· 𝑁)↑-𝐽) / 2) · ((((2 ·
𝑁) ·
(abs‘𝐶))↑𝐽) / (((2 · 𝑁) · (abs‘𝐶)) −
1)))) |
132 | 47 | recnd 11004 |
. . . . . . 7
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶)) − 1) ∈
ℂ) |
133 | 110, 132,
57 | divrecd 11754 |
. . . . . 6
⊢ (𝜑 → ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) / (((2 · 𝑁) · (abs‘𝐶)) − 1)) = ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) · (1 / (((2 · 𝑁) · (abs‘𝐶)) −
1)))) |
134 | 133 | oveq2d 7287 |
. . . . 5
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) / (((2 · 𝑁) · (abs‘𝐶)) − 1))) = ((((2 · 𝑁)↑-𝐽) / 2) · ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) · (1 / (((2 · 𝑁) · (abs‘𝐶)) −
1))))) |
135 | 58 | recnd 11004 |
. . . . . . 7
⊢ (𝜑 → (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)) ∈
ℂ) |
136 | 74, 110, 135 | mulassd 10999 |
. . . . . 6
⊢ (𝜑 → (((((2 · 𝑁)↑-𝐽) / 2) · (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) · (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1))) = ((((2 ·
𝑁)↑-𝐽) / 2) · ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) · (1 / (((2 · 𝑁) · (abs‘𝐶)) −
1))))) |
137 | 136 | eqcomd 2746 |
. . . . 5
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) · (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)))) = (((((2
· 𝑁)↑-𝐽) / 2) · (((2 ·
𝑁) ·
(abs‘𝐶))↑𝐽)) · (1 / (((2 ·
𝑁) ·
(abs‘𝐶)) −
1)))) |
138 | 86, 110, 62, 44 | div23d 11788 |
. . . . . . . 8
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) · (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) / 2) = ((((2 · 𝑁)↑-𝐽) / 2) · (((2 · 𝑁) · (abs‘𝐶))↑𝐽))) |
139 | 138 | eqcomd 2746 |
. . . . . . 7
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) = ((((2 · 𝑁)↑-𝐽) · (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) / 2)) |
140 | 88, 70 | jca 512 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · 𝑁) ∈ ℂ ∧ (2
· 𝑁) ≠
0)) |
141 | 34 | recnd 11004 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (abs‘𝐶) ∈
ℂ) |
142 | 12, 5, 51 | knoppndvlem13 34700 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ≠ 0) |
143 | 33, 142 | absne0d 15157 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (abs‘𝐶) ≠ 0) |
144 | 141, 143 | jca 512 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((abs‘𝐶) ∈ ℂ ∧
(abs‘𝐶) ≠
0)) |
145 | 140, 144,
7 | 3jca 1127 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2 · 𝑁) ∈ ℂ ∧ (2
· 𝑁) ≠ 0) ∧
((abs‘𝐶) ∈
ℂ ∧ (abs‘𝐶)
≠ 0) ∧ 𝐽 ∈
ℤ)) |
146 | | mulexpz 13821 |
. . . . . . . . . . 11
⊢ ((((2
· 𝑁) ∈ ℂ
∧ (2 · 𝑁) ≠
0) ∧ ((abs‘𝐶)
∈ ℂ ∧ (abs‘𝐶) ≠ 0) ∧ 𝐽 ∈ ℤ) → (((2 · 𝑁) · (abs‘𝐶))↑𝐽) = (((2 · 𝑁)↑𝐽) · ((abs‘𝐶)↑𝐽))) |
147 | 145, 146 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶))↑𝐽) = (((2 · 𝑁)↑𝐽) · ((abs‘𝐶)↑𝐽))) |
148 | 147 | oveq2d 7287 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) · (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) = (((2 · 𝑁)↑-𝐽) · (((2 · 𝑁)↑𝐽) · ((abs‘𝐶)↑𝐽)))) |
149 | 88, 6 | expcld 13862 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 · 𝑁)↑𝐽) ∈ ℂ) |
150 | 42 | recnd 11004 |
. . . . . . . . . . 11
⊢ (𝜑 → ((abs‘𝐶)↑𝐽) ∈ ℂ) |
151 | 86, 149, 150 | mulassd 10999 |
. . . . . . . . . 10
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) · ((2 · 𝑁)↑𝐽)) · ((abs‘𝐶)↑𝐽)) = (((2 · 𝑁)↑-𝐽) · (((2 · 𝑁)↑𝐽) · ((abs‘𝐶)↑𝐽)))) |
152 | 151 | eqcomd 2746 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) · (((2 · 𝑁)↑𝐽) · ((abs‘𝐶)↑𝐽))) = ((((2 · 𝑁)↑-𝐽) · ((2 · 𝑁)↑𝐽)) · ((abs‘𝐶)↑𝐽))) |
153 | 140, 71, 7 | jca32 516 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((2 · 𝑁) ∈ ℂ ∧ (2
· 𝑁) ≠ 0) ∧
(-𝐽 ∈ ℤ ∧
𝐽 ∈
ℤ))) |
154 | | expaddz 13825 |
. . . . . . . . . . . . . 14
⊢ ((((2
· 𝑁) ∈ ℂ
∧ (2 · 𝑁) ≠
0) ∧ (-𝐽 ∈ ℤ
∧ 𝐽 ∈ ℤ))
→ ((2 · 𝑁)↑(-𝐽 + 𝐽)) = (((2 · 𝑁)↑-𝐽) · ((2 · 𝑁)↑𝐽))) |
155 | 153, 154 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2 · 𝑁)↑(-𝐽 + 𝐽)) = (((2 · 𝑁)↑-𝐽) · ((2 · 𝑁)↑𝐽))) |
156 | 155 | eqcomd 2746 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) · ((2 · 𝑁)↑𝐽)) = ((2 · 𝑁)↑(-𝐽 + 𝐽))) |
157 | 71 | zcnd 12426 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → -𝐽 ∈ ℂ) |
158 | 6 | nn0cnd 12295 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐽 ∈ ℂ) |
159 | 157, 158 | addcomd 11177 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (-𝐽 + 𝐽) = (𝐽 + -𝐽)) |
160 | 158 | negidd 11322 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐽 + -𝐽) = 0) |
161 | 159, 160 | eqtrd 2780 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (-𝐽 + 𝐽) = 0) |
162 | 161 | oveq2d 7287 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · 𝑁)↑(-𝐽 + 𝐽)) = ((2 · 𝑁)↑0)) |
163 | 88 | exp0d 13856 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · 𝑁)↑0) = 1) |
164 | 156, 162,
163 | 3eqtrd 2784 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) · ((2 · 𝑁)↑𝐽)) = 1) |
165 | 164 | oveq1d 7286 |
. . . . . . . . . 10
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) · ((2 · 𝑁)↑𝐽)) · ((abs‘𝐶)↑𝐽)) = (1 · ((abs‘𝐶)↑𝐽))) |
166 | 150 | mulid2d 10994 |
. . . . . . . . . 10
⊢ (𝜑 → (1 ·
((abs‘𝐶)↑𝐽)) = ((abs‘𝐶)↑𝐽)) |
167 | 165, 166 | eqtrd 2780 |
. . . . . . . . 9
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) · ((2 · 𝑁)↑𝐽)) · ((abs‘𝐶)↑𝐽)) = ((abs‘𝐶)↑𝐽)) |
168 | 148, 152,
167 | 3eqtrd 2784 |
. . . . . . . 8
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) · (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) = ((abs‘𝐶)↑𝐽)) |
169 | 168 | oveq1d 7286 |
. . . . . . 7
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) · (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) / 2) = (((abs‘𝐶)↑𝐽) / 2)) |
170 | 139, 169 | eqtrd 2780 |
. . . . . 6
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) = (((abs‘𝐶)↑𝐽) / 2)) |
171 | 170 | oveq1d 7286 |
. . . . 5
⊢ (𝜑 → (((((2 · 𝑁)↑-𝐽) / 2) · (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) · (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1))) =
((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) |
172 | 134, 137,
171 | 3eqtrd 2784 |
. . . 4
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) / (((2 · 𝑁) · (abs‘𝐶)) − 1))) = ((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2 · 𝑁) · (abs‘𝐶)) −
1)))) |
173 | 131, 172 | breqtrd 5105 |
. . 3
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · (((((2 · 𝑁) · (abs‘𝐶))↑𝐽) − 1) / (((2 · 𝑁) · (abs‘𝐶)) − 1))) ≤
((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) |
174 | 114, 173 | eqbrtrd 5101 |
. 2
⊢ (𝜑 → ((abs‘(𝐵 − 𝐴)) · Σ𝑖 ∈ (0...(𝐽 − 1))(((2 · 𝑁) · (abs‘𝐶))↑𝑖)) ≤ ((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2 · 𝑁) · (abs‘𝐶)) −
1)))) |
175 | 23, 41, 59, 60, 174 | letrd 11132 |
1
⊢ (𝜑 → (abs‘(Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖))) ≤ ((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2 · 𝑁) · (abs‘𝐶)) −
1)))) |