Metamath Proof Explorer

Theorem knoppndvlem4

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 15-Jun-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

Ref Expression
Hypotheses knoppndvlem4.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
knoppndvlem4.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
knoppndvlem4.w ⊢ W = w ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ w ⁡ i
knoppndvlem4.a ⊢ φ → A ∈ ℝ
knoppndvlem4.c ⊢ φ → C ∈ − 1 1
knoppndvlem4.n ⊢ φ → N ∈ ℕ
Assertion knoppndvlem4 ⊢ φ → seq 0 + F ⁡ A ⇝ W ⁡ A

Proof

Step Hyp Ref Expression
1 knoppndvlem4.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 knoppndvlem4.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
3 knoppndvlem4.w ⊢ W = w ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ w ⁡ i
4 knoppndvlem4.a ⊢ φ → A ∈ ℝ
5 knoppndvlem4.c ⊢ φ → C ∈ − 1 1
6 knoppndvlem4.n ⊢ φ → N ∈ ℕ
7 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
8 0zd ⊢ φ → 0 ∈ ℤ
9 5 knoppndvlem3 ⊢ φ → C ∈ ℝ ∧ C < 1
10 9 simpld ⊢ φ → C ∈ ℝ
11 1 2 6 10 knoppcnlem8 ⊢ φ → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m : ℕ 0 ⟶ ℂ ℝ
12 seqex ⊢ seq 0 + F ⁡ A ∈ V
13 12 a1i ⊢ φ → seq 0 + F ⁡ A ∈ V
14 6 adantr ⊢ φ ∧ k ∈ ℕ 0 → N ∈ ℕ
15 10 adantr ⊢ φ ∧ k ∈ ℕ 0 → C ∈ ℝ
16 simpr ⊢ φ ∧ k ∈ ℕ 0 → k ∈ ℕ 0
17 1 2 14 15 16 knoppcnlem7 ⊢ φ ∧ k ∈ ℕ 0 → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k = v ∈ ℝ ⟼ seq 0 + F ⁡ v ⁡ k
18 17 fveq1d ⊢ φ ∧ k ∈ ℕ 0 → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k ⁡ A = v ∈ ℝ ⟼ seq 0 + F ⁡ v ⁡ k ⁡ A
19 eqid ⊢ v ∈ ℝ ⟼ seq 0 + F ⁡ v ⁡ k = v ∈ ℝ ⟼ seq 0 + F ⁡ v ⁡ k
20 fveq2 ⊢ v = A → F ⁡ v = F ⁡ A
21 20 seqeq3d ⊢ v = A → seq 0 + F ⁡ v = seq 0 + F ⁡ A
22 21 fveq1d ⊢ v = A → seq 0 + F ⁡ v ⁡ k = seq 0 + F ⁡ A ⁡ k
23 fvexd ⊢ φ → seq 0 + F ⁡ A ⁡ k ∈ V
24 19 22 4 23 fvmptd3 ⊢ φ → v ∈ ℝ ⟼ seq 0 + F ⁡ v ⁡ k ⁡ A = seq 0 + F ⁡ A ⁡ k
25 24 adantr ⊢ φ ∧ k ∈ ℕ 0 → v ∈ ℝ ⟼ seq 0 + F ⁡ v ⁡ k ⁡ A = seq 0 + F ⁡ A ⁡ k
26 18 25 eqtrd ⊢ φ ∧ k ∈ ℕ 0 → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k ⁡ A = seq 0 + F ⁡ A ⁡ k
27 9 simprd ⊢ φ → C < 1
28 1 2 3 6 10 27 knoppcnlem9 ⊢ φ → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⇝u ⁡ ℝ W
29 7 8 11 4 13 26 28 ulmclm ⊢ φ → seq 0 + F ⁡ A ⇝ W ⁡ A