Definition df-vdwap 17006

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 17003	. 2 class AP
2		vk	. . 3 setvar 𝑘
3		cn0 12526	. . 3 class ℕ0
4		va	. . . 4 setvar 𝑎
5		vd	. . . 4 setvar 𝑑
6		cn 12266	. . . 4 class ℕ
7		vm	. . . . . 6 setvar 𝑚
8		cc0 11155	. . . . . . 7 class 0
9	2	cv 1539	. . . . . . . 8 class 𝑘
10		c1 11156	. . . . . . . 8 class 1
11		cmin 11492	. . . . . . . 8 class −
12	9, 10, 11	co 7431	. . . . . . 7 class (𝑘 − 1)
13		cfz 13547	. . . . . . 7 class ...
14	8, 12, 13	co 7431	. . . . . 6 class (0...(𝑘 − 1))
15	4	cv 1539	. . . . . . 7 class 𝑎
16	7	cv 1539	. . . . . . . 8 class 𝑚
17	5	cv 1539	. . . . . . . 8 class 𝑑
18		cmul 11160	. . . . . . . 8 class ·
19	16, 17, 18	co 7431	. . . . . . 7 class (𝑚 · 𝑑)
20		caddc 11158	. . . . . . 7 class +
21	15, 19, 20	co 7431	. . . . . 6 class (𝑎 + (𝑚 · 𝑑))
22	7, 14, 21	cmpt 5225	. . . . 5 class (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑)))
23	22	crn 5686	. . . 4 class ran (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑)))
24	4, 5, 6, 6, 23	cmpo 7433	. . 3 class (𝑎 ∈ ℕ, 𝑑 ∈ ℕ ↦ ran (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑))))
25	2, 3, 24	cmpt 5225	. 2 class (𝑘 ∈ ℕ0 ↦ (𝑎 ∈ ℕ, 𝑑 ∈ ℕ ↦ ran (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑)))))
26	1, 25	wceq 1540	1 wff AP = (𝑘 ∈ ℕ0 ↦ (𝑎 ∈ ℕ, 𝑑 ∈ ℕ ↦ ran (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑)))))

This definition is referenced by:  vdwapfval  17009