Metamath Proof Explorer

Theorem knoppcnlem11

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

Ref Expression
Hypotheses knoppcnlem11.t ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
knoppcnlem11.f ⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
knoppcnlem11.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
knoppcnlem11.1 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
Assertion knoppcnlem11 ( 𝜑 → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) : ℕ0 ⟶ ( ℝ –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 knoppcnlem11.t ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2 knoppcnlem11.f ⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3 knoppcnlem11.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 knoppcnlem11.1 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
5 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ∈ ℕ )
6 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ ℝ )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
8 1 2 5 6 7 knoppcnlem7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) = ( 𝑤 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) ‘ 𝑘 ) ) )
9 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) = ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) )
10 simplr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) → 𝑘 ∈ ℕ0 )
11 elnn0uz ⊢ ( 𝑘 ∈ ℕ0 ↔ 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
12 10 11 sylib ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) → 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
13 5 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → 𝑁 ∈ ℕ )
14 6 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → 𝐶 ∈ ℝ )
15 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → 𝑤 ∈ ℝ )
16 elfzuz ⊢ ( 𝑙 ∈ ( 0 ... 𝑘 ) → 𝑙 ∈ ( ℤ≥ ‘ 0 ) )
17 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
18 16 17 eleqtrrdi ⊢ ( 𝑙 ∈ ( 0 ... 𝑘 ) → 𝑙 ∈ ℕ0 )
19 18 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → 𝑙 ∈ ℕ0 )
20 1 2 13 14 15 19 knoppcnlem3 ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) ∈ ℝ )
21 20 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) ∈ ℂ )
22 9 12 21 fsumser ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) → Σ 𝑙 ∈ ( 0 ... 𝑘 ) ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) = ( seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) ‘ 𝑘 ) )
23 22 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑤 ∈ ℝ ) → ( seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) ‘ 𝑘 ) = Σ 𝑙 ∈ ( 0 ... 𝑘 ) ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) )
24 23 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑤 ∈ ℝ ↦ ( seq 0 ( + , ( 𝐹 ‘ 𝑤 ) ) ‘ 𝑘 ) ) = ( 𝑤 ∈ ℝ ↦ Σ 𝑙 ∈ ( 0 ... 𝑘 ) ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) ) )
25 8 24 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) = ( 𝑤 ∈ ℝ ↦ Σ 𝑙 ∈ ( 0 ... 𝑘 ) ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) ) )
26 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
27 retopon ⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
28 27 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) )
29 fzfid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 0 ... 𝑘 ) ∈ Fin )
30 5 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → 𝑁 ∈ ℕ )
31 6 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → 𝐶 ∈ ℝ )
32 18 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → 𝑙 ∈ ℕ0 )
33 1 2 30 31 32 knoppcnlem10 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑙 ∈ ( 0 ... 𝑘 ) ) → ( 𝑤 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
34 26 28 29 33 fsumcn ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑤 ∈ ℝ ↦ Σ 𝑙 ∈ ( 0 ... 𝑘 ) ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
35 ax-resscn ⊢ ℝ ⊆ ℂ
36 ssid ⊢ ℂ ⊆ ℂ
37 35 36 pm3.2i ⊢ ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ )
38 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
39 26 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
40 39 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
41 26 38 40 cncfcn ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℝ –cn→ ℂ ) = ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
42 37 41 ax-mp ⊢ ( ℝ –cn→ ℂ ) = ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) )
43 34 42 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑤 ∈ ℝ ↦ Σ 𝑙 ∈ ( 0 ... 𝑘 ) ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑙 ) ) ∈ ( ℝ –cn→ ℂ ) )
44 25 43 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ∈ ( ℝ –cn→ ℂ ) )
45 44 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ) : ℕ0 ⟶ ( ℝ –cn→ ℂ ) )
46 0z ⊢ 0 ∈ ℤ
47 seqfn ⊢ ( 0 ∈ ℤ → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) Fn ( ℤ≥ ‘ 0 ) )
48 46 47 ax-mp ⊢ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) Fn ( ℤ≥ ‘ 0 )
49 17 fneq2i ⊢ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) Fn ℕ0 ↔ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) Fn ( ℤ≥ ‘ 0 ) )
50 48 49 mpbir ⊢ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) Fn ℕ0
51 dffn5 ⊢ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) Fn ℕ0 ↔ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ) )
52 50 51 mpbi ⊢ seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) )
53 52 feq1i ⊢ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) : ℕ0 ⟶ ( ℝ –cn→ ℂ ) ↔ ( 𝑘 ∈ ℕ0 ↦ ( seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ) : ℕ0 ⟶ ( ℝ –cn→ ℂ ) )
54 45 53 sylibr ⊢ ( 𝜑 → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) : ℕ0 ⟶ ( ℝ –cn→ ℂ ) )