Proof of Theorem knoppndvlem10
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | knoppndvlem10.t | . . . . . . 7
⊢ 𝑇 = (𝑥 ∈ ℝ ↦
(abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) | 
| 2 |  | knoppndvlem10.f | . . . . . . 7
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) | 
| 3 |  | knoppndvlem10.b | . . . . . . 7
⊢ 𝐵 = ((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1)) | 
| 4 |  | knoppndvlem10.c | . . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) | 
| 5 | 4 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 2 ∥ 𝑀) → 𝐶 ∈ (-1(,)1)) | 
| 6 |  | knoppndvlem10.j | . . . . . . . 8
⊢ (𝜑 → 𝐽 ∈
ℕ0) | 
| 7 | 6 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 2 ∥ 𝑀) → 𝐽 ∈
ℕ0) | 
| 8 |  | knoppndvlem10.m | . . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 9 | 8 | peano2zd 12727 | . . . . . . . 8
⊢ (𝜑 → (𝑀 + 1) ∈ ℤ) | 
| 10 | 9 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 2 ∥ 𝑀) → (𝑀 + 1) ∈ ℤ) | 
| 11 |  | knoppndvlem10.n | . . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 12 | 11 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 2 ∥ 𝑀) → 𝑁 ∈ ℕ) | 
| 13 |  | notnot 142 | . . . . . . . . 9
⊢ (2
∥ 𝑀 → ¬
¬ 2 ∥ 𝑀) | 
| 14 | 13 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 2 ∥ 𝑀) → ¬ ¬ 2 ∥ 𝑀) | 
| 15 | 8 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 2 ∥ 𝑀) → 𝑀 ∈ ℤ) | 
| 16 |  | oddp1even 16382 | . . . . . . . . 9
⊢ (𝑀 ∈ ℤ → (¬ 2
∥ 𝑀 ↔ 2 ∥
(𝑀 + 1))) | 
| 17 | 15, 16 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 2 ∥ 𝑀) → (¬ 2 ∥ 𝑀 ↔ 2 ∥ (𝑀 + 1))) | 
| 18 | 14, 17 | mtbid 324 | . . . . . . 7
⊢ ((𝜑 ∧ 2 ∥ 𝑀) → ¬ 2 ∥ (𝑀 + 1)) | 
| 19 | 1, 2, 3, 5, 7, 10,
12, 18 | knoppndvlem9 36522 | . . . . . 6
⊢ ((𝜑 ∧ 2 ∥ 𝑀) → ((𝐹‘𝐵)‘𝐽) = ((𝐶↑𝐽) / 2)) | 
| 20 |  | knoppndvlem10.a | . . . . . . 7
⊢ 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀) | 
| 21 | 14 | notnotrd 133 | . . . . . . 7
⊢ ((𝜑 ∧ 2 ∥ 𝑀) → 2 ∥ 𝑀) | 
| 22 | 1, 2, 20, 5, 7, 15, 12, 21 | knoppndvlem8 36521 | . . . . . 6
⊢ ((𝜑 ∧ 2 ∥ 𝑀) → ((𝐹‘𝐴)‘𝐽) = 0) | 
| 23 | 19, 22 | oveq12d 7450 | . . . . 5
⊢ ((𝜑 ∧ 2 ∥ 𝑀) → (((𝐹‘𝐵)‘𝐽) − ((𝐹‘𝐴)‘𝐽)) = (((𝐶↑𝐽) / 2) − 0)) | 
| 24 | 4 | knoppndvlem3 36516 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐶 ∈ ℝ ∧ (abs‘𝐶) < 1)) | 
| 25 | 24 | simpld 494 | . . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 26 | 25 | recnd 11290 | . . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 27 | 26, 6 | expcld 14187 | . . . . . . . 8
⊢ (𝜑 → (𝐶↑𝐽) ∈ ℂ) | 
| 28 |  | 2cnd 12345 | . . . . . . . 8
⊢ (𝜑 → 2 ∈
ℂ) | 
| 29 |  | 2ne0 12371 | . . . . . . . . 9
⊢ 2 ≠
0 | 
| 30 | 29 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 2 ≠ 0) | 
| 31 | 27, 28, 30 | divcld 12044 | . . . . . . 7
⊢ (𝜑 → ((𝐶↑𝐽) / 2) ∈ ℂ) | 
| 32 | 31 | subid1d 11610 | . . . . . 6
⊢ (𝜑 → (((𝐶↑𝐽) / 2) − 0) = ((𝐶↑𝐽) / 2)) | 
| 33 | 32 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 2 ∥ 𝑀) → (((𝐶↑𝐽) / 2) − 0) = ((𝐶↑𝐽) / 2)) | 
| 34 | 23, 33 | eqtrd 2776 | . . . 4
⊢ ((𝜑 ∧ 2 ∥ 𝑀) → (((𝐹‘𝐵)‘𝐽) − ((𝐹‘𝐴)‘𝐽)) = ((𝐶↑𝐽) / 2)) | 
| 35 | 34 | fveq2d 6909 | . . 3
⊢ ((𝜑 ∧ 2 ∥ 𝑀) → (abs‘(((𝐹‘𝐵)‘𝐽) − ((𝐹‘𝐴)‘𝐽))) = (abs‘((𝐶↑𝐽) / 2))) | 
| 36 | 3 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 𝐵 = ((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1))) | 
| 37 | 6 | nn0zd 12641 | . . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ ℤ) | 
| 38 | 11, 37, 9 | knoppndvlem1 36514 | . . . . . . . . 9
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · (𝑀 + 1)) ∈ ℝ) | 
| 39 | 36, 38 | eqeltrd 2840 | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 40 | 1, 2, 11, 25, 39, 6 | knoppcnlem3 36497 | . . . . . . 7
⊢ (𝜑 → ((𝐹‘𝐵)‘𝐽) ∈ ℝ) | 
| 41 | 40 | recnd 11290 | . . . . . 6
⊢ (𝜑 → ((𝐹‘𝐵)‘𝐽) ∈ ℂ) | 
| 42 | 20 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀)) | 
| 43 | 11, 37, 8 | knoppndvlem1 36514 | . . . . . . . . 9
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀) ∈ ℝ) | 
| 44 | 42, 43 | eqeltrd 2840 | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 45 | 1, 2, 11, 25, 44, 6 | knoppcnlem3 36497 | . . . . . . 7
⊢ (𝜑 → ((𝐹‘𝐴)‘𝐽) ∈ ℝ) | 
| 46 | 45 | recnd 11290 | . . . . . 6
⊢ (𝜑 → ((𝐹‘𝐴)‘𝐽) ∈ ℂ) | 
| 47 | 41, 46 | abssubd 15493 | . . . . 5
⊢ (𝜑 → (abs‘(((𝐹‘𝐵)‘𝐽) − ((𝐹‘𝐴)‘𝐽))) = (abs‘(((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽)))) | 
| 48 | 47 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑀) → (abs‘(((𝐹‘𝐵)‘𝐽) − ((𝐹‘𝐴)‘𝐽))) = (abs‘(((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽)))) | 
| 49 | 4 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑀) → 𝐶 ∈ (-1(,)1)) | 
| 50 | 6 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑀) → 𝐽 ∈
ℕ0) | 
| 51 | 8 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑀) → 𝑀 ∈ ℤ) | 
| 52 | 11 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑀) → 𝑁 ∈ ℕ) | 
| 53 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑀) → ¬ 2 ∥ 𝑀) | 
| 54 | 1, 2, 20, 49, 50, 51, 52, 53 | knoppndvlem9 36522 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑀) → ((𝐹‘𝐴)‘𝐽) = ((𝐶↑𝐽) / 2)) | 
| 55 | 9 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑀) → (𝑀 + 1) ∈ ℤ) | 
| 56 | 51, 16 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑀) → (¬ 2 ∥ 𝑀 ↔ 2 ∥ (𝑀 + 1))) | 
| 57 | 53, 56 | mpbid 232 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑀) → 2 ∥ (𝑀 + 1)) | 
| 58 | 1, 2, 3, 49, 50, 55, 52, 57 | knoppndvlem8 36521 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑀) → ((𝐹‘𝐵)‘𝐽) = 0) | 
| 59 | 54, 58 | oveq12d 7450 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑀) → (((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽)) = (((𝐶↑𝐽) / 2) − 0)) | 
| 60 | 32 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑀) → (((𝐶↑𝐽) / 2) − 0) = ((𝐶↑𝐽) / 2)) | 
| 61 | 59, 60 | eqtrd 2776 | . . . . 5
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑀) → (((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽)) = ((𝐶↑𝐽) / 2)) | 
| 62 | 61 | fveq2d 6909 | . . . 4
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑀) → (abs‘(((𝐹‘𝐴)‘𝐽) − ((𝐹‘𝐵)‘𝐽))) = (abs‘((𝐶↑𝐽) / 2))) | 
| 63 | 48, 62 | eqtrd 2776 | . . 3
⊢ ((𝜑 ∧ ¬ 2 ∥ 𝑀) → (abs‘(((𝐹‘𝐵)‘𝐽) − ((𝐹‘𝐴)‘𝐽))) = (abs‘((𝐶↑𝐽) / 2))) | 
| 64 | 35, 63 | pm2.61dan 812 | . 2
⊢ (𝜑 → (abs‘(((𝐹‘𝐵)‘𝐽) − ((𝐹‘𝐴)‘𝐽))) = (abs‘((𝐶↑𝐽) / 2))) | 
| 65 | 27, 28, 30 | absdivd 15495 | . . 3
⊢ (𝜑 → (abs‘((𝐶↑𝐽) / 2)) = ((abs‘(𝐶↑𝐽)) / (abs‘2))) | 
| 66 | 26, 6 | absexpd 15492 | . . . 4
⊢ (𝜑 → (abs‘(𝐶↑𝐽)) = ((abs‘𝐶)↑𝐽)) | 
| 67 |  | 0le2 12369 | . . . . . 6
⊢ 0 ≤
2 | 
| 68 |  | 2re 12341 | . . . . . . 7
⊢ 2 ∈
ℝ | 
| 69 | 68 | absidi 15417 | . . . . . 6
⊢ (0 ≤ 2
→ (abs‘2) = 2) | 
| 70 | 67, 69 | ax-mp 5 | . . . . 5
⊢
(abs‘2) = 2 | 
| 71 | 70 | a1i 11 | . . . 4
⊢ (𝜑 → (abs‘2) =
2) | 
| 72 | 66, 71 | oveq12d 7450 | . . 3
⊢ (𝜑 → ((abs‘(𝐶↑𝐽)) / (abs‘2)) = (((abs‘𝐶)↑𝐽) / 2)) | 
| 73 | 65, 72 | eqtrd 2776 | . 2
⊢ (𝜑 → (abs‘((𝐶↑𝐽) / 2)) = (((abs‘𝐶)↑𝐽) / 2)) | 
| 74 | 64, 73 | eqtrd 2776 | 1
⊢ (𝜑 → (abs‘(((𝐹‘𝐵)‘𝐽) − ((𝐹‘𝐴)‘𝐽))) = (((abs‘𝐶)↑𝐽) / 2)) |