Metamath Proof Explorer

Theorem cos5t

Description: Five-times-angle formula for cosine, in pure cosine form. (Contributed by Ender Ting, 20-Apr-2026)

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

Proof

Step Hyp Ref Expression
1 picn 
 |-  _pi e. CC
2 2cn 
 |-  2 e. CC
3 2ne0 
 |-  2 =/= 0
4 1 2 3 divcli 
 |-  ( _pi / 2 ) e. CC
5 4 a1i 
 |-  ( A e. CC -> ( _pi / 2 ) e. CC )
6 5cn 
 |-  5 e. CC
7 6 a1i 
 |-  ( A e. CC -> 5 e. CC )
8 id 
 |-  ( A e. CC -> A e. CC )
9 7 8 mulcld 
 |-  ( A e. CC -> ( 5 x. A ) e. CC )
10 5 9 subcld 
 |-  ( A e. CC -> ( ( _pi / 2 ) - ( 5 x. A ) ) e. CC )
11 1zzd 
 |-  ( A e. CC -> 1 e. ZZ )
12 sinper 
 |-  ( ( ( ( _pi / 2 ) - ( 5 x. A ) ) e. CC /\ 1 e. ZZ ) -> ( sin ` ( ( ( _pi / 2 ) - ( 5 x. A ) ) + ( 1 x. ( 2 x. _pi ) ) ) ) = ( sin ` ( ( _pi / 2 ) - ( 5 x. A ) ) ) )
13 10 11 12 syl2anc 
 |-  ( A e. CC -> ( sin ` ( ( ( _pi / 2 ) - ( 5 x. A ) ) + ( 1 x. ( 2 x. _pi ) ) ) ) = ( sin ` ( ( _pi / 2 ) - ( 5 x. A ) ) ) )
14 7 5 8 subdid 
 |-  ( A e. CC -> ( 5 x. ( ( _pi / 2 ) - A ) ) = ( ( 5 x. ( _pi / 2 ) ) - ( 5 x. A ) ) )
15 4 mullidi 
 |-  ( 1 x. ( _pi / 2 ) ) = ( _pi / 2 )
16 15 eqcomi 
 |-  ( _pi / 2 ) = ( 1 x. ( _pi / 2 ) )
17 16 a1i 
 |-  ( A e. CC -> ( _pi / 2 ) = ( 1 x. ( _pi / 2 ) ) )
18 2 1 mulcli 
 |-  ( 2 x. _pi ) e. CC
19 18 mullidi 
 |-  ( 1 x. ( 2 x. _pi ) ) = ( 2 x. _pi )
20 1 2 3 divcan2i 
 |-  ( 2 x. ( _pi / 2 ) ) = _pi
21 20 eqcomi 
 |-  _pi = ( 2 x. ( _pi / 2 ) )
22 21 oveq2i 
 |-  ( 2 x. _pi ) = ( 2 x. ( 2 x. ( _pi / 2 ) ) )
23 2 2 4 mulassi 
 |-  ( ( 2 x. 2 ) x. ( _pi / 2 ) ) = ( 2 x. ( 2 x. ( _pi / 2 ) ) )
24 2t2e4 
 |-  ( 2 x. 2 ) = 4
25 24 oveq1i 
 |-  ( ( 2 x. 2 ) x. ( _pi / 2 ) ) = ( 4 x. ( _pi / 2 ) )
26 23 25 eqtr3i 
 |-  ( 2 x. ( 2 x. ( _pi / 2 ) ) ) = ( 4 x. ( _pi / 2 ) )
27 19 22 26 3eqtri 
 |-  ( 1 x. ( 2 x. _pi ) ) = ( 4 x. ( _pi / 2 ) )
28 27 a1i 
 |-  ( A e. CC -> ( 1 x. ( 2 x. _pi ) ) = ( 4 x. ( _pi / 2 ) ) )
29 17 28 oveq12d 
 |-  ( A e. CC -> ( ( _pi / 2 ) + ( 1 x. ( 2 x. _pi ) ) ) = ( ( 1 x. ( _pi / 2 ) ) + ( 4 x. ( _pi / 2 ) ) ) )
30 1cnd 
 |-  ( A e. CC -> 1 e. CC )
31 4cn 
 |-  4 e. CC
32 31 a1i 
 |-  ( A e. CC -> 4 e. CC )
33 30 32 5 adddird 
 |-  ( A e. CC -> ( ( 1 + 4 ) x. ( _pi / 2 ) ) = ( ( 1 x. ( _pi / 2 ) ) + ( 4 x. ( _pi / 2 ) ) ) )
34 ax-1cn 
 |-  1 e. CC
35 df-5 
 |-  5 = ( 4 + 1 )
36 31 34 35 comraddi 
 |-  5 = ( 1 + 4 )
37 36 eqcomi 
 |-  ( 1 + 4 ) = 5
38 37 a1i 
 |-  ( A e. CC -> ( 1 + 4 ) = 5 )
39 38 oveq1d 
 |-  ( A e. CC -> ( ( 1 + 4 ) x. ( _pi / 2 ) ) = ( 5 x. ( _pi / 2 ) ) )
40 29 33 39 3eqtr2d 
 |-  ( A e. CC -> ( ( _pi / 2 ) + ( 1 x. ( 2 x. _pi ) ) ) = ( 5 x. ( _pi / 2 ) ) )
41 40 oveq1d 
 |-  ( A e. CC -> ( ( ( _pi / 2 ) + ( 1 x. ( 2 x. _pi ) ) ) - ( 5 x. A ) ) = ( ( 5 x. ( _pi / 2 ) ) - ( 5 x. A ) ) )
42 34 18 mulcli 
 |-  ( 1 x. ( 2 x. _pi ) ) e. CC
43 42 a1i 
 |-  ( A e. CC -> ( 1 x. ( 2 x. _pi ) ) e. CC )
44 5 43 9 addsubd 
 |-  ( A e. CC -> ( ( ( _pi / 2 ) + ( 1 x. ( 2 x. _pi ) ) ) - ( 5 x. A ) ) = ( ( ( _pi / 2 ) - ( 5 x. A ) ) + ( 1 x. ( 2 x. _pi ) ) ) )
45 14 41 44 3eqtr2rd 
 |-  ( A e. CC -> ( ( ( _pi / 2 ) - ( 5 x. A ) ) + ( 1 x. ( 2 x. _pi ) ) ) = ( 5 x. ( ( _pi / 2 ) - A ) ) )
46 45 fveq2d 
 |-  ( A e. CC -> ( sin ` ( ( ( _pi / 2 ) - ( 5 x. A ) ) + ( 1 x. ( 2 x. _pi ) ) ) ) = ( sin ` ( 5 x. ( ( _pi / 2 ) - A ) ) ) )
47 sinhalfpim 
 |-  ( ( 5 x. A ) e. CC -> ( sin ` ( ( _pi / 2 ) - ( 5 x. A ) ) ) = ( cos ` ( 5 x. A ) ) )
48 9 47 syl 
 |-  ( A e. CC -> ( sin ` ( ( _pi / 2 ) - ( 5 x. A ) ) ) = ( cos ` ( 5 x. A ) ) )
49 13 46 48 3eqtr3rd 
 |-  ( A e. CC -> ( cos ` ( 5 x. A ) ) = ( sin ` ( 5 x. ( ( _pi / 2 ) - A ) ) ) )
50 5 8 subcld 
 |-  ( A e. CC -> ( ( _pi / 2 ) - A ) e. CC )
51 sin5t 
 |-  ( ( ( _pi / 2 ) - A ) e. CC -> ( sin ` ( 5 x. ( ( _pi / 2 ) - A ) ) ) = ( ( ( ; 1 6 x. ( ( sin ` ( ( _pi / 2 ) - A ) ) ^ 5 ) ) - ( ; 2 0 x. ( ( sin ` ( ( _pi / 2 ) - A ) ) ^ 3 ) ) ) + ( 5 x. ( sin ` ( ( _pi / 2 ) - A ) ) ) ) )
52 50 51 syl 
 |-  ( A e. CC -> ( sin ` ( 5 x. ( ( _pi / 2 ) - A ) ) ) = ( ( ( ; 1 6 x. ( ( sin ` ( ( _pi / 2 ) - A ) ) ^ 5 ) ) - ( ; 2 0 x. ( ( sin ` ( ( _pi / 2 ) - A ) ) ^ 3 ) ) ) + ( 5 x. ( sin ` ( ( _pi / 2 ) - A ) ) ) ) )
53 sinhalfpim 
 |-  ( A e. CC -> ( sin ` ( ( _pi / 2 ) - A ) ) = ( cos ` A ) )
54 53 oveq1d 
 |-  ( A e. CC -> ( ( sin ` ( ( _pi / 2 ) - A ) ) ^ 5 ) = ( ( cos ` A ) ^ 5 ) )
55 54 oveq2d 
 |-  ( A e. CC -> ( ; 1 6 x. ( ( sin ` ( ( _pi / 2 ) - A ) ) ^ 5 ) ) = ( ; 1 6 x. ( ( cos ` A ) ^ 5 ) ) )
56 53 oveq1d 
 |-  ( A e. CC -> ( ( sin ` ( ( _pi / 2 ) - A ) ) ^ 3 ) = ( ( cos ` A ) ^ 3 ) )
57 56 oveq2d 
 |-  ( A e. CC -> ( ; 2 0 x. ( ( sin ` ( ( _pi / 2 ) - A ) ) ^ 3 ) ) = ( ; 2 0 x. ( ( cos ` A ) ^ 3 ) ) )
58 55 57 oveq12d 
 |-  ( A e. CC -> ( ( ; 1 6 x. ( ( sin ` ( ( _pi / 2 ) - A ) ) ^ 5 ) ) - ( ; 2 0 x. ( ( sin ` ( ( _pi / 2 ) - A ) ) ^ 3 ) ) ) = ( ( ; 1 6 x. ( ( cos ` A ) ^ 5 ) ) - ( ; 2 0 x. ( ( cos ` A ) ^ 3 ) ) ) )
59 53 oveq2d 
 |-  ( A e. CC -> ( 5 x. ( sin ` ( ( _pi / 2 ) - A ) ) ) = ( 5 x. ( cos ` A ) ) )
60 58 59 oveq12d 
 |-  ( A e. CC -> ( ( ( ; 1 6 x. ( ( sin ` ( ( _pi / 2 ) - A ) ) ^ 5 ) ) - ( ; 2 0 x. ( ( sin ` ( ( _pi / 2 ) - A ) ) ^ 3 ) ) ) + ( 5 x. ( sin ` ( ( _pi / 2 ) - A ) ) ) ) = ( ( ( ; 1 6 x. ( ( cos ` A ) ^ 5 ) ) - ( ; 2 0 x. ( ( cos ` A ) ^ 3 ) ) ) + ( 5 x. ( cos ` A ) ) ) )
61 49 52 60 3eqtrd 
 |-  ( A e. CC -> ( cos ` ( 5 x. A ) ) = ( ( ( ; 1 6 x. ( ( cos ` A ) ^ 5 ) ) - ( ; 2 0 x. ( ( cos ` A ) ^ 3 ) ) ) + ( 5 x. ( cos ` A ) ) ) )