Metamath Proof Explorer

Theorem sin5tlem2

Description: Lemma 2 for quintupled angle sine calculation, multiplicating triple angle cosine by cosine straight and converting into sine. (Contributed by Ender Ting, 16-Apr-2026)

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

Proof

Step Hyp Ref Expression
1 4cn ⊢ 4 ∈ ℂ
2 1 a1i ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → 4 ∈ ℂ )
3 simp1 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → 𝑁 ∈ ℂ )
4 3nn0 ⊢ 3 ∈ ℕ0
5 4 a1i ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → 3 ∈ ℕ0 )
6 3 5 expcld ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 𝑁 ↑ 3 ) ∈ ℂ )
7 2 6 mulcld ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 4 · ( 𝑁 ↑ 3 ) ) ∈ ℂ )
8 3cn ⊢ 3 ∈ ℂ
9 8 a1i ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → 3 ∈ ℂ )
10 9 3 mulcld ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 3 · 𝑁 ) ∈ ℂ )
11 7 10 3 subdird ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( ( 4 · ( 𝑁 ↑ 3 ) ) − ( 3 · 𝑁 ) ) · 𝑁 ) = ( ( ( 4 · ( 𝑁 ↑ 3 ) ) · 𝑁 ) − ( ( 3 · 𝑁 ) · 𝑁 ) ) )
12 2 6 3 mulassd ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( 4 · ( 𝑁 ↑ 3 ) ) · 𝑁 ) = ( 4 · ( ( 𝑁 ↑ 3 ) · 𝑁 ) ) )
13 2t2e4 ⊢ ( 2 · 2 ) = 4
14 df-4 ⊢ 4 = ( 3 + 1 )
15 13 14 eqtri ⊢ ( 2 · 2 ) = ( 3 + 1 )
16 15 a1i ⊢ ( 𝑁 ∈ ℂ → ( 2 · 2 ) = ( 3 + 1 ) )
17 16 oveq2d ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 ↑ ( 2 · 2 ) ) = ( 𝑁 ↑ ( 3 + 1 ) ) )
18 id ⊢ ( 𝑁 ∈ ℂ → 𝑁 ∈ ℂ )
19 2nn0 ⊢ 2 ∈ ℕ0
20 19 a1i ⊢ ( 𝑁 ∈ ℂ → 2 ∈ ℕ0 )
21 18 20 20 expmuld ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 ↑ ( 2 · 2 ) ) = ( ( 𝑁 ↑ 2 ) ↑ 2 ) )
22 4 a1i ⊢ ( 𝑁 ∈ ℂ → 3 ∈ ℕ0 )
23 18 22 expp1d ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 ↑ ( 3 + 1 ) ) = ( ( 𝑁 ↑ 3 ) · 𝑁 ) )
24 17 21 23 3eqtr3rd ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 ↑ 3 ) · 𝑁 ) = ( ( 𝑁 ↑ 2 ) ↑ 2 ) )
25 24 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( 𝑁 ↑ 3 ) · 𝑁 ) = ( ( 𝑁 ↑ 2 ) ↑ 2 ) )
26 25 oveq2d ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 4 · ( ( 𝑁 ↑ 3 ) · 𝑁 ) ) = ( 4 · ( ( 𝑁 ↑ 2 ) ↑ 2 ) ) )
27 oveq1 ⊢ ( ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) → ( ( 𝑁 ↑ 2 ) ↑ 2 ) = ( ( 1 − ( 𝑀 ↑ 2 ) ) ↑ 2 ) )
28 27 oveq2d ⊢ ( ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) → ( 4 · ( ( 𝑁 ↑ 2 ) ↑ 2 ) ) = ( 4 · ( ( 1 − ( 𝑀 ↑ 2 ) ) ↑ 2 ) ) )
29 28 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 4 · ( ( 𝑁 ↑ 2 ) ↑ 2 ) ) = ( 4 · ( ( 1 − ( 𝑀 ↑ 2 ) ) ↑ 2 ) ) )
30 12 26 29 3eqtrd ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( 4 · ( 𝑁 ↑ 3 ) ) · 𝑁 ) = ( 4 · ( ( 1 − ( 𝑀 ↑ 2 ) ) ↑ 2 ) ) )
31 1cnd ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → 1 ∈ ℂ )
32 simp2 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → 𝑀 ∈ ℂ )
33 19 a1i ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → 2 ∈ ℕ0 )
34 32 33 expcld ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 𝑀 ↑ 2 ) ∈ ℂ )
35 binom2sub ⊢ ( ( 1 ∈ ℂ ∧ ( 𝑀 ↑ 2 ) ∈ ℂ ) → ( ( 1 − ( 𝑀 ↑ 2 ) ) ↑ 2 ) = ( ( ( 1 ↑ 2 ) − ( 2 · ( 1 · ( 𝑀 ↑ 2 ) ) ) ) + ( ( 𝑀 ↑ 2 ) ↑ 2 ) ) )
36 31 34 35 syl2anc ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( 1 − ( 𝑀 ↑ 2 ) ) ↑ 2 ) = ( ( ( 1 ↑ 2 ) − ( 2 · ( 1 · ( 𝑀 ↑ 2 ) ) ) ) + ( ( 𝑀 ↑ 2 ) ↑ 2 ) ) )
37 sq1 ⊢ ( 1 ↑ 2 ) = 1
38 37 a1i ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 1 ↑ 2 ) = 1 )
39 34 mullidd ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 1 · ( 𝑀 ↑ 2 ) ) = ( 𝑀 ↑ 2 ) )
40 39 oveq2d ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 2 · ( 1 · ( 𝑀 ↑ 2 ) ) ) = ( 2 · ( 𝑀 ↑ 2 ) ) )
41 38 40 oveq12d ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( 1 ↑ 2 ) − ( 2 · ( 1 · ( 𝑀 ↑ 2 ) ) ) ) = ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) )
42 13 eqcomi ⊢ 4 = ( 2 · 2 )
43 42 a1i ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → 4 = ( 2 · 2 ) )
44 43 oveq2d ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 𝑀 ↑ 4 ) = ( 𝑀 ↑ ( 2 · 2 ) ) )
45 32 33 33 expmuld ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 𝑀 ↑ ( 2 · 2 ) ) = ( ( 𝑀 ↑ 2 ) ↑ 2 ) )
46 44 45 eqtr2d ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( 𝑀 ↑ 2 ) ↑ 2 ) = ( 𝑀 ↑ 4 ) )
47 41 46 oveq12d ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( ( 1 ↑ 2 ) − ( 2 · ( 1 · ( 𝑀 ↑ 2 ) ) ) ) + ( ( 𝑀 ↑ 2 ) ↑ 2 ) ) = ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) )
48 36 47 eqtrd ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( 1 − ( 𝑀 ↑ 2 ) ) ↑ 2 ) = ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) )
49 48 oveq2d ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 4 · ( ( 1 − ( 𝑀 ↑ 2 ) ) ↑ 2 ) ) = ( 4 · ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) ) )
50 30 49 eqtrd ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( 4 · ( 𝑁 ↑ 3 ) ) · 𝑁 ) = ( 4 · ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) ) )
51 9 3 3 mulassd ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( 3 · 𝑁 ) · 𝑁 ) = ( 3 · ( 𝑁 · 𝑁 ) ) )
52 sqval ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 ↑ 2 ) = ( 𝑁 · 𝑁 ) )
53 52 eqcomd ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 · 𝑁 ) = ( 𝑁 ↑ 2 ) )
54 53 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 𝑁 · 𝑁 ) = ( 𝑁 ↑ 2 ) )
55 54 oveq2d ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 3 · ( 𝑁 · 𝑁 ) ) = ( 3 · ( 𝑁 ↑ 2 ) ) )
56 oveq2 ⊢ ( ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) → ( 3 · ( 𝑁 ↑ 2 ) ) = ( 3 · ( 1 − ( 𝑀 ↑ 2 ) ) ) )
57 56 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( 3 · ( 𝑁 ↑ 2 ) ) = ( 3 · ( 1 − ( 𝑀 ↑ 2 ) ) ) )
58 51 55 57 3eqtrd ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( 3 · 𝑁 ) · 𝑁 ) = ( 3 · ( 1 − ( 𝑀 ↑ 2 ) ) ) )
59 50 58 oveq12d ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( ( 4 · ( 𝑁 ↑ 3 ) ) · 𝑁 ) − ( ( 3 · 𝑁 ) · 𝑁 ) ) = ( ( 4 · ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) ) − ( 3 · ( 1 − ( 𝑀 ↑ 2 ) ) ) ) )
60 11 59 eqtrd ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( ( 4 · ( 𝑁 ↑ 3 ) ) − ( 3 · 𝑁 ) ) · 𝑁 ) = ( ( 4 · ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) ) − ( 3 · ( 1 − ( 𝑀 ↑ 2 ) ) ) ) )