Metamath Proof Explorer

Theorem rmyluc

Description: The Y sequence is a Lucas sequence, definable via this second-order recurrence with rmy0 and rmy1 . Part 3 of equation 2.12 of JonesMatijasevic p. 695. JonesMatijasevic uses this theorem to redefine the X and Y sequences to have domain ( ZZ X. ZZ ) , which simplifies some later theorems. It may shorten the derivation to use this as our initial definition. Incidentally, the X sequence satisfies the exact same recurrence. (Contributed by Stefan O'Rear, 1-Oct-2014)

Ref Expression
Assertion rmyluc ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) = ( ( 2 · ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 peano2z ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 + 1 ) ∈ ℤ )
2 frmy ⊢ Yrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℤ
3 2 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 + 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) ∈ ℤ )
4 1 3 sylan2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) ∈ ℤ )
5 4 zcnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) ∈ ℂ )
6 2cn ⊢ 2 ∈ ℂ
7 2 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℤ )
8 7 zcnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) ∈ ℂ )
9 eluzelcn ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℂ )
10 9 adantr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → 𝐴 ∈ ℂ )
11 8 10 mulcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) ∈ ℂ )
12 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) ∈ ℂ ) → ( 2 · ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) ) ∈ ℂ )
13 6 11 12 sylancr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 2 · ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) ) ∈ ℂ )
14 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
15 2 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑁 − 1 ) ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∈ ℤ )
16 14 15 sylan2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∈ ℤ )
17 16 zcnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) ∈ ℂ )
18 13 17 subcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 2 · ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) ∈ ℂ )
19 rmyp1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) + ( 𝐴 Xrm 𝑁 ) ) )
20 rmym1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 − 1 ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) − ( 𝐴 Xrm 𝑁 ) ) )
21 19 20 oveq12d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm ( 𝑁 + 1 ) ) + ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) = ( ( ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) + ( 𝐴 Xrm 𝑁 ) ) + ( ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) − ( 𝐴 Xrm 𝑁 ) ) ) )
22 frmx ⊢ Xrm : ( ( ℤ≥ ‘ 2 ) × ℤ ) ⟶ ℕ0
23 22 fovcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℕ0 )
24 23 nn0cnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Xrm 𝑁 ) ∈ ℂ )
25 11 24 11 ppncand ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) + ( 𝐴 Xrm 𝑁 ) ) + ( ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) − ( 𝐴 Xrm 𝑁 ) ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) + ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) ) )
26 13 17 npcand ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 2 · ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) + ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) = ( 2 · ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) ) )
27 11 2timesd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 2 · ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) ) = ( ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) + ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) ) )
28 26 27 eqtr2d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) + ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) ) = ( ( ( 2 · ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) + ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )
29 21 25 28 3eqtrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 Yrm ( 𝑁 + 1 ) ) + ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) = ( ( ( 2 · ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) + ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )
30 5 18 17 29 addcan2ad ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm ( 𝑁 + 1 ) ) = ( ( 2 · ( ( 𝐴 Yrm 𝑁 ) · 𝐴 ) ) − ( 𝐴 Yrm ( 𝑁 − 1 ) ) ) )