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 ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
knoppcnlem11.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
knoppcnlem11.n ⊢ φ → N ∈ ℕ
knoppcnlem11.1 ⊢ φ → C ∈ ℝ
Assertion knoppcnlem11 ⊢ φ → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m : ℕ 0 ⟶ ℝ ⟶cn ℂ

Proof

Step Hyp Ref Expression
1 knoppcnlem11.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 knoppcnlem11.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
3 knoppcnlem11.n ⊢ φ → N ∈ ℕ
4 knoppcnlem11.1 ⊢ φ → C ∈ ℝ
5 3 adantr ⊢ φ ∧ k ∈ ℕ 0 → N ∈ ℕ
6 4 adantr ⊢ φ ∧ k ∈ ℕ 0 → C ∈ ℝ
7 simpr ⊢ φ ∧ k ∈ ℕ 0 → k ∈ ℕ 0
8 1 2 5 6 7 knoppcnlem7 ⊢ φ ∧ k ∈ ℕ 0 → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k = w ∈ ℝ ⟼ seq 0 + F ⁡ w ⁡ k
9 eqidd ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ ∧ l ∈ 0 … k → F ⁡ w ⁡ l = F ⁡ w ⁡ l
10 simplr ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ → k ∈ ℕ 0
11 elnn0uz ⊢ k ∈ ℕ 0 ↔ k ∈ ℤ ≥ 0
12 10 11 sylib ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ → k ∈ ℤ ≥ 0
13 5 ad2antrr ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ ∧ l ∈ 0 … k → N ∈ ℕ
14 6 ad2antrr ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ ∧ l ∈ 0 … k → C ∈ ℝ
15 simplr ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ ∧ l ∈ 0 … k → w ∈ ℝ
16 elfzuz ⊢ l ∈ 0 … k → l ∈ ℤ ≥ 0
17 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
18 16 17 eleqtrrdi ⊢ l ∈ 0 … k → l ∈ ℕ 0
19 18 adantl ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ ∧ l ∈ 0 … k → l ∈ ℕ 0
20 1 2 13 14 15 19 knoppcnlem3 ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ ∧ l ∈ 0 … k → F ⁡ w ⁡ l ∈ ℝ
21 20 recnd ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ ∧ l ∈ 0 … k → F ⁡ w ⁡ l ∈ ℂ
22 9 12 21 fsumser ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ → ∑ l = 0 k F ⁡ w ⁡ l = seq 0 + F ⁡ w ⁡ k
23 22 eqcomd ⊢ φ ∧ k ∈ ℕ 0 ∧ w ∈ ℝ → seq 0 + F ⁡ w ⁡ k = ∑ l = 0 k F ⁡ w ⁡ l
24 23 mpteq2dva ⊢ φ ∧ k ∈ ℕ 0 → w ∈ ℝ ⟼ seq 0 + F ⁡ w ⁡ k = w ∈ ℝ ⟼ ∑ l = 0 k F ⁡ w ⁡ l
25 8 24 eqtrd ⊢ φ ∧ k ∈ ℕ 0 → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k = w ∈ ℝ ⟼ ∑ l = 0 k F ⁡ w ⁡ l
26 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
27 retopon ⊢ topGen ⁡ ran ⁡ . ∈ TopOn ⁡ ℝ
28 27 a1i ⊢ φ ∧ k ∈ ℕ 0 → topGen ⁡ ran ⁡ . ∈ TopOn ⁡ ℝ
29 fzfid ⊢ φ ∧ k ∈ ℕ 0 → 0 … k ∈ Fin
30 5 adantr ⊢ φ ∧ k ∈ ℕ 0 ∧ l ∈ 0 … k → N ∈ ℕ
31 6 adantr ⊢ φ ∧ k ∈ ℕ 0 ∧ l ∈ 0 … k → C ∈ ℝ
32 18 adantl ⊢ φ ∧ k ∈ ℕ 0 ∧ l ∈ 0 … k → l ∈ ℕ 0
33 1 2 30 31 32 knoppcnlem10 ⊢ φ ∧ k ∈ ℕ 0 ∧ l ∈ 0 … k → w ∈ ℝ ⟼ F ⁡ w ⁡ l ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld
34 26 28 29 33 fsumcn ⊢ φ ∧ k ∈ ℕ 0 → w ∈ ℝ ⟼ ∑ l = 0 k F ⁡ w ⁡ l ∈ topGen ⁡ ran ⁡ . Cn TopOpen ⁡ ℂ fld
35 ax-resscn ⊢ ℝ ⊆ ℂ
36 ssid ⊢ ℂ ⊆ ℂ
37 35 36 pm3.2i ⊢ ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ
38 26 tgioo2 ⊢ topGen ⁡ ran ⁡ . = TopOpen ⁡ ℂ fld ↾ 𝑡 ℝ
39 26 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
40 39 toponrestid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ
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 ⊢ φ ∧ k ∈ ℕ 0 → w ∈ ℝ ⟼ ∑ l = 0 k F ⁡ w ⁡ l : ℝ ⟶cn ℂ
44 25 43 eqeltrd ⊢ φ ∧ k ∈ ℕ 0 → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k : ℝ ⟶cn ℂ
45 44 fmpttd ⊢ φ → k ∈ ℕ 0 ⟼ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k : ℕ 0 ⟶ ℝ ⟶cn ℂ
46 0z ⊢ 0 ∈ ℤ
47 seqfn ⊢ 0 ∈ ℤ → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m Fn ℤ ≥ 0
48 46 47 ax-mp ⊢ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m Fn ℤ ≥ 0
49 17 fneq2i ⊢ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m Fn ℕ 0 ↔ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m Fn ℤ ≥ 0
50 48 49 mpbir ⊢ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m Fn ℕ 0
51 dffn5 ⊢ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m Fn ℕ 0 ↔ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m = k ∈ ℕ 0 ⟼ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k
52 50 51 mpbi ⊢ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m = k ∈ ℕ 0 ⟼ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k
53 52 feq1i ⊢ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m : ℕ 0 ⟶ ℝ ⟶cn ℂ ↔ k ∈ ℕ 0 ⟼ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k : ℕ 0 ⟶ ℝ ⟶cn ℂ
54 45 53 sylibr ⊢ φ → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m : ℕ 0 ⟶ ℝ ⟶cn ℂ