Metamath Proof Explorer

Theorem knoppf

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

Ref Expression
Hypotheses knoppf.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
knoppf.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
knoppf.w ⊢ W = w ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ w ⁡ i
knoppf.c ⊢ φ → C ∈ − 1 1
knoppf.n ⊢ φ → N ∈ ℕ
Assertion knoppf ⊢ φ → W : ℝ ⟶ ℝ

Proof

Step Hyp Ref Expression
1 knoppf.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 knoppf.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
3 knoppf.w ⊢ W = w ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ w ⁡ i
4 knoppf.c ⊢ φ → C ∈ − 1 1
5 knoppf.n ⊢ φ → N ∈ ℕ
6 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
7 0zd ⊢ φ ∧ w ∈ ℝ → 0 ∈ ℤ
8 eqidd ⊢ φ ∧ w ∈ ℝ ∧ i ∈ ℕ 0 → F ⁡ w ⁡ i = F ⁡ w ⁡ i
9 5 adantr ⊢ φ ∧ w ∈ ℝ → N ∈ ℕ
10 9 adantr ⊢ φ ∧ w ∈ ℝ ∧ i ∈ ℕ 0 → N ∈ ℕ
11 4 knoppndvlem3 ⊢ φ → C ∈ ℝ ∧ C < 1
12 11 simpld ⊢ φ → C ∈ ℝ
13 12 adantr ⊢ φ ∧ w ∈ ℝ → C ∈ ℝ
14 13 adantr ⊢ φ ∧ w ∈ ℝ ∧ i ∈ ℕ 0 → C ∈ ℝ
15 simpr ⊢ φ ∧ w ∈ ℝ → w ∈ ℝ
16 15 adantr ⊢ φ ∧ w ∈ ℝ ∧ i ∈ ℕ 0 → w ∈ ℝ
17 simpr ⊢ φ ∧ w ∈ ℝ ∧ i ∈ ℕ 0 → i ∈ ℕ 0
18 1 2 10 14 16 17 knoppcnlem3 ⊢ φ ∧ w ∈ ℝ ∧ i ∈ ℕ 0 → F ⁡ w ⁡ i ∈ ℝ
19 fveq2 ⊢ w = z → F ⁡ w = F ⁡ z
20 19 fveq1d ⊢ w = z → F ⁡ w ⁡ i = F ⁡ z ⁡ i
21 20 sumeq2sdv ⊢ w = z → ∑ i ∈ ℕ 0 F ⁡ w ⁡ i = ∑ i ∈ ℕ 0 F ⁡ z ⁡ i
22 21 cbvmptv ⊢ w ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ w ⁡ i = z ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ z ⁡ i
23 3 22 eqtri ⊢ W = z ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ z ⁡ i
24 4 adantr ⊢ φ ∧ w ∈ ℝ → C ∈ − 1 1
25 1 2 23 15 24 9 knoppndvlem4 ⊢ φ ∧ w ∈ ℝ → seq 0 + F ⁡ w ⇝ W ⁡ w
26 seqex ⊢ seq 0 + F ⁡ w ∈ V
27 fvex ⊢ W ⁡ w ∈ V
28 26 27 breldm ⊢ seq 0 + F ⁡ w ⇝ W ⁡ w → seq 0 + F ⁡ w ∈ dom ⁡ ⇝
29 25 28 syl ⊢ φ ∧ w ∈ ℝ → seq 0 + F ⁡ w ∈ dom ⁡ ⇝
30 6 7 8 18 29 isumrecl ⊢ φ ∧ w ∈ ℝ → ∑ i ∈ ℕ 0 F ⁡ w ⁡ i ∈ ℝ
31 30 3 fmptd ⊢ φ → W : ℝ ⟶ ℝ