Metamath Proof Explorer

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 = ( k e. NN0 |-> ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( k - 1 ) ) |-> ( a + ( m x. d ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cvdwa 
 |-  AP
1 vk 
 |-  k
2 cn0 
 |-  NN0
3 va 
 |-  a
4 cn 
 |-  NN
5 vd 
 |-  d
6 vm 
 |-  m
7 cc0 
 |-  0
8 cfz 
 |-  ...
9 1 cv 
 |-  k
10 cmin 
 |-  -
11 c1 
 |-  1
12 9 11 10 co 
 |-  ( k - 1 )
13 7 12 8 co 
 |-  ( 0 ... ( k - 1 ) )
14 3 cv 
 |-  a
15 caddc 
 |-  +
16 6 cv 
 |-  m
17 cmul 
 |-  x.
18 5 cv 
 |-  d
19 16 18 17 co 
 |-  ( m x. d )
20 14 19 15 co 
 |-  ( a + ( m x. d ) )
21 6 13 20 cmpt 
 |-  ( m e. ( 0 ... ( k - 1 ) ) |-> ( a + ( m x. d ) ) )
22 21 crn 
 |-  ran ( m e. ( 0 ... ( k - 1 ) ) |-> ( a + ( m x. d ) ) )
23 3 5 4 4 22 cmpo 
 |-  ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( k - 1 ) ) |-> ( a + ( m x. d ) ) ) )
24 1 2 23 cmpt 
 |-  ( k e. NN0 |-> ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( k - 1 ) ) |-> ( a + ( m x. d ) ) ) ) )
25 0 24 wceq 
 |-  AP = ( k e. NN0 |-> ( a e. NN , d e. NN |-> ran ( m e. ( 0 ... ( k - 1 ) ) |-> ( a + ( m x. d ) ) ) ) )