Metamath Proof Explorer

Theorem knoppcnlem7

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

Ref Expression
Hypotheses knoppcnlem7.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
knoppcnlem7.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
knoppcnlem7.n ⊢ φ → N ∈ ℕ
knoppcnlem7.1 ⊢ φ → C ∈ ℝ
knoppcnlem7.2 ⊢ φ → M ∈ ℕ 0
Assertion knoppcnlem7 ⊢ φ → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ M = w ∈ ℝ ⟼ seq 0 + F ⁡ w ⁡ M

Proof

Step Hyp Ref Expression
1 knoppcnlem7.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 knoppcnlem7.f ⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y
3 knoppcnlem7.n ⊢ φ → N ∈ ℕ
4 knoppcnlem7.1 ⊢ φ → C ∈ ℝ
5 knoppcnlem7.2 ⊢ φ → M ∈ ℕ 0
6 reex ⊢ ℝ ∈ V
7 6 a1i ⊢ φ → ℝ ∈ V
8 elnn0uz ⊢ M ∈ ℕ 0 ↔ M ∈ ℤ ≥ 0
9 5 8 sylib ⊢ φ → M ∈ ℤ ≥ 0
10 eqid ⊢ m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m = m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m
11 10 a1i ⊢ φ ∧ k ∈ 0 … M → m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m = m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m
12 fveq2 ⊢ z = w → F ⁡ z = F ⁡ w
13 12 fveq1d ⊢ z = w → F ⁡ z ⁡ m = F ⁡ w ⁡ m
14 13 cbvmptv ⊢ z ∈ ℝ ⟼ F ⁡ z ⁡ m = w ∈ ℝ ⟼ F ⁡ w ⁡ m
15 14 a1i ⊢ φ ∧ k ∈ 0 … M ∧ m = k → z ∈ ℝ ⟼ F ⁡ z ⁡ m = w ∈ ℝ ⟼ F ⁡ w ⁡ m
16 fveq2 ⊢ m = k → F ⁡ w ⁡ m = F ⁡ w ⁡ k
17 16 mpteq2dv ⊢ m = k → w ∈ ℝ ⟼ F ⁡ w ⁡ m = w ∈ ℝ ⟼ F ⁡ w ⁡ k
18 17 adantl ⊢ φ ∧ k ∈ 0 … M ∧ m = k → w ∈ ℝ ⟼ F ⁡ w ⁡ m = w ∈ ℝ ⟼ F ⁡ w ⁡ k
19 15 18 eqtrd ⊢ φ ∧ k ∈ 0 … M ∧ m = k → z ∈ ℝ ⟼ F ⁡ z ⁡ m = w ∈ ℝ ⟼ F ⁡ w ⁡ k
20 elfznn0 ⊢ k ∈ 0 … M → k ∈ ℕ 0
21 20 adantl ⊢ φ ∧ k ∈ 0 … M → k ∈ ℕ 0
22 6 mptex ⊢ w ∈ ℝ ⟼ F ⁡ w ⁡ k ∈ V
23 22 a1i ⊢ φ ∧ k ∈ 0 … M → w ∈ ℝ ⟼ F ⁡ w ⁡ k ∈ V
24 11 19 21 23 fvmptd ⊢ φ ∧ k ∈ 0 … M → m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ k = w ∈ ℝ ⟼ F ⁡ w ⁡ k
25 7 9 24 seqof ⊢ φ → seq 0 ∘ f ⁡ + m ∈ ℕ 0 ⟼ z ∈ ℝ ⟼ F ⁡ z ⁡ m ⁡ M = w ∈ ℝ ⟼ seq 0 + F ⁡ w ⁡ M