Definition df-vdwap 16900

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 16897	. 2 class AP
2		vk	. . 3 setvar 𝑘
3		cn0 12471	. . 3 class ℕ0
4		va	. . . 4 setvar 𝑎
5		vd	. . . 4 setvar 𝑑
6		cn 12211	. . . 4 class ℕ
7		vm	. . . . . 6 setvar 𝑚
8		cc0 11109	. . . . . . 7 class 0
9	2	cv 1540	. . . . . . . 8 class 𝑘
10		c1 11110	. . . . . . . 8 class 1
11		cmin 11443	. . . . . . . 8 class −
12	9, 10, 11	co 7408	. . . . . . 7 class (𝑘 − 1)
13		cfz 13483	. . . . . . 7 class ...
14	8, 12, 13	co 7408	. . . . . 6 class (0...(𝑘 − 1))
15	4	cv 1540	. . . . . . 7 class 𝑎
16	7	cv 1540	. . . . . . . 8 class 𝑚
17	5	cv 1540	. . . . . . . 8 class 𝑑
18		cmul 11114	. . . . . . . 8 class ·
19	16, 17, 18	co 7408	. . . . . . 7 class (𝑚 · 𝑑)
20		caddc 11112	. . . . . . 7 class +
21	15, 19, 20	co 7408	. . . . . 6 class (𝑎 + (𝑚 · 𝑑))
22	7, 14, 21	cmpt 5231	. . . . 5 class (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑)))
23	22	crn 5677	. . . 4 class ran (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑)))
24	4, 5, 6, 6, 23	cmpo 7410	. . 3 class (𝑎 ∈ ℕ, 𝑑 ∈ ℕ ↦ ran (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑))))
25	2, 3, 24	cmpt 5231	. 2 class (𝑘 ∈ ℕ0 ↦ (𝑎 ∈ ℕ, 𝑑 ∈ ℕ ↦ ran (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑)))))
26	1, 25	wceq 1541	1 wff AP = (𝑘 ∈ ℕ0 ↦ (𝑎 ∈ ℕ, 𝑑 ∈ ℕ ↦ ran (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑)))))

This definition is referenced by:  vdwapfval  16903