Metamath Proof Explorer

Theorem cos5teq

Description: Five-times-angle formula for cosine, substitution helper. (Contributed by Ender Ting, 9-May-2026)

Ref Expression
Assertion cos5teq 
|- ( ( A e. CC /\ B = ( 5 x. A ) /\ C = ( cos ` A ) ) -> ( cos ` B ) = ( ( ( ; 1 6 x. ( C ^ 5 ) ) - ( ; 2 0 x. ( C ^ 3 ) ) ) + ( 5 x. C ) ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( A e. CC /\ B = ( 5 x. A ) /\ C = ( cos ` A ) ) -> B = ( 5 x. A ) )
2 1 fveq2d 
 |-  ( ( A e. CC /\ B = ( 5 x. A ) /\ C = ( cos ` A ) ) -> ( cos ` B ) = ( cos ` ( 5 x. A ) ) )
3 cos5t 
 |-  ( A e. CC -> ( cos ` ( 5 x. A ) ) = ( ( ( ; 1 6 x. ( ( cos ` A ) ^ 5 ) ) - ( ; 2 0 x. ( ( cos ` A ) ^ 3 ) ) ) + ( 5 x. ( cos ` A ) ) ) )
4 3 3ad2ant1 
 |-  ( ( A e. CC /\ B = ( 5 x. A ) /\ C = ( cos ` A ) ) -> ( cos ` ( 5 x. A ) ) = ( ( ( ; 1 6 x. ( ( cos ` A ) ^ 5 ) ) - ( ; 2 0 x. ( ( cos ` A ) ^ 3 ) ) ) + ( 5 x. ( cos ` A ) ) ) )
5 eqcom 
 |-  ( C = ( cos ` A ) <-> ( cos ` A ) = C )
6 5 biimpi 
 |-  ( C = ( cos ` A ) -> ( cos ` A ) = C )
7 6 oveq1d 
 |-  ( C = ( cos ` A ) -> ( ( cos ` A ) ^ 5 ) = ( C ^ 5 ) )
8 7 oveq2d 
 |-  ( C = ( cos ` A ) -> ( ; 1 6 x. ( ( cos ` A ) ^ 5 ) ) = ( ; 1 6 x. ( C ^ 5 ) ) )
9 6 oveq1d 
 |-  ( C = ( cos ` A ) -> ( ( cos ` A ) ^ 3 ) = ( C ^ 3 ) )
10 9 oveq2d 
 |-  ( C = ( cos ` A ) -> ( ; 2 0 x. ( ( cos ` A ) ^ 3 ) ) = ( ; 2 0 x. ( C ^ 3 ) ) )
11 8 10 oveq12d 
 |-  ( C = ( cos ` A ) -> ( ( ; 1 6 x. ( ( cos ` A ) ^ 5 ) ) - ( ; 2 0 x. ( ( cos ` A ) ^ 3 ) ) ) = ( ( ; 1 6 x. ( C ^ 5 ) ) - ( ; 2 0 x. ( C ^ 3 ) ) ) )
12 6 oveq2d 
 |-  ( C = ( cos ` A ) -> ( 5 x. ( cos ` A ) ) = ( 5 x. C ) )
13 11 12 oveq12d 
 |-  ( C = ( cos ` A ) -> ( ( ( ; 1 6 x. ( ( cos ` A ) ^ 5 ) ) - ( ; 2 0 x. ( ( cos ` A ) ^ 3 ) ) ) + ( 5 x. ( cos ` A ) ) ) = ( ( ( ; 1 6 x. ( C ^ 5 ) ) - ( ; 2 0 x. ( C ^ 3 ) ) ) + ( 5 x. C ) ) )
14 13 3ad2ant3 
 |-  ( ( A e. CC /\ B = ( 5 x. A ) /\ C = ( cos ` A ) ) -> ( ( ( ; 1 6 x. ( ( cos ` A ) ^ 5 ) ) - ( ; 2 0 x. ( ( cos ` A ) ^ 3 ) ) ) + ( 5 x. ( cos ` A ) ) ) = ( ( ( ; 1 6 x. ( C ^ 5 ) ) - ( ; 2 0 x. ( C ^ 3 ) ) ) + ( 5 x. C ) ) )
15 2 4 14 3eqtrd 
 |-  ( ( A e. CC /\ B = ( 5 x. A ) /\ C = ( cos ` A ) ) -> ( cos ` B ) = ( ( ( ; 1 6 x. ( C ^ 5 ) ) - ( ; 2 0 x. ( C ^ 3 ) ) ) + ( 5 x. C ) ) )