Metamath Proof Explorer

Theorem sin5tlem3

Description: Lemma 3 for quintupled angle sine calculation, multiplicating triple angle cosine by double angle sine. (Contributed by Ender Ting, 16-Apr-2026)

Ref Expression
Assertion sin5tlem3 ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( ( 4 · ( 𝑁 ↑ 3 ) ) − ( 3 · 𝑁 ) ) · ( 2 · ( 𝑀 · 𝑁 ) ) ) = ( ( ( 4 · ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) ) − ( 3 · ( 1 − ( 𝑀 ↑ 2 ) ) ) ) · ( 2 · 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → 𝑀 ∈ ℂ )
2 simp1 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → 𝑁 ∈ ℂ )
3 1 2 mulcomd ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 𝑀 · 𝑁 ) = ( 𝑁 · 𝑀 ) )
4 3 oveq2d ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 2 · ( 𝑀 · 𝑁 ) ) = ( 2 · ( 𝑁 · 𝑀 ) ) )
5 2cnd ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → 2 ∈ ℂ )
6 5 2 1 mul12d ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 2 · ( 𝑁 · 𝑀 ) ) = ( 𝑁 · ( 2 · 𝑀 ) ) )
7 4 6 eqtrd ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 2 · ( 𝑀 · 𝑁 ) ) = ( 𝑁 · ( 2 · 𝑀 ) ) )
8 7 oveq2d ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( ( 4 · ( 𝑁 ↑ 3 ) ) − ( 3 · 𝑁 ) ) · ( 2 · ( 𝑀 · 𝑁 ) ) ) = ( ( ( 4 · ( 𝑁 ↑ 3 ) ) − ( 3 · 𝑁 ) ) · ( 𝑁 · ( 2 · 𝑀 ) ) ) )
9 4cn ⊢ 4 ∈ ℂ
10 9 a1i ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → 4 ∈ ℂ )
11 3nn0 ⊢ 3 ∈ ℕ0
12 11 a1i ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → 3 ∈ ℕ0 )
13 2 12 expcld ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 𝑁 ↑ 3 ) ∈ ℂ )
14 10 13 mulcld ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 4 · ( 𝑁 ↑ 3 ) ) ∈ ℂ )
15 3cn ⊢ 3 ∈ ℂ
16 15 a1i ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → 3 ∈ ℂ )
17 16 2 mulcld ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 3 · 𝑁 ) ∈ ℂ )
18 14 17 subcld ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( 4 · ( 𝑁 ↑ 3 ) ) − ( 3 · 𝑁 ) ) ∈ ℂ )
19 5 1 mulcld ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 2 · 𝑀 ) ∈ ℂ )
20 18 2 19 mulassd ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( ( ( 4 · ( 𝑁 ↑ 3 ) ) − ( 3 · 𝑁 ) ) · 𝑁 ) · ( 2 · 𝑀 ) ) = ( ( ( 4 · ( 𝑁 ↑ 3 ) ) − ( 3 · 𝑁 ) ) · ( 𝑁 · ( 2 · 𝑀 ) ) ) )
21 sin5tlem2 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( ( 4 · ( 𝑁 ↑ 3 ) ) − ( 3 · 𝑁 ) ) · 𝑁 ) = ( ( 4 · ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) ) − ( 3 · ( 1 − ( 𝑀 ↑ 2 ) ) ) ) )
22 21 oveq1d ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( ( ( 4 · ( 𝑁 ↑ 3 ) ) − ( 3 · 𝑁 ) ) · 𝑁 ) · ( 2 · 𝑀 ) ) = ( ( ( 4 · ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) ) − ( 3 · ( 1 − ( 𝑀 ↑ 2 ) ) ) ) · ( 2 · 𝑀 ) ) )
23 8 20 22 3eqtr2d ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( ( 4 · ( 𝑁 ↑ 3 ) ) − ( 3 · 𝑁 ) ) · ( 2 · ( 𝑀 · 𝑁 ) ) ) = ( ( ( 4 · ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) ) − ( 3 · ( 1 − ( 𝑀 ↑ 2 ) ) ) ) · ( 2 · 𝑀 ) ) )