Theorem knoppndvlem9

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

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

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem9.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		knoppndvlem9.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3		knoppndvlem9.a	⊢ 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 )
4		knoppndvlem9.c	⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
5		knoppndvlem9.j	⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
6		knoppndvlem9.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
7		knoppndvlem9.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
8		knoppndvlem9.1	⊢ ( 𝜑 → ¬ 2 ∥ 𝑀 )
9	1 2 3 5 6 7	knoppndvlem7	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) = ( ( 𝐶 ↑ 𝐽 ) · ( 𝑇 ‘ ( 𝑀 / 2 ) ) ) )
10		odd2np1	⊢ ( 𝑀 ∈ ℤ → ( ¬ 2 ∥ 𝑀 ↔ ∃ 𝑚 ∈ ℤ ( ( 2 · 𝑚 ) + 1 ) = 𝑀 ) )
11	6 10	syl	⊢ ( 𝜑 → ( ¬ 2 ∥ 𝑀 ↔ ∃ 𝑚 ∈ ℤ ( ( 2 · 𝑚 ) + 1 ) = 𝑀 ) )
12	8 11	mpbid	⊢ ( 𝜑 → ∃ 𝑚 ∈ ℤ ( ( 2 · 𝑚 ) + 1 ) = 𝑀 )
13		eqcom	⊢ ( ( ( 2 · 𝑚 ) + 1 ) = 𝑀 ↔ 𝑀 = ( ( 2 · 𝑚 ) + 1 ) )
14	13	biimpi	⊢ ( ( ( 2 · 𝑚 ) + 1 ) = 𝑀 → 𝑀 = ( ( 2 · 𝑚 ) + 1 ) )
15	14	oveq1d	⊢ ( ( ( 2 · 𝑚 ) + 1 ) = 𝑀 → ( 𝑀 / 2 ) = ( ( ( 2 · 𝑚 ) + 1 ) / 2 ) )
16	15	adantl	⊢ ( ( 𝑚 ∈ ℤ ∧ ( ( 2 · 𝑚 ) + 1 ) = 𝑀 ) → ( 𝑀 / 2 ) = ( ( ( 2 · 𝑚 ) + 1 ) / 2 ) )
17	16	adantl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ ( ( 2 · 𝑚 ) + 1 ) = 𝑀 ) ) → ( 𝑀 / 2 ) = ( ( ( 2 · 𝑚 ) + 1 ) / 2 ) )
18		2cnd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → 2 ∈ ℂ )
19		zcn	⊢ ( 𝑚 ∈ ℤ → 𝑚 ∈ ℂ )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → 𝑚 ∈ ℂ )
21	18 20	mulcld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( 2 · 𝑚 ) ∈ ℂ )
22		1cnd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → 1 ∈ ℂ )
23		2ne0	⊢ 2 ≠ 0
24	23	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → 2 ≠ 0 )
25	21 22 18 24	divdird	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( 2 · 𝑚 ) + 1 ) / 2 ) = ( ( ( 2 · 𝑚 ) / 2 ) + ( 1 / 2 ) ) )
26	20 18 24	divcan3d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( 2 · 𝑚 ) / 2 ) = 𝑚 )
27	26	oveq1d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( 2 · 𝑚 ) / 2 ) + ( 1 / 2 ) ) = ( 𝑚 + ( 1 / 2 ) ) )
28	25 27	eqtrd	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( ( ( 2 · 𝑚 ) + 1 ) / 2 ) = ( 𝑚 + ( 1 / 2 ) ) )
29	28	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ ( ( 2 · 𝑚 ) + 1 ) = 𝑀 ) ) → ( ( ( 2 · 𝑚 ) + 1 ) / 2 ) = ( 𝑚 + ( 1 / 2 ) ) )
30	17 29	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ ( ( 2 · 𝑚 ) + 1 ) = 𝑀 ) ) → ( 𝑀 / 2 ) = ( 𝑚 + ( 1 / 2 ) ) )
31	30	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ ( ( 2 · 𝑚 ) + 1 ) = 𝑀 ) ) → ( 𝑇 ‘ ( 𝑀 / 2 ) ) = ( 𝑇 ‘ ( 𝑚 + ( 1 / 2 ) ) ) )
32		id	⊢ ( 𝑚 ∈ ℤ → 𝑚 ∈ ℤ )
33	1 32	dnizphlfeqhlf	⊢ ( 𝑚 ∈ ℤ → ( 𝑇 ‘ ( 𝑚 + ( 1 / 2 ) ) ) = ( 1 / 2 ) )
34	33	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℤ ) → ( 𝑇 ‘ ( 𝑚 + ( 1 / 2 ) ) ) = ( 1 / 2 ) )
35	34	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ ( ( 2 · 𝑚 ) + 1 ) = 𝑀 ) ) → ( 𝑇 ‘ ( 𝑚 + ( 1 / 2 ) ) ) = ( 1 / 2 ) )
36	31 35	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ ( ( 2 · 𝑚 ) + 1 ) = 𝑀 ) ) → ( 𝑇 ‘ ( 𝑀 / 2 ) ) = ( 1 / 2 ) )
37	12 36	rexlimddv	⊢ ( 𝜑 → ( 𝑇 ‘ ( 𝑀 / 2 ) ) = ( 1 / 2 ) )
38	37	oveq2d	⊢ ( 𝜑 → ( ( 𝐶 ↑ 𝐽 ) · ( 𝑇 ‘ ( 𝑀 / 2 ) ) ) = ( ( 𝐶 ↑ 𝐽 ) · ( 1 / 2 ) ) )
39	4	knoppndvlem3	⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ( abs ‘ 𝐶 ) < 1 ) )
40	39	simpld	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
41	40	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
42	41 5	expcld	⊢ ( 𝜑 → ( 𝐶 ↑ 𝐽 ) ∈ ℂ )
43		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
44		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
45	23	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
46	42 43 44 45	div12d	⊢ ( 𝜑 → ( ( 𝐶 ↑ 𝐽 ) · ( 1 / 2 ) ) = ( 1 · ( ( 𝐶 ↑ 𝐽 ) / 2 ) ) )
47	42 44 45	divcld	⊢ ( 𝜑 → ( ( 𝐶 ↑ 𝐽 ) / 2 ) ∈ ℂ )
48	47	mulid2d	⊢ ( 𝜑 → ( 1 · ( ( 𝐶 ↑ 𝐽 ) / 2 ) ) = ( ( 𝐶 ↑ 𝐽 ) / 2 ) )
49	46 48	eqtrd	⊢ ( 𝜑 → ( ( 𝐶 ↑ 𝐽 ) · ( 1 / 2 ) ) = ( ( 𝐶 ↑ 𝐽 ) / 2 ) )
50	9 38 49	3eqtrd	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) = ( ( 𝐶 ↑ 𝐽 ) / 2 ) )