Metamath Proof Explorer

Theorem knoppcnlem10

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

Ref Expression
Hypotheses knoppcnlem10.t ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
knoppcnlem10.f ⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
knoppcnlem10.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
knoppcnlem10.1 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
knoppcnlem10.2 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
Assertion knoppcnlem10 ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑀 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )

Proof

Step Hyp Ref Expression
1 knoppcnlem10.t ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2 knoppcnlem10.f ⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3 knoppcnlem10.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 knoppcnlem10.1 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
5 knoppcnlem10.2 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
6 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → 𝑧 ∈ ℝ )
7 5 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → 𝑀 ∈ ℕ0 )
8 2 6 7 knoppcnlem1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑀 ) = ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ) )
9 8 mpteq2dva ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑀 ) ) = ( 𝑧 ∈ ℝ ↦ ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ) ) )
10 retopon ⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
11 10 a1i ⊢ ( 𝜑 → ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) )
12 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
13 12 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
14 13 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
15 4 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
16 15 5 expcld ⊢ ( 𝜑 → ( 𝐶 ↑ 𝑀 ) ∈ ℂ )
17 11 14 16 cnmptc ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( 𝐶 ↑ 𝑀 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
18 2re ⊢ 2 ∈ ℝ
19 18 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
20 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
21 3 20 syl ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
22 19 21 remulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
23 22 5 reexpcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ 𝑀 ) ∈ ℝ )
24 23 recnd ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ 𝑀 ) ∈ ℂ )
25 11 14 24 cnmptc ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( ( 2 · 𝑁 ) ↑ 𝑀 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
26 12 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
27 26 oveq2i ⊢ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) = ( ( topGen ‘ ran (,) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
28 13 topontopi ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
29 cnrest2r ⊢ ( ( TopOpen ‘ ℂfld ) ∈ Top → ( ( topGen ‘ ran (,) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ⊆ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
30 28 29 ax-mp ⊢ ( ( topGen ‘ ran (,) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ⊆ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) )
31 27 30 eqsstri ⊢ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) ⊆ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) )
32 11 cnmptid ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ 𝑧 ) ∈ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) )
33 31 32 sselid ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ 𝑧 ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
34 12 mulcn ⊢ · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
35 34 a1i ⊢ ( 𝜑 → · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
36 11 25 33 35 cnmpt12f ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
37 23 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ( ( 2 · 𝑁 ) ↑ 𝑀 ) ∈ ℝ )
38 37 6 remulcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ∈ ℝ )
39 38 fmpttd ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) : ℝ ⟶ ℝ )
40 39 frnd ⊢ ( 𝜑 → ran ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ⊆ ℝ )
41 ax-resscn ⊢ ℝ ⊆ ℂ
42 41 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
43 14 40 42 3jca ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ran ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ⊆ ℝ ∧ ℝ ⊆ ℂ ) )
44 cnrest2 ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ran ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) )
45 43 44 syl ⊢ ( 𝜑 → ( ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) )
46 36 45 mpbid ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) )
47 46 27 eleqtrrdi ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) )
48 ssid ⊢ ℂ ⊆ ℂ
49 41 48 pm3.2i ⊢ ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ )
50 cncfss ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℝ –cn→ ℝ ) ⊆ ( ℝ –cn→ ℂ ) )
51 49 50 ax-mp ⊢ ( ℝ –cn→ ℝ ) ⊆ ( ℝ –cn→ ℂ )
52 1 dnicn ⊢ 𝑇 ∈ ( ℝ –cn→ ℝ )
53 52 a1i ⊢ ( 𝜑 → 𝑇 ∈ ( ℝ –cn→ ℝ ) )
54 51 53 sselid ⊢ ( 𝜑 → 𝑇 ∈ ( ℝ –cn→ ℂ ) )
55 13 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
56 12 26 55 cncfcn ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℝ –cn→ ℂ ) = ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
57 49 56 ax-mp ⊢ ( ℝ –cn→ ℂ ) = ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) )
58 54 57 eleqtrdi ⊢ ( 𝜑 → 𝑇 ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
59 11 47 58 cnmpt11f ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
60 11 17 59 35 cnmpt12f ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
61 9 60 eqeltrd ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑀 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )