Metamath Proof Explorer

Definition df-vdwap

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cvdwa class AP
1 vk setvar k
2 cn0 class ℕ 0
3 va setvar a
4 cn class ℕ
5 vd setvar d
6 vm setvar m
7 cc0 class 0
8 cfz class …
9 1 cv setvar k
10 cmin class −
11 c1 class 1
12 9 11 10 co class k − 1
13 7 12 8 co class 0 … k − 1
14 3 cv setvar a
15 caddc class +
16 6 cv setvar m
17 cmul class ×
18 5 cv setvar d
19 16 18 17 co class m ⁢ d
20 14 19 15 co class a + m ⁢ d
21 6 13 20 cmpt class m ∈ 0 … k − 1 ⟼ a + m ⁢ d
22 21 crn class ran ⁡ m ∈ 0 … k − 1 ⟼ a + m ⁢ d
23 3 5 4 4 22 cmpo class a ∈ ℕ , d ∈ ℕ ⟼ ran ⁡ m ∈ 0 … k − 1 ⟼ a + m ⁢ d
24 1 2 23 cmpt class k ∈ ℕ 0 ⟼ a ∈ ℕ , d ∈ ℕ ⟼ ran ⁡ m ∈ 0 … k − 1 ⟼ a + m ⁢ d
25 0 24 wceq wff AP = k ∈ ℕ 0 ⟼ a ∈ ℕ , d ∈ ℕ ⟼ ran ⁡ m ∈ 0 … k − 1 ⟼ a + m ⁢ d