Theorem knoppndvlem10

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

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

Proof

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