Metamath Proof Explorer

Theorem knoppndvlem7

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 15-Jun-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

Ref Expression
Hypotheses knoppndvlem7.t ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
knoppndvlem7.f ⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
knoppndvlem7.a ⊢ 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 )
knoppndvlem7.j ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
knoppndvlem7.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
knoppndvlem7.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion knoppndvlem7 ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) = ( ( 𝐶 ↑ 𝐽 ) · ( 𝑇 ‘ ( 𝑀 / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 knoppndvlem7.t ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2 knoppndvlem7.f ⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3 knoppndvlem7.a ⊢ 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 )
4 knoppndvlem7.j ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
5 knoppndvlem7.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
6 knoppndvlem7.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7 3 a1i ⊢ ( 𝜑 → 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) )
8 4 nn0zd ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
9 6 8 5 knoppndvlem1 ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ∈ ℝ )
10 7 9 eqeltrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
11 2 10 4 knoppcnlem1 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) = ( ( 𝐶 ↑ 𝐽 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · 𝐴 ) ) ) )
12 3 oveq2i ⊢ ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · 𝐴 ) = ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) )
13 12 a1i ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · 𝐴 ) = ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ) )
14 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
15 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
16 6 15 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
17 16 zcnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
18 14 17 mulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ )
19 18 4 expcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ 𝐽 ) ∈ ℂ )
20 2ne0 ⊢ 2 ≠ 0
21 20 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
22 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
23 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
24 16 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
25 0lt1 ⊢ 0 < 1
26 25 a1i ⊢ ( 𝜑 → 0 < 1 )
27 nnge1 ⊢ ( 𝑁 ∈ ℕ → 1 ≤ 𝑁 )
28 6 27 syl ⊢ ( 𝜑 → 1 ≤ 𝑁 )
29 22 23 24 26 28 ltletrd ⊢ ( 𝜑 → 0 < 𝑁 )
30 22 29 ltned ⊢ ( 𝜑 → 0 ≠ 𝑁 )
31 30 necomd ⊢ ( 𝜑 → 𝑁 ≠ 0 )
32 14 17 21 31 mulne0d ⊢ ( 𝜑 → ( 2 · 𝑁 ) ≠ 0 )
33 8 znegcld ⊢ ( 𝜑 → - 𝐽 ∈ ℤ )
34 18 32 33 expclzd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ∈ ℂ )
35 34 14 21 divcld ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ∈ ℂ )
36 5 zcnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
37 19 35 36 mulassd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) · 𝑀 ) = ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ) )
38 37 eqcomd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ) = ( ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) · 𝑀 ) )
39 19 34 14 21 divassd ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ) / 2 ) = ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) )
40 39 eqcomd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) = ( ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ) / 2 ) )
41 18 32 8 expnegd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ - 𝐽 ) = ( 1 / ( ( 2 · 𝑁 ) ↑ 𝐽 ) ) )
42 41 oveq2d ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ) = ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( 1 / ( ( 2 · 𝑁 ) ↑ 𝐽 ) ) ) )
43 18 32 8 expne0d ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ 𝐽 ) ≠ 0 )
44 19 43 recidd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( 1 / ( ( 2 · 𝑁 ) ↑ 𝐽 ) ) ) = 1 )
45 42 44 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ) = 1 )
46 45 oveq1d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( 2 · 𝑁 ) ↑ - 𝐽 ) ) / 2 ) = ( 1 / 2 ) )
47 40 46 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) = ( 1 / 2 ) )
48 47 oveq1d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) ) · 𝑀 ) = ( ( 1 / 2 ) · 𝑀 ) )
49 36 14 21 divrec2d ⊢ ( 𝜑 → ( 𝑀 / 2 ) = ( ( 1 / 2 ) · 𝑀 ) )
50 49 eqcomd ⊢ ( 𝜑 → ( ( 1 / 2 ) · 𝑀 ) = ( 𝑀 / 2 ) )
51 38 48 50 3eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ) = ( 𝑀 / 2 ) )
52 13 51 eqtrd ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · 𝐴 ) = ( 𝑀 / 2 ) )
53 52 fveq2d ⊢ ( 𝜑 → ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · 𝐴 ) ) = ( 𝑇 ‘ ( 𝑀 / 2 ) ) )
54 53 oveq2d ⊢ ( 𝜑 → ( ( 𝐶 ↑ 𝐽 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝐽 ) · 𝐴 ) ) ) = ( ( 𝐶 ↑ 𝐽 ) · ( 𝑇 ‘ ( 𝑀 / 2 ) ) ) )
55 11 54 eqtrd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) = ( ( 𝐶 ↑ 𝐽 ) · ( 𝑇 ‘ ( 𝑀 / 2 ) ) ) )