Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-vdwap Structured version   Unicode version

Definition df-vdwap 14693
 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
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-vdwap
StepHypRef Expression
1 cvdwa 14690 . 2 AP
2 vk . . 3
3 cn0 10835 . . 3
4 va . . . 4
5 vd . . . 4
6 cn 10575 . . . 4
7 vm . . . . . 6
8 cc0 9521 . . . . . . 7
92cv 1404 . . . . . . . 8
10 c1 9522 . . . . . . . 8
11 cmin 9840 . . . . . . . 8
129, 10, 11co 6277 . . . . . . 7
13 cfz 11724 . . . . . . 7
148, 12, 13co 6277 . . . . . 6
154cv 1404 . . . . . . 7
167cv 1404 . . . . . . . 8
175cv 1404 . . . . . . . 8
18 cmul 9526 . . . . . . . 8
1916, 17, 18co 6277 . . . . . . 7
20 caddc 9524 . . . . . . 7
2115, 19, 20co 6277 . . . . . 6
227, 14, 21cmpt 4452 . . . . 5
2322crn 4823 . . . 4
244, 5, 6, 6, 23cmpt2 6279 . . 3
252, 3, 24cmpt 4452 . 2
261, 25wceq 1405 1 AP
 Colors of variables: wff setvar class This definition is referenced by:  vdwapfval  14696
 Copyright terms: Public domain W3C validator