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

Definition df-vdwap 16002
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 = (𝑘 ∈ ℕ0 ↦ (𝑎 ∈ ℕ, 𝑑 ∈ ℕ ↦ ran (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑)))))
Distinct variable group:   𝑎,𝑑,𝑘,𝑚

Detailed syntax breakdown of Definition df-vdwap
StepHypRef Expression
1 cvdwa 15999 . 2 class AP
2 vk . . 3 setvar 𝑘
3 cn0 11576 . . 3 class 0
4 va . . . 4 setvar 𝑎
5 vd . . . 4 setvar 𝑑
6 cn 11310 . . . 4 class
7 vm . . . . . 6 setvar 𝑚
8 cc0 10222 . . . . . . 7 class 0
92cv 1652 . . . . . . . 8 class 𝑘
10 c1 10223 . . . . . . . 8 class 1
11 cmin 10554 . . . . . . . 8 class
129, 10, 11co 6876 . . . . . . 7 class (𝑘 − 1)
13 cfz 12576 . . . . . . 7 class ...
148, 12, 13co 6876 . . . . . 6 class (0...(𝑘 − 1))
154cv 1652 . . . . . . 7 class 𝑎
167cv 1652 . . . . . . . 8 class 𝑚
175cv 1652 . . . . . . . 8 class 𝑑
18 cmul 10227 . . . . . . . 8 class ·
1916, 17, 18co 6876 . . . . . . 7 class (𝑚 · 𝑑)
20 caddc 10225 . . . . . . 7 class +
2115, 19, 20co 6876 . . . . . 6 class (𝑎 + (𝑚 · 𝑑))
227, 14, 21cmpt 4920 . . . . 5 class (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑)))
2322crn 5311 . . . 4 class ran (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑)))
244, 5, 6, 6, 23cmpt2 6878 . . 3 class (𝑎 ∈ ℕ, 𝑑 ∈ ℕ ↦ ran (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑))))
252, 3, 24cmpt 4920 . 2 class (𝑘 ∈ ℕ0 ↦ (𝑎 ∈ ℕ, 𝑑 ∈ ℕ ↦ ran (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑)))))
261, 25wceq 1653 1 wff AP = (𝑘 ∈ ℕ0 ↦ (𝑎 ∈ ℕ, 𝑑 ∈ ℕ ↦ ran (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑)))))
Colors of variables: wff setvar class
This definition is referenced by:  vdwapfval  16005
  Copyright terms: Public domain W3C validator