Metamath Proof Explorer

Theorem rmym1

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

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

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( N e. ZZ -> N e. CC )
2 1 adantl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> N e. CC )
3 ax-1cn 
 |-  1 e. CC
4 negsub 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( N + -u 1 ) = ( N - 1 ) )
5 2 3 4 sylancl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( N + -u 1 ) = ( N - 1 ) )
6 5 eqcomd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( N - 1 ) = ( N + -u 1 ) )
7 6 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY ( N - 1 ) ) = ( A rmY ( N + -u 1 ) ) )
8 neg1z 
 |-  -u 1 e. ZZ
9 rmyadd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ -u 1 e. ZZ ) -> ( A rmY ( N + -u 1 ) ) = ( ( ( A rmY N ) x. ( A rmX -u 1 ) ) + ( ( A rmX N ) x. ( A rmY -u 1 ) ) ) )
10 8 9 mp3an3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY ( N + -u 1 ) ) = ( ( ( A rmY N ) x. ( A rmX -u 1 ) ) + ( ( A rmX N ) x. ( A rmY -u 1 ) ) ) )
11 1z 
 |-  1 e. ZZ
12 rmxneg 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ 1 e. ZZ ) -> ( A rmX -u 1 ) = ( A rmX 1 ) )
13 11 12 mpan2 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmX -u 1 ) = ( A rmX 1 ) )
14 rmx1 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmX 1 ) = A )
15 13 14 eqtrd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmX -u 1 ) = A )
16 15 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX -u 1 ) = A )
17 16 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmY N ) x. ( A rmX -u 1 ) ) = ( ( A rmY N ) x. A ) )
18 rmyneg 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ 1 e. ZZ ) -> ( A rmY -u 1 ) = -u ( A rmY 1 ) )
19 11 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 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY -u 1 ) = -u 1 )
24 23 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) x. ( A rmY -u 1 ) ) = ( ( A rmX N ) x. -u 1 ) )
25 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
26 25 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
27 26 nn0cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. CC )
28 neg1cn 
 |-  -u 1 e. CC
29 mulcom 
 |-  ( ( ( A rmX N ) e. CC /\ -u 1 e. CC ) -> ( ( A rmX N ) x. -u 1 ) = ( -u 1 x. ( A rmX N ) ) )
30 27 28 29 sylancl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) x. -u 1 ) = ( -u 1 x. ( A rmX N ) ) )
31 27 mulm1d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( -u 1 x. ( A rmX N ) ) = -u ( A rmX N ) )
32 24 30 31 3eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) x. ( A rmY -u 1 ) ) = -u ( A rmX N ) )
33 17 32 oveq12d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A rmY N ) x. ( A rmX -u 1 ) ) + ( ( A rmX N ) x. ( A rmY -u 1 ) ) ) = ( ( ( A rmY N ) x. A ) + -u ( A rmX N ) ) )
34 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
35 34 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )
36 35 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. CC )
37 eluzelcn 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. CC )
38 37 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> A e. CC )
39 36 38 mulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmY N ) x. A ) e. CC )
40 39 27 negsubd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A rmY N ) x. A ) + -u ( A rmX N ) ) = ( ( ( A rmY N ) x. A ) - ( A rmX N ) ) )
41 33 40 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A rmY N ) x. ( A rmX -u 1 ) ) + ( ( A rmX N ) x. ( A rmY -u 1 ) ) ) = ( ( ( A rmY N ) x. A ) - ( A rmX N ) ) )
42 7 10 41 3eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY ( N - 1 ) ) = ( ( ( A rmY N ) x. A ) - ( A rmX N ) ) )