Metamath Proof Explorer

Theorem jm2.21

Description: Lemma for jm2.20nn . Express X and Y values as a binomial. (Contributed by Stefan O'Rear, 26-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 rmbaserp 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) e. RR+ )
2 1 rpcnne0d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) e. CC /\ ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) =/= 0 ) )
3 expmulz 
 |-  ( ( ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) e. CC /\ ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) =/= 0 ) /\ ( N e. ZZ /\ J e. ZZ ) ) -> ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ ( N x. J ) ) = ( ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) ^ J ) )
4 2 3 sylan 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ J e. ZZ ) ) -> ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ ( N x. J ) ) = ( ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) ^ J ) )
5 zmulcl 
 |-  ( ( N e. ZZ /\ J e. ZZ ) -> ( N x. J ) e. ZZ )
6 rmxyval 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N x. J ) e. ZZ ) -> ( ( A rmX ( N x. J ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY ( N x. J ) ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ ( N x. J ) ) )
7 5 6 sylan2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ J e. ZZ ) ) -> ( ( A rmX ( N x. J ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY ( N x. J ) ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ ( N x. J ) ) )
8 rmxyval 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) )
9 8 adantrr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ J e. ZZ ) ) -> ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) )
10 9 oveq1d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ J e. ZZ ) ) -> ( ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) ^ J ) = ( ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) ^ J ) )
11 4 7 10 3eqtr4d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( N e. ZZ /\ J e. ZZ ) ) -> ( ( A rmX ( N x. J ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY ( N x. J ) ) ) ) = ( ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) ^ J ) )
12 11 3impb 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. ZZ ) -> ( ( A rmX ( N x. J ) ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY ( N x. J ) ) ) ) = ( ( ( A rmX N ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY N ) ) ) ^ J ) )