Metamath Proof Explorer


Theorem rmyluc2

Description: Lucas sequence property of Y with better output ordering. (Contributed by Stefan O'Rear, 16-Oct-2014)

Ref Expression
Assertion rmyluc2 A 2 N A Y rm N + 1 = 2 A A Y rm N A Y rm N 1

Proof

Step Hyp Ref Expression
1 rmyluc A 2 N A Y rm N + 1 = 2 A Y rm N A A Y rm N 1
2 frmy Y rm : 2 ×
3 2 fovcl A 2 N A Y rm N
4 3 zcnd A 2 N A Y rm N
5 eluzelcn A 2 A
6 5 adantr A 2 N A
7 4 6 mulcomd A 2 N A Y rm N A = A A Y rm N
8 7 oveq2d A 2 N 2 A Y rm N A = 2 A A Y rm N
9 2cnd A 2 N 2
10 9 6 4 mulassd A 2 N 2 A A Y rm N = 2 A A Y rm N
11 8 10 eqtr4d A 2 N 2 A Y rm N A = 2 A A Y rm N
12 11 oveq1d A 2 N 2 A Y rm N A A Y rm N 1 = 2 A A Y rm N A Y rm N 1
13 1 12 eqtrd A 2 N A Y rm N + 1 = 2 A A Y rm N A Y rm N 1