Definition df-vdwap 14486

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

Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-vdwap

Step	Hyp	Ref	Expression
1		cvdwa 14483	. 2
2		vk	. . 3
3		cn0 10820	. . 3
4		va	. . . 4
5		vd	. . . 4
6		cn 10561	. . . 4
7		vm	. . . . . 6
8		cc0 9513	. . . . . . 7
9	2	cv 1394	. . . . . . . 8
10		c1 9514	. . . . . . . 8
11		cmin 9828	. . . . . . . 8
12	9, 10, 11	co 6296	. . . . . . 7
13		cfz 11701	. . . . . . 7
14	8, 12, 13	co 6296	. . . . . 6
15	4	cv 1394	. . . . . . 7
16	7	cv 1394	. . . . . . . 8
17	5	cv 1394	. . . . . . . 8
18		cmul 9518	. . . . . . . 8
19	16, 17, 18	co 6296	. . . . . . 7
20		caddc 9516	. . . . . . 7
21	15, 19, 20	co 6296	. . . . . 6
22	7, 14, 21	cmpt 4510	. . . . 5
23	22	crn 5005	. . . 4
24	4, 5, 6, 6, 23	cmpt2 6298	. . 3
25	2, 3, 24	cmpt 4510	. 2
26	1, 25	wceq 1395	1

This definition is referenced by:  vdwapfval  14489