Metamath Proof Explorer

Theorem rmxp1

Description: Special addition-of-1 formula for X sequence. Part 1 of equation 2.9 of JonesMatijasevic p. 695. (Contributed by Stefan O'Rear, 19-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 1z 
 |-  1 e. ZZ
2 rmxadd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ 1 e. ZZ ) -> ( A rmX ( N + 1 ) ) = ( ( ( A rmX N ) x. ( A rmX 1 ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) x. ( A rmY 1 ) ) ) ) )
3 1 2 mp3an3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX ( N + 1 ) ) = ( ( ( A rmX N ) x. ( A rmX 1 ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) x. ( A rmY 1 ) ) ) ) )
4 rmx1 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmX 1 ) = A )
5 4 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX 1 ) = A )
6 5 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) x. ( A rmX 1 ) ) = ( ( A rmX N ) x. A ) )
7 rmy1 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY 1 ) = 1 )
8 7 oveq2d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A rmY N ) x. ( A rmY 1 ) ) = ( ( A rmY N ) x. 1 ) )
9 8 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmY N ) x. ( A rmY 1 ) ) = ( ( A rmY N ) x. 1 ) )
10 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
11 10 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )
12 11 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. CC )
13 12 mulid1d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmY N ) x. 1 ) = ( A rmY N ) )
14 9 13 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmY N ) x. ( A rmY 1 ) ) = ( A rmY N ) )
15 14 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) x. ( A rmY 1 ) ) ) = ( ( ( A ^ 2 ) - 1 ) x. ( A rmY N ) ) )
16 6 15 oveq12d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A rmX N ) x. ( A rmX 1 ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) x. ( A rmY 1 ) ) ) ) = ( ( ( A rmX N ) x. A ) + ( ( ( A ^ 2 ) - 1 ) x. ( A rmY N ) ) ) )
17 3 16 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX ( N + 1 ) ) = ( ( ( A rmX N ) x. A ) + ( ( ( A ^ 2 ) - 1 ) x. ( A rmY N ) ) ) )