Proof of Theorem knoppndvlem17
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | knoppndvlem17.c | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) | 
| 2 | 1 | knoppndvlem3 36516 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶 ∈ ℝ ∧ (abs‘𝐶) < 1)) | 
| 3 | 2 | simpld 494 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 4 | 3 | recnd 11290 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 5 | 4 | abscld 15476 | . . . . . . . . . 10
⊢ (𝜑 → (abs‘𝐶) ∈
ℝ) | 
| 6 |  | knoppndvlem17.j | . . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈
ℕ0) | 
| 7 | 5, 6 | reexpcld 14204 | . . . . . . . . 9
⊢ (𝜑 → ((abs‘𝐶)↑𝐽) ∈ ℝ) | 
| 8 |  | 2re 12341 | . . . . . . . . . 10
⊢ 2 ∈
ℝ | 
| 9 | 8 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℝ) | 
| 10 |  | 2ne0 12371 | . . . . . . . . . 10
⊢ 2 ≠
0 | 
| 11 | 10 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 2 ≠ 0) | 
| 12 | 7, 9, 11 | redivcld 12096 | . . . . . . . 8
⊢ (𝜑 → (((abs‘𝐶)↑𝐽) / 2) ∈ ℝ) | 
| 13 | 12 | recnd 11290 | . . . . . . 7
⊢ (𝜑 → (((abs‘𝐶)↑𝐽) / 2) ∈ ℂ) | 
| 14 |  | 1red 11263 | . . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℝ) | 
| 15 |  | knoppndvlem17.n | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 16 | 15 | nnred 12282 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 17 | 9, 16 | remulcld 11292 | . . . . . . . . . . . 12
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ) | 
| 18 | 17, 5 | remulcld 11292 | . . . . . . . . . . 11
⊢ (𝜑 → ((2 · 𝑁) · (abs‘𝐶)) ∈
ℝ) | 
| 19 | 18, 14 | resubcld 11692 | . . . . . . . . . 10
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶)) − 1) ∈
ℝ) | 
| 20 |  | 0red 11265 | . . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℝ) | 
| 21 |  | 0lt1 11786 | . . . . . . . . . . . . . 14
⊢ 0 <
1 | 
| 22 | 21 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → 0 < 1) | 
| 23 |  | knoppndvlem17.1 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 < (𝑁 · (abs‘𝐶))) | 
| 24 | 1, 15, 23 | knoppndvlem12 36525 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶)) ≠ 1 ∧ 1 < (((2
· 𝑁) ·
(abs‘𝐶)) −
1))) | 
| 25 | 24 | simprd 495 | . . . . . . . . . . . . 13
⊢ (𝜑 → 1 < (((2 · 𝑁) · (abs‘𝐶)) − 1)) | 
| 26 | 20, 14, 19, 22, 25 | lttrd 11423 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 < (((2 · 𝑁) · (abs‘𝐶)) − 1)) | 
| 27 | 19, 26 | jca 511 | . . . . . . . . . . 11
⊢ (𝜑 → ((((2 · 𝑁) · (abs‘𝐶)) − 1) ∈ ℝ
∧ 0 < (((2 · 𝑁) · (abs‘𝐶)) − 1))) | 
| 28 |  | gt0ne0 11729 | . . . . . . . . . . 11
⊢ (((((2
· 𝑁) ·
(abs‘𝐶)) − 1)
∈ ℝ ∧ 0 < (((2 · 𝑁) · (abs‘𝐶)) − 1)) → (((2 · 𝑁) · (abs‘𝐶)) − 1) ≠
0) | 
| 29 | 27, 28 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶)) − 1) ≠
0) | 
| 30 | 14, 19, 29 | redivcld 12096 | . . . . . . . . 9
⊢ (𝜑 → (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1)) ∈
ℝ) | 
| 31 | 14, 30 | resubcld 11692 | . . . . . . . 8
⊢ (𝜑 → (1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) − 1)))
∈ ℝ) | 
| 32 | 31 | recnd 11290 | . . . . . . 7
⊢ (𝜑 → (1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) − 1)))
∈ ℂ) | 
| 33 | 13, 32 | mulcomd 11283 | . . . . . 6
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) · (1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) = ((1 − (1 / (((2 · 𝑁) · (abs‘𝐶)) − 1))) · (((abs‘𝐶)↑𝐽) / 2))) | 
| 34 | 33 | oveq1d 7447 | . . . . 5
⊢ (𝜑 → (((((abs‘𝐶)↑𝐽) / 2) · (1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) / (((2 · 𝑁)↑-𝐽) / 2)) = (((1 − (1 / (((2 ·
𝑁) ·
(abs‘𝐶)) − 1)))
· (((abs‘𝐶)↑𝐽) / 2)) / (((2 · 𝑁)↑-𝐽) / 2))) | 
| 35 |  | 2rp 13040 | . . . . . . . . . . 11
⊢ 2 ∈
ℝ+ | 
| 36 | 35 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → 2 ∈
ℝ+) | 
| 37 | 15 | nnrpd 13076 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
ℝ+) | 
| 38 | 36, 37 | rpmulcld 13094 | . . . . . . . . 9
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ+) | 
| 39 | 6 | nn0zd 12641 | . . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ ℤ) | 
| 40 | 39 | znegcld 12726 | . . . . . . . . 9
⊢ (𝜑 → -𝐽 ∈ ℤ) | 
| 41 | 38, 40 | rpexpcld 14287 | . . . . . . . 8
⊢ (𝜑 → ((2 · 𝑁)↑-𝐽) ∈
ℝ+) | 
| 42 | 41 | rphalfcld 13090 | . . . . . . 7
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) / 2) ∈
ℝ+) | 
| 43 | 42 | rpcnd 13080 | . . . . . 6
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) / 2) ∈ ℂ) | 
| 44 | 42 | rpne0d 13083 | . . . . . 6
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) / 2) ≠ 0) | 
| 45 | 32, 13, 43, 44 | divassd 12079 | . . . . 5
⊢ (𝜑 → (((1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) − 1)))
· (((abs‘𝐶)↑𝐽) / 2)) / (((2 · 𝑁)↑-𝐽) / 2)) = ((1 − (1 / (((2 ·
𝑁) ·
(abs‘𝐶)) − 1)))
· ((((abs‘𝐶)↑𝐽) / 2) / (((2 · 𝑁)↑-𝐽) / 2)))) | 
| 46 | 13, 43, 44 | divcld 12044 | . . . . . . 7
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) / (((2 · 𝑁)↑-𝐽) / 2)) ∈ ℂ) | 
| 47 | 32, 46 | mulcomd 11283 | . . . . . 6
⊢ (𝜑 → ((1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) − 1)))
· ((((abs‘𝐶)↑𝐽) / 2) / (((2 · 𝑁)↑-𝐽) / 2))) = (((((abs‘𝐶)↑𝐽) / 2) / (((2 · 𝑁)↑-𝐽) / 2)) · (1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1))))) | 
| 48 | 7 | recnd 11290 | . . . . . . . . 9
⊢ (𝜑 → ((abs‘𝐶)↑𝐽) ∈ ℂ) | 
| 49 | 41 | rpcnd 13080 | . . . . . . . . 9
⊢ (𝜑 → ((2 · 𝑁)↑-𝐽) ∈ ℂ) | 
| 50 | 9 | recnd 11290 | . . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℂ) | 
| 51 | 41 | rpne0d 13083 | . . . . . . . . 9
⊢ (𝜑 → ((2 · 𝑁)↑-𝐽) ≠ 0) | 
| 52 | 48, 49, 50, 51, 11 | divcan7d 12072 | . . . . . . . 8
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) / (((2 · 𝑁)↑-𝐽) / 2)) = (((abs‘𝐶)↑𝐽) / ((2 · 𝑁)↑-𝐽))) | 
| 53 | 17 | recnd 11290 | . . . . . . . . . . 11
⊢ (𝜑 → (2 · 𝑁) ∈
ℂ) | 
| 54 | 38 | rpne0d 13083 | . . . . . . . . . . 11
⊢ (𝜑 → (2 · 𝑁) ≠ 0) | 
| 55 | 53, 54, 39 | expnegd 14194 | . . . . . . . . . 10
⊢ (𝜑 → ((2 · 𝑁)↑-𝐽) = (1 / ((2 · 𝑁)↑𝐽))) | 
| 56 | 55 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝜑 → (((abs‘𝐶)↑𝐽) / ((2 · 𝑁)↑-𝐽)) = (((abs‘𝐶)↑𝐽) / (1 / ((2 · 𝑁)↑𝐽)))) | 
| 57 |  | 1cnd 11257 | . . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℂ) | 
| 58 | 53, 6 | expcld 14187 | . . . . . . . . . 10
⊢ (𝜑 → ((2 · 𝑁)↑𝐽) ∈ ℂ) | 
| 59 | 20, 22 | gtned 11397 | . . . . . . . . . 10
⊢ (𝜑 → 1 ≠ 0) | 
| 60 | 53, 54, 39 | expne0d 14193 | . . . . . . . . . 10
⊢ (𝜑 → ((2 · 𝑁)↑𝐽) ≠ 0) | 
| 61 | 48, 57, 58, 59, 60 | divdiv2d 12076 | . . . . . . . . 9
⊢ (𝜑 → (((abs‘𝐶)↑𝐽) / (1 / ((2 · 𝑁)↑𝐽))) = ((((abs‘𝐶)↑𝐽) · ((2 · 𝑁)↑𝐽)) / 1)) | 
| 62 | 48, 58 | mulcld 11282 | . . . . . . . . . . 11
⊢ (𝜑 → (((abs‘𝐶)↑𝐽) · ((2 · 𝑁)↑𝐽)) ∈ ℂ) | 
| 63 | 62 | div1d 12036 | . . . . . . . . . 10
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) · ((2 · 𝑁)↑𝐽)) / 1) = (((abs‘𝐶)↑𝐽) · ((2 · 𝑁)↑𝐽))) | 
| 64 | 48, 58 | mulcomd 11283 | . . . . . . . . . 10
⊢ (𝜑 → (((abs‘𝐶)↑𝐽) · ((2 · 𝑁)↑𝐽)) = (((2 · 𝑁)↑𝐽) · ((abs‘𝐶)↑𝐽))) | 
| 65 | 53, 54 | jca 511 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((2 · 𝑁) ∈ ℂ ∧ (2
· 𝑁) ≠
0)) | 
| 66 | 5 | recnd 11290 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (abs‘𝐶) ∈
ℂ) | 
| 67 | 1, 15, 23 | knoppndvlem13 36526 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ≠ 0) | 
| 68 | 4, 67 | absne0d 15487 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (abs‘𝐶) ≠ 0) | 
| 69 | 66, 68 | jca 511 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((abs‘𝐶) ∈ ℂ ∧
(abs‘𝐶) ≠
0)) | 
| 70 | 65, 69, 39 | 3jca 1128 | . . . . . . . . . . . 12
⊢ (𝜑 → (((2 · 𝑁) ∈ ℂ ∧ (2
· 𝑁) ≠ 0) ∧
((abs‘𝐶) ∈
ℂ ∧ (abs‘𝐶)
≠ 0) ∧ 𝐽 ∈
ℤ)) | 
| 71 |  | mulexpz 14144 | . . . . . . . . . . . 12
⊢ ((((2
· 𝑁) ∈ ℂ
∧ (2 · 𝑁) ≠
0) ∧ ((abs‘𝐶)
∈ ℂ ∧ (abs‘𝐶) ≠ 0) ∧ 𝐽 ∈ ℤ) → (((2 · 𝑁) · (abs‘𝐶))↑𝐽) = (((2 · 𝑁)↑𝐽) · ((abs‘𝐶)↑𝐽))) | 
| 72 | 70, 71 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (((2 · 𝑁) · (abs‘𝐶))↑𝐽) = (((2 · 𝑁)↑𝐽) · ((abs‘𝐶)↑𝐽))) | 
| 73 | 72 | eqcomd 2742 | . . . . . . . . . 10
⊢ (𝜑 → (((2 · 𝑁)↑𝐽) · ((abs‘𝐶)↑𝐽)) = (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) | 
| 74 | 63, 64, 73 | 3eqtrd 2780 | . . . . . . . . 9
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) · ((2 · 𝑁)↑𝐽)) / 1) = (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) | 
| 75 | 56, 61, 74 | 3eqtrd 2780 | . . . . . . . 8
⊢ (𝜑 → (((abs‘𝐶)↑𝐽) / ((2 · 𝑁)↑-𝐽)) = (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) | 
| 76 | 52, 75 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) / (((2 · 𝑁)↑-𝐽) / 2)) = (((2 · 𝑁) · (abs‘𝐶))↑𝐽)) | 
| 77 | 76 | oveq1d 7447 | . . . . . 6
⊢ (𝜑 → (((((abs‘𝐶)↑𝐽) / 2) / (((2 · 𝑁)↑-𝐽) / 2)) · (1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) = ((((2 · 𝑁)
· (abs‘𝐶))↑𝐽) · (1 − (1 / (((2 ·
𝑁) ·
(abs‘𝐶)) −
1))))) | 
| 78 | 47, 77 | eqtrd 2776 | . . . . 5
⊢ (𝜑 → ((1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) − 1)))
· ((((abs‘𝐶)↑𝐽) / 2) / (((2 · 𝑁)↑-𝐽) / 2))) = ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) · (1 − (1 / (((2 ·
𝑁) ·
(abs‘𝐶)) −
1))))) | 
| 79 | 34, 45, 78 | 3eqtrd 2780 | . . . 4
⊢ (𝜑 → (((((abs‘𝐶)↑𝐽) / 2) · (1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) / (((2 · 𝑁)↑-𝐽) / 2)) = ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) · (1 − (1 / (((2 ·
𝑁) ·
(abs‘𝐶)) −
1))))) | 
| 80 | 79 | eqcomd 2742 | . . 3
⊢ (𝜑 → ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) · (1 − (1 / (((2 ·
𝑁) ·
(abs‘𝐶)) −
1)))) = (((((abs‘𝐶)↑𝐽) / 2) · (1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) / (((2 · 𝑁)↑-𝐽) / 2))) | 
| 81 | 12, 31 | remulcld 11292 | . . . 4
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) · (1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) ∈ ℝ) | 
| 82 |  | knoppndvlem17.t | . . . . . . 7
⊢ 𝑇 = (𝑥 ∈ ℝ ↦
(abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) | 
| 83 |  | knoppndvlem17.f | . . . . . . 7
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) | 
| 84 |  | knoppndvlem17.w | . . . . . . 7
⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0
((𝐹‘𝑤)‘𝑖)) | 
| 85 |  | knoppndvlem17.b | . . . . . . . . 9
⊢ 𝐵 = ((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1)) | 
| 86 | 85 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 𝐵 = ((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1))) | 
| 87 |  | knoppndvlem17.m | . . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 88 | 87 | peano2zd 12727 | . . . . . . . . 9
⊢ (𝜑 → (𝑀 + 1) ∈ ℤ) | 
| 89 | 15, 39, 88 | knoppndvlem1 36514 | . . . . . . . 8
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1)) ∈ ℝ) | 
| 90 | 86, 89 | eqeltrd 2840 | . . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 91 | 2 | simprd 495 | . . . . . . 7
⊢ (𝜑 → (abs‘𝐶) < 1) | 
| 92 | 82, 83, 84, 90, 15, 3, 91 | knoppcld 36507 | . . . . . 6
⊢ (𝜑 → (𝑊‘𝐵) ∈ ℂ) | 
| 93 |  | knoppndvlem17.a | . . . . . . . . 9
⊢ 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀) | 
| 94 | 93 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀)) | 
| 95 | 15, 39, 87 | knoppndvlem1 36514 | . . . . . . . 8
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀) ∈ ℝ) | 
| 96 | 94, 95 | eqeltrd 2840 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 97 | 82, 83, 84, 96, 15, 3, 91 | knoppcld 36507 | . . . . . 6
⊢ (𝜑 → (𝑊‘𝐴) ∈ ℂ) | 
| 98 | 92, 97 | subcld 11621 | . . . . 5
⊢ (𝜑 → ((𝑊‘𝐵) − (𝑊‘𝐴)) ∈ ℂ) | 
| 99 | 98 | abscld 15476 | . . . 4
⊢ (𝜑 → (abs‘((𝑊‘𝐵) − (𝑊‘𝐴))) ∈ ℝ) | 
| 100 | 82, 83, 84, 93, 85, 1, 6, 87, 15, 23 | knoppndvlem15 36528 | . . . 4
⊢ (𝜑 → ((((abs‘𝐶)↑𝐽) / 2) · (1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) ≤ (abs‘((𝑊‘𝐵) − (𝑊‘𝐴)))) | 
| 101 | 81, 99, 42, 100 | lediv1dd 13136 | . . 3
⊢ (𝜑 → (((((abs‘𝐶)↑𝐽) / 2) · (1 − (1 / (((2
· 𝑁) ·
(abs‘𝐶)) −
1)))) / (((2 · 𝑁)↑-𝐽) / 2)) ≤ ((abs‘((𝑊‘𝐵) − (𝑊‘𝐴))) / (((2 · 𝑁)↑-𝐽) / 2))) | 
| 102 | 80, 101 | eqbrtrd 5164 | . 2
⊢ (𝜑 → ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) · (1 − (1 / (((2 ·
𝑁) ·
(abs‘𝐶)) −
1)))) ≤ ((abs‘((𝑊‘𝐵) − (𝑊‘𝐴))) / (((2 · 𝑁)↑-𝐽) / 2))) | 
| 103 | 93, 85, 6, 87, 15 | knoppndvlem16 36529 | . . . 4
⊢ (𝜑 → (𝐵 − 𝐴) = (((2 · 𝑁)↑-𝐽) / 2)) | 
| 104 | 103 | eqcomd 2742 | . . 3
⊢ (𝜑 → (((2 · 𝑁)↑-𝐽) / 2) = (𝐵 − 𝐴)) | 
| 105 | 104 | oveq2d 7448 | . 2
⊢ (𝜑 → ((abs‘((𝑊‘𝐵) − (𝑊‘𝐴))) / (((2 · 𝑁)↑-𝐽) / 2)) = ((abs‘((𝑊‘𝐵) − (𝑊‘𝐴))) / (𝐵 − 𝐴))) | 
| 106 | 102, 105 | breqtrd 5168 | 1
⊢ (𝜑 → ((((2 · 𝑁) · (abs‘𝐶))↑𝐽) · (1 − (1 / (((2 ·
𝑁) ·
(abs‘𝐶)) −
1)))) ≤ ((abs‘((𝑊‘𝐵) − (𝑊‘𝐴))) / (𝐵 − 𝐴))) |