Theorem cnndvlem1

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

	Ref	Expression
Hypotheses	cnndvlem1.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
	cnndvlem1.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( ( 1 / 2 ) ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 3 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
	cnndvlem1.w	⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
Assertion	cnndvlem1	⊢ ( 𝑊 ∈ ( ℝ –cn→ ℝ ) ∧ dom ( ℝ D 𝑊 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		cnndvlem1.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		cnndvlem1.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( ( 1 / 2 ) ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 3 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3		cnndvlem1.w	⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
4		3nn	⊢ 3 ∈ ℕ
5	4	a1i	⊢ ( ⊤ → 3 ∈ ℕ )
6		neg1rr	⊢ - 1 ∈ ℝ
7	6	rexri	⊢ - 1 ∈ ℝ*
8		1re	⊢ 1 ∈ ℝ
9	8	rexri	⊢ 1 ∈ ℝ*
10		halfre	⊢ ( 1 / 2 ) ∈ ℝ
11	10	rexri	⊢ ( 1 / 2 ) ∈ ℝ*
12	7 9 11	3pm3.2i	⊢ ( - 1 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ ( 1 / 2 ) ∈ ℝ* )
13		neg1lt0	⊢ - 1 < 0
14		halfgt0	⊢ 0 < ( 1 / 2 )
15	13 14	pm3.2i	⊢ ( - 1 < 0 ∧ 0 < ( 1 / 2 ) )
16		0re	⊢ 0 ∈ ℝ
17	6 16 10	lttri	⊢ ( ( - 1 < 0 ∧ 0 < ( 1 / 2 ) ) → - 1 < ( 1 / 2 ) )
18	15 17	ax-mp	⊢ - 1 < ( 1 / 2 )
19		halflt1	⊢ ( 1 / 2 ) < 1
20	18 19	pm3.2i	⊢ ( - 1 < ( 1 / 2 ) ∧ ( 1 / 2 ) < 1 )
21	12 20	pm3.2i	⊢ ( ( - 1 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ ( 1 / 2 ) ∈ ℝ* ) ∧ ( - 1 < ( 1 / 2 ) ∧ ( 1 / 2 ) < 1 ) )
22		elioo3g	⊢ ( ( 1 / 2 ) ∈ ( - 1 (,) 1 ) ↔ ( ( - 1 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ ( 1 / 2 ) ∈ ℝ* ) ∧ ( - 1 < ( 1 / 2 ) ∧ ( 1 / 2 ) < 1 ) ) )
23	21 22	mpbir	⊢ ( 1 / 2 ) ∈ ( - 1 (,) 1 )
24	23	a1i	⊢ ( ⊤ → ( 1 / 2 ) ∈ ( - 1 (,) 1 ) )
25	1 2 3 5 24	knoppcn2	⊢ ( ⊤ → 𝑊 ∈ ( ℝ –cn→ ℝ ) )
26	25	mptru	⊢ 𝑊 ∈ ( ℝ –cn→ ℝ )
27		2cn	⊢ 2 ∈ ℂ
28	27	mulid2i	⊢ ( 1 · 2 ) = 2
29		2lt3	⊢ 2 < 3
30	28 29	eqbrtri	⊢ ( 1 · 2 ) < 3
31		2pos	⊢ 0 < 2
32	4	nnrei	⊢ 3 ∈ ℝ
33		2re	⊢ 2 ∈ ℝ
34	8 32 33	ltmuldivi	⊢ ( 0 < 2 → ( ( 1 · 2 ) < 3 ↔ 1 < ( 3 / 2 ) ) )
35	31 34	ax-mp	⊢ ( ( 1 · 2 ) < 3 ↔ 1 < ( 3 / 2 ) )
36	30 35	mpbi	⊢ 1 < ( 3 / 2 )
37	16 10 14	ltleii	⊢ 0 ≤ ( 1 / 2 )
38	10	absidi	⊢ ( 0 ≤ ( 1 / 2 ) → ( abs ‘ ( 1 / 2 ) ) = ( 1 / 2 ) )
39	37 38	ax-mp	⊢ ( abs ‘ ( 1 / 2 ) ) = ( 1 / 2 )
40	39	oveq2i	⊢ ( 3 · ( abs ‘ ( 1 / 2 ) ) ) = ( 3 · ( 1 / 2 ) )
41	4	nncni	⊢ 3 ∈ ℂ
42		2ne0	⊢ 2 ≠ 0
43	41 27 42	divreci	⊢ ( 3 / 2 ) = ( 3 · ( 1 / 2 ) )
44	43	eqcomi	⊢ ( 3 · ( 1 / 2 ) ) = ( 3 / 2 )
45	40 44	eqtri	⊢ ( 3 · ( abs ‘ ( 1 / 2 ) ) ) = ( 3 / 2 )
46	36 45	breqtrri	⊢ 1 < ( 3 · ( abs ‘ ( 1 / 2 ) ) )
47	46	a1i	⊢ ( ⊤ → 1 < ( 3 · ( abs ‘ ( 1 / 2 ) ) ) )
48	1 2 3 24 5 47	knoppndv	⊢ ( ⊤ → dom ( ℝ D 𝑊 ) = ∅ )
49	48	mptru	⊢ dom ( ℝ D 𝑊 ) = ∅
50	26 49	pm3.2i	⊢ ( 𝑊 ∈ ( ℝ –cn→ ℝ ) ∧ dom ( ℝ D 𝑊 ) = ∅ )