Metamath Proof Explorer

Theorem rmxluc

Description: The X sequence is a Lucas (second-order integer recurrence) sequence. Part 3 of equation 2.11 of JonesMatijasevic p. 695. (Contributed by Stefan O'Rear, 14-Oct-2014)

Ref Expression
Assertion rmxluc 
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX ( N + 1 ) ) = ( ( ( 2 x. A ) x. ( A rmX N ) ) - ( A rmX ( N - 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
2 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
3 2 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N - 1 ) e. ZZ ) -> ( A rmX ( N - 1 ) ) e. NN0 )
4 3 nn0cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N - 1 ) e. ZZ ) -> ( A rmX ( N - 1 ) ) e. CC )
5 1 4 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX ( N - 1 ) ) e. CC )
6 peano2z 
 |-  ( N e. ZZ -> ( N + 1 ) e. ZZ )
7 2 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N + 1 ) e. ZZ ) -> ( A rmX ( N + 1 ) ) e. NN0 )
8 7 nn0cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N + 1 ) e. ZZ ) -> ( A rmX ( N + 1 ) ) e. CC )
9 6 8 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX ( N + 1 ) ) e. CC )
10 5 9 addcomd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX ( N - 1 ) ) + ( A rmX ( N + 1 ) ) ) = ( ( A rmX ( N + 1 ) ) + ( A rmX ( N - 1 ) ) ) )
11 rmxp1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX ( N + 1 ) ) = ( ( ( A rmX N ) x. A ) + ( ( ( A ^ 2 ) - 1 ) x. ( A rmY N ) ) ) )
12 rmxm1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX ( N - 1 ) ) = ( ( A x. ( A rmX N ) ) - ( ( ( A ^ 2 ) - 1 ) x. ( A rmY N ) ) ) )
13 11 12 oveq12d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX ( N + 1 ) ) + ( A rmX ( N - 1 ) ) ) = ( ( ( ( A rmX N ) x. A ) + ( ( ( A ^ 2 ) - 1 ) x. ( A rmY N ) ) ) + ( ( A x. ( A rmX N ) ) - ( ( ( A ^ 2 ) - 1 ) x. ( A rmY N ) ) ) ) )
14 2 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
15 14 nn0cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. CC )
16 eluzelcn 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. CC )
17 16 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> A e. CC )
18 15 17 mulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) x. A ) e. CC )
19 rmspecnonsq 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) )
20 19 eldifad 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. NN )
21 20 nncnd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. CC )
22 21 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A ^ 2 ) - 1 ) e. CC )
23 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
24 23 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )
25 24 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. CC )
26 22 25 mulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A ^ 2 ) - 1 ) x. ( A rmY N ) ) e. CC )
27 17 15 mulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A x. ( A rmX N ) ) e. CC )
28 18 26 27 ppncand 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( ( A rmX N ) x. A ) + ( ( ( A ^ 2 ) - 1 ) x. ( A rmY N ) ) ) + ( ( A x. ( A rmX N ) ) - ( ( ( A ^ 2 ) - 1 ) x. ( A rmY N ) ) ) ) = ( ( ( A rmX N ) x. A ) + ( A x. ( A rmX N ) ) ) )
29 15 17 mulcomd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) x. A ) = ( A x. ( A rmX N ) ) )
30 29 oveq1d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A rmX N ) x. A ) + ( A x. ( A rmX N ) ) ) = ( ( A x. ( A rmX N ) ) + ( A x. ( A rmX N ) ) ) )
31 2cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> 2 e. CC )
32 31 17 15 mulassd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( 2 x. A ) x. ( A rmX N ) ) = ( 2 x. ( A x. ( A rmX N ) ) ) )
33 27 2timesd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( 2 x. ( A x. ( A rmX N ) ) ) = ( ( A x. ( A rmX N ) ) + ( A x. ( A rmX N ) ) ) )
34 32 33 eqtr2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A x. ( A rmX N ) ) + ( A x. ( A rmX N ) ) ) = ( ( 2 x. A ) x. ( A rmX N ) ) )
35 28 30 34 3eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( ( A rmX N ) x. A ) + ( ( ( A ^ 2 ) - 1 ) x. ( A rmY N ) ) ) + ( ( A x. ( A rmX N ) ) - ( ( ( A ^ 2 ) - 1 ) x. ( A rmY N ) ) ) ) = ( ( 2 x. A ) x. ( A rmX N ) ) )
36 10 13 35 3eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX ( N - 1 ) ) + ( A rmX ( N + 1 ) ) ) = ( ( 2 x. A ) x. ( A rmX N ) ) )
37 2cn 
 |-  2 e. CC
38 mulcl 
 |-  ( ( 2 e. CC /\ A e. CC ) -> ( 2 x. A ) e. CC )
39 37 17 38 sylancr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( 2 x. A ) e. CC )
40 39 15 mulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( 2 x. A ) x. ( A rmX N ) ) e. CC )
41 40 5 9 subaddd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( ( 2 x. A ) x. ( A rmX N ) ) - ( A rmX ( N - 1 ) ) ) = ( A rmX ( N + 1 ) ) <-> ( ( A rmX ( N - 1 ) ) + ( A rmX ( N + 1 ) ) ) = ( ( 2 x. A ) x. ( A rmX N ) ) ) )
42 36 41 mpbird 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( 2 x. A ) x. ( A rmX N ) ) - ( A rmX ( N - 1 ) ) ) = ( A rmX ( N + 1 ) ) )
43 42 eqcomd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX ( N + 1 ) ) = ( ( ( 2 x. A ) x. ( A rmX N ) ) - ( A rmX ( N - 1 ) ) ) )