Definition df-vdwap 15672

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.)

Assertion

Ref	Expression
df-vdwap	|- AP = ( k e. NN0 |-> ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( k - 1 ) ) |-> ( a + ( m x. d ) ) ) ) )

Distinct variable group:   a, d, k, m

Detailed syntax breakdown of Definition df-vdwap

Step	Hyp	Ref	Expression
1		cvdwa 15669	. 2 class AP
2		vk	. . 3 setvar k
3		cn0 11292	. . 3 class NN0
4		va	. . . 4 setvar a
5		vd	. . . 4 setvar d
6		cn 11020	. . . 4 class NN
7		vm	. . . . . 6 setvar m
8		cc0 9936	. . . . . . 7 class 0
9	2	cv 1482	. . . . . . . 8 class k
10		c1 9937	. . . . . . . 8 class 1
11		cmin 10266	. . . . . . . 8 class -
12	9, 10, 11	co 6650	. . . . . . 7 class ( k - 1 )
13		cfz 12326	. . . . . . 7 class ...
14	8, 12, 13	co 6650	. . . . . 6 class ( 0 ... ( k - 1 ) )
15	4	cv 1482	. . . . . . 7 class a
16	7	cv 1482	. . . . . . . 8 class m
17	5	cv 1482	. . . . . . . 8 class d
18		cmul 9941	. . . . . . . 8 class x.
19	16, 17, 18	co 6650	. . . . . . 7 class ( m x. d )
20		caddc 9939	. . . . . . 7 class +
21	15, 19, 20	co 6650	. . . . . 6 class ( a + ( m x. d ) )
22	7, 14, 21	cmpt 4729	. . . . 5 class ( m e. ( 0 ... ( k - 1 ) ) |-> ( a + ( m x. d ) ) )
23	22	crn 5115	. . . 4 class ran ( m e. ( 0 ... ( k - 1 ) ) |-> ( a + ( m x. d ) ) )
24	4, 5, 6, 6, 23	cmpt2 6652	. . 3 class ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( k - 1 ) ) |-> ( a + ( m x. d ) ) ) )
25	2, 3, 24	cmpt 4729	. 2 class ( k e. NN0 |-> ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( k - 1 ) ) |-> ( a + ( m x. d ) ) ) ) )
26	1, 25	wceq 1483	1 wff AP = ( k e. NN0 |-> ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( k - 1 ) ) |-> ( a + ( m x. d ) ) ) ) )

This definition is referenced by:  vdwapfval  15675