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 ⊢A∈ℤ≥2∧N∈ℤ→AYrmN+1=2⁢AYrmN⁢A−AYrmN−1

Proof

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