Theorem knoppndvlem8

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

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

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem8.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		knoppndvlem8.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3		knoppndvlem8.a	⊢ 𝐴 = ( ( ( ( 2 · 𝑁 ) ↑ - 𝐽 ) / 2 ) · 𝑀 )
4		knoppndvlem8.c	⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
5		knoppndvlem8.j	⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
6		knoppndvlem8.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
7		knoppndvlem8.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
8		knoppndvlem8.1	⊢ ( 𝜑 → 2 ∥ 𝑀 )
9	1 2 3 5 6 7	knoppndvlem7	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) = ( ( 𝐶 ↑ 𝐽 ) · ( 𝑇 ‘ ( 𝑀 / 2 ) ) ) )
10		2z	⊢ 2 ∈ ℤ
11	10	a1i	⊢ ( 𝜑 → 2 ∈ ℤ )
12		2ne0	⊢ 2 ≠ 0
13	12	a1i	⊢ ( 𝜑 → 2 ≠ 0 )
14	11 13 6	3jca	⊢ ( 𝜑 → ( 2 ∈ ℤ ∧ 2 ≠ 0 ∧ 𝑀 ∈ ℤ ) )
15		dvdsval2	⊢ ( ( 2 ∈ ℤ ∧ 2 ≠ 0 ∧ 𝑀 ∈ ℤ ) → ( 2 ∥ 𝑀 ↔ ( 𝑀 / 2 ) ∈ ℤ ) )
16	14 15	syl	⊢ ( 𝜑 → ( 2 ∥ 𝑀 ↔ ( 𝑀 / 2 ) ∈ ℤ ) )
17	8 16	mpbid	⊢ ( 𝜑 → ( 𝑀 / 2 ) ∈ ℤ )
18	1 17	dnizeq0	⊢ ( 𝜑 → ( 𝑇 ‘ ( 𝑀 / 2 ) ) = 0 )
19	18	oveq2d	⊢ ( 𝜑 → ( ( 𝐶 ↑ 𝐽 ) · ( 𝑇 ‘ ( 𝑀 / 2 ) ) ) = ( ( 𝐶 ↑ 𝐽 ) · 0 ) )
20	4	knoppndvlem3	⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ( abs ‘ 𝐶 ) < 1 ) )
21	20	simpld	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
22	21	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
23	22 5	expcld	⊢ ( 𝜑 → ( 𝐶 ↑ 𝐽 ) ∈ ℂ )
24	23	mul01d	⊢ ( 𝜑 → ( ( 𝐶 ↑ 𝐽 ) · 0 ) = 0 )
25	9 19 24	3eqtrd	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝐽 ) = 0 )