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 ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) = ( ( ( 2 · 𝐴 ) · ( 𝐴 Yrm 𝑁 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 rmyluc ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) = ( ( 2 · ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )
2 frmy Yrm : ( ( ℤ ‘ 2 ) × ℤ ) ⟶ ℤ
3 2 fovcl ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
4 3 zcnd ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℂ )
5 eluzelcn ( 𝐴 ∈ ( ℤ ‘ 2 ) → 𝐴 ∈ ℂ )
6 5 adantr ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → 𝐴 ∈ ℂ )
7 4 6 mulcomd ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) = ( 𝐴 · ( 𝐴 Yrm 𝑁 ) ) )
8 7 oveq2d ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 2 · ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) ) = ( 2 · ( 𝐴 · ( 𝐴 Yrm 𝑁 ) ) ) )
9 2cnd ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → 2 ∈ ℂ )
10 9 6 4 mulassd ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 2 · 𝐴 ) · ( 𝐴 Yrm 𝑁 ) ) = ( 2 · ( 𝐴 · ( 𝐴 Yrm 𝑁 ) ) ) )
11 8 10 eqtr4d ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 2 · ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) ) = ( ( 2 · 𝐴 ) · ( 𝐴 Yrm 𝑁 ) ) )
12 11 oveq1d ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 2 · ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) = ( ( ( 2 · 𝐴 ) · ( 𝐴 Yrm 𝑁 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )
13 1 12 eqtrd ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) = ( ( ( 2 · 𝐴 ) · ( 𝐴 Yrm 𝑁 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )