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 ( 𝐴 ∈ ℂ → ( cos ‘ ( 5 · 𝐴 ) ) = ( ( ( 1 6 · ( ( cos ‘ 𝐴 ) ↑ 5 ) ) − ( 2 0 · ( ( cos ‘ 𝐴 ) ↑ 3 ) ) ) + ( 5 · ( cos ‘ 𝐴 ) ) ) )

Proof

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