Theorem knoppcnlem4

Description: Lemma for knoppcn . (Contributed by Asger C. Ipsen, 4-Apr-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

	Ref	Expression
Hypotheses	knoppcnlem4.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
	knoppcnlem4.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)$$
	knoppcnlem4.n	$$⊢\phi \to N\in \mathbb{N}$$
	knoppcnlem4.1	$$⊢\phi \to C\in ℝ$$
	knoppcnlem4.2	$$⊢\phi \to A\in ℝ$$
	knoppcnlem4.3	$$⊢\phi \to M\in {\mathbb{N}}_0$$
Assertion	knoppcnlem4	$$⊢\phi \to \left|F\left(A\right)\left(M\right)\right|\le \left(m\in {\mathbb{N}}_0⟼{\left|C\right|}^m\right)\left(M\right)$$

Proof

Step	Hyp	Ref	Expression
1		knoppcnlem4.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
2		knoppcnlem4.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		knoppcnlem4.n	$$⊢\phi \to N\in \mathbb{N}$$
4		knoppcnlem4.1	$$⊢\phi \to C\in ℝ$$
5		knoppcnlem4.2	$$⊢\phi \to A\in ℝ$$
6		knoppcnlem4.3	$$⊢\phi \to M\in {\mathbb{N}}_0$$
7	2 5 6	knoppcnlem1	$$⊢\phi \to F\left(A\right)\left(M\right)=C^{M}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)$$
8	7	fveq2d	$$⊢\phi \to \left|F\left(A\right)\left(M\right)\right|=\left|C^{M}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\right|$$
9	4	recnd	$$⊢\phi \to C\in ℂ$$
10	9 6	expcld	$$⊢\phi \to C^M\in ℂ$$
11		2re	$$⊢2\in ℝ$$
12	11	a1i	$$⊢\phi \to 2\in ℝ$$
13		nnre	$$⊢N\in \mathbb{N}\to N\in ℝ$$
14	3 13	syl	$$⊢\phi \to N\in ℝ$$
15	12 14	remulcld	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℝ$$
16	15 6	reexpcld	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^M\in ℝ$$
17	16 5	remulcld	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\in ℝ$$
18	1 17	dnicld2	$$⊢\phi \to T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\in ℝ$$
19	18	recnd	$$⊢\phi \to T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\in ℂ$$
20	10 19	absmuld	$$⊢\phi \to \left|C^{M}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\right|=\left|C^M\right|\left|T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\right|$$
21	9 6	absexpd	$$⊢\phi \to \left|C^M\right|={\left|C\right|}^M$$
22	21	oveq1d	$$⊢\phi \to \left|C^M\right|\left|T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\right|={\left|C\right|}^M\left|T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\right|$$
23	20 22	eqtrd	$$⊢\phi \to \left|C^{M}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\right|={\left|C\right|}^M\left|T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\right|$$
24	19	abscld	$$⊢\phi \to \left|T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\right|\in ℝ$$
25		1red	$$⊢\phi \to 1\in ℝ$$
26	9	abscld	$$⊢\phi \to \left|C\right|\in ℝ$$
27	26 6	reexpcld	$$⊢\phi \to {\left|C\right|}^M\in ℝ$$
28	9	absge0d	$$⊢\phi \to 0\le \left|C\right|$$
29	26 6 28	expge0d	$$⊢\phi \to 0\le {\left|C\right|}^M$$
30	1	dnival	$$⊢{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\in ℝ\to T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)=\left|⌊{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A+\left(\frac{1}{2}\right)⌋-{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right|$$
31	17 30	syl	$$⊢\phi \to T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)=\left|⌊{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A+\left(\frac{1}{2}\right)⌋-{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right|$$
32	31	fveq2d	$$⊢\phi \to \left|T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\right|=\left|\left|⌊{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A+\left(\frac{1}{2}\right)⌋-{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right|\right|$$
33		halfre	$$⊢\frac{1}{2}\in ℝ$$
34	33	a1i	$$⊢\phi \to \frac{1}{2}\in ℝ$$
35	17 34	readdcld	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A+\left(\frac{1}{2}\right)\in ℝ$$
36		reflcl	$$⊢{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A+\left(\frac{1}{2}\right)\in ℝ\to ⌊{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A+\left(\frac{1}{2}\right)⌋\in ℝ$$
37	35 36	syl	$$⊢\phi \to ⌊{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A+\left(\frac{1}{2}\right)⌋\in ℝ$$
38	37 17	resubcld	$$⊢\phi \to ⌊{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A+\left(\frac{1}{2}\right)⌋-{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\in ℝ$$
39	38	recnd	$$⊢\phi \to ⌊{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A+\left(\frac{1}{2}\right)⌋-{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\in ℂ$$
40		absidm	$$⊢⌊{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A+\left(\frac{1}{2}\right)⌋-{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\in ℂ\to \left|\left|⌊{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A+\left(\frac{1}{2}\right)⌋-{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right|\right|=\left|⌊{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A+\left(\frac{1}{2}\right)⌋-{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right|$$
41	39 40	syl	$$⊢\phi \to \left|\left|⌊{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A+\left(\frac{1}{2}\right)⌋-{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right|\right|=\left|⌊{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A+\left(\frac{1}{2}\right)⌋-{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right|$$
42	32 41	eqtrd	$$⊢\phi \to \left|T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\right|=\left|⌊{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A+\left(\frac{1}{2}\right)⌋-{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right|$$
43	31 18	eqeltrrd	$$⊢\phi \to \left|⌊{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A+\left(\frac{1}{2}\right)⌋-{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right|\in ℝ$$
44		rddif	$$⊢{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\in ℝ\to \left|⌊{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A+\left(\frac{1}{2}\right)⌋-{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right|\le \frac{1}{2}$$
45	17 44	syl	$$⊢\phi \to \left|⌊{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A+\left(\frac{1}{2}\right)⌋-{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right|\le \frac{1}{2}$$
46		halflt1	$$⊢\frac{1}{2}<1$$
47		1re	$$⊢1\in ℝ$$
48	33 47	ltlei	$$⊢\frac{1}{2}<1\to \frac{1}{2}\le 1$$
49	46 48	ax-mp	$$⊢\frac{1}{2}\le 1$$
50	49	a1i	$$⊢\phi \to \frac{1}{2}\le 1$$
51	43 34 25 45 50	letrd	$$⊢\phi \to \left|⌊{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A+\left(\frac{1}{2}\right)⌋-{2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right|\le 1$$
52	42 51	eqbrtrd	$$⊢\phi \to \left|T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\right|\le 1$$
53	24 25 27 29 52	lemul2ad	$$⊢\phi \to {\left|C\right|}^M\left|T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\right|\le {\left|C\right|}^M\cdot 1$$
54		ax-1rid	$$⊢{\left|C\right|}^M\in ℝ\to {\left|C\right|}^M\cdot 1={\left|C\right|}^M$$
55	27 54	syl	$$⊢\phi \to {\left|C\right|}^M\cdot 1={\left|C\right|}^M$$
56	53 55	breqtrd	$$⊢\phi \to {\left|C\right|}^M\left|T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\right|\le {\left|C\right|}^M$$
57	23 56	eqbrtrd	$$⊢\phi \to \left|C^{M}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\right|\le {\left|C\right|}^M$$
58		eqidd	$$⊢\phi \to \left(m\in {\mathbb{N}}_0⟼{\left|C\right|}^m\right)=\left(m\in {\mathbb{N}}_0⟼{\left|C\right|}^m\right)$$
59		oveq2	$$⊢m=M\to {\left|C\right|}^m={\left|C\right|}^M$$
60	59	adantl	$$⊢\left(\phi \wedge m=M\right)\to {\left|C\right|}^m={\left|C\right|}^M$$
61	58 60 6 27	fvmptd	$$⊢\phi \to \left(m\in {\mathbb{N}}_0⟼{\left|C\right|}^m\right)\left(M\right)={\left|C\right|}^M$$
62	61	eqcomd	$$⊢\phi \to {\left|C\right|}^M=\left(m\in {\mathbb{N}}_0⟼{\left|C\right|}^m\right)\left(M\right)$$
63	57 62	breqtrd	$$⊢\phi \to \left|C^{M}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{M}A\right)\right|\le \left(m\in {\mathbb{N}}_0⟼{\left|C\right|}^m\right)\left(M\right)$$
64	8 63	eqbrtrd	$$⊢\phi \to \left|F\left(A\right)\left(M\right)\right|\le \left(m\in {\mathbb{N}}_0⟼{\left|C\right|}^m\right)\left(M\right)$$