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 5 2timesi ⊢ ( 2 · 4 ) = ( 4 + 4 )
27 4p4e8 ⊢ ( 4 + 4 ) = 8
28 26 27 eqtri ⊢ ( 2 · 4 ) = 8
29 28 a1i ⊢ ( 𝑁 ∈ ℂ → ( 2 · 4 ) = 8 )
30 2nn0 ⊢ 2 ∈ ℕ0
31 30 a1i ⊢ ( 𝑁 ∈ ℂ → 2 ∈ ℕ0 )
32 3 8 31 expaddd ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 ↑ ( 2 + 3 ) ) = ( ( 𝑁 ↑ 2 ) · ( 𝑁 ↑ 3 ) ) )
33 2cn ⊢ 2 ∈ ℂ
34 3p2e5 ⊢ ( 3 + 2 ) = 5
35 1 33 34 addcomli ⊢ ( 2 + 3 ) = 5
36 35 oveq2i ⊢ ( 𝑁 ↑ ( 2 + 3 ) ) = ( 𝑁 ↑ 5 )
37 32 36 eqtr3di ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 ↑ 2 ) · ( 𝑁 ↑ 3 ) ) = ( 𝑁 ↑ 5 ) )
38 29 37 oveq12d ⊢ ( 𝑁 ∈ ℂ → ( ( 2 · 4 ) · ( ( 𝑁 ↑ 2 ) · ( 𝑁 ↑ 3 ) ) ) = ( 8 · ( 𝑁 ↑ 5 ) ) )
39 25 38 eqtrd ⊢ ( 𝑁 ∈ ℂ → ( ( 2 · ( 𝑁 ↑ 2 ) ) · ( 4 · ( 𝑁 ↑ 3 ) ) ) = ( 8 · ( 𝑁 ↑ 5 ) ) )
40 2 3 12 13 mul4d ⊢ ( 𝑁 ∈ ℂ → ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) = ( ( 3 · 2 ) · ( 𝑁 · ( 𝑁 ↑ 2 ) ) ) )
41 3t2e6 ⊢ ( 3 · 2 ) = 6
42 41 a1i ⊢ ( 𝑁 ∈ ℂ → ( 3 · 2 ) = 6 )
43 df-3 ⊢ 3 = ( 2 + 1 )
44 43 oveq2i ⊢ ( 𝑁 ↑ 3 ) = ( 𝑁 ↑ ( 2 + 1 ) )
45 3 31 expp1d ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 ↑ ( 2 + 1 ) ) = ( ( 𝑁 ↑ 2 ) · 𝑁 ) )
46 13 3 mulcomd ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 ↑ 2 ) · 𝑁 ) = ( 𝑁 · ( 𝑁 ↑ 2 ) ) )
47 45 46 eqtrd ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 ↑ ( 2 + 1 ) ) = ( 𝑁 · ( 𝑁 ↑ 2 ) ) )
48 44 47 eqtr2id ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 · ( 𝑁 ↑ 2 ) ) = ( 𝑁 ↑ 3 ) )
49 42 48 oveq12d ⊢ ( 𝑁 ∈ ℂ → ( ( 3 · 2 ) · ( 𝑁 · ( 𝑁 ↑ 2 ) ) ) = ( 6 · ( 𝑁 ↑ 3 ) ) )
50 40 49 eqtrd ⊢ ( 𝑁 ∈ ℂ → ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) = ( 6 · ( 𝑁 ↑ 3 ) ) )
51 10 mullidd ⊢ ( 𝑁 ∈ ℂ → ( 1 · ( 4 · ( 𝑁 ↑ 3 ) ) ) = ( 4 · ( 𝑁 ↑ 3 ) ) )
52 50 51 oveq12d ⊢ ( 𝑁 ∈ ℂ → ( ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) + ( 1 · ( 4 · ( 𝑁 ↑ 3 ) ) ) ) = ( ( 6 · ( 𝑁 ↑ 3 ) ) + ( 4 · ( 𝑁 ↑ 3 ) ) ) )
53 6cn ⊢ 6 ∈ ℂ
54 53 a1i ⊢ ( 𝑁 ∈ ℂ → 6 ∈ ℂ )
55 54 6 9 adddird ⊢ ( 𝑁 ∈ ℂ → ( ( 6 + 4 ) · ( 𝑁 ↑ 3 ) ) = ( ( 6 · ( 𝑁 ↑ 3 ) ) + ( 4 · ( 𝑁 ↑ 3 ) ) ) )
56 6p4e10 ⊢ ( 6 + 4 ) = 1 0
57 56 a1i ⊢ ( 𝑁 ∈ ℂ → ( 6 + 4 ) = 1 0 )
58 57 oveq1d ⊢ ( 𝑁 ∈ ℂ → ( ( 6 + 4 ) · ( 𝑁 ↑ 3 ) ) = ( 1 0 · ( 𝑁 ↑ 3 ) ) )
59 52 55 58 3eqtr2d ⊢ ( 𝑁 ∈ ℂ → ( ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) + ( 1 · ( 4 · ( 𝑁 ↑ 3 ) ) ) ) = ( 1 0 · ( 𝑁 ↑ 3 ) ) )
60 39 59 oveq12d ⊢ ( 𝑁 ∈ ℂ → ( ( ( 2 · ( 𝑁 ↑ 2 ) ) · ( 4 · ( 𝑁 ↑ 3 ) ) ) − ( ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) + ( 1 · ( 4 · ( 𝑁 ↑ 3 ) ) ) ) ) = ( ( 8 · ( 𝑁 ↑ 5 ) ) − ( 1 0 · ( 𝑁 ↑ 3 ) ) ) )
61 4 mulridd ⊢ ( 𝑁 ∈ ℂ → ( ( 3 · 𝑁 ) · 1 ) = ( 3 · 𝑁 ) )
62 60 61 oveq12d ⊢ ( 𝑁 ∈ ℂ → ( ( ( ( 2 · ( 𝑁 ↑ 2 ) ) · ( 4 · ( 𝑁 ↑ 3 ) ) ) − ( ( ( 3 · 𝑁 ) · ( 2 · ( 𝑁 ↑ 2 ) ) ) + ( 1 · ( 4 · ( 𝑁 ↑ 3 ) ) ) ) ) + ( ( 3 · 𝑁 ) · 1 ) ) = ( ( ( 8 · ( 𝑁 ↑ 5 ) ) − ( 1 0 · ( 𝑁 ↑ 3 ) ) ) + ( 3 · 𝑁 ) ) )
63 15 24 62 3eqtrd ⊢ ( 𝑁 ∈ ℂ → ( ( ( 3 · 𝑁 ) − ( 4 · ( 𝑁 ↑ 3 ) ) ) · ( 1 − ( 2 · ( 𝑁 ↑ 2 ) ) ) ) = ( ( ( 8 · ( 𝑁 ↑ 5 ) ) − ( 1 0 · ( 𝑁 ↑ 3 ) ) ) + ( 3 · 𝑁 ) ) )