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

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 = ( 5 · 𝐴 ) ∧ 𝐶 = ( cos ‘ 𝐴 ) ) → 𝐵 = ( 5 · 𝐴 ) )
2 1 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 = ( 5 · 𝐴 ) ∧ 𝐶 = ( cos ‘ 𝐴 ) ) → ( cos ‘ 𝐵 ) = ( cos ‘ ( 5 · 𝐴 ) ) )
3 cos5t ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( 5 · 𝐴 ) ) = ( ( ( 1 6 · ( ( cos ‘ 𝐴 ) ↑ 5 ) ) − ( 2 0 · ( ( cos ‘ 𝐴 ) ↑ 3 ) ) ) + ( 5 · ( cos ‘ 𝐴 ) ) ) )
4 3 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 = ( 5 · 𝐴 ) ∧ 𝐶 = ( cos ‘ 𝐴 ) ) → ( cos ‘ ( 5 · 𝐴 ) ) = ( ( ( 1 6 · ( ( cos ‘ 𝐴 ) ↑ 5 ) ) − ( 2 0 · ( ( cos ‘ 𝐴 ) ↑ 3 ) ) ) + ( 5 · ( cos ‘ 𝐴 ) ) ) )
5 eqcom ⊢ ( 𝐶 = ( cos ‘ 𝐴 ) ↔ ( cos ‘ 𝐴 ) = 𝐶 )
6 5 biimpi ⊢ ( 𝐶 = ( cos ‘ 𝐴 ) → ( cos ‘ 𝐴 ) = 𝐶 )
7 6 oveq1d ⊢ ( 𝐶 = ( cos ‘ 𝐴 ) → ( ( cos ‘ 𝐴 ) ↑ 5 ) = ( 𝐶 ↑ 5 ) )
8 7 oveq2d ⊢ ( 𝐶 = ( cos ‘ 𝐴 ) → ( 1 6 · ( ( cos ‘ 𝐴 ) ↑ 5 ) ) = ( 1 6 · ( 𝐶 ↑ 5 ) ) )
9 6 oveq1d ⊢ ( 𝐶 = ( cos ‘ 𝐴 ) → ( ( cos ‘ 𝐴 ) ↑ 3 ) = ( 𝐶 ↑ 3 ) )
10 9 oveq2d ⊢ ( 𝐶 = ( cos ‘ 𝐴 ) → ( 2 0 · ( ( cos ‘ 𝐴 ) ↑ 3 ) ) = ( 2 0 · ( 𝐶 ↑ 3 ) ) )
11 8 10 oveq12d ⊢ ( 𝐶 = ( cos ‘ 𝐴 ) → ( ( 1 6 · ( ( cos ‘ 𝐴 ) ↑ 5 ) ) − ( 2 0 · ( ( cos ‘ 𝐴 ) ↑ 3 ) ) ) = ( ( 1 6 · ( 𝐶 ↑ 5 ) ) − ( 2 0 · ( 𝐶 ↑ 3 ) ) ) )
12 6 oveq2d ⊢ ( 𝐶 = ( cos ‘ 𝐴 ) → ( 5 · ( cos ‘ 𝐴 ) ) = ( 5 · 𝐶 ) )
13 11 12 oveq12d ⊢ ( 𝐶 = ( cos ‘ 𝐴 ) → ( ( ( 1 6 · ( ( cos ‘ 𝐴 ) ↑ 5 ) ) − ( 2 0 · ( ( cos ‘ 𝐴 ) ↑ 3 ) ) ) + ( 5 · ( cos ‘ 𝐴 ) ) ) = ( ( ( 1 6 · ( 𝐶 ↑ 5 ) ) − ( 2 0 · ( 𝐶 ↑ 3 ) ) ) + ( 5 · 𝐶 ) ) )
14 13 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 = ( 5 · 𝐴 ) ∧ 𝐶 = ( cos ‘ 𝐴 ) ) → ( ( ( 1 6 · ( ( cos ‘ 𝐴 ) ↑ 5 ) ) − ( 2 0 · ( ( cos ‘ 𝐴 ) ↑ 3 ) ) ) + ( 5 · ( cos ‘ 𝐴 ) ) ) = ( ( ( 1 6 · ( 𝐶 ↑ 5 ) ) − ( 2 0 · ( 𝐶 ↑ 3 ) ) ) + ( 5 · 𝐶 ) ) )
15 2 4 14 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 = ( 5 · 𝐴 ) ∧ 𝐶 = ( cos ‘ 𝐴 ) ) → ( cos ‘ 𝐵 ) = ( ( ( 1 6 · ( 𝐶 ↑ 5 ) ) − ( 2 0 · ( 𝐶 ↑ 3 ) ) ) + ( 5 · 𝐶 ) ) )