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 e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY ( N + 1 ) ) = ( ( 2 x. ( ( A rmY N ) x. A ) ) - ( A rmY ( N - 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 peano2z 
 |-  ( N e. ZZ -> ( N + 1 ) e. ZZ )
2 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
3 2 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N + 1 ) e. ZZ ) -> ( A rmY ( N + 1 ) ) e. ZZ )
4 1 3 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY ( N + 1 ) ) e. ZZ )
5 4 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY ( N + 1 ) ) e. CC )
6 2cn 
 |-  2 e. CC
7 2 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )
8 7 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. CC )
9 eluzelcn 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. CC )
10 9 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> A e. CC )
11 8 10 mulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmY N ) x. A ) e. CC )
12 mulcl 
 |-  ( ( 2 e. CC /\ ( ( A rmY N ) x. A ) e. CC ) -> ( 2 x. ( ( A rmY N ) x. A ) ) e. CC )
13 6 11 12 sylancr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( 2 x. ( ( A rmY N ) x. A ) ) e. CC )
14 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
15 2 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N - 1 ) e. ZZ ) -> ( A rmY ( N - 1 ) ) e. ZZ )
16 14 15 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY ( N - 1 ) ) e. ZZ )
17 16 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY ( N - 1 ) ) e. CC )
18 13 17 subcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( 2 x. ( ( A rmY N ) x. A ) ) - ( A rmY ( N - 1 ) ) ) e. CC )
19 rmyp1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY ( N + 1 ) ) = ( ( ( A rmY N ) x. A ) + ( A rmX N ) ) )
20 rmym1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY ( N - 1 ) ) = ( ( ( A rmY N ) x. A ) - ( A rmX N ) ) )
21 19 20 oveq12d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmY ( N + 1 ) ) + ( A rmY ( N - 1 ) ) ) = ( ( ( ( A rmY N ) x. A ) + ( A rmX N ) ) + ( ( ( A rmY N ) x. A ) - ( A rmX N ) ) ) )
22 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
23 22 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
24 23 nn0cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. CC )
25 11 24 11 ppncand 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( ( A rmY N ) x. A ) + ( A rmX N ) ) + ( ( ( A rmY N ) x. A ) - ( A rmX N ) ) ) = ( ( ( A rmY N ) x. A ) + ( ( A rmY N ) x. A ) ) )
26 13 17 npcand 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( 2 x. ( ( A rmY N ) x. A ) ) - ( A rmY ( N - 1 ) ) ) + ( A rmY ( N - 1 ) ) ) = ( 2 x. ( ( A rmY N ) x. A ) ) )
27 11 2timesd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( 2 x. ( ( A rmY N ) x. A ) ) = ( ( ( A rmY N ) x. A ) + ( ( A rmY N ) x. A ) ) )
28 26 27 eqtr2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A rmY N ) x. A ) + ( ( A rmY N ) x. A ) ) = ( ( ( 2 x. ( ( A rmY N ) x. A ) ) - ( A rmY ( N - 1 ) ) ) + ( A rmY ( N - 1 ) ) ) )
29 21 25 28 3eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmY ( N + 1 ) ) + ( A rmY ( N - 1 ) ) ) = ( ( ( 2 x. ( ( A rmY N ) x. A ) ) - ( A rmY ( N - 1 ) ) ) + ( A rmY ( N - 1 ) ) ) )
30 5 18 17 29 addcan2ad 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY ( N + 1 ) ) = ( ( 2 x. ( ( A rmY N ) x. A ) ) - ( A rmY ( N - 1 ) ) ) )