Metamath Proof Explorer

Theorem sin5tlem1

Description: Lemma 1 for quintupled angle sine calculation, expanding triple-angle sine times double-angle cosine. (Contributed by Ender Ting, 16-Mar-2026)

Ref Expression
Assertion sin5tlem1 ( 𝑁 ∈ ℂ → ( ( ( 3 · 𝑁 ) − ( 4 · ( 𝑁 ↑ 3 ) ) ) · ( 1 − ( 2 · ( 𝑁 ↑ 2 ) ) ) ) = ( ( ( 8 · ( 𝑁 ↑ 5 ) ) − ( 1 0 · ( 𝑁 ↑ 3 ) ) ) + ( 3 · 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 3cn ⊢ 3 ∈ ℂ
2 1 a1i ⊢ ( 𝑁 ∈ ℂ → 3 ∈ ℂ )
3 id ⊢ ( 𝑁 ∈ ℂ → 𝑁 ∈ ℂ )
4 2 3 mulcld ⊢ ( 𝑁 ∈ ℂ → ( 3 · 𝑁 ) ∈ ℂ )
5 4cn ⊢ 4 ∈ ℂ
6 5 a1i ⊢ ( 𝑁 ∈ ℂ → 4 ∈ ℂ )
7 3nn0 ⊢ 3 ∈ ℕ0
8 7 a1i ⊢ ( 𝑁 ∈ ℂ → 3 ∈ ℕ0 )
9 3 8 expcld ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 ↑ 3 ) ∈ ℂ )
10 6 9 mulcld ⊢ ( 𝑁 ∈ ℂ → ( 4 · ( 𝑁 ↑ 3 ) ) ∈ ℂ )
11 1cnd ⊢ ( 𝑁 ∈ ℂ → 1 ∈ ℂ )
12 2cnd ⊢ ( 𝑁 ∈ ℂ → 2 ∈ ℂ )
13 sqcl ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 ↑ 2 ) ∈ ℂ )
14 12 13 mulcld ⊢ ( 𝑁 ∈ ℂ → ( 2 · ( 𝑁 ↑ 2 ) ) ∈ ℂ )
15 4 10 11 14 mulsubd ⊢ ( 𝑁 ∈ ℂ → ( ( ( 3 · 𝑁 ) − ( 4 · ( 𝑁 ↑ 3 ) ) ) · ( 1 − ( 2 · ( 𝑁 ↑ 2 ) ) ) ) = ( ( ( ( 3 · 𝑁 ) · 1 ) + ( ( 2 · ( 𝑁 ↑ 2 ) ) · ( 4 · ( 𝑁 ↑ 3 ) ) ) ) − ( ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) + ( 1 · ( 4 · ( 𝑁 ↑ 3 ) ) ) ) ) )
16 4 11 mulcld ⊢ ( 𝑁 ∈ ℂ → ( ( 3 · 𝑁 ) · 1 ) ∈ ℂ )
17 14 10 mulcld ⊢ ( 𝑁 ∈ ℂ → ( ( 2 · ( 𝑁 ↑ 2 ) ) · ( 4 · ( 𝑁 ↑ 3 ) ) ) ∈ ℂ )
18 16 17 addcomd ⊢ ( 𝑁 ∈ ℂ → ( ( ( 3 · 𝑁 ) · 1 ) + ( ( 2 · ( 𝑁 ↑ 2 ) ) · ( 4 · ( 𝑁 ↑ 3 ) ) ) ) = ( ( ( 2 · ( 𝑁 ↑ 2 ) ) · ( 4 · ( 𝑁 ↑ 3 ) ) ) + ( ( 3 · 𝑁 ) · 1 ) ) )
19 18 oveq1d ⊢ ( 𝑁 ∈ ℂ → ( ( ( ( 3 · 𝑁 ) · 1 ) + ( ( 2 · ( 𝑁 ↑ 2 ) ) · ( 4 · ( 𝑁 ↑ 3 ) ) ) ) − ( ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) + ( 1 · ( 4 · ( 𝑁 ↑ 3 ) ) ) ) ) = ( ( ( ( 2 · ( 𝑁 ↑ 2 ) ) · ( 4 · ( 𝑁 ↑ 3 ) ) ) + ( ( 3 · 𝑁 ) · 1 ) ) − ( ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) + ( 1 · ( 4 · ( 𝑁 ↑ 3 ) ) ) ) ) )
20 4 14 mulcld ⊢ ( 𝑁 ∈ ℂ → ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) ∈ ℂ )
21 11 10 mulcld ⊢ ( 𝑁 ∈ ℂ → ( 1 · ( 4 · ( 𝑁 ↑ 3 ) ) ) ∈ ℂ )
22 20 21 addcld ⊢ ( 𝑁 ∈ ℂ → ( ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) + ( 1 · ( 4 · ( 𝑁 ↑ 3 ) ) ) ) ∈ ℂ )
23 17 16 22 addsubd ⊢ ( 𝑁 ∈ ℂ → ( ( ( ( 2 · ( 𝑁 ↑ 2 ) ) · ( 4 · ( 𝑁 ↑ 3 ) ) ) + ( ( 3 · 𝑁 ) · 1 ) ) − ( ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) + ( 1 · ( 4 · ( 𝑁 ↑ 3 ) ) ) ) ) = ( ( ( ( 2 · ( 𝑁 ↑ 2 ) ) · ( 4 · ( 𝑁 ↑ 3 ) ) ) − ( ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) + ( 1 · ( 4 · ( 𝑁 ↑ 3 ) ) ) ) ) + ( ( 3 · 𝑁 ) · 1 ) ) )
24 19 23 eqtrd ⊢ ( 𝑁 ∈ ℂ → ( ( ( ( 3 · 𝑁 ) · 1 ) + ( ( 2 · ( 𝑁 ↑ 2 ) ) · ( 4 · ( 𝑁 ↑ 3 ) ) ) ) − ( ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) + ( 1 · ( 4 · ( 𝑁 ↑ 3 ) ) ) ) ) = ( ( ( ( 2 · ( 𝑁 ↑ 2 ) ) · ( 4 · ( 𝑁 ↑ 3 ) ) ) − ( ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) + ( 1 · ( 4 · ( 𝑁 ↑ 3 ) ) ) ) ) + ( ( 3 · 𝑁 ) · 1 ) ) )
25 12 13 6 9 mul4d ⊢ ( 𝑁 ∈ ℂ → ( ( 2 · ( 𝑁 ↑ 2 ) ) · ( 4 · ( 𝑁 ↑ 3 ) ) ) = ( ( 2 · 4 ) · ( ( 𝑁 ↑ 2 ) · ( 𝑁 ↑ 3 ) ) ) )
26 2t4e8 ⊢ ( 2 · 4 ) = 8
27 26 a1i ⊢ ( 𝑁 ∈ ℂ → ( 2 · 4 ) = 8 )
28 2nn0 ⊢ 2 ∈ ℕ0
29 28 a1i ⊢ ( 𝑁 ∈ ℂ → 2 ∈ ℕ0 )
30 3 8 29 expaddd ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 ↑ ( 2 + 3 ) ) = ( ( 𝑁 ↑ 2 ) · ( 𝑁 ↑ 3 ) ) )
31 2cn ⊢ 2 ∈ ℂ
32 3p2e5 ⊢ ( 3 + 2 ) = 5
33 1 31 32 addcomli ⊢ ( 2 + 3 ) = 5
34 33 oveq2i ⊢ ( 𝑁 ↑ ( 2 + 3 ) ) = ( 𝑁 ↑ 5 )
35 30 34 eqtr3di ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 ↑ 2 ) · ( 𝑁 ↑ 3 ) ) = ( 𝑁 ↑ 5 ) )
36 27 35 oveq12d ⊢ ( 𝑁 ∈ ℂ → ( ( 2 · 4 ) · ( ( 𝑁 ↑ 2 ) · ( 𝑁 ↑ 3 ) ) ) = ( 8 · ( 𝑁 ↑ 5 ) ) )
37 25 36 eqtrd ⊢ ( 𝑁 ∈ ℂ → ( ( 2 · ( 𝑁 ↑ 2 ) ) · ( 4 · ( 𝑁 ↑ 3 ) ) ) = ( 8 · ( 𝑁 ↑ 5 ) ) )
38 2 3 12 13 mul4d ⊢ ( 𝑁 ∈ ℂ → ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) = ( ( 3 · 2 ) · ( 𝑁 · ( 𝑁 ↑ 2 ) ) ) )
39 3t2e6 ⊢ ( 3 · 2 ) = 6
40 39 a1i ⊢ ( 𝑁 ∈ ℂ → ( 3 · 2 ) = 6 )
41 df-3 ⊢ 3 = ( 2 + 1 )
42 41 oveq2i ⊢ ( 𝑁 ↑ 3 ) = ( 𝑁 ↑ ( 2 + 1 ) )
43 3 29 expp1d ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 ↑ ( 2 + 1 ) ) = ( ( 𝑁 ↑ 2 ) · 𝑁 ) )
44 13 3 mulcomd ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 ↑ 2 ) · 𝑁 ) = ( 𝑁 · ( 𝑁 ↑ 2 ) ) )
45 43 44 eqtrd ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 ↑ ( 2 + 1 ) ) = ( 𝑁 · ( 𝑁 ↑ 2 ) ) )
46 42 45 eqtr2id ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 · ( 𝑁 ↑ 2 ) ) = ( 𝑁 ↑ 3 ) )
47 40 46 oveq12d ⊢ ( 𝑁 ∈ ℂ → ( ( 3 · 2 ) · ( 𝑁 · ( 𝑁 ↑ 2 ) ) ) = ( 6 · ( 𝑁 ↑ 3 ) ) )
48 38 47 eqtrd ⊢ ( 𝑁 ∈ ℂ → ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) = ( 6 · ( 𝑁 ↑ 3 ) ) )
49 10 mullidd ⊢ ( 𝑁 ∈ ℂ → ( 1 · ( 4 · ( 𝑁 ↑ 3 ) ) ) = ( 4 · ( 𝑁 ↑ 3 ) ) )
50 48 49 oveq12d ⊢ ( 𝑁 ∈ ℂ → ( ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) + ( 1 · ( 4 · ( 𝑁 ↑ 3 ) ) ) ) = ( ( 6 · ( 𝑁 ↑ 3 ) ) + ( 4 · ( 𝑁 ↑ 3 ) ) ) )
51 6cn ⊢ 6 ∈ ℂ
52 51 a1i ⊢ ( 𝑁 ∈ ℂ → 6 ∈ ℂ )
53 52 6 9 adddird ⊢ ( 𝑁 ∈ ℂ → ( ( 6 + 4 ) · ( 𝑁 ↑ 3 ) ) = ( ( 6 · ( 𝑁 ↑ 3 ) ) + ( 4 · ( 𝑁 ↑ 3 ) ) ) )
54 6p4e10 ⊢ ( 6 + 4 ) = 1 0
55 54 a1i ⊢ ( 𝑁 ∈ ℂ → ( 6 + 4 ) = 1 0 )
56 55 oveq1d ⊢ ( 𝑁 ∈ ℂ → ( ( 6 + 4 ) · ( 𝑁 ↑ 3 ) ) = ( 1 0 · ( 𝑁 ↑ 3 ) ) )
57 50 53 56 3eqtr2d ⊢ ( 𝑁 ∈ ℂ → ( ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) + ( 1 · ( 4 · ( 𝑁 ↑ 3 ) ) ) ) = ( 1 0 · ( 𝑁 ↑ 3 ) ) )
58 37 57 oveq12d ⊢ ( 𝑁 ∈ ℂ → ( ( ( 2 · ( 𝑁 ↑ 2 ) ) · ( 4 · ( 𝑁 ↑ 3 ) ) ) − ( ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) + ( 1 · ( 4 · ( 𝑁 ↑ 3 ) ) ) ) ) = ( ( 8 · ( 𝑁 ↑ 5 ) ) − ( 1 0 · ( 𝑁 ↑ 3 ) ) ) )
59 4 mulridd ⊢ ( 𝑁 ∈ ℂ → ( ( 3 · 𝑁 ) · 1 ) = ( 3 · 𝑁 ) )
60 58 59 oveq12d ⊢ ( 𝑁 ∈ ℂ → ( ( ( ( 2 · ( 𝑁 ↑ 2 ) ) · ( 4 · ( 𝑁 ↑ 3 ) ) ) − ( ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) + ( 1 · ( 4 · ( 𝑁 ↑ 3 ) ) ) ) ) + ( ( 3 · 𝑁 ) · 1 ) ) = ( ( ( 8 · ( 𝑁 ↑ 5 ) ) − ( 1 0 · ( 𝑁 ↑ 3 ) ) ) + ( 3 · 𝑁 ) ) )
61 15 24 60 3eqtrd ⊢ ( 𝑁 ∈ ℂ → ( ( ( 3 · 𝑁 ) − ( 4 · ( 𝑁 ↑ 3 ) ) ) · ( 1 − ( 2 · ( 𝑁 ↑ 2 ) ) ) ) = ( ( ( 8 · ( 𝑁 ↑ 5 ) ) − ( 1 0 · ( 𝑁 ↑ 3 ) ) ) + ( 3 · 𝑁 ) ) )