Metamath Proof Explorer

Theorem rmydbl

Description: "Double-angle formula" for Y-values. Equation 2.14 of JonesMatijasevic p. 695. (Contributed by Stefan O'Rear, 2-Oct-2014)

Ref Expression
Assertion rmydbl 
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY ( 2 x. N ) ) = ( ( 2 x. ( A rmX N ) ) x. ( A rmY 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 2 2timesd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( 2 x. N ) = ( N + N ) )
4 3 oveq2d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY ( 2 x. N ) ) = ( A rmY ( N + N ) ) )
5 rmyadd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N e. ZZ ) -> ( A rmY ( N + N ) ) = ( ( ( A rmY N ) x. ( A rmX N ) ) + ( ( A rmX N ) x. ( A rmY N ) ) ) )
6 5 3anidm23 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY ( N + N ) ) = ( ( ( A rmY N ) x. ( A rmX N ) ) + ( ( A rmX N ) x. ( A rmY N ) ) ) )
7 2cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> 2 e. CC )
8 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
9 8 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
10 9 nn0cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. CC )
11 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
12 11 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )
13 12 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. CC )
14 7 10 13 mulassd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( 2 x. ( A rmX N ) ) x. ( A rmY N ) ) = ( 2 x. ( ( A rmX N ) x. ( A rmY N ) ) ) )
15 10 13 mulcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) x. ( A rmY N ) ) e. CC )
16 15 2timesd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( 2 x. ( ( A rmX N ) x. ( A rmY N ) ) ) = ( ( ( A rmX N ) x. ( A rmY N ) ) + ( ( A rmX N ) x. ( A rmY N ) ) ) )
17 10 13 mulcomd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) x. ( A rmY N ) ) = ( ( A rmY N ) x. ( A rmX N ) ) )
18 17 oveq1d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A rmX N ) x. ( A rmY N ) ) + ( ( A rmX N ) x. ( A rmY N ) ) ) = ( ( ( A rmY N ) x. ( A rmX N ) ) + ( ( A rmX N ) x. ( A rmY N ) ) ) )
19 14 16 18 3eqtrrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A rmY N ) x. ( A rmX N ) ) + ( ( A rmX N ) x. ( A rmY N ) ) ) = ( ( 2 x. ( A rmX N ) ) x. ( A rmY N ) ) )
20 4 6 19 3eqtrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY ( 2 x. N ) ) = ( ( 2 x. ( A rmX N ) ) x. ( A rmY N ) ) )