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 ... 𝐽 ) ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑖 ) )