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 ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
knoppcnlem10.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
knoppcnlem10.n ⊢ φ → N ∈ ℕ
knoppcnlem10.1 ⊢ φ → C ∈ ℝ
knoppcnlem10.2 ⊢ φ → M ∈ ℕ 0
Assertion knoppcnlem10 ⊢ φ → z ∈ ℝ ⟼ F ⁡ z ⁡ M ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld

Proof

Step Hyp Ref Expression
1 knoppcnlem10.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 knoppcnlem10.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
3 knoppcnlem10.n ⊢ φ → N ∈ ℕ
4 knoppcnlem10.1 ⊢ φ → C ∈ ℝ
5 knoppcnlem10.2 ⊢ φ → M ∈ ℕ 0
6 simpr ⊢ φ ∧ z ∈ ℝ → z ∈ ℝ
7 5 adantr ⊢ φ ∧ z ∈ ℝ → M ∈ ℕ 0
8 2 6 7 knoppcnlem1 ⊢ φ ∧ z ∈ ℝ → F ⁡ z ⁡ M = C M ⁢ T ⁡ 2 ⋅ N M ⁢ z
9 8 mpteq2dva ⊢ φ → z ∈ ℝ ⟼ F ⁡ z ⁡ M = z ∈ ℝ ⟼ C M ⁢ T ⁡ 2 ⋅ N M ⁢ z
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 ⊢ φ → C ∈ ℂ
16 15 5 expcld ⊢ φ → C M ∈ ℂ
17 11 14 16 cnmptc ⊢ φ → z ∈ ℝ ⟼ C M ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld
18 2cnd ⊢ φ → 2 ∈ ℂ
19 3 nncnd ⊢ φ → N ∈ ℂ
20 18 19 mulcld ⊢ φ → 2 ⋅ N ∈ ℂ
21 20 5 expcld ⊢ φ → 2 ⋅ N M ∈ ℂ
22 11 14 21 cnmptc ⊢ φ → z ∈ ℝ ⟼ 2 ⋅ N M ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld
23 12 tgioo2 ⊢ topGen ⁡ ran ⁡ . = TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
24 23 oveq2i ⊢ topGen ⁡ ran ⁡ . Cn topGen ⁡ ran ⁡ . = topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
25 12 cnfldtop ⊢ TopOpen ⁡ ℂ fld ∈ Top
26 cnrest2r ⊢ TopOpen ⁡ ℂ fld ∈ Top → topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ ⊆ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld
27 25 26 ax-mp ⊢ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ ⊆ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld
28 24 27 eqsstri ⊢ topGen ⁡ ran ⁡ . Cn topGen ⁡ ran ⁡ . ⊆ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld
29 11 cnmptid ⊢ φ → z ∈ ℝ ⟼ z ∈ topGen ⁡ ran ⁡ . Cn topGen ⁡ ran ⁡ .
30 28 29 sselid ⊢ φ → z ∈ ℝ ⟼ z ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld
31 12 mpomulcn ⊢ u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
32 31 a1i ⊢ φ → u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
33 oveq12 ⊢ u = 2 ⋅ N M ∧ v = z → u ⁢ v = 2 ⋅ N M ⁢ z
34 11 22 30 14 14 32 33 cnmpt12 ⊢ φ → z ∈ ℝ ⟼ 2 ⋅ N M ⁢ z ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld
35 2re ⊢ 2 ∈ ℝ
36 35 a1i ⊢ φ → 2 ∈ ℝ
37 3 nnred ⊢ φ → N ∈ ℝ
38 36 37 remulcld ⊢ φ → 2 ⋅ N ∈ ℝ
39 38 5 reexpcld ⊢ φ → 2 ⋅ N M ∈ ℝ
40 39 adantr ⊢ φ ∧ z ∈ ℝ → 2 ⋅ N M ∈ ℝ
41 40 6 remulcld ⊢ φ ∧ z ∈ ℝ → 2 ⋅ N M ⁢ z ∈ ℝ
42 41 fmpttd ⊢ φ → z ∈ ℝ ⟼ 2 ⋅ N M ⁢ z : ℝ ⟶ ℝ
43 42 frnd ⊢ φ → ran ⁡ z ∈ ℝ ⟼ 2 ⋅ N M ⁢ z ⊆ ℝ
44 ax-resscn ⊢ ℝ ⊆ ℂ
45 44 a1i ⊢ φ → ℝ ⊆ ℂ
46 cnrest2 ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ ∧ ran ⁡ z ∈ ℝ ⟼ 2 ⋅ N M ⁢ z ⊆ ℝ ∧ ℝ ⊆ ℂ → z ∈ ℝ ⟼ 2 ⋅ N M ⁢ z ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld ↔ z ∈ ℝ ⟼ 2 ⋅ N M ⁢ z ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
47 13 43 45 46 mp3an2i ⊢ φ → z ∈ ℝ ⟼ 2 ⋅ N M ⁢ z ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld ↔ z ∈ ℝ ⟼ 2 ⋅ N M ⁢ z ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
48 34 47 mpbid ⊢ φ → z ∈ ℝ ⟼ 2 ⋅ N M ⁢ z ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
49 48 24 eleqtrrdi ⊢ φ → z ∈ ℝ ⟼ 2 ⋅ N M ⁢ z ∈ topGen ⁡ ran ⁡ . Cn topGen ⁡ ran ⁡ .
50 ssid ⊢ ℂ ⊆ ℂ
51 cncfss ⊢ ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ → ℝ ⟶cn ℝ ⊆ ℝ ⟶cn ℂ
52 44 50 51 mp2an ⊢ ℝ ⟶cn ℝ ⊆ ℝ ⟶cn ℂ
53 1 dnicn ⊢ T : ℝ ⟶cn ℝ
54 53 a1i ⊢ φ → T : ℝ ⟶cn ℝ
55 52 54 sselid ⊢ φ → T : ℝ ⟶cn ℂ
56 13 toponrestid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ
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 ⊢ φ → T ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld
60 11 49 59 cnmpt11f ⊢ φ → z ∈ ℝ ⟼ T ⁡ 2 ⋅ N M ⁢ z ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld
61 oveq12 ⊢ u = C M ∧ v = T ⁡ 2 ⋅ N M ⁢ z → u ⁢ v = C M ⁢ T ⁡ 2 ⋅ N M ⁢ z
62 11 17 60 14 14 32 61 cnmpt12 ⊢ φ → z ∈ ℝ ⟼ C M ⁢ T ⁡ 2 ⋅ N M ⁢ z ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld
63 9 62 eqeltrd ⊢ φ → z ∈ ℝ ⟼ F ⁡ z ⁡ M ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld