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 ⊢ N ∈ ℂ ∧ M ∈ ℂ ∧ N 2 = 1 − M 2 → 4 ⁢ N 3 − 3 ⋅ N ⁢ 2 ⁢ M ⋅ N = 4 ⁢ 1 - 2 ⁢ M 2 + M 4 − 3 ⁢ 1 − M 2 ⁢ 2 ⋅ M

Proof

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