Theorem cnndvlem1

Description: Lemma for cnndv . (Contributed by Asger C. Ipsen, 25-Aug-2021)

	Ref	Expression
Hypotheses	cnndvlem1.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
	cnndvlem1.f	$$⊢F=\left(y\in ℝ⟼\left(n\in {\mathbb{N}}_0⟼{\left(\frac{1}{2}\right)}^{n}T\left({2\cdot 3}^{n}y\right)\right)\right)$$
	cnndvlem1.w	$$⊢W=\left(w\in ℝ⟼\sum _{i\in {\mathbb{N}}_0}F\left(w\right)\left(i\right)\right)$$
Assertion	cnndvlem1	$$⊢\left(W:ℝ\underset{cn}{⟶}ℝ\wedge \mathrm{dom}{W}_{ℝ}^{\prime }=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		cnndvlem1.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
2		cnndvlem1.f	$$⊢F=\left(y\in ℝ⟼\left(n\in {\mathbb{N}}_0⟼{\left(\frac{1}{2}\right)}^{n}T\left({2\cdot 3}^{n}y\right)\right)\right)$$
3		cnndvlem1.w	$$⊢W=\left(w\in ℝ⟼\sum _{i\in {\mathbb{N}}_0}F\left(w\right)\left(i\right)\right)$$
4		3nn	$$⊢3\in \mathbb{N}$$
5	4	a1i	$$⊢\top \to 3\in \mathbb{N}$$
6		neg1rr	$$⊢-1\in ℝ$$
7	6	rexri	$$⊢-1\in {ℝ}^{*}$$
8		1re	$$⊢1\in ℝ$$
9	8	rexri	$$⊢1\in {ℝ}^{*}$$
10		halfre	$$⊢\frac{1}{2}\in ℝ$$
11	10	rexri	$$⊢\frac{1}{2}\in {ℝ}^{*}$$
12	7 9 11	3pm3.2i	$$⊢\left(-1\in {ℝ}^{*}\wedge 1\in {ℝ}^{*}\wedge \frac{1}{2}\in {ℝ}^{*}\right)$$
13		neg1lt0	$$⊢-1<0$$
14		halfgt0	$$⊢0<\frac{1}{2}$$
15	13 14	pm3.2i	$$⊢\left(-1<0\wedge 0<\frac{1}{2}\right)$$
16		0re	$$⊢0\in ℝ$$
17	6 16 10	lttri	$$⊢\left(-1<0\wedge 0<\frac{1}{2}\right)\to -1<\frac{1}{2}$$
18	15 17	ax-mp	$$⊢-1<\frac{1}{2}$$
19		halflt1	$$⊢\frac{1}{2}<1$$
20	18 19	pm3.2i	$$⊢\left(-1<\frac{1}{2}\wedge \frac{1}{2}<1\right)$$
21	12 20	pm3.2i	$$⊢\left(\left(-1\in {ℝ}^{*}\wedge 1\in {ℝ}^{*}\wedge \frac{1}{2}\in {ℝ}^{*}\right)\wedge \left(-1<\frac{1}{2}\wedge \frac{1}{2}<1\right)\right)$$
22		elioo3g	$$⊢\frac{1}{2}\in \left(-1,1\right)\leftrightarrow \left(\left(-1\in {ℝ}^{*}\wedge 1\in {ℝ}^{*}\wedge \frac{1}{2}\in {ℝ}^{*}\right)\wedge \left(-1<\frac{1}{2}\wedge \frac{1}{2}<1\right)\right)$$
23	21 22	mpbir	$$⊢\frac{1}{2}\in \left(-1,1\right)$$
24	23	a1i	$$⊢\top \to \frac{1}{2}\in \left(-1,1\right)$$
25	1 2 3 5 24	knoppcn2	$$⊢\top \to W:ℝ\underset{cn}{⟶}ℝ$$
26	25	mptru	$$⊢W:ℝ\underset{cn}{⟶}ℝ$$
27		2cn	$$⊢2\in ℂ$$
28	27	mullidi	$$⊢1\cdot 2=2$$
29		2lt3	$$⊢2<3$$
30	28 29	eqbrtri	$$⊢1\cdot 2<3$$
31		2pos	$$⊢0<2$$
32	4	nnrei	$$⊢3\in ℝ$$
33		2re	$$⊢2\in ℝ$$
34	8 32 33	ltmuldivi	$$⊢0<2\to \left(1\cdot 2<3\leftrightarrow 1<\frac{3}{2}\right)$$
35	31 34	ax-mp	$$⊢1\cdot 2<3\leftrightarrow 1<\frac{3}{2}$$
36	30 35	mpbi	$$⊢1<\frac{3}{2}$$
37	16 10 14	ltleii	$$⊢0\le \frac{1}{2}$$
38	10	absidi	$$⊢0\le \frac{1}{2}\to \left|\frac{1}{2}\right|=\frac{1}{2}$$
39	37 38	ax-mp	$$⊢\left|\frac{1}{2}\right|=\frac{1}{2}$$
40	39	oveq2i	$$⊢3\left|\frac{1}{2}\right|=3\left(\frac{1}{2}\right)$$
41	4	nncni	$$⊢3\in ℂ$$
42		2ne0	$$⊢2\ne 0$$
43	41 27 42	divreci	$$⊢\frac{3}{2}=3\left(\frac{1}{2}\right)$$
44	43	eqcomi	$$⊢3\left(\frac{1}{2}\right)=\frac{3}{2}$$
45	40 44	eqtri	$$⊢3\left|\frac{1}{2}\right|=\frac{3}{2}$$
46	36 45	breqtrri	$$⊢1<3\left|\frac{1}{2}\right|$$
47	46	a1i	$$⊢\top \to 1<3\left|\frac{1}{2}\right|$$
48	1 2 3 24 5 47	knoppndv	$$⊢\top \to \mathrm{dom}{W}_{ℝ}^{\prime }=\varnothing$$
49	48	mptru	$$⊢\mathrm{dom}{W}_{ℝ}^{\prime }=\varnothing$$
50	26 49	pm3.2i	$$⊢\left(W:ℝ\underset{cn}{⟶}ℝ\wedge \mathrm{dom}{W}_{ℝ}^{\prime }=\varnothing \right)$$