Metamath Proof Explorer

Theorem knoppcnlem9

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

Ref Expression
Hypotheses knoppcnlem9.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
knoppcnlem9.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
knoppcnlem9.w ⊢ W = w ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ w ⁡ i
knoppcnlem9.n ⊢ φ → N ∈ ℕ
knoppcnlem9.1 ⊢ φ → C ∈ ℝ
knoppcnlem9.2 ⊢ φ → C < 1
Assertion knoppcnlem9 ⊢ φ → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ W

Proof

Step Hyp Ref Expression
1 knoppcnlem9.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 knoppcnlem9.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
3 knoppcnlem9.w ⊢ W = w ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ w ⁡ i
4 knoppcnlem9.n ⊢ φ → N ∈ ℕ
5 knoppcnlem9.1 ⊢ φ → C ∈ ℝ
6 knoppcnlem9.2 ⊢ φ → C < 1
7 1 2 4 5 6 knoppcnlem6 ⊢ φ → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ∈ dom ⁡ ⇝u ⁡ ℝ
8 seqex ⊢ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ∈ V
9 8 eldm ⊢ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ∈ dom ⁡ ⇝u ⁡ ℝ ↔ ∃ f seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f
10 7 9 sylib ⊢ φ → ∃ f seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f
11 simpr ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f
12 ulmcl ⊢ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f → f : ℝ ⟶ ℂ
13 12 feqmptd ⊢ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f → f = w ∈ ℝ ⟼ f ⁡ w
14 13 adantl ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f → f = w ∈ ℝ ⟼ f ⁡ w
15 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
16 0zd ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f ∧ w ∈ ℝ → 0 ∈ ℤ
17 eqidd ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f ∧ w ∈ ℝ ∧ i ∈ ℕ 0 → F ⁡ w ⁡ i = F ⁡ w ⁡ i
18 4 ad2antrr ⊢ φ ∧ w ∈ ℝ ∧ i ∈ ℕ 0 → N ∈ ℕ
19 5 ad2antrr ⊢ φ ∧ w ∈ ℝ ∧ i ∈ ℕ 0 → C ∈ ℝ
20 simplr ⊢ φ ∧ w ∈ ℝ ∧ i ∈ ℕ 0 → w ∈ ℝ
21 simpr ⊢ φ ∧ w ∈ ℝ ∧ i ∈ ℕ 0 → i ∈ ℕ 0
22 1 2 18 19 20 21 knoppcnlem3 ⊢ φ ∧ w ∈ ℝ ∧ i ∈ ℕ 0 → F ⁡ w ⁡ i ∈ ℝ
23 22 adantllr ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f ∧ w ∈ ℝ ∧ i ∈ ℕ 0 → F ⁡ w ⁡ i ∈ ℝ
24 23 recnd ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f ∧ w ∈ ℝ ∧ i ∈ ℕ 0 → F ⁡ w ⁡ i ∈ ℂ
25 1 2 4 5 knoppcnlem8 ⊢ φ → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m : ℕ 0 ⟶ ℂ ℝ
26 25 ad2antrr ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f ∧ w ∈ ℝ → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m : ℕ 0 ⟶ ℂ ℝ
27 simpr ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f ∧ w ∈ ℝ → w ∈ ℝ
28 seqex ⊢ seq 0 + F ⁡ w ∈ V
29 28 a1i ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f ∧ w ∈ ℝ → seq 0 + F ⁡ w ∈ V
30 4 ad2antrr ⊢ φ ∧ w ∈ ℝ ∧ k ∈ ℕ 0 → N ∈ ℕ
31 5 ad2antrr ⊢ φ ∧ w ∈ ℝ ∧ k ∈ ℕ 0 → C ∈ ℝ
32 simpr ⊢ φ ∧ w ∈ ℝ ∧ k ∈ ℕ 0 → k ∈ ℕ 0
33 1 2 30 31 32 knoppcnlem7 ⊢ φ ∧ w ∈ ℝ ∧ k ∈ ℕ 0 → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k = v ∈ ℝ ⟼ seq 0 + F ⁡ v ⁡ k
34 33 adantllr ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f ∧ w ∈ ℝ ∧ k ∈ ℕ 0 → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k = v ∈ ℝ ⟼ seq 0 + F ⁡ v ⁡ k
35 34 fveq1d ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f ∧ w ∈ ℝ ∧ k ∈ ℕ 0 → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k ⁡ w = v ∈ ℝ ⟼ seq 0 + F ⁡ v ⁡ k ⁡ w
36 eqid ⊢ v ∈ ℝ ⟼ seq 0 + F ⁡ v ⁡ k = v ∈ ℝ ⟼ seq 0 + F ⁡ v ⁡ k
37 fveq2 ⊢ v = w → F ⁡ v = F ⁡ w
38 37 seqeq3d ⊢ v = w → seq 0 + F ⁡ v = seq 0 + F ⁡ w
39 38 fveq1d ⊢ v = w → seq 0 + F ⁡ v ⁡ k = seq 0 + F ⁡ w ⁡ k
40 27 adantr ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f ∧ w ∈ ℝ ∧ k ∈ ℕ 0 → w ∈ ℝ
41 fvexd ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f ∧ w ∈ ℝ ∧ k ∈ ℕ 0 → seq 0 + F ⁡ w ⁡ k ∈ V
42 36 39 40 41 fvmptd3 ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f ∧ w ∈ ℝ ∧ k ∈ ℕ 0 → v ∈ ℝ ⟼ seq 0 + F ⁡ v ⁡ k ⁡ w = seq 0 + F ⁡ w ⁡ k
43 35 42 eqtrd ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f ∧ w ∈ ℝ ∧ k ∈ ℕ 0 → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k ⁡ w = seq 0 + F ⁡ w ⁡ k
44 simplr ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f ∧ w ∈ ℝ → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f
45 15 16 26 27 29 43 44 ulmclm ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f ∧ w ∈ ℝ → seq 0 + F ⁡ w ⇝ f ⁡ w
46 15 16 17 24 45 isumclim ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f ∧ w ∈ ℝ → ∑ i ∈ ℕ 0 F ⁡ w ⁡ i = f ⁡ w
47 46 eqcomd ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f ∧ w ∈ ℝ → f ⁡ w = ∑ i ∈ ℕ 0 F ⁡ w ⁡ i
48 47 mpteq2dva ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f → w ∈ ℝ ⟼ f ⁡ w = w ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ w ⁡ i
49 3 a1i ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f → W = w ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ w ⁡ i
50 49 eqcomd ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f → w ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ w ⁡ i = W
51 14 48 50 3eqtrd ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f → f = W
52 11 51 breqtrd ⊢ φ ∧ seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ W
53 52 ex ⊢ φ → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ W
54 53 exlimdv ⊢ φ → ∃ f seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ f → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ W
55 10 54 mpd ⊢ φ → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ W