Metamath Proof Explorer

Theorem vdwapfval

Description: Define the arithmetic progression function, which takes as input a length k , a start point a , and a step d and outputs the set of points in this progression. (Contributed by Mario Carneiro, 18-Aug-2014)

		Ref	Expression
	Assertion	vdwapfval	$⊢ K \in ℕ_{0} \to AP (K) = (a \in ℕ, d \in ℕ ⟼ ran (m \in (0 \dots K - 1) ⟼ a + m d))$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (k = K \land a \in ℕ \land d \in ℕ) \to k = K$
2	1	oveq1d	$⊢ (k = K \land a \in ℕ \land d \in ℕ) \to k - 1 = K - 1$
3	2	oveq2d	$⊢ (k = K \land a \in ℕ \land d \in ℕ) \to (0 \dots k - 1) = (0 \dots K - 1)$
4	3	mpteq1d	$⊢ (k = K \land a \in ℕ \land d \in ℕ) \to (m \in (0 \dots k - 1) ⟼ a + m d) = (m \in (0 \dots K - 1) ⟼ a + m d)$
5	4	rneqd	$⊢ (k = K \land a \in ℕ \land d \in ℕ) \to ran (m \in (0 \dots k - 1) ⟼ a + m d) = ran (m \in (0 \dots K - 1) ⟼ a + m d)$
6	5	mpoeq3dva	$⊢ k = K \to (a \in ℕ, d \in ℕ ⟼ ran (m \in (0 \dots k - 1) ⟼ a + m d)) = (a \in ℕ, d \in ℕ ⟼ ran (m \in (0 \dots K - 1) ⟼ a + m d))$
7		df-vdwap	$⊢ AP = (k \in ℕ_{0} ⟼ (a \in ℕ, d \in ℕ ⟼ ran (m \in (0 \dots k - 1) ⟼ a + m d)))$
8		nnex	$⊢ ℕ \in V$
9	8 8	mpoex	$⊢ (a \in ℕ, d \in ℕ ⟼ ran (m \in (0 \dots K - 1) ⟼ a + m d)) \in V$
10	6 7 9	fvmpt	$⊢ K \in ℕ_{0} \to AP (K) = (a \in ℕ, d \in ℕ ⟼ ran (m \in (0 \dots K - 1) ⟼ a + m d))$