Metamath Proof Explorer

Theorem rmxm1

Description: Subtraction of 1 formula for X sequence. Part 1 of equation 2.10 of JonesMatijasevic p. 695. (Contributed by Stefan O'Rear, 14-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 neg1z 
 |-  -u 1 e. ZZ
2 rmxadd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ -u 1 e. ZZ ) -> ( A rmX ( N + -u 1 ) ) = ( ( ( A rmX N ) x. ( A rmX -u 1 ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) x. ( A rmY -u 1 ) ) ) ) )
3 1 2 mp3an3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX ( N + -u 1 ) ) = ( ( ( A rmX N ) x. ( A rmX -u 1 ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) x. ( A rmY -u 1 ) ) ) ) )
4 1z 
 |-  1 e. ZZ
5 rmxneg 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ 1 e. ZZ ) -> ( A rmX -u 1 ) = ( A rmX 1 ) )
6 4 5 mpan2 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmX -u 1 ) = ( A rmX 1 ) )
7 rmx1 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmX 1 ) = A )
8 6 7 eqtrd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmX -u 1 ) = A )
9 8 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX -u 1 ) = A )
10 9 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) x. ( A rmX -u 1 ) ) = ( ( A rmX N ) x. A ) )
11 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
12 11 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
13 12 nn0cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. CC )
14 eluzelcn 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. CC )
15 14 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> A e. CC )
16 13 15 mulcomd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) x. A ) = ( A x. ( A rmX N ) ) )
17 10 16 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) x. ( A rmX -u 1 ) ) = ( A x. ( A rmX N ) ) )
18 rmyneg 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ 1 e. ZZ ) -> ( A rmY -u 1 ) = -u ( A rmY 1 ) )
19 4 18 mpan2 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY -u 1 ) = -u ( A rmY 1 ) )
20 rmy1 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY 1 ) = 1 )
21 20 negeqd 
 |-  ( A e. ( ZZ>= ` 2 ) -> -u ( A rmY 1 ) = -u 1 )
22 19 21 eqtrd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY -u 1 ) = -u 1 )
23 22 oveq2d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A rmY N ) x. ( A rmY -u 1 ) ) = ( ( A rmY N ) x. -u 1 ) )
24 23 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmY N ) x. ( A rmY -u 1 ) ) = ( ( A rmY N ) x. -u 1 ) )
25 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
26 25 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )
27 26 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. CC )
28 ax-1cn 
 |-  1 e. CC
29 mulneg2 
 |-  ( ( ( A rmY N ) e. CC /\ 1 e. CC ) -> ( ( A rmY N ) x. -u 1 ) = -u ( ( A rmY N ) x. 1 ) )
30 27 28 29 sylancl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmY N ) x. -u 1 ) = -u ( ( A rmY N ) x. 1 ) )
31 27 mulid1d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmY N ) x. 1 ) = ( A rmY N ) )
32 31 negeqd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> -u ( ( A rmY N ) x. 1 ) = -u ( A rmY N ) )
33 30 32 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmY N ) x. -u 1 ) = -u ( A rmY N ) )
34 24 33 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmY N ) x. ( A rmY -u 1 ) ) = -u ( A rmY N ) )
35 34 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) x. ( A rmY -u 1 ) ) ) = ( ( ( A ^ 2 ) - 1 ) x. -u ( A rmY N ) ) )
36 rmspecnonsq 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) )
37 36 eldifad 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. NN )
38 37 nncnd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. CC )
39 38 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A ^ 2 ) - 1 ) e. CC )
40 39 27 mulneg2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A ^ 2 ) - 1 ) x. -u ( A rmY N ) ) = -u ( ( ( A ^ 2 ) - 1 ) x. ( A rmY N ) ) )
41 35 40 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) x. ( A rmY -u 1 ) ) ) = -u ( ( ( A ^ 2 ) - 1 ) x. ( A rmY N ) ) )
42 17 41 oveq12d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A rmX N ) x. ( A rmX -u 1 ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) x. ( A rmY -u 1 ) ) ) ) = ( ( A x. ( A rmX N ) ) + -u ( ( ( A ^ 2 ) - 1 ) x. ( A rmY N ) ) ) )
43 3 42 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX ( N + -u 1 ) ) = ( ( A x. ( A rmX N ) ) + -u ( ( ( A ^ 2 ) - 1 ) x. ( A rmY N ) ) ) )
44 zcn 
 |-  ( N e. ZZ -> N e. CC )
45 44 adantl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> N e. CC )
46 negsub 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( N + -u 1 ) = ( N - 1 ) )
47 45 28 46 sylancl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( N + -u 1 ) = ( N - 1 ) )
48 47 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX ( N + -u 1 ) ) = ( A rmX ( N - 1 ) ) )
49 15 13 mulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A x. ( A rmX N ) ) e. CC )
50 39 27 mulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A ^ 2 ) - 1 ) x. ( A rmY N ) ) e. CC )
51 49 50 negsubd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A x. ( A rmX N ) ) + -u ( ( ( A ^ 2 ) - 1 ) x. ( A rmY N ) ) ) = ( ( A x. ( A rmX N ) ) - ( ( ( A ^ 2 ) - 1 ) x. ( A rmY N ) ) ) )
52 43 48 51 3eqtr3d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX ( N - 1 ) ) = ( ( A x. ( A rmX N ) ) - ( ( ( A ^ 2 ) - 1 ) x. ( A rmY N ) ) ) )