Theorem knoppf

Description: Knopp's function is a function. (Contributed by Asger C. Ipsen, 25-Aug-2021)

	Ref	Expression
Hypotheses	knoppf.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
	knoppf.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
	knoppf.w	⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
	knoppf.c	⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
	knoppf.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion	knoppf	⊢ ( 𝜑 → 𝑊 : ℝ ⟶ ℝ )

Proof

Step	Hyp	Ref	Expression
1		knoppf.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		knoppf.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3		knoppf.w	⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
4		knoppf.c	⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
5		knoppf.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
6		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
7		0zd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → 0 ∈ ℤ )
8		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
9	5	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → 𝑁 ∈ ℕ )
10	9	adantr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑖 ∈ ℕ0 ) → 𝑁 ∈ ℕ )
11	4	knoppndvlem3	⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ( abs ‘ 𝐶 ) < 1 ) )
12	11	simpld	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → 𝐶 ∈ ℝ )
14	13	adantr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑖 ∈ ℕ0 ) → 𝐶 ∈ ℝ )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → 𝑤 ∈ ℝ )
16	15	adantr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑖 ∈ ℕ0 ) → 𝑤 ∈ ℝ )
17		simpr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℕ0 )
18	1 2 10 14 16 17	knoppcnlem3	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) ∈ ℝ )
19		fveq2	⊢ ( 𝑤 = 𝑧 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) )
20	19	fveq1d	⊢ ( 𝑤 = 𝑧 → ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) = ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑖 ) )
21	20	sumeq2sdv	⊢ ( 𝑤 = 𝑧 → Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) = Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑖 ) )
22	21	cbvmptv	⊢ ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) ) = ( 𝑧 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑖 ) )
23	3 22	eqtri	⊢ 𝑊 = ( 𝑧 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑖 ) )
24	4	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → 𝐶 ∈ ( - 1 (,) 1 ) )
25	1 2 23 15 24 9	knoppndvlem4	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) ⇝ ( 𝑊 ‘ 𝑤 ) )
26		seqex	⊢ seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) ∈ V
27		fvex	⊢ ( 𝑊 ‘ 𝑤 ) ∈ V
28	26 27	breldm	⊢ ( seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) ⇝ ( 𝑊 ‘ 𝑤 ) → seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) ∈ dom ⇝ )
29	25 28	syl	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) ∈ dom ⇝ )
30	6 7 8 18 29	isumrecl	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) ∈ ℝ )
31	30 3	fmptd	⊢ ( 𝜑 → 𝑊 : ℝ ⟶ ℝ )