knoppcnlem7

	Ref	Expression
Hypotheses	knoppcnlem7.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
	knoppcnlem7.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ C^{n} T ({2 \cdot N}^{n} y)))$
	knoppcnlem7.n	$⊢ φ \to N \in ℕ$
	knoppcnlem7.1	$⊢ φ \to C \in ℝ$
	knoppcnlem7.2	$⊢ φ \to M \in ℕ_{0}$
Assertion	knoppcnlem7	$⊢ φ \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) (M) = (w \in ℝ ⟼ seq 0 (+ F (w)) (M))$

Proof

Step	Hyp	Ref	Expression
1		knoppcnlem7.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
2		knoppcnlem7.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ C^{n} T ({2 \cdot N}^{n} y)))$
3		knoppcnlem7.n	$⊢ φ \to N \in ℕ$
4		knoppcnlem7.1	$⊢ φ \to C \in ℝ$
5		knoppcnlem7.2	$⊢ φ \to M \in ℕ_{0}$
6		reex	$⊢ ℝ \in V$
7	6	a1i	$⊢ φ \to ℝ \in V$
8		elnn0uz	$⊢ M \in ℕ_{0} \leftrightarrow M \in ℤ_{\geq 0}$
9	5 8	sylib	$⊢ φ \to M \in ℤ_{\geq 0}$
10		eqid	$⊢ (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m))) = (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))$
11	10	a1i	$⊢ (φ \land k \in (0 \dots M)) \to (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m))) = (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))$
12		fveq2	$⊢ z = w \to F (z) = F (w)$
13	12	fveq1d	$⊢ z = w \to F (z) (m) = F (w) (m)$
14	13	cbvmptv	$⊢ (z \in ℝ ⟼ F (z) (m)) = (w \in ℝ ⟼ F (w) (m))$
15	14	a1i	$⊢ ((φ \land k \in (0 \dots M)) \land m = k) \to (z \in ℝ ⟼ F (z) (m)) = (w \in ℝ ⟼ F (w) (m))$
16		fveq2	$⊢ m = k \to F (w) (m) = F (w) (k)$
17	16	mpteq2dv	$⊢ m = k \to (w \in ℝ ⟼ F (w) (m)) = (w \in ℝ ⟼ F (w) (k))$
18	17	adantl	$⊢ ((φ \land k \in (0 \dots M)) \land m = k) \to (w \in ℝ ⟼ F (w) (m)) = (w \in ℝ ⟼ F (w) (k))$
19	15 18	eqtrd	$⊢ ((φ \land k \in (0 \dots M)) \land m = k) \to (z \in ℝ ⟼ F (z) (m)) = (w \in ℝ ⟼ F (w) (k))$
20		elfznn0	$⊢ k \in (0 \dots M) \to k \in ℕ_{0}$
21	20	adantl	$⊢ (φ \land k \in (0 \dots M)) \to k \in ℕ_{0}$
22	6	mptex	$⊢ (w \in ℝ ⟼ F (w) (k)) \in V$
23	22	a1i	$⊢ (φ \land k \in (0 \dots M)) \to (w \in ℝ ⟼ F (w) (k)) \in V$
24	11 19 21 23	fvmptd	$⊢ (φ \land k \in (0 \dots M)) \to (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m))) (k) = (w \in ℝ ⟼ F (w) (k))$
25	7 9 24	seqof	$⊢ φ \to seq 0 (\circ_{f} +, (m \in ℕ_{0} ⟼ (z \in ℝ ⟼ F (z) (m)))) (M) = (w \in ℝ ⟼ seq 0 (+ F (w)) (M))$

Metamath Proof Explorer

Theorem knoppcnlem7

Proof