Definition df-vdwap 15510

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

Assertion

Ref	Expression
df-vdwap	⊢ AP = (𝑘 ∈ ℕ0 ↦ (𝑎 ∈ ℕ, 𝑑 ∈ ℕ ↦ ran (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑)))))

Distinct variable group:   𝑎,𝑑,𝑘,𝑚

Detailed syntax breakdown of Definition df-vdwap

Step	Hyp	Ref	Expression
1		cvdwa 15507	. 2 class AP
2		vk	. . 3 setvar 𝑘
3		cn0 11169	. . 3 class ℕ0
4		va	. . . 4 setvar 𝑎
5		vd	. . . 4 setvar 𝑑
6		cn 10897	. . . 4 class ℕ
7		vm	. . . . . 6 setvar 𝑚
8		cc0 9815	. . . . . . 7 class 0
9	2	cv 1474	. . . . . . . 8 class 𝑘
10		c1 9816	. . . . . . . 8 class 1
11		cmin 10145	. . . . . . . 8 class −
12	9, 10, 11	co 6549	. . . . . . 7 class (𝑘 − 1)
13		cfz 12197	. . . . . . 7 class ...
14	8, 12, 13	co 6549	. . . . . 6 class (0...(𝑘 − 1))
15	4	cv 1474	. . . . . . 7 class 𝑎
16	7	cv 1474	. . . . . . . 8 class 𝑚
17	5	cv 1474	. . . . . . . 8 class 𝑑
18		cmul 9820	. . . . . . . 8 class ·
19	16, 17, 18	co 6549	. . . . . . 7 class (𝑚 · 𝑑)
20		caddc 9818	. . . . . . 7 class +
21	15, 19, 20	co 6549	. . . . . 6 class (𝑎 + (𝑚 · 𝑑))
22	7, 14, 21	cmpt 4643	. . . . 5 class (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑)))
23	22	crn 5039	. . . 4 class ran (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑)))
24	4, 5, 6, 6, 23	cmpt2 6551	. . 3 class (𝑎 ∈ ℕ, 𝑑 ∈ ℕ ↦ ran (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑))))
25	2, 3, 24	cmpt 4643	. 2 class (𝑘 ∈ ℕ0 ↦ (𝑎 ∈ ℕ, 𝑑 ∈ ℕ ↦ ran (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑)))))
26	1, 25	wceq 1475	1 wff AP = (𝑘 ∈ ℕ0 ↦ (𝑎 ∈ ℕ, 𝑑 ∈ ℕ ↦ ran (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑)))))

This definition is referenced by:  vdwapfval  15513