Proof of Theorem knoppndvlem15
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | knoppndvlem15.c | . . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) | 
| 2 | 1 | knoppndvlem3 36516 | . . . . . . . . . 10
⊢ (𝜑 → (𝐶 ∈ ℝ ∧ (abs‘𝐶) < 1)) | 
| 3 | 2 | simpld 494 | . . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 4 | 3 | recnd 11290 | . . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 5 | 4 | abscld 15476 | . . . . . . 7
⊢ (𝜑 → (abs‘𝐶) ∈
ℝ) | 
| 6 |  | knoppndvlem15.j | . . . . . . 7
⊢ (𝜑 → 𝐽 ∈
ℕ0) | 
| 7 | 5, 6 | reexpcld 14204 | . . . . . 6
⊢ (𝜑 → ((abs‘𝐶)↑𝐽) ∈ ℝ) | 
| 8 |  | 2re 12341 | . . . . . . 7
⊢ 2 ∈
ℝ | 
| 9 | 8 | a1i 11 | . . . . . 6
⊢ (𝜑 → 2 ∈
ℝ) | 
| 10 |  | 2ne0 12371 | . . . . . . 7
⊢ 2 ≠
0 | 
| 11 | 10 | a1i 11 | . . . . . 6
⊢ (𝜑 → 2 ≠ 0) | 
| 12 | 7, 9, 11 | redivcld 12096 | . . . . 5
⊢ (𝜑 → (((abs‘𝐶)↑𝐽) / 2) ∈ ℝ) | 
| 13 |  | 1red 11263 | . . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) | 
| 14 |  | knoppndvlem15.n | . . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 15 | 14 | nnred 12282 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 16 | 9, 15 | remulcld 11292 | . . . . . . . . 9
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ) | 
| 17 | 16, 5 | remulcld 11292 | . . . . . . . 8
⊢ (𝜑 → ((2 · 𝑁) · (abs‘𝐶)) ∈
ℝ) | 
| 18 | 17, 13 | resubcld 11692 | . . . . . . 7
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶)) − 1) ∈
ℝ) | 
| 19 |  | 0red 11265 | . . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℝ) | 
| 20 |  | 0lt1 11786 | . . . . . . . . . . 11
⊢ 0 <
1 | 
| 21 | 20 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → 0 < 1) | 
| 22 |  | knoppndvlem15.1 | . . . . . . . . . . . 12
⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶))) | 
| 23 | 1, 14, 22 | knoppndvlem12 36525 | . . . . . . . . . . 11
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶)) ≠ 1 ∧ 1 < (((2
· 𝑁) ·
(abs‘𝐶)) −
1))) | 
| 24 | 23 | simprd 495 | . . . . . . . . . 10
⊢ (𝜑 → 1 < (((2 · 𝑁) · (abs‘𝐶)) − 1)) | 
| 25 | 19, 13, 18, 21, 24 | lttrd 11423 | . . . . . . . . 9
⊢ (𝜑 → 0 < (((2 · 𝑁) · (abs‘𝐶)) − 1)) | 
| 26 | 18, 25 | jca 511 | . . . . . . . 8
⊢ (𝜑 → ((((2 · 𝑁) · (abs‘𝐶)) − 1) ∈ ℝ
∧ 0 < (((2 · 𝑁) · (abs‘𝐶)) − 1))) | 
| 27 |  | gt0ne0 11729 | . . . . . . . 8
⊢ (((((2
· 𝑁) ·
(abs‘𝐶)) − 1)
∈ ℝ ∧ 0 < (((2 · 𝑁) · (abs‘𝐶)) − 1)) → (((2 · 𝑁) · (abs‘𝐶)) − 1) ≠
0) | 
| 28 | 26, 27 | syl 17 | . . . . . . 7
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶)) − 1) ≠
0) | 
| 29 | 13, 18, 28 | redivcld 12096 | . . . . . 6
⊢ (𝜑 → (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)) ∈
ℝ) | 
| 30 | 13, 29 | resubcld 11692 | . . . . 5
⊢ (𝜑 → (1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) − 1)))
∈ ℝ) | 
| 31 | 12, 30 | remulcld 11292 | . . . 4
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) · (1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) ∈ ℝ) | 
| 32 |  | knoppndvlem15.t | . . . . . . . . 9
⊢ 𝑇 = (𝑥 ∈ ℝ ↦
(abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) | 
| 33 |  | knoppndvlem15.f | . . . . . . . . 9
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) | 
| 34 |  | knoppndvlem15.a | . . . . . . . . . . 11
⊢ 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀) | 
| 35 | 34 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀)) | 
| 36 | 6 | nn0zd 12641 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ ℤ) | 
| 37 |  | knoppndvlem15.m | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 38 | 14, 36, 37 | knoppndvlem1 36514 | . . . . . . . . . 10
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀) ∈ ℝ) | 
| 39 | 35, 38 | eqeltrd 2840 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 40 | 32, 33, 14, 3, 39, 6 | knoppcnlem3 36497 | . . . . . . . 8
⊢ (𝜑 → ((𝐹‘𝐴)‘𝐽) ∈ ℝ) | 
| 41 | 40 | recnd 11290 | . . . . . . 7
⊢ (𝜑 → ((𝐹‘𝐴)‘𝐽) ∈ ℂ) | 
| 42 |  | knoppndvlem15.b | . . . . . . . . . . 11
⊢ 𝐵 = ((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1)) | 
| 43 | 42 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 = ((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1))) | 
| 44 | 37 | peano2zd 12727 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑀 + 1) ∈ ℤ) | 
| 45 | 14, 36, 44 | knoppndvlem1 36514 | . . . . . . . . . 10
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1)) ∈ ℝ) | 
| 46 | 43, 45 | eqeltrd 2840 | . . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 47 | 32, 33, 14, 3, 46, 6 | knoppcnlem3 36497 | . . . . . . . 8
⊢ (𝜑 → ((𝐹‘𝐵)‘𝐽) ∈ ℝ) | 
| 48 | 47 | recnd 11290 | . . . . . . 7
⊢ (𝜑 → ((𝐹‘𝐵)‘𝐽) ∈ ℂ) | 
| 49 | 41, 48 | subcld 11621 | . . . . . 6
⊢ (𝜑 → (((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽)) ∈ ℂ) | 
| 50 | 49 | abscld 15476 | . . . . 5
⊢ (𝜑 → (abs‘(((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽))) ∈ ℝ) | 
| 51 | 32, 33, 46, 3, 14 | knoppndvlem5 36518 | . . . . . . . 8
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) ∈ ℝ) | 
| 52 | 51 | recnd 11290 | . . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) ∈ ℂ) | 
| 53 | 32, 33, 39, 3, 14 | knoppndvlem5 36518 | . . . . . . . 8
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖) ∈ ℝ) | 
| 54 | 53 | recnd 11290 | . . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖) ∈ ℂ) | 
| 55 | 52, 54 | subcld 11621 | . . . . . 6
⊢ (𝜑 → (Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖)) ∈ ℂ) | 
| 56 | 55 | abscld 15476 | . . . . 5
⊢ (𝜑 → (abs‘(Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖))) ∈ ℝ) | 
| 57 | 50, 56 | resubcld 11692 | . . . 4
⊢ (𝜑 → ((abs‘(((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽))) − (abs‘(Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖)))) ∈ ℝ) | 
| 58 | 49, 55 | subcld 11621 | . . . . 5
⊢ (𝜑 → ((((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽)) − (Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖))) ∈ ℂ) | 
| 59 | 58 | abscld 15476 | . . . 4
⊢ (𝜑 → (abs‘((((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽)) − (Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖)))) ∈ ℝ) | 
| 60 | 12, 29 | jca 511 | . . . . . . . 8
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) ∈ ℝ ∧ (1 / (((2
· 𝑁) ·
(abs‘𝐶)) − 1))
∈ ℝ)) | 
| 61 |  | remulcl 11241 | . . . . . . . 8
⊢
(((((abs‘𝐶)↑𝐽) / 2) ∈ ℝ ∧ (1 / (((2
· 𝑁) ·
(abs‘𝐶)) − 1))
∈ ℝ) → ((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1))) ∈
ℝ) | 
| 62 | 60, 61 | syl 17 | . . . . . . 7
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1))) ∈
ℝ) | 
| 63 | 12, 62 | jca 511 | . . . . . 6
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) ∈ ℝ ∧
((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2
· 𝑁) ·
(abs‘𝐶)) − 1)))
∈ ℝ)) | 
| 64 |  | resubcl 11574 | . . . . . 6
⊢
(((((abs‘𝐶)↑𝐽) / 2) ∈ ℝ ∧
((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2
· 𝑁) ·
(abs‘𝐶)) − 1)))
∈ ℝ) → ((((abs‘𝐶)↑𝐽) / 2) − ((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)))) ∈
ℝ) | 
| 65 | 63, 64 | syl 17 | . . . . 5
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) − ((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)))) ∈
ℝ) | 
| 66 | 12 | recnd 11290 | . . . . . . 7
⊢ (𝜑 → (((abs‘𝐶)↑𝐽) / 2) ∈ ℂ) | 
| 67 |  | 1cnd 11257 | . . . . . . 7
⊢ (𝜑 → 1 ∈
ℂ) | 
| 68 | 29 | recnd 11290 | . . . . . . 7
⊢ (𝜑 → (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)) ∈
ℂ) | 
| 69 | 66, 67, 68 | subdid 11720 | . . . . . 6
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) · (1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) = (((((abs‘𝐶)↑𝐽) / 2) · 1) −
((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1))))) | 
| 70 | 66 | mulridd 11279 | . . . . . . . 8
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) · 1) = (((abs‘𝐶)↑𝐽) / 2)) | 
| 71 | 70 | oveq1d 7447 | . . . . . . 7
⊢ (𝜑 → (((((abs‘𝐶)↑𝐽) / 2) · 1) −
((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) = ((((abs‘𝐶)↑𝐽) / 2) − ((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2 · 𝑁) · (abs‘𝐶)) −
1))))) | 
| 72 | 65 | leidd 11830 | . . . . . . 7
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) − ((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)))) ≤
((((abs‘𝐶)↑𝐽) / 2) −
((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1))))) | 
| 73 | 71, 72 | eqbrtrd 5164 | . . . . . 6
⊢ (𝜑 → (((((abs‘𝐶)↑𝐽) / 2) · 1) −
((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) ≤ ((((abs‘𝐶)↑𝐽) / 2) − ((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2 · 𝑁) · (abs‘𝐶)) −
1))))) | 
| 74 | 69, 73 | eqbrtrd 5164 | . . . . 5
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) · (1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) ≤ ((((abs‘𝐶)↑𝐽) / 2) − ((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2 · 𝑁) · (abs‘𝐶)) −
1))))) | 
| 75 | 12, 29 | remulcld 11292 | . . . . . 6
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1))) ∈
ℝ) | 
| 76 | 12 | leidd 11830 | . . . . . . 7
⊢ (𝜑 → (((abs‘𝐶)↑𝐽) / 2) ≤ (((abs‘𝐶)↑𝐽) / 2)) | 
| 77 | 41, 48 | abssubd 15493 | . . . . . . . . 9
⊢ (𝜑 → (abs‘(((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽))) = (abs‘(((𝐹‘𝐵)‘𝐽) − ((𝐹‘𝐴)‘𝐽)))) | 
| 78 | 32, 33, 34, 42, 1, 6, 37, 14 | knoppndvlem10 36523 | . . . . . . . . 9
⊢ (𝜑 → (abs‘(((𝐹‘𝐵)‘𝐽) − ((𝐹‘𝐴)‘𝐽))) = (((abs‘𝐶)↑𝐽) / 2)) | 
| 79 | 77, 78 | eqtrd 2776 | . . . . . . . 8
⊢ (𝜑 → (abs‘(((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽))) = (((abs‘𝐶)↑𝐽) / 2)) | 
| 80 | 79 | eqcomd 2742 | . . . . . . 7
⊢ (𝜑 → (((abs‘𝐶)↑𝐽) / 2) = (abs‘(((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽)))) | 
| 81 | 76, 80 | breqtrd 5168 | . . . . . 6
⊢ (𝜑 → (((abs‘𝐶)↑𝐽) / 2) ≤ (abs‘(((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽)))) | 
| 82 | 32, 33, 34, 42, 1, 6, 37, 14, 22 | knoppndvlem14 36527 | . . . . . 6
⊢ (𝜑 → (abs‘(Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖))) ≤ ((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2 · 𝑁) · (abs‘𝐶)) −
1)))) | 
| 83 | 12, 56, 50, 75, 81, 82 | le2subd 11884 | . . . . 5
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) − ((((abs‘𝐶)↑𝐽) / 2) · (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)))) ≤
((abs‘(((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽))) − (abs‘(Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖))))) | 
| 84 | 31, 65, 57, 74, 83 | letrd 11419 | . . . 4
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) · (1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) ≤ ((abs‘(((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽))) − (abs‘(Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖))))) | 
| 85 | 49, 55 | abs2difd 15497 | . . . 4
⊢ (𝜑 → ((abs‘(((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽))) − (abs‘(Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖)))) ≤ (abs‘((((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽)) − (Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖))))) | 
| 86 | 31, 57, 59, 84, 85 | letrd 11419 | . . 3
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) · (1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) ≤ (abs‘((((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽)) − (Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖))))) | 
| 87 | 49, 55 | abssubd 15493 | . . 3
⊢ (𝜑 → (abs‘((((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽)) − (Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖)))) = (abs‘((Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖)) − (((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽))))) | 
| 88 | 86, 87 | breqtrd 5168 | . 2
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) · (1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) ≤ (abs‘((Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖)) − (((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽))))) | 
| 89 |  | knoppndvlem15.w | . . . . . . . 8
⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0
((𝐹‘𝑤)‘𝑖)) | 
| 90 | 32, 33, 89, 42, 1, 6, 44, 14 | knoppndvlem6 36519 | . . . . . . 7
⊢ (𝜑 → (𝑊‘𝐵) = Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐵)‘𝑖)) | 
| 91 |  | elnn0uz 12924 | . . . . . . . . 9
⊢ (𝐽 ∈ ℕ0
↔ 𝐽 ∈
(ℤ≥‘0)) | 
| 92 | 6, 91 | sylib 218 | . . . . . . . 8
⊢ (𝜑 → 𝐽 ∈
(ℤ≥‘0)) | 
| 93 | 14 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐽)) → 𝑁 ∈ ℕ) | 
| 94 | 3 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐽)) → 𝐶 ∈ ℝ) | 
| 95 | 46 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐽)) → 𝐵 ∈ ℝ) | 
| 96 |  | elfznn0 13661 | . . . . . . . . . . 11
⊢ (𝑖 ∈ (0...𝐽) → 𝑖 ∈ ℕ0) | 
| 97 | 96 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐽)) → 𝑖 ∈ ℕ0) | 
| 98 | 32, 33, 93, 94, 95, 97 | knoppcnlem3 36497 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐽)) → ((𝐹‘𝐵)‘𝑖) ∈ ℝ) | 
| 99 | 98 | recnd 11290 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐽)) → ((𝐹‘𝐵)‘𝑖) ∈ ℂ) | 
| 100 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑖 = 𝐽 → ((𝐹‘𝐵)‘𝑖) = ((𝐹‘𝐵)‘𝐽)) | 
| 101 | 92, 99, 100 | fsumm1 15788 | . . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐵)‘𝑖) = (Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) + ((𝐹‘𝐵)‘𝐽))) | 
| 102 | 90, 101 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 → (𝑊‘𝐵) = (Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) + ((𝐹‘𝐵)‘𝐽))) | 
| 103 | 32, 33, 89, 34, 1, 6, 37, 14 | knoppndvlem6 36519 | . . . . . . 7
⊢ (𝜑 → (𝑊‘𝐴) = Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐴)‘𝑖)) | 
| 104 | 39 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐽)) → 𝐴 ∈ ℝ) | 
| 105 | 32, 33, 93, 94, 104, 97 | knoppcnlem3 36497 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐽)) → ((𝐹‘𝐴)‘𝑖) ∈ ℝ) | 
| 106 | 105 | recnd 11290 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝐽)) → ((𝐹‘𝐴)‘𝑖) ∈ ℂ) | 
| 107 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑖 = 𝐽 → ((𝐹‘𝐴)‘𝑖) = ((𝐹‘𝐴)‘𝐽)) | 
| 108 | 92, 106, 107 | fsumm1 15788 | . . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐴)‘𝑖) = (Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖) + ((𝐹‘𝐴)‘𝐽))) | 
| 109 | 103, 108 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 → (𝑊‘𝐴) = (Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖) + ((𝐹‘𝐴)‘𝐽))) | 
| 110 | 102, 109 | oveq12d 7450 | . . . . 5
⊢ (𝜑 → ((𝑊‘𝐵) − (𝑊‘𝐴)) = ((Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) + ((𝐹‘𝐵)‘𝐽)) − (Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖) + ((𝐹‘𝐴)‘𝐽)))) | 
| 111 | 52, 54, 41, 48 | subadd4d 11669 | . . . . . 6
⊢ (𝜑 → ((Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖)) − (((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽))) = ((Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) + ((𝐹‘𝐵)‘𝐽)) − (Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖) + ((𝐹‘𝐴)‘𝐽)))) | 
| 112 | 111 | eqcomd 2742 | . . . . 5
⊢ (𝜑 → ((Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) + ((𝐹‘𝐵)‘𝐽)) − (Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖) + ((𝐹‘𝐴)‘𝐽))) = ((Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖)) − (((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽)))) | 
| 113 | 110, 112 | eqtrd 2776 | . . . 4
⊢ (𝜑 → ((𝑊‘𝐵) − (𝑊‘𝐴)) = ((Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖)) − (((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽)))) | 
| 114 | 113 | fveq2d 6909 | . . 3
⊢ (𝜑 → (abs‘((𝑊‘𝐵) − (𝑊‘𝐴))) = (abs‘((Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖)) − (((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽))))) | 
| 115 | 114 | eqcomd 2742 | . 2
⊢ (𝜑 → (abs‘((Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐵)‘𝑖) − Σ𝑖 ∈ (0...(𝐽 − 1))((𝐹‘𝐴)‘𝑖)) − (((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽)))) = (abs‘((𝑊‘𝐵) − (𝑊‘𝐴)))) | 
| 116 | 88, 115 | breqtrd 5168 | 1
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) · (1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) ≤ (abs‘((𝑊‘𝐵) − (𝑊‘𝐴)))) |