Metamath Proof Explorer

Theorem knoppndvlem6

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

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

Proof

Step Hyp Ref Expression
1 knoppndvlem6.t ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2 knoppndvlem6.f ⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3 knoppndvlem6.w ⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
4 knoppndvlem6.a ⊢ 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 )
5 knoppndvlem6.c ⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
6 knoppndvlem6.j ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
7 knoppndvlem6.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
8 knoppndvlem6.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
9 fveq2 ⊢ ( 𝑤 = 𝐴 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝐴 ) )
10 9 fveq1d ⊢ ( 𝑤 = 𝐴 → ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) )
11 10 sumeq2sdv ⊢ ( 𝑤 = 𝐴 → Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) = Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) )
12 4 a1i ⊢ ( 𝜑 → 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) )
13 6 nn0zd ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
14 8 13 7 knoppndvlem1 ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ∈ ℝ )
15 12 14 eqeltrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
16 sumex ⊢ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ∈ V
17 16 a1i ⊢ ( 𝜑 → Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ∈ V )
18 3 11 15 17 fvmptd3 ⊢ ( 𝜑 → ( 𝑊 ‘ 𝐴 ) = Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) )
19 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
20 eqid ⊢ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) = ( ℤ≥ ‘ ( 𝐽 + 1 ) )
21 peano2nn0 ⊢ ( 𝐽 ∈ ℕ0 → ( 𝐽 + 1 ) ∈ ℕ0 )
22 6 21 syl ⊢ ( 𝜑 → ( 𝐽 + 1 ) ∈ ℕ0 )
23 eqidd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) )
24 8 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑁 ∈ ℕ )
25 5 knoppndvlem3 ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ( abs ‘ 𝐶 ) < 1 ) )
26 25 simpld ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝐶 ∈ ℝ )
28 15 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝐴 ∈ ℝ )
29 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℕ0 )
30 1 2 24 27 28 29 knoppcnlem3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ∈ ℝ )
31 30 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ∈ ℂ )
32 1 2 3 15 5 8 knoppndvlem4 ⊢ ( 𝜑 → seq 0 ( + , ( 𝐹 ‘ 𝐴 ) ) ⇝ ( 𝑊 ‘ 𝐴 ) )
33 seqex ⊢ seq 0 ( + , ( 𝐹 ‘ 𝐴 ) ) ∈ V
34 fvex ⊢ ( 𝑊 ‘ 𝐴 ) ∈ V
35 33 34 breldm ⊢ ( seq 0 ( + , ( 𝐹 ‘ 𝐴 ) ) ⇝ ( 𝑊 ‘ 𝐴 ) → seq 0 ( + , ( 𝐹 ‘ 𝐴 ) ) ∈ dom ⇝ )
36 32 35 syl ⊢ ( 𝜑 → seq 0 ( + , ( 𝐹 ‘ 𝐴 ) ) ∈ dom ⇝ )
37 19 20 22 23 31 36 isumsplit ⊢ ( 𝜑 → Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) = ( Σ 𝑖 ∈ ( 0 ... ( ( 𝐽 + 1 ) − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) + Σ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) )
38 6 nn0cnd ⊢ ( 𝜑 → 𝐽 ∈ ℂ )
39 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
40 38 39 pncand ⊢ ( 𝜑 → ( ( 𝐽 + 1 ) − 1 ) = 𝐽 )
41 40 oveq2d ⊢ ( 𝜑 → ( 0 ... ( ( 𝐽 + 1 ) − 1 ) ) = ( 0 ... 𝐽 ) )
42 41 sumeq1d ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( ( 𝐽 + 1 ) − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) = Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) )
43 42 oveq1d ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 0 ... ( ( 𝐽 + 1 ) − 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) + Σ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) = ( Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) + Σ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) )
44 18 37 43 3eqtrd ⊢ ( 𝜑 → ( 𝑊 ‘ 𝐴 ) = ( Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) + Σ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) )
45 15 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → 𝐴 ∈ ℝ )
46 eluznn0 ⊢ ( ( ( 𝐽 + 1 ) ∈ ℕ0 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → 𝑖 ∈ ℕ0 )
47 22 46 sylan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → 𝑖 ∈ ℕ0 )
48 2 45 47 knoppcnlem1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) = ( ( 𝐶 ↑ 𝑖 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) )
49 4 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) )
50 49 oveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) = ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ) )
51 8 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → 𝑁 ∈ ℕ )
52 47 nn0zd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → 𝑖 ∈ ℤ )
53 13 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → 𝐽 ∈ ℤ )
54 7 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → 𝑀 ∈ ℤ )
55 eluzle ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) → ( 𝐽 + 1 ) ≤ 𝑖 )
56 55 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → ( 𝐽 + 1 ) ≤ 𝑖 )
57 53 52 jca ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → ( 𝐽 ∈ ℤ ∧ 𝑖 ∈ ℤ ) )
58 zltp1le ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 𝐽 < 𝑖 ↔ ( 𝐽 + 1 ) ≤ 𝑖 ) )
59 57 58 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → ( 𝐽 < 𝑖 ↔ ( 𝐽 + 1 ) ≤ 𝑖 ) )
60 56 59 mpbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → 𝐽 < 𝑖 )
61 51 52 53 54 60 knoppndvlem2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 ) ) ∈ ℤ )
62 50 61 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ∈ ℤ )
63 1 62 dnizeq0 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) = 0 )
64 63 oveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → ( ( 𝐶 ↑ 𝑖 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑖 ) · 𝐴 ) ) ) = ( ( 𝐶 ↑ 𝑖 ) · 0 ) )
65 26 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
66 65 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → 𝐶 ∈ ℂ )
67 66 47 expcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → ( 𝐶 ↑ 𝑖 ) ∈ ℂ )
68 67 mul01d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → ( ( 𝐶 ↑ 𝑖 ) · 0 ) = 0 )
69 48 64 68 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ) → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) = 0 )
70 69 sumeq2dv ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) = Σ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) 0 )
71 ssidd ⊢ ( 𝜑 → ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ⊆ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) )
72 71 orcd ⊢ ( 𝜑 → ( ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ⊆ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ∨ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ∈ Fin ) )
73 sumz ⊢ ( ( ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ⊆ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ∨ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ∈ Fin ) → Σ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) 0 = 0 )
74 72 73 syl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) 0 = 0 )
75 70 74 eqtrd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) = 0 )
76 75 oveq2d ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) + Σ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) = ( Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) + 0 ) )
77 1 2 15 26 8 knoppndvlem5 ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ∈ ℝ )
78 77 recnd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ∈ ℂ )
79 78 addridd ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) + 0 ) = Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) )
80 76 79 eqtrd ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) + Σ 𝑖 ∈ ( ℤ≥ ‘ ( 𝐽 + 1 ) ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) ) = Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) )
81 44 80 eqtrd ⊢ ( 𝜑 → ( 𝑊 ‘ 𝐴 ) = Σ 𝑖 ∈ ( 0 ... 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) )