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	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
	knoppndvlem7.f	$$⊢F=\left(y\in ℝ⟼\left(n\in {\mathbb{N}}_0⟼C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}y\right)\right)\right)$$
	knoppndvlem7.a	$$⊢A=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
	knoppndvlem7.j	$$⊢\phi \to J\in {\mathbb{N}}_0$$
	knoppndvlem7.m	$$⊢\phi \to M\in \mathbb{Z}$$
	knoppndvlem7.n	$$⊢\phi \to N\in \mathbb{N}$$
Assertion	knoppndvlem7	$$⊢\phi \to F\left(A\right)\left(J\right)=C^{J}T\left(\frac{M}{2}\right)$$

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem7.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
2		knoppndvlem7.f	$$⊢F=\left(y\in ℝ⟼\left(n\in {\mathbb{N}}_0⟼C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}y\right)\right)\right)$$
3		knoppndvlem7.a	$$⊢A=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
4		knoppndvlem7.j	$$⊢\phi \to J\in {\mathbb{N}}_0$$
5		knoppndvlem7.m	$$⊢\phi \to M\in \mathbb{Z}$$
6		knoppndvlem7.n	$$⊢\phi \to N\in \mathbb{N}$$
7	3	a1i	$$⊢\phi \to A=\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
8	4	nn0zd	$$⊢\phi \to J\in \mathbb{Z}$$
9	6 8 5	knoppndvlem1	$$⊢\phi \to \left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℝ$$
10	7 9	eqeltrd	$$⊢\phi \to A\in ℝ$$
11	2 10 4	knoppcnlem1	$$⊢\phi \to F\left(A\right)\left(J\right)=C^{J}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{J}A\right)$$
12	3	oveq2i	$$⊢{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{J}A={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
13	12	a1i	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{J}A={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
14		2cnd	$$⊢\phi \to 2\in ℂ$$
15		nnz	$$⊢N\in \mathbb{N}\to N\in \mathbb{Z}$$
16	6 15	syl	$$⊢\phi \to N\in \mathbb{Z}$$
17	16	zcnd	$$⊢\phi \to N\in ℂ$$
18	14 17	mulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
19	18 4	expcld	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J\in ℂ$$
20		2ne0	$$⊢2\ne 0$$
21	20	a1i	$$⊢\phi \to 2\ne 0$$
22		0red	$$⊢\phi \to 0\in ℝ$$
23		1red	$$⊢\phi \to 1\in ℝ$$
24	16	zred	$$⊢\phi \to N\in ℝ$$
25		0lt1	$$⊢0<1$$
26	25	a1i	$$⊢\phi \to 0<1$$
27		nnge1	$$⊢N\in \mathbb{N}\to 1\le N$$
28	6 27	syl	$$⊢\phi \to 1\le N$$
29	22 23 24 26 28	ltletrd	$$⊢\phi \to 0<N$$
30	22 29	ltned	$$⊢\phi \to 0\ne N$$
31	30	necomd	$$⊢\phi \to N\ne 0$$
32	14 17 21 31	mulne0d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\ne 0$$
33	8	znegcld	$$⊢\phi \to -J\in \mathbb{Z}$$
34	18 32 33	expclzd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}\in ℂ$$
35	34 14 21	divcld	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\in ℂ$$
36	5	zcnd	$$⊢\phi \to M\in ℂ$$
37	19 35 36	mulassd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
38	37	eqcomd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
39	19 34 14 21	divassd	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)$$
40	39	eqcomd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)=\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}$$
41	18 32 8	expnegd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}=\frac{1}{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J}$$
42	41	oveq2d	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}={2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J\left(\frac{1}{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J}\right)$$
43	18 32 8	expne0d	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J\ne 0$$
44	19 43	recidd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J\left(\frac{1}{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J}\right)=1$$
45	42 44	eqtrd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}=1$$
46	45	oveq1d	$$⊢\phi \to \frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}=\frac{1}{2}$$
47	40 46	eqtrd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)=\frac{1}{2}$$
48	47	oveq1d	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=\left(\frac{1}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
49	36 14 21	divrec2d	$$⊢\phi \to \frac{M}{2}=\left(\frac{1}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
50	49	eqcomd	$$⊢\phi \to \left(\frac{1}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=\frac{M}{2}$$
51	38 48 50	3eqtrd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^J\left(\frac{{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{-J}}{2}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=\frac{M}{2}$$
52	13 51	eqtrd	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{J}A=\frac{M}{2}$$
53	52	fveq2d	$$⊢\phi \to T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{J}A\right)=T\left(\frac{M}{2}\right)$$
54	53	oveq2d	$$⊢\phi \to C^{J}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{J}A\right)=C^{J}T\left(\frac{M}{2}\right)$$
55	11 54	eqtrd	$$⊢\phi \to F\left(A\right)\left(J\right)=C^{J}T\left(\frac{M}{2}\right)$$