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 12641 | . . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ ℤ) | 
| 8 |  | knoppndvlem14.m | . . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 9 | 8 | peano2zd 12727 | . . . . . . . 8
⊢ (𝜑 → (𝑀 + 1) ∈ ℤ) | 
| 10 | 5, 7, 9 | knoppndvlem1 36514 | . . . . . . 7
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1)) ∈ ℝ) | 
| 11 | 4, 10 | eqeltrd 2840 | . . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 12 |  | knoppndvlem14.c | . . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) | 
| 13 | 12 | knoppndvlem3 36516 | . . . . . . 7
⊢ (𝜑 → (𝐶 ∈ ℝ ∧ (abs‘𝐶) < 1)) | 
| 14 | 13 | simpld 494 | . . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 15 | 1, 2, 11, 14, 5 | knoppndvlem5 36518 | . . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) ∈ ℝ) | 
| 16 |  | knoppndvlem14.a | . . . . . . . 8
⊢ 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀) | 
| 17 | 16 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀)) | 
| 18 | 5, 7, 8 | knoppndvlem1 36514 | . . . . . . 7
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀) ∈ ℝ) | 
| 19 | 17, 18 | eqeltrd 2840 | . . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 20 | 1, 2, 19, 14, 5 | knoppndvlem5 36518 | . . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖) ∈ ℝ) | 
| 21 | 15, 20 | resubcld 11692 | . . . 4
⊢ (𝜑 → (Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖)) ∈ ℝ) | 
| 22 | 21 | recnd 11290 | . . 3
⊢ (𝜑 → (Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖)) ∈ ℂ) | 
| 23 | 22 | abscld 15476 | . 2
⊢ (𝜑 → (abs‘(Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖))) ∈ ℝ) | 
| 24 | 11, 19 | resubcld 11692 | . . . . 5
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) | 
| 25 | 24 | recnd 11290 | . . . 4
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℂ) | 
| 26 | 25 | abscld 15476 | . . 3
⊢ (𝜑 → (abs‘(𝐵 − 𝐴)) ∈ ℝ) | 
| 27 |  | fzfid 14015 | . . . 4
⊢ (𝜑 → (0...(𝐽 − 1)) ∈ Fin) | 
| 28 |  | 2re 12341 | . . . . . . . . 9
⊢ 2 ∈
ℝ | 
| 29 | 28 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 2 ∈
ℝ) | 
| 30 |  | nnre 12274 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) | 
| 31 | 5, 30 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 32 | 29, 31 | remulcld 11292 | . . . . . . 7
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ) | 
| 33 | 14 | recnd 11290 | . . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 34 | 33 | abscld 15476 | . . . . . . 7
⊢ (𝜑 → (abs‘𝐶) ∈
ℝ) | 
| 35 | 32, 34 | remulcld 11292 | . . . . . 6
⊢ (𝜑 → ((2 · 𝑁) · (abs‘𝐶)) ∈
ℝ) | 
| 36 | 35 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐽 − 1))) → ((2 · 𝑁) · (abs‘𝐶)) ∈
ℝ) | 
| 37 |  | elfznn0 13661 | . . . . . 6
⊢ (𝑖 ∈ (0...(𝐽 − 1)) → 𝑖 ∈ ℕ0) | 
| 38 | 37 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐽 − 1))) → 𝑖 ∈ ℕ0) | 
| 39 | 36, 38 | reexpcld 14204 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐽 − 1))) → (((2 · 𝑁) · (abs‘𝐶))↑𝑖) ∈ ℝ) | 
| 40 | 27, 39 | fsumrecl 15771 | . . 3
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐽 − 1))(((2 · 𝑁) · (abs‘𝐶))↑𝑖) ∈ ℝ) | 
| 41 | 26, 40 | remulcld 11292 | . 2
⊢ (𝜑 → ((abs‘(𝐵 − 𝐴)) · Σ𝑖 ∈ (0...(𝐽 − 1))(((2 · 𝑁) · (abs‘𝐶))↑𝑖)) ∈ ℝ) | 
| 42 | 34, 6 | reexpcld 14204 | . . . 4
⊢ (𝜑 → ((abs‘𝐶)↑𝐽) ∈ ℝ) | 
| 43 |  | 2ne0 12371 | . . . . 5
⊢ 2 ≠
0 | 
| 44 | 43 | a1i 11 | . . . 4
⊢ (𝜑 → 2 ≠ 0) | 
| 45 | 42, 29, 44 | redivcld 12096 | . . 3
⊢ (𝜑 → (((abs‘𝐶)↑𝐽) / 2) ∈ ℝ) | 
| 46 |  | 1red 11263 | . . . 4
⊢ (𝜑 → 1 ∈
ℝ) | 
| 47 | 35, 46 | resubcld 11692 | . . . 4
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶)) − 1) ∈
ℝ) | 
| 48 |  | 0red 11265 | . . . . . 6
⊢ (𝜑 → 0 ∈
ℝ) | 
| 49 |  | 0lt1 11786 | . . . . . . . 8
⊢ 0 <
1 | 
| 50 | 49 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 0 < 1) | 
| 51 |  | knoppndvlem14.1 | . . . . . . . . 9
⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶))) | 
| 52 | 12, 5, 51 | knoppndvlem12 36525 | . . . . . . . 8
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶)) ≠ 1 ∧ 1 < (((2
· 𝑁) ·
(abs‘𝐶)) −
1))) | 
| 53 | 52 | simprd 495 | . . . . . . 7
⊢ (𝜑 → 1 < (((2 · 𝑁) · (abs‘𝐶)) − 1)) | 
| 54 | 48, 46, 47, 50, 53 | lttrd 11423 | . . . . . 6
⊢ (𝜑 → 0 < (((2 · 𝑁) · (abs‘𝐶)) − 1)) | 
| 55 | 48, 54 | jca 511 | . . . . 5
⊢ (𝜑 → (0 ∈ ℝ ∧ 0
< (((2 · 𝑁)
· (abs‘𝐶))
− 1))) | 
| 56 |  | ltne 11359 | . . . . 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 12096 | . . 3
⊢ (𝜑 → (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)) ∈
ℝ) | 
| 59 | 45, 58 | remulcld 11292 | . 2
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1))) ∈
ℝ) | 
| 60 | 1, 2, 19, 11, 12, 6, 5 | knoppndvlem11 36524 | . 2
⊢ (𝜑 → (abs‘(Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖))) ≤ ((abs‘(𝐵 − 𝐴)) · Σ𝑖 ∈ (0...(𝐽 − 1))(((2 · 𝑁) · (abs‘𝐶))↑𝑖))) | 
| 61 | 4, 17 | oveq12d 7450 | . . . . . . 7
⊢ (𝜑 → (𝐵 − 𝐴) = (((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1)) − ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀))) | 
| 62 | 29 | recnd 11290 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ∈
ℂ) | 
| 63 | 31 | recnd 11290 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 64 |  | nnge1 12295 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 1 ≤
𝑁) | 
| 65 | 5, 64 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ≤ 𝑁) | 
| 66 | 48, 46, 31, 50, 65 | ltletrd 11422 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 < 𝑁) | 
| 67 | 48, 66 | jca 511 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (0 ∈ ℝ ∧ 0
< 𝑁)) | 
| 68 |  | ltne 11359 | . . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ 0 < 𝑁) → 𝑁 ≠ 0) | 
| 69 | 67, 68 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ≠ 0) | 
| 70 | 62, 63, 44, 69 | mulne0d 11916 | . . . . . . . . . . . . 13
⊢ (𝜑 → (2 · 𝑁) ≠ 0) | 
| 71 | 7 | znegcld 12726 | . . . . . . . . . . . . 13
⊢ (𝜑 → -𝐽 ∈ ℤ) | 
| 72 | 32, 70, 71 | reexpclzd 14289 | . . . . . . . . . . . 12
⊢ (𝜑 → ((2 · 𝑁)↑-𝐽) ∈ ℝ) | 
| 73 | 72, 29, 44 | redivcld 12096 | . . . . . . . . . . 11
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) / 2) ∈ ℝ) | 
| 74 | 73 | recnd 11290 | . . . . . . . . . 10
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) / 2) ∈ ℂ) | 
| 75 | 9 | zcnd 12725 | . . . . . . . . . 10
⊢ (𝜑 → (𝑀 + 1) ∈ ℂ) | 
| 76 | 8 | zcnd 12725 | . . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℂ) | 
| 77 | 74, 75, 76 | subdid 11720 | . . . . . . . . 9
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · ((𝑀 + 1) − 𝑀)) = (((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1)) − ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀))) | 
| 78 | 77 | eqcomd 2742 | . . . . . . . 8
⊢ (𝜑 → (((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1)) − ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀)) = ((((2 · 𝑁)↑-𝐽) / 2) · ((𝑀 + 1) − 𝑀))) | 
| 79 |  | 1cnd 11257 | . . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℂ) | 
| 80 | 76, 79 | pncan2d 11623 | . . . . . . . . 9
⊢ (𝜑 → ((𝑀 + 1) − 𝑀) = 1) | 
| 81 | 80 | oveq2d 7448 | . . . . . . . 8
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · ((𝑀 + 1) − 𝑀)) = ((((2 · 𝑁)↑-𝐽) / 2) · 1)) | 
| 82 | 74 | mulridd 11279 | . . . . . . . 8
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · 1) = (((2 · 𝑁)↑-𝐽) / 2)) | 
| 83 | 78, 81, 82 | 3eqtrd 2780 | . . . . . . 7
⊢ (𝜑 → (((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1)) − ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀)) = (((2 · 𝑁)↑-𝐽) / 2)) | 
| 84 | 61, 83 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 → (𝐵 − 𝐴) = (((2 · 𝑁)↑-𝐽) / 2)) | 
| 85 | 84 | fveq2d 6909 | . . . . 5
⊢ (𝜑 → (abs‘(𝐵 − 𝐴)) = (abs‘(((2 · 𝑁)↑-𝐽) / 2))) | 
| 86 | 72 | recnd 11290 | . . . . . . 7
⊢ (𝜑 → ((2 · 𝑁)↑-𝐽) ∈ ℂ) | 
| 87 | 86, 62, 44 | absdivd 15495 | . . . . . 6
⊢ (𝜑 → (abs‘(((2 ·
𝑁)↑-𝐽) / 2)) = ((abs‘((2 · 𝑁)↑-𝐽)) / (abs‘2))) | 
| 88 | 62, 63 | mulcld 11282 | . . . . . . . . . 10
⊢ (𝜑 → (2 · 𝑁) ∈
ℂ) | 
| 89 | 88, 70, 71 | 3jca 1128 | . . . . . . . . 9
⊢ (𝜑 → ((2 · 𝑁) ∈ ℂ ∧ (2
· 𝑁) ≠ 0 ∧
-𝐽 ∈
ℤ)) | 
| 90 |  | absexpz 15345 | . . . . . . . . 9
⊢ (((2
· 𝑁) ∈ ℂ
∧ (2 · 𝑁) ≠ 0
∧ -𝐽 ∈ ℤ)
→ (abs‘((2 · 𝑁)↑-𝐽)) = ((abs‘(2 · 𝑁))↑-𝐽)) | 
| 91 | 89, 90 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (abs‘((2 ·
𝑁)↑-𝐽)) = ((abs‘(2 · 𝑁))↑-𝐽)) | 
| 92 | 62, 63 | absmuld 15494 | . . . . . . . . . 10
⊢ (𝜑 → (abs‘(2 ·
𝑁)) = ((abs‘2)
· (abs‘𝑁))) | 
| 93 |  | 0le2 12369 | . . . . . . . . . . . . . 14
⊢ 0 ≤
2 | 
| 94 | 28, 93 | pm3.2i 470 | . . . . . . . . . . . . 13
⊢ (2 ∈
ℝ ∧ 0 ≤ 2) | 
| 95 |  | absid 15336 | . . . . . . . . . . . . 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 11410 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ 𝑁) | 
| 99 | 31, 98 | absidd 15462 | . . . . . . . . . . 11
⊢ (𝜑 → (abs‘𝑁) = 𝑁) | 
| 100 | 97, 99 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝜑 → ((abs‘2) ·
(abs‘𝑁)) = (2
· 𝑁)) | 
| 101 | 92, 100 | eqtrd 2776 | . . . . . . . . 9
⊢ (𝜑 → (abs‘(2 ·
𝑁)) = (2 · 𝑁)) | 
| 102 | 101 | oveq1d 7447 | . . . . . . . 8
⊢ (𝜑 → ((abs‘(2 ·
𝑁))↑-𝐽) = ((2 · 𝑁)↑-𝐽)) | 
| 103 | 91, 102 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → (abs‘((2 ·
𝑁)↑-𝐽)) = ((2 · 𝑁)↑-𝐽)) | 
| 104 | 103, 97 | oveq12d 7450 | . . . . . 6
⊢ (𝜑 → ((abs‘((2 ·
𝑁)↑-𝐽)) / (abs‘2)) = (((2 · 𝑁)↑-𝐽) / 2)) | 
| 105 | 87, 104 | eqtrd 2776 | . . . . 5
⊢ (𝜑 → (abs‘(((2 ·
𝑁)↑-𝐽) / 2)) = (((2 · 𝑁)↑-𝐽) / 2)) | 
| 106 | 85, 105 | eqtrd 2776 | . . . 4
⊢ (𝜑 → (abs‘(𝐵 − 𝐴)) = (((2 · 𝑁)↑-𝐽) / 2)) | 
| 107 | 35 | recnd 11290 | . . . . . 6
⊢ (𝜑 → ((2 · 𝑁) · (abs‘𝐶)) ∈
ℂ) | 
| 108 | 52 | simpld 494 | . . . . . 6
⊢ (𝜑 → ((2 · 𝑁) · (abs‘𝐶)) ≠ 1) | 
| 109 | 107, 108,
6 | geoser 15904 | . . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐽 − 1))(((2 · 𝑁) · (abs‘𝐶))↑𝑖) = ((1 − (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) / (1 − ((2 · 𝑁) · (abs‘𝐶))))) | 
| 110 | 107, 6 | expcld 14187 | . . . . . 6
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶))↑𝐽) ∈ ℂ) | 
| 111 | 108 | necomd 2995 | . . . . . 6
⊢ (𝜑 → 1 ≠ ((2 · 𝑁) · (abs‘𝐶))) | 
| 112 | 79, 110, 79, 107, 111 | div2subd 12094 | . . . . 5
⊢ (𝜑 → ((1 − (((2 ·
𝑁) ·
(abs‘𝐶))↑𝐽)) / (1 − ((2 ·
𝑁) ·
(abs‘𝐶)))) = (((((2
· 𝑁) ·
(abs‘𝐶))↑𝐽) − 1) / (((2 ·
𝑁) ·
(abs‘𝐶)) −
1))) | 
| 113 | 109, 112 | eqtrd 2776 | . . . 4
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐽 − 1))(((2 · 𝑁) · (abs‘𝐶))↑𝑖) = (((((2 · 𝑁) · (abs‘𝐶))↑𝐽) − 1) / (((2 · 𝑁) · (abs‘𝐶)) − 1))) | 
| 114 | 106, 113 | oveq12d 7450 | . . 3
⊢ (𝜑 → ((abs‘(𝐵 − 𝐴)) · Σ𝑖 ∈ (0...(𝐽 − 1))(((2 · 𝑁) · (abs‘𝐶))↑𝑖)) = ((((2 · 𝑁)↑-𝐽) / 2) · (((((2 · 𝑁) · (abs‘𝐶))↑𝐽) − 1) / (((2 · 𝑁) · (abs‘𝐶)) −
1)))) | 
| 115 | 113, 40 | eqeltrrd 2841 | . . . . 5
⊢ (𝜑 → (((((2 · 𝑁) · (abs‘𝐶))↑𝐽) − 1) / (((2 · 𝑁) · (abs‘𝐶)) − 1)) ∈
ℝ) | 
| 116 | 35, 6 | reexpcld 14204 | . . . . . 6
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶))↑𝐽) ∈ ℝ) | 
| 117 | 116, 47, 57 | redivcld 12096 | . . . . 5
⊢ (𝜑 → ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) / (((2 · 𝑁) · (abs‘𝐶)) − 1)) ∈
ℝ) | 
| 118 |  | 2rp 13040 | . . . . . . 7
⊢ 2 ∈
ℝ+ | 
| 119 | 118 | a1i 11 | . . . . . 6
⊢ (𝜑 → 2 ∈
ℝ+) | 
| 120 | 119 | rpgt0d 13081 | . . . . . . . . . 10
⊢ (𝜑 → 0 < 2) | 
| 121 | 29, 31, 120, 66 | mulgt0d 11417 | . . . . . . . . 9
⊢ (𝜑 → 0 < (2 · 𝑁)) | 
| 122 | 32, 71, 121 | 3jca 1128 | . . . . . . . 8
⊢ (𝜑 → ((2 · 𝑁) ∈ ℝ ∧ -𝐽 ∈ ℤ ∧ 0 < (2
· 𝑁))) | 
| 123 |  | expgt0 14137 | . . . . . . . 8
⊢ (((2
· 𝑁) ∈ ℝ
∧ -𝐽 ∈ ℤ
∧ 0 < (2 · 𝑁)) → 0 < ((2 · 𝑁)↑-𝐽)) | 
| 124 | 122, 123 | syl 17 | . . . . . . 7
⊢ (𝜑 → 0 < ((2 · 𝑁)↑-𝐽)) | 
| 125 | 48, 72, 124 | ltled 11410 | . . . . . 6
⊢ (𝜑 → 0 ≤ ((2 · 𝑁)↑-𝐽)) | 
| 126 | 72, 119, 125 | divge0d 13118 | . . . . 5
⊢ (𝜑 → 0 ≤ (((2 · 𝑁)↑-𝐽) / 2)) | 
| 127 | 116, 46 | resubcld 11692 | . . . . . 6
⊢ (𝜑 → ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) − 1) ∈
ℝ) | 
| 128 | 47, 54 | elrpd 13075 | . . . . . 6
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶)) − 1) ∈
ℝ+) | 
| 129 | 116 | lem1d 12202 | . . . . . 6
⊢ (𝜑 → ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) − 1) ≤ (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) | 
| 130 | 127, 116,
128, 129 | lediv1dd 13136 | . . . . 5
⊢ (𝜑 → (((((2 · 𝑁) · (abs‘𝐶))↑𝐽) − 1) / (((2 · 𝑁) · (abs‘𝐶)) − 1)) ≤ ((((2
· 𝑁) ·
(abs‘𝐶))↑𝐽) / (((2 · 𝑁) · (abs‘𝐶)) − 1))) | 
| 131 | 115, 117,
73, 126, 130 | lemul2ad 12209 | . . . 4
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · (((((2 · 𝑁) · (abs‘𝐶))↑𝐽) − 1) / (((2 · 𝑁) · (abs‘𝐶)) − 1))) ≤ ((((2
· 𝑁)↑-𝐽) / 2) · ((((2 ·
𝑁) ·
(abs‘𝐶))↑𝐽) / (((2 · 𝑁) · (abs‘𝐶)) −
1)))) | 
| 132 | 47 | recnd 11290 | . . . . . . 7
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶)) − 1) ∈
ℂ) | 
| 133 | 110, 132,
57 | divrecd 12047 | . . . . . 6
⊢ (𝜑 → ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) / (((2 · 𝑁) · (abs‘𝐶)) − 1)) = ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) · (1 / (((2 · 𝑁) · (abs‘𝐶)) −
1)))) | 
| 134 | 133 | oveq2d 7448 | . . . . 5
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) / (((2 · 𝑁) · (abs‘𝐶)) − 1))) = ((((2 · 𝑁)↑-𝐽) / 2) · ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) · (1 / (((2 · 𝑁) · (abs‘𝐶)) −
1))))) | 
| 135 | 58 | recnd 11290 | . . . . . . 7
⊢ (𝜑 → (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)) ∈
ℂ) | 
| 136 | 74, 110, 135 | mulassd 11285 | . . . . . 6
⊢ (𝜑 → (((((2 · 𝑁)↑-𝐽) / 2) · (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) · (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1))) = ((((2 ·
𝑁)↑-𝐽) / 2) · ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) · (1 / (((2 · 𝑁) · (abs‘𝐶)) −
1))))) | 
| 137 | 136 | eqcomd 2742 | . . . . 5
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) · (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)))) = (((((2
· 𝑁)↑-𝐽) / 2) · (((2 ·
𝑁) ·
(abs‘𝐶))↑𝐽)) · (1 / (((2 ·
𝑁) ·
(abs‘𝐶)) −
1)))) | 
| 138 | 86, 110, 62, 44 | div23d 12081 | . . . . . . . 8
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) · (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) / 2) = ((((2 · 𝑁)↑-𝐽) / 2) · (((2 · 𝑁) · (abs‘𝐶))↑𝐽))) | 
| 139 | 138 | eqcomd 2742 | . . . . . . 7
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) = ((((2 · 𝑁)↑-𝐽) · (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) / 2)) | 
| 140 | 88, 70 | jca 511 | . . . . . . . . . . . 12
⊢ (𝜑 → ((2 · 𝑁) ∈ ℂ ∧ (2
· 𝑁) ≠
0)) | 
| 141 | 34 | recnd 11290 | . . . . . . . . . . . . 13
⊢ (𝜑 → (abs‘𝐶) ∈
ℂ) | 
| 142 | 12, 5, 51 | knoppndvlem13 36526 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ≠ 0) | 
| 143 | 33, 142 | absne0d 15487 | . . . . . . . . . . . . 13
⊢ (𝜑 → (abs‘𝐶) ≠ 0) | 
| 144 | 141, 143 | jca 511 | . . . . . . . . . . . 12
⊢ (𝜑 → ((abs‘𝐶) ∈ ℂ ∧
(abs‘𝐶) ≠
0)) | 
| 145 | 140, 144,
7 | 3jca 1128 | . . . . . . . . . . 11
⊢ (𝜑 → (((2 · 𝑁) ∈ ℂ ∧ (2
· 𝑁) ≠ 0) ∧
((abs‘𝐶) ∈
ℂ ∧ (abs‘𝐶)
≠ 0) ∧ 𝐽 ∈
ℤ)) | 
| 146 |  | mulexpz 14144 | . . . . . . . . . . 11
⊢ ((((2
· 𝑁) ∈ ℂ
∧ (2 · 𝑁) ≠
0) ∧ ((abs‘𝐶)
∈ ℂ ∧ (abs‘𝐶) ≠ 0) ∧ 𝐽 ∈ ℤ) → (((2 · 𝑁) · (abs‘𝐶))↑𝐽) = (((2 · 𝑁)↑𝐽) · ((abs‘𝐶)↑𝐽))) | 
| 147 | 145, 146 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶))↑𝐽) = (((2 · 𝑁)↑𝐽) · ((abs‘𝐶)↑𝐽))) | 
| 148 | 147 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) · (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) = (((2 · 𝑁)↑-𝐽) · (((2 · 𝑁)↑𝐽) · ((abs‘𝐶)↑𝐽)))) | 
| 149 | 88, 6 | expcld 14187 | . . . . . . . . . . 11
⊢ (𝜑 → ((2 · 𝑁)↑𝐽) ∈ ℂ) | 
| 150 | 42 | recnd 11290 | . . . . . . . . . . 11
⊢ (𝜑 → ((abs‘𝐶)↑𝐽) ∈ ℂ) | 
| 151 | 86, 149, 150 | mulassd 11285 | . . . . . . . . . 10
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) · ((2 · 𝑁)↑𝐽)) · ((abs‘𝐶)↑𝐽)) = (((2 · 𝑁)↑-𝐽) · (((2 · 𝑁)↑𝐽) · ((abs‘𝐶)↑𝐽)))) | 
| 152 | 151 | eqcomd 2742 | . . . . . . . . 9
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) · (((2 · 𝑁)↑𝐽) · ((abs‘𝐶)↑𝐽))) = ((((2 · 𝑁)↑-𝐽) · ((2 · 𝑁)↑𝐽)) · ((abs‘𝐶)↑𝐽))) | 
| 153 | 140, 71, 7 | jca32 515 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((2 · 𝑁) ∈ ℂ ∧ (2
· 𝑁) ≠ 0) ∧
(-𝐽 ∈ ℤ ∧
𝐽 ∈
ℤ))) | 
| 154 |  | expaddz 14148 | . . . . . . . . . . . . . 14
⊢ ((((2
· 𝑁) ∈ ℂ
∧ (2 · 𝑁) ≠
0) ∧ (-𝐽 ∈ ℤ
∧ 𝐽 ∈ ℤ))
→ ((2 · 𝑁)↑(-𝐽 + 𝐽)) = (((2 · 𝑁)↑-𝐽) · ((2 · 𝑁)↑𝐽))) | 
| 155 | 153, 154 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((2 · 𝑁)↑(-𝐽 + 𝐽)) = (((2 · 𝑁)↑-𝐽) · ((2 · 𝑁)↑𝐽))) | 
| 156 | 155 | eqcomd 2742 | . . . . . . . . . . . 12
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) · ((2 · 𝑁)↑𝐽)) = ((2 · 𝑁)↑(-𝐽 + 𝐽))) | 
| 157 | 71 | zcnd 12725 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → -𝐽 ∈ ℂ) | 
| 158 | 6 | nn0cnd 12591 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐽 ∈ ℂ) | 
| 159 | 157, 158 | addcomd 11464 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (-𝐽 + 𝐽) = (𝐽 + -𝐽)) | 
| 160 | 158 | negidd 11611 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐽 + -𝐽) = 0) | 
| 161 | 159, 160 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ (𝜑 → (-𝐽 + 𝐽) = 0) | 
| 162 | 161 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝜑 → ((2 · 𝑁)↑(-𝐽 + 𝐽)) = ((2 · 𝑁)↑0)) | 
| 163 | 88 | exp0d 14181 | . . . . . . . . . . . 12
⊢ (𝜑 → ((2 · 𝑁)↑0) = 1) | 
| 164 | 156, 162,
163 | 3eqtrd 2780 | . . . . . . . . . . 11
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) · ((2 · 𝑁)↑𝐽)) = 1) | 
| 165 | 164 | oveq1d 7447 | . . . . . . . . . 10
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) · ((2 · 𝑁)↑𝐽)) · ((abs‘𝐶)↑𝐽)) = (1 · ((abs‘𝐶)↑𝐽))) | 
| 166 | 150 | mullidd 11280 | . . . . . . . . . 10
⊢ (𝜑 → (1 ·
((abs‘𝐶)↑𝐽)) = ((abs‘𝐶)↑𝐽)) | 
| 167 | 165, 166 | eqtrd 2776 | . . . . . . . . 9
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) · ((2 · 𝑁)↑𝐽)) · ((abs‘𝐶)↑𝐽)) = ((abs‘𝐶)↑𝐽)) | 
| 168 | 148, 152,
167 | 3eqtrd 2780 | . . . . . . . 8
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) · (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) = ((abs‘𝐶)↑𝐽)) | 
| 169 | 168 | oveq1d 7447 | . . . . . . 7
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) · (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) / 2) = (((abs‘𝐶)↑𝐽) / 2)) | 
| 170 | 139, 169 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) = (((abs‘𝐶)↑𝐽) / 2)) | 
| 171 | 170 | oveq1d 7447 | . . . . 5
⊢ (𝜑 → (((((2 · 𝑁)↑-𝐽) / 2) · (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) · (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1))) =
((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) | 
| 172 | 134, 137,
171 | 3eqtrd 2780 | . . . 4
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) / (((2 · 𝑁) · (abs‘𝐶)) − 1))) = ((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2 · 𝑁) · (abs‘𝐶)) −
1)))) | 
| 173 | 131, 172 | breqtrd 5168 | . . 3
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · (((((2 · 𝑁) · (abs‘𝐶))↑𝐽) − 1) / (((2 · 𝑁) · (abs‘𝐶)) − 1))) ≤
((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) | 
| 174 | 114, 173 | eqbrtrd 5164 | . 2
⊢ (𝜑 → ((abs‘(𝐵 − 𝐴)) · Σ𝑖 ∈ (0...(𝐽 − 1))(((2 · 𝑁) · (abs‘𝐶))↑𝑖)) ≤ ((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2 · 𝑁) · (abs‘𝐶)) −
1)))) | 
| 175 | 23, 41, 59, 60, 174 | letrd 11419 | 1
⊢ (𝜑 → (abs‘(Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖))) ≤ ((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2 · 𝑁) · (abs‘𝐶)) −
1)))) |