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 ) ) ) )