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

Definition df-vdwap 14011
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
StepHypRef Expression
1 cvdwa 14008 . 2  class AP
2 vk . . 3  setvar  k
3 cn0 10566 . . 3  class  NN0
4 va . . . 4  setvar  a
5 vd . . . 4  setvar  d
6 cn 10309 . . . 4  class  NN
7 vm . . . . . 6  setvar  m
8 cc0 9269 . . . . . . 7  class  0
92cv 1361 . . . . . . . 8  class  k
10 c1 9270 . . . . . . . 8  class  1
11 cmin 9582 . . . . . . . 8  class  -
129, 10, 11co 6080 . . . . . . 7  class  ( k  -  1 )
13 cfz 11423 . . . . . . 7  class  ...
148, 12, 13co 6080 . . . . . 6  class  ( 0 ... ( k  - 
1 ) )
154cv 1361 . . . . . . 7  class  a
167cv 1361 . . . . . . . 8  class  m
175cv 1361 . . . . . . . 8  class  d
18 cmul 9274 . . . . . . . 8  class  x.
1916, 17, 18co 6080 . . . . . . 7  class  ( m  x.  d )
20 caddc 9272 . . . . . . 7  class  +
2115, 19, 20co 6080 . . . . . 6  class  ( a  +  ( m  x.  d ) )
227, 14, 21cmpt 4338 . . . . 5  class  ( m  e.  ( 0 ... ( k  -  1 ) )  |->  ( a  +  ( m  x.  d ) ) )
2322crn 4828 . . . 4  class  ran  (
m  e.  ( 0 ... ( k  - 
1 ) )  |->  ( a  +  ( m  x.  d ) ) )
244, 5, 6, 6, 23cmpt2 6082 . . 3  class  ( a  e.  NN ,  d  e.  NN  |->  ran  (
m  e.  ( 0 ... ( k  - 
1 ) )  |->  ( a  +  ( m  x.  d ) ) ) )
252, 3, 24cmpt 4338 . 2  class  ( k  e.  NN0  |->  ( a  e.  NN ,  d  e.  NN  |->  ran  (
m  e.  ( 0 ... ( k  - 
1 ) )  |->  ( a  +  ( m  x.  d ) ) ) ) )
261, 25wceq 1362 1  wff AP  =  ( k  e.  NN0  |->  ( a  e.  NN ,  d  e.  NN  |->  ran  (
m  e.  ( 0 ... ( k  - 
1 ) )  |->  ( a  +  ( m  x.  d ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  vdwapfval  14014
  Copyright terms: Public domain W3C validator