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 ∈ ℕ 0 → AP ⁡ K = a ∈ ℕ , d ∈ ℕ ⟼ ran ⁡ m ∈ 0 … K − 1 ⟼ a + m ⁢ d

Proof

Step Hyp Ref Expression
1 simp1 ⊢ k = K ∧ a ∈ ℕ ∧ d ∈ ℕ → k = K
2 1 oveq1d ⊢ k = K ∧ a ∈ ℕ ∧ d ∈ ℕ → k − 1 = K − 1
3 2 oveq2d ⊢ k = K ∧ a ∈ ℕ ∧ d ∈ ℕ → 0 … k − 1 = 0 … K − 1
4 3 mpteq1d ⊢ k = K ∧ a ∈ ℕ ∧ d ∈ ℕ → m ∈ 0 … k − 1 ⟼ a + m ⁢ d = m ∈ 0 … K − 1 ⟼ a + m ⁢ d
5 4 rneqd ⊢ k = K ∧ a ∈ ℕ ∧ d ∈ ℕ → ran ⁡ m ∈ 0 … k − 1 ⟼ a + m ⁢ d = ran ⁡ m ∈ 0 … K − 1 ⟼ a + m ⁢ d
6 5 mpoeq3dva ⊢ k = K → a ∈ ℕ , d ∈ ℕ ⟼ ran ⁡ m ∈ 0 … k − 1 ⟼ a + m ⁢ d = a ∈ ℕ , d ∈ ℕ ⟼ ran ⁡ m ∈ 0 … K − 1 ⟼ a + m ⁢ d
7 df-vdwap ⊢ AP = k ∈ ℕ 0 ⟼ a ∈ ℕ , d ∈ ℕ ⟼ ran ⁡ m ∈ 0 … k − 1 ⟼ a + m ⁢ d
8 nnex ⊢ ℕ ∈ V
9 8 8 mpoex ⊢ a ∈ ℕ , d ∈ ℕ ⟼ ran ⁡ m ∈ 0 … K − 1 ⟼ a + m ⁢ d ∈ V
10 6 7 9 fvmpt ⊢ K ∈ ℕ 0 → AP ⁡ K = a ∈ ℕ , d ∈ ℕ ⟼ ran ⁡ m ∈ 0 … K − 1 ⟼ a + m ⁢ d