Metamath Proof Explorer


Theorem rmyfval

Description: Value of the Y sequence. Not used after rmxyval is proved. (Contributed by Stefan O'Rear, 21-Sep-2014)

Ref Expression
Assertion rmyfval A 2 N A Y rm N = 2 nd b 0 × 1 st b + A 2 1 2 nd b -1 A + A 2 1 N

Proof

Step Hyp Ref Expression
1 oveq1 a = A a 2 = A 2
2 1 fvoveq1d a = A a 2 1 = A 2 1
3 2 oveq1d a = A a 2 1 2 nd b = A 2 1 2 nd b
4 3 oveq2d a = A 1 st b + a 2 1 2 nd b = 1 st b + A 2 1 2 nd b
5 4 mpteq2dv a = A b 0 × 1 st b + a 2 1 2 nd b = b 0 × 1 st b + A 2 1 2 nd b
6 5 cnveqd a = A b 0 × 1 st b + a 2 1 2 nd b -1 = b 0 × 1 st b + A 2 1 2 nd b -1
7 6 adantr a = A n = N b 0 × 1 st b + a 2 1 2 nd b -1 = b 0 × 1 st b + A 2 1 2 nd b -1
8 id a = A a = A
9 8 2 oveq12d a = A a + a 2 1 = A + A 2 1
10 id n = N n = N
11 9 10 oveqan12d a = A n = N a + a 2 1 n = A + A 2 1 N
12 7 11 fveq12d a = A n = N b 0 × 1 st b + a 2 1 2 nd b -1 a + a 2 1 n = b 0 × 1 st b + A 2 1 2 nd b -1 A + A 2 1 N
13 12 fveq2d a = A n = N 2 nd b 0 × 1 st b + a 2 1 2 nd b -1 a + a 2 1 n = 2 nd b 0 × 1 st b + A 2 1 2 nd b -1 A + A 2 1 N
14 df-rmy Y rm = a 2 , n 2 nd b 0 × 1 st b + a 2 1 2 nd b -1 a + a 2 1 n
15 fvex 2 nd b 0 × 1 st b + A 2 1 2 nd b -1 A + A 2 1 N V
16 13 14 15 ovmpoa A 2 N A Y rm N = 2 nd b 0 × 1 st b + A 2 1 2 nd b -1 A + A 2 1 N