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 = ( 𝑘 ∈ ℕ0 ↦ ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvdwa	⊢ AP
1		vk	⊢ 𝑘
2		cn0	⊢ ℕ0
3		va	⊢ 𝑎
4		cn	⊢ ℕ
5		vd	⊢ 𝑑
6		vm	⊢ 𝑚
7		cc0	⊢ 0
8		cfz	⊢ ...
9	1	cv	⊢ 𝑘
10		cmin	⊢ −
11		c1	⊢ 1
12	9 11 10	co	⊢ ( 𝑘 − 1 )
13	7 12 8	co	⊢ ( 0 ... ( 𝑘 − 1 ) )
14	3	cv	⊢ 𝑎
15		caddc	⊢ +
16	6	cv	⊢ 𝑚
17		cmul	⊢ ·
18	5	cv	⊢ 𝑑
19	16 18 17	co	⊢ ( 𝑚 · 𝑑 )
20	14 19 15	co	⊢ ( 𝑎 + ( 𝑚 · 𝑑 ) )
21	6 13 20	cmpt	⊢ ( 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) )
22	21	crn	⊢ ran ( 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) )
23	3 5 4 4 22	cmpo	⊢ ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) )
24	1 2 23	cmpt	⊢ ( 𝑘 ∈ ℕ0 ↦ ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ) )
25	0 24	wceq	⊢ AP = ( 𝑘 ∈ ℕ0 ↦ ( 𝑎 ∈ ℕ , 𝑑 ∈ ℕ ↦ ran ( 𝑚 ∈ ( 0 ... ( 𝑘 − 1 ) ) ↦ ( 𝑎 + ( 𝑚 · 𝑑 ) ) ) ) )