Metamath Proof Explorer

Theorem rmyp1

Description: Special addition of 1 formula for Y sequence. Part 2 of equation 2.9 of JonesMatijasevic p. 695. (Contributed by Stefan O'Rear, 24-Sep-2014)

Ref Expression
Assertion rmyp1 
|- ( ( 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 1z 
 |-  1 e. ZZ
2 rmyadd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ 1 e. ZZ ) -> ( A rmY ( N + 1 ) ) = ( ( ( A rmY N ) x. ( A rmX 1 ) ) + ( ( A rmX N ) x. ( A rmY 1 ) ) ) )
3 1 2 mp3an3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY ( N + 1 ) ) = ( ( ( A rmY N ) x. ( A rmX 1 ) ) + ( ( A rmX N ) x. ( A rmY 1 ) ) ) )
4 rmx1 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmX 1 ) = A )
5 4 oveq2d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A rmY N ) x. ( A rmX 1 ) ) = ( ( A rmY N ) x. A ) )
6 5 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmY N ) x. ( A rmX 1 ) ) = ( ( A rmY N ) x. A ) )
7 rmy1 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY 1 ) = 1 )
8 7 oveq2d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A rmX N ) x. ( A rmY 1 ) ) = ( ( A rmX N ) x. 1 ) )
9 8 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) x. ( A rmY 1 ) ) = ( ( A rmX N ) x. 1 ) )
10 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
11 10 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
12 11 nn0cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. CC )
13 12 mulid1d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) x. 1 ) = ( A rmX N ) )
14 9 13 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) x. ( A rmY 1 ) ) = ( A rmX N ) )
15 6 14 oveq12d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A rmY N ) x. ( A rmX 1 ) ) + ( ( A rmX N ) x. ( A rmY 1 ) ) ) = ( ( ( A rmY N ) x. A ) + ( A rmX N ) ) )
16 3 15 eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY ( N + 1 ) ) = ( ( ( A rmY N ) x. A ) + ( A rmX N ) ) )