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) Avoid ax-mulf . (Revised by GG, 19-Apr-2025)

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 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
19 3 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
20 18 19 mulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ )
21 20 5 expcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ 𝑀 ) ∈ ℂ )
22 11 14 21 cnmptc ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( ( 2 · 𝑁 ) ↑ 𝑀 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
23 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
24 23 oveq2i ⊢ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) = ( ( topGen ‘ ran (,) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
25 12 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
26 cnrest2r ⊢ ( ( TopOpen ‘ ℂfld ) ∈ Top → ( ( topGen ‘ ran (,) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ⊆ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
27 25 26 ax-mp ⊢ ( ( topGen ‘ ran (,) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ⊆ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) )
28 24 27 eqsstri ⊢ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) ⊆ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) )
29 11 cnmptid ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ 𝑧 ) ∈ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) )
30 28 29 sselid ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ 𝑧 ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
31 12 mpomulcn ⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
32 31 a1i ⊢ ( 𝜑 → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
33 oveq12 ⊢ ( ( 𝑢 = ( ( 2 · 𝑁 ) ↑ 𝑀 ) ∧ 𝑣 = 𝑧 ) → ( 𝑢 · 𝑣 ) = ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) )
34 11 22 30 14 14 32 33 cnmpt12 ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
35 2re ⊢ 2 ∈ ℝ
36 35 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
37 3 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
38 36 37 remulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
39 38 5 reexpcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ 𝑀 ) ∈ ℝ )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ( ( 2 · 𝑁 ) ↑ 𝑀 ) ∈ ℝ )
41 40 6 remulcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ∈ ℝ )
42 41 fmpttd ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) : ℝ ⟶ ℝ )
43 42 frnd ⊢ ( 𝜑 → ran ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ⊆ ℝ )
44 ax-resscn ⊢ ℝ ⊆ ℂ
45 44 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
46 cnrest2 ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ran ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ⊆ ℝ ∧ ℝ ⊆ ℂ ) → ( ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) )
47 13 43 45 46 mp3an2i ⊢ ( 𝜑 → ( ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) )
48 34 47 mpbid ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) )
49 48 24 eleqtrrdi ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( topGen ‘ ran (,) ) ) )
50 ssid ⊢ ℂ ⊆ ℂ
51 cncfss ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℝ –cn→ ℝ ) ⊆ ( ℝ –cn→ ℂ ) )
52 44 50 51 mp2an ⊢ ( ℝ –cn→ ℝ ) ⊆ ( ℝ –cn→ ℂ )
53 1 dnicn ⊢ 𝑇 ∈ ( ℝ –cn→ ℝ )
54 53 a1i ⊢ ( 𝜑 → 𝑇 ∈ ( ℝ –cn→ ℝ ) )
55 52 54 sselid ⊢ ( 𝜑 → 𝑇 ∈ ( ℝ –cn→ ℂ ) )
56 13 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
57 12 23 56 cncfcn ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℝ –cn→ ℂ ) = ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
58 44 50 57 mp2an ⊢ ( ℝ –cn→ ℂ ) = ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) )
59 55 58 eleqtrdi ⊢ ( 𝜑 → 𝑇 ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
60 11 49 59 cnmpt11f ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
61 oveq12 ⊢ ( ( 𝑢 = ( 𝐶 ↑ 𝑀 ) ∧ 𝑣 = ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ) → ( 𝑢 · 𝑣 ) = ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ) )
62 11 17 60 14 14 32 61 cnmpt12 ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝑧 ) ) ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )
63 9 62 eqeltrd ⊢ ( 𝜑 → ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑀 ) ) ∈ ( ( topGen ‘ ran (,) ) Cn ( TopOpen ‘ ℂfld ) ) )