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 ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐ด Yrm ( 2 ยท ๐‘ ) ) = ( ( 2 ยท ( ๐ด Xrm ๐‘ ) ) ยท ( ๐ด Yrm ๐‘ ) ) )

Proof

Step Hyp Ref Expression
1 zcn โŠข ( ๐‘ โˆˆ โ„ค โ†’ ๐‘ โˆˆ โ„‚ )
2 1 adantl โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ๐‘ โˆˆ โ„‚ )
3 2 2timesd โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( 2 ยท ๐‘ ) = ( ๐‘ + ๐‘ ) )
4 3 oveq2d โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐ด Yrm ( 2 ยท ๐‘ ) ) = ( ๐ด Yrm ( ๐‘ + ๐‘ ) ) )
5 rmyadd โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐ด Yrm ( ๐‘ + ๐‘ ) ) = ( ( ( ๐ด Yrm ๐‘ ) ยท ( ๐ด Xrm ๐‘ ) ) + ( ( ๐ด Xrm ๐‘ ) ยท ( ๐ด Yrm ๐‘ ) ) ) )
6 5 3anidm23 โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐ด Yrm ( ๐‘ + ๐‘ ) ) = ( ( ( ๐ด Yrm ๐‘ ) ยท ( ๐ด Xrm ๐‘ ) ) + ( ( ๐ด Xrm ๐‘ ) ยท ( ๐ด Yrm ๐‘ ) ) ) )
7 2cnd โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ 2 โˆˆ โ„‚ )
8 frmx โŠข Xrm : ( ( โ„คโ‰ฅ โ€˜ 2 ) ร— โ„ค ) โŸถ โ„•0
9 8 fovcl โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐ด Xrm ๐‘ ) โˆˆ โ„•0 )
10 9 nn0cnd โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐ด Xrm ๐‘ ) โˆˆ โ„‚ )
11 frmy โŠข Yrm : ( ( โ„คโ‰ฅ โ€˜ 2 ) ร— โ„ค ) โŸถ โ„ค
12 11 fovcl โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐ด Yrm ๐‘ ) โˆˆ โ„ค )
13 12 zcnd โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐ด Yrm ๐‘ ) โˆˆ โ„‚ )
14 7 10 13 mulassd โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( 2 ยท ( ๐ด Xrm ๐‘ ) ) ยท ( ๐ด Yrm ๐‘ ) ) = ( 2 ยท ( ( ๐ด Xrm ๐‘ ) ยท ( ๐ด Yrm ๐‘ ) ) ) )
15 10 13 mulcld โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐ด Xrm ๐‘ ) ยท ( ๐ด Yrm ๐‘ ) ) โˆˆ โ„‚ )
16 15 2timesd โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( 2 ยท ( ( ๐ด Xrm ๐‘ ) ยท ( ๐ด Yrm ๐‘ ) ) ) = ( ( ( ๐ด Xrm ๐‘ ) ยท ( ๐ด Yrm ๐‘ ) ) + ( ( ๐ด Xrm ๐‘ ) ยท ( ๐ด Yrm ๐‘ ) ) ) )
17 10 13 mulcomd โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐ด Xrm ๐‘ ) ยท ( ๐ด Yrm ๐‘ ) ) = ( ( ๐ด Yrm ๐‘ ) ยท ( ๐ด Xrm ๐‘ ) ) )
18 17 oveq1d โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ( ๐ด Xrm ๐‘ ) ยท ( ๐ด Yrm ๐‘ ) ) + ( ( ๐ด Xrm ๐‘ ) ยท ( ๐ด Yrm ๐‘ ) ) ) = ( ( ( ๐ด Yrm ๐‘ ) ยท ( ๐ด Xrm ๐‘ ) ) + ( ( ๐ด Xrm ๐‘ ) ยท ( ๐ด Yrm ๐‘ ) ) ) )
19 14 16 18 3eqtrrd โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ( ๐ด Yrm ๐‘ ) ยท ( ๐ด Xrm ๐‘ ) ) + ( ( ๐ด Xrm ๐‘ ) ยท ( ๐ด Yrm ๐‘ ) ) ) = ( ( 2 ยท ( ๐ด Xrm ๐‘ ) ) ยท ( ๐ด Yrm ๐‘ ) ) )
20 4 6 19 3eqtrd โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐ด Yrm ( 2 ยท ๐‘ ) ) = ( ( 2 ยท ( ๐ด Xrm ๐‘ ) ) ยท ( ๐ด Yrm ๐‘ ) ) )