Metamath Proof Explorer


Theorem vdwapval

Description: Value of the arithmetic progression function. (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Assertion vdwapval K 0 A D X A AP K D m 0 K 1 X = A + m D

Proof

Step Hyp Ref Expression
1 vdwapfval K 0 AP K = a , d ran m 0 K 1 a + m d
2 1 3ad2ant1 K 0 A D AP K = a , d ran m 0 K 1 a + m d
3 2 oveqd K 0 A D A AP K D = A a , d ran m 0 K 1 a + m d D
4 oveq2 d = D m d = m D
5 oveq12 a = A m d = m D a + m d = A + m D
6 4 5 sylan2 a = A d = D a + m d = A + m D
7 6 mpteq2dv a = A d = D m 0 K 1 a + m d = m 0 K 1 A + m D
8 7 rneqd a = A d = D ran m 0 K 1 a + m d = ran m 0 K 1 A + m D
9 eqid a , d ran m 0 K 1 a + m d = a , d ran m 0 K 1 a + m d
10 ovex 0 K 1 V
11 10 mptex m 0 K 1 A + m D V
12 11 rnex ran m 0 K 1 A + m D V
13 8 9 12 ovmpoa A D A a , d ran m 0 K 1 a + m d D = ran m 0 K 1 A + m D
14 13 3adant1 K 0 A D A a , d ran m 0 K 1 a + m d D = ran m 0 K 1 A + m D
15 3 14 eqtrd K 0 A D A AP K D = ran m 0 K 1 A + m D
16 eqid m 0 K 1 A + m D = m 0 K 1 A + m D
17 16 rnmpt ran m 0 K 1 A + m D = x | m 0 K 1 x = A + m D
18 15 17 eqtrdi K 0 A D A AP K D = x | m 0 K 1 x = A + m D
19 18 eleq2d K 0 A D X A AP K D X x | m 0 K 1 x = A + m D
20 id X = A + m D X = A + m D
21 ovex A + m D V
22 20 21 eqeltrdi X = A + m D X V
23 22 rexlimivw m 0 K 1 X = A + m D X V
24 eqeq1 x = X x = A + m D X = A + m D
25 24 rexbidv x = X m 0 K 1 x = A + m D m 0 K 1 X = A + m D
26 23 25 elab3 X x | m 0 K 1 x = A + m D m 0 K 1 X = A + m D
27 19 26 bitrdi K 0 A D X A AP K D m 0 K 1 X = A + m D