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 ⊢ 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 2re ⊢ 2 ∈ ℝ
19 18 a1i ⊢ φ → 2 ∈ ℝ
20 nnre ⊢ N ∈ ℕ → N ∈ ℝ
21 3 20 syl ⊢ φ → N ∈ ℝ
22 19 21 remulcld ⊢ φ → 2 ⋅ N ∈ ℝ
23 22 5 reexpcld ⊢ φ → 2 ⋅ N M ∈ ℝ
24 23 recnd ⊢ φ → 2 ⋅ N M ∈ ℂ
25 11 14 24 cnmptc ⊢ φ → z ∈ ℝ ⟼ 2 ⋅ N M ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld
26 12 tgioo2 ⊢ topGen ⁡ ran ⁡ . = TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
27 26 oveq2i ⊢ topGen ⁡ ran ⁡ . Cn topGen ⁡ ran ⁡ . = topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
28 13 topontopi ⊢ TopOpen ⁡ ℂ fld ∈ Top
29 cnrest2r ⊢ TopOpen ⁡ ℂ fld ∈ Top → topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ ⊆ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld
30 28 29 ax-mp ⊢ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ ⊆ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld
31 27 30 eqsstri ⊢ topGen ⁡ ran ⁡ . Cn topGen ⁡ ran ⁡ . ⊆ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld
32 11 cnmptid ⊢ φ → z ∈ ℝ ⟼ z ∈ topGen ⁡ ran ⁡ . Cn topGen ⁡ ran ⁡ .
33 31 32 sseldi ⊢ φ → z ∈ ℝ ⟼ z ∈ 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 ⊢ φ → z ∈ ℝ ⟼ 2 ⋅ N M ⁢ z ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld
37 23 adantr ⊢ φ ∧ z ∈ ℝ → 2 ⋅ N M ∈ ℝ
38 37 6 remulcld ⊢ φ ∧ z ∈ ℝ → 2 ⋅ N M ⁢ z ∈ ℝ
39 38 fmpttd ⊢ φ → z ∈ ℝ ⟼ 2 ⋅ N M ⁢ z : ℝ ⟶ ℝ
40 39 frnd ⊢ φ → ran ⁡ z ∈ ℝ ⟼ 2 ⋅ N M ⁢ z ⊆ ℝ
41 ax-resscn ⊢ ℝ ⊆ ℂ
42 41 a1i ⊢ φ → ℝ ⊆ ℂ
43 14 40 42 3jca ⊢ φ → TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ ∧ ran ⁡ z ∈ ℝ ⟼ 2 ⋅ N M ⁢ z ⊆ ℝ ∧ ℝ ⊆ ℂ
44 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 ↾ 𝑡 ℝ
45 43 44 syl ⊢ φ → z ∈ ℝ ⟼ 2 ⋅ N M ⁢ z ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld ↔ z ∈ ℝ ⟼ 2 ⋅ N M ⁢ z ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
46 36 45 mpbid ⊢ φ → z ∈ ℝ ⟼ 2 ⋅ N M ⁢ z ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
47 46 27 eleqtrrdi ⊢ φ → z ∈ ℝ ⟼ 2 ⋅ N M ⁢ z ∈ 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 ⊢ T : ℝ ⟶cn ℝ
53 52 a1i ⊢ φ → T : ℝ ⟶cn ℝ
54 51 53 sseldi ⊢ φ → T : ℝ ⟶cn ℂ
55 13 toponrestid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ
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 ⊢ φ → T ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld
59 11 47 58 cnmpt11f ⊢ φ → z ∈ ℝ ⟼ T ⁡ 2 ⋅ N M ⁢ z ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld
60 11 17 59 35 cnmpt12f ⊢ φ → z ∈ ℝ ⟼ C M ⁢ T ⁡ 2 ⋅ N M ⁢ z ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld
61 9 60 eqeltrd ⊢ φ → z ∈ ℝ ⟼ F ⁡ z ⁡ M ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld