cos3t - Mathbox for Ender Ting

	Mathbox for Ender Ting		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cos3t		Structured version Visualization version GIF version

Theorem cos3t 47419

Description: Triple-angle formula for cosine, in pure cosine form. (Contributed by Ender Ting, 16-Mar-2026.)

**Assertion**
Ref	Expression
cos3t	⊢ (𝐴 ∈ ℂ → (cos‘(3 · 𝐴)) = ((4 · ((cos‘𝐴)↑3)) − (3 · (cos‘𝐴))))

**Proof of Theorem cos3t**
Step	Hyp	Ref	Expression
1		df-3 12276	. . . . 5 ⊢ 3 = (2 + 1)
2	1	oveq1i 7400	. . . 4 ⊢ (3 · 𝐴) = ((2 + 1) · 𝐴)
3		2cnd 12291	. . . . 5 ⊢ (𝐴 ∈ ℂ → 2 ∈ ℂ)
4		1cnd 11170	. . . . 5 ⊢ (𝐴 ∈ ℂ → 1 ∈ ℂ)
5		id 22	. . . . 5 ⊢ (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
6	3, 4, 5	adddird 11202	. . . 4 ⊢ (𝐴 ∈ ℂ → ((2 + 1) · 𝐴) = ((2 · 𝐴) + (1 · 𝐴)))
7	2, 6	eqtrid 2808	. . 3 ⊢ (𝐴 ∈ ℂ → (3 · 𝐴) = ((2 · 𝐴) + (1 · 𝐴)))
8	7	fveq2d 6865	. 2 ⊢ (𝐴 ∈ ℂ → (cos‘(3 · 𝐴)) = (cos‘((2 · 𝐴) + (1 · 𝐴))))
9	3, 5	mulcld 11197	. . 3 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) ∈ ℂ)
10	4, 5	mulcld 11197	. . 3 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) ∈ ℂ)
11		cosadd 16178	. . 3 ⊢ (((2 · 𝐴) ∈ ℂ ∧ (1 · 𝐴) ∈ ℂ) → (cos‘((2 · 𝐴) + (1 · 𝐴))) = (((cos‘(2 · 𝐴)) · (cos‘(1 · 𝐴))) − ((sin‘(2 · 𝐴)) · (sin‘(1 · 𝐴)))))
12	9, 10, 11	syl2anc 593	. 2 ⊢ (𝐴 ∈ ℂ → (cos‘((2 · 𝐴) + (1 · 𝐴))) = (((cos‘(2 · 𝐴)) · (cos‘(1 · 𝐴))) − ((sin‘(2 · 𝐴)) · (sin‘(1 · 𝐴)))))
13		cos2t 16191	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (cos‘(2 · 𝐴)) = ((2 · ((cos‘𝐴)↑2)) − 1))
14		mullid 11175	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
15	14	fveq2d 6865	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (cos‘(1 · 𝐴)) = (cos‘𝐴))
16	13, 15	oveq12d 7408	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((cos‘(2 · 𝐴)) · (cos‘(1 · 𝐴))) = (((2 · ((cos‘𝐴)↑2)) − 1) · (cos‘𝐴)))
17		coscl 16140	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (cos‘𝐴) ∈ ℂ)
18	17	sqcld 14152	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((cos‘𝐴)↑2) ∈ ℂ)
19	3, 18	mulcld 11197	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (2 · ((cos‘𝐴)↑2)) ∈ ℂ)
20	19, 4, 17	subdird 11639	. . . . 5 ⊢ (𝐴 ∈ ℂ → (((2 · ((cos‘𝐴)↑2)) − 1) · (cos‘𝐴)) = (((2 · ((cos‘𝐴)↑2)) · (cos‘𝐴)) − (1 · (cos‘𝐴))))
21	3, 18, 17	mulassd 11200	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((2 · ((cos‘𝐴)↑2)) · (cos‘𝐴)) = (2 · (((cos‘𝐴)↑2) · (cos‘𝐴))))
22	1	oveq2i 7401	. . . . . . . . 9 ⊢ ((cos‘𝐴)↑3) = ((cos‘𝐴)↑(2 + 1))
23		2nn0 12493	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
24	23	a1i 11	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → 2 ∈ ℕ₀)
25	17, 24	expp1d 14155	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((cos‘𝐴)↑(2 + 1)) = (((cos‘𝐴)↑2) · (cos‘𝐴)))
26	22, 25	eqtr2id 2809	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((cos‘𝐴)↑2) · (cos‘𝐴)) = ((cos‘𝐴)↑3))
27	26	oveq2d 7406	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (2 · (((cos‘𝐴)↑2) · (cos‘𝐴))) = (2 · ((cos‘𝐴)↑3)))
28	21, 27	eqtrd 2796	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((2 · ((cos‘𝐴)↑2)) · (cos‘𝐴)) = (2 · ((cos‘𝐴)↑3)))
29	28	oveq1d 7405	. . . . 5 ⊢ (𝐴 ∈ ℂ → (((2 · ((cos‘𝐴)↑2)) · (cos‘𝐴)) − (1 · (cos‘𝐴))) = ((2 · ((cos‘𝐴)↑3)) − (1 · (cos‘𝐴))))
30	16, 20, 29	3eqtrd 2800	. . . 4 ⊢ (𝐴 ∈ ℂ → ((cos‘(2 · 𝐴)) · (cos‘(1 · 𝐴))) = ((2 · ((cos‘𝐴)↑3)) − (1 · (cos‘𝐴))))
31		sin2t 16190	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (sin‘(2 · 𝐴)) = (2 · ((sin‘𝐴) · (cos‘𝐴))))
32	14	fveq2d 6865	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (sin‘(1 · 𝐴)) = (sin‘𝐴))
33	31, 32	oveq12d 7408	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((sin‘(2 · 𝐴)) · (sin‘(1 · 𝐴))) = ((2 · ((sin‘𝐴) · (cos‘𝐴))) · (sin‘𝐴)))
34		sincl 16139	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (sin‘𝐴) ∈ ℂ)
35	34, 17	mulcld 11197	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((sin‘𝐴) · (cos‘𝐴)) ∈ ℂ)
36	3, 35, 34	mulassd 11200	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((2 · ((sin‘𝐴) · (cos‘𝐴))) · (sin‘𝐴)) = (2 · (((sin‘𝐴) · (cos‘𝐴)) · (sin‘𝐴))))
37	34, 17, 34	mulassd 11200	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((sin‘𝐴) · (cos‘𝐴)) · (sin‘𝐴)) = ((sin‘𝐴) · ((cos‘𝐴) · (sin‘𝐴))))
38	34, 17, 34	mul12d 11387	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((sin‘𝐴) · ((cos‘𝐴) · (sin‘𝐴))) = ((cos‘𝐴) · ((sin‘𝐴) · (sin‘𝐴))))
39	34	sqvald 14151	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((sin‘𝐴)↑2) = ((sin‘𝐴) · (sin‘𝐴)))
40	39	eqcomd 2767	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((sin‘𝐴) · (sin‘𝐴)) = ((sin‘𝐴)↑2))
41	40	oveq2d 7406	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((cos‘𝐴) · ((sin‘𝐴) · (sin‘𝐴))) = ((cos‘𝐴) · ((sin‘𝐴)↑2)))
42	37, 38, 41	3eqtrd 2800	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (((sin‘𝐴) · (cos‘𝐴)) · (sin‘𝐴)) = ((cos‘𝐴) · ((sin‘𝐴)↑2)))
43	34	sqcld 14152	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((sin‘𝐴)↑2) ∈ ℂ)
44		sincossq 16189	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (((sin‘𝐴)↑2) + ((cos‘𝐴)↑2)) = 1)
45	43, 18, 44	mvlraddd 11592	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((sin‘𝐴)↑2) = (1 − ((cos‘𝐴)↑2)))
46	45	oveq2d 7406	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((cos‘𝐴) · ((sin‘𝐴)↑2)) = ((cos‘𝐴) · (1 − ((cos‘𝐴)↑2))))
47	17, 4, 18	subdid 11638	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → ((cos‘𝐴) · (1 − ((cos‘𝐴)↑2))) = (((cos‘𝐴) · 1) − ((cos‘𝐴) · ((cos‘𝐴)↑2))))
48	17	mulridd 11194	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((cos‘𝐴) · 1) = (cos‘𝐴))
49	1	a1i 11	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → 3 = (2 + 1))
50	49	oveq2d 7406	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ((cos‘𝐴)↑3) = ((cos‘𝐴)↑(2 + 1)))
51	18, 17	mulcomd 11198	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (((cos‘𝐴)↑2) · (cos‘𝐴)) = ((cos‘𝐴) · ((cos‘𝐴)↑2)))
52	50, 25, 51	3eqtrrd 2801	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → ((cos‘𝐴) · ((cos‘𝐴)↑2)) = ((cos‘𝐴)↑3))
53	48, 52	oveq12d 7408	. . . . . . . . 9 ⊢ (𝐴 ∈ ℂ → (((cos‘𝐴) · 1) − ((cos‘𝐴) · ((cos‘𝐴)↑2))) = ((cos‘𝐴) − ((cos‘𝐴)↑3)))
54	47, 53	eqtrd 2796	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → ((cos‘𝐴) · (1 − ((cos‘𝐴)↑2))) = ((cos‘𝐴) − ((cos‘𝐴)↑3)))
55	42, 46, 54	3eqtrd 2800	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((sin‘𝐴) · (cos‘𝐴)) · (sin‘𝐴)) = ((cos‘𝐴) − ((cos‘𝐴)↑3)))
56	55	oveq2d 7406	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (2 · (((sin‘𝐴) · (cos‘𝐴)) · (sin‘𝐴))) = (2 · ((cos‘𝐴) − ((cos‘𝐴)↑3))))
57	36, 56	eqtrd 2796	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((2 · ((sin‘𝐴) · (cos‘𝐴))) · (sin‘𝐴)) = (2 · ((cos‘𝐴) − ((cos‘𝐴)↑3))))
58		3nn0 12494	. . . . . . . 8 ⊢ 3 ∈ ℕ₀
59	58	a1i 11	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → 3 ∈ ℕ₀)
60	17, 59	expcld 14154	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((cos‘𝐴)↑3) ∈ ℂ)
61	3, 17, 60	subdid 11638	. . . . 5 ⊢ (𝐴 ∈ ℂ → (2 · ((cos‘𝐴) − ((cos‘𝐴)↑3))) = ((2 · (cos‘𝐴)) − (2 · ((cos‘𝐴)↑3))))
62	33, 57, 61	3eqtrd 2800	. . . 4 ⊢ (𝐴 ∈ ℂ → ((sin‘(2 · 𝐴)) · (sin‘(1 · 𝐴))) = ((2 · (cos‘𝐴)) − (2 · ((cos‘𝐴)↑3))))
63	30, 62	oveq12d 7408	. . 3 ⊢ (𝐴 ∈ ℂ → (((cos‘(2 · 𝐴)) · (cos‘(1 · 𝐴))) − ((sin‘(2 · 𝐴)) · (sin‘(1 · 𝐴)))) = (((2 · ((cos‘𝐴)↑3)) − (1 · (cos‘𝐴))) − ((2 · (cos‘𝐴)) − (2 · ((cos‘𝐴)↑3)))))
64	3, 60	mulcld 11197	. . . 4 ⊢ (𝐴 ∈ ℂ → (2 · ((cos‘𝐴)↑3)) ∈ ℂ)
65	4, 17	mulcld 11197	. . . 4 ⊢ (𝐴 ∈ ℂ → (1 · (cos‘𝐴)) ∈ ℂ)
66	3, 17	mulcld 11197	. . . 4 ⊢ (𝐴 ∈ ℂ → (2 · (cos‘𝐴)) ∈ ℂ)
67	64, 65, 66, 64	subadd4d 11585	. . 3 ⊢ (𝐴 ∈ ℂ → (((2 · ((cos‘𝐴)↑3)) − (1 · (cos‘𝐴))) − ((2 · (cos‘𝐴)) − (2 · ((cos‘𝐴)↑3)))) = (((2 · ((cos‘𝐴)↑3)) + (2 · ((cos‘𝐴)↑3))) − ((1 · (cos‘𝐴)) + (2 · (cos‘𝐴)))))
68	3, 3, 60	adddird 11202	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((2 + 2) · ((cos‘𝐴)↑3)) = ((2 · ((cos‘𝐴)↑3)) + (2 · ((cos‘𝐴)↑3))))
69		2p2e4 12347	. . . . . . 7 ⊢ (2 + 2) = 4
70	69	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (2 + 2) = 4)
71	70	oveq1d 7405	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((2 + 2) · ((cos‘𝐴)↑3)) = (4 · ((cos‘𝐴)↑3)))
72	68, 71	eqtr3d 2798	. . . 4 ⊢ (𝐴 ∈ ℂ → ((2 · ((cos‘𝐴)↑3)) + (2 · ((cos‘𝐴)↑3))) = (4 · ((cos‘𝐴)↑3)))
73	4, 3, 17	adddird 11202	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((1 + 2) · (cos‘𝐴)) = ((1 · (cos‘𝐴)) + (2 · (cos‘𝐴))))
74		1p2e3 12355	. . . . . . 7 ⊢ (1 + 2) = 3
75	74	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (1 + 2) = 3)
76	75	oveq1d 7405	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((1 + 2) · (cos‘𝐴)) = (3 · (cos‘𝐴)))
77	73, 76	eqtr3d 2798	. . . 4 ⊢ (𝐴 ∈ ℂ → ((1 · (cos‘𝐴)) + (2 · (cos‘𝐴))) = (3 · (cos‘𝐴)))
78	72, 77	oveq12d 7408	. . 3 ⊢ (𝐴 ∈ ℂ → (((2 · ((cos‘𝐴)↑3)) + (2 · ((cos‘𝐴)↑3))) − ((1 · (cos‘𝐴)) + (2 · (cos‘𝐴)))) = ((4 · ((cos‘𝐴)↑3)) − (3 · (cos‘𝐴))))
79	63, 67, 78	3eqtrd 2800	. 2 ⊢ (𝐴 ∈ ℂ → (((cos‘(2 · 𝐴)) · (cos‘(1 · 𝐴))) − ((sin‘(2 · 𝐴)) · (sin‘(1 · 𝐴)))) = ((4 · ((cos‘𝐴)↑3)) − (3 · (cos‘𝐴))))
80	8, 12, 79	3eqtrd 2800	1 ⊢ (𝐴 ∈ ℂ → (cos‘(3 · 𝐴)) = ((4 · ((cos‘𝐴)↑3)) − (3 · (cos‘𝐴))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1559 ∈ wcel 2141 ‘cfv 6515 (class class class)co 7390 ℂcc 11066 1c1 11069 + caddc 11071 · cmul 11073 − cmin 11409 2c2 12267 3c3 12268 4c4 12269 ℕ₀cn0 12476 ↑cexp 14069 sincsin 16074 cosccos 16075

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5321 ax-pr 5389 ax-un 7712 ax-inf2 9591 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-int 4905 df-iun 4950 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5540 df-eprel 5545 df-po 5553 df-so 5554 df-fr 5598 df-se 5599 df-we 5600 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-rn 5656 df-res 5657 df-ima 5658 df-pred 6282 df-ord 6343 df-on 6344 df-lim 6345 df-suc 6346 df-iota 6471 df-fun 6517 df-fn 6518 df-f 6519 df-f1 6520 df-fo 6521 df-f1o 6522 df-fv 6523 df-isom 6524 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7841 df-1st 7964 df-2nd 7965 df-frecs 8255 df-wrecs 8286 df-recs 8335 df-rdg 8374 df-1o 8430 df-er 8671 df-pm 8804 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-sup 9383 df-inf 9384 df-oi 9453 df-card 9892 df-pnf 11213 df-mnf 11214 df-xr 11215 df-ltxr 11216 df-le 11217 df-sub 11411 df-neg 11412 df-div 11840 df-nn 12206 df-2 12275 df-3 12276 df-4 12277 df-n0 12477 df-z 12564 df-uz 12835 df-rp 12989 df-ico 13350 df-fz 13508 df-fzo 13655 df-fl 13797 df-seq 14010 df-exp 14070 df-fac 14282 df-bc 14311 df-hash 14339 df-shft 15075 df-cj 15107 df-re 15108 df-im 15109 df-sqrt 15243 df-abs 15244 df-limsup 15479 df-clim 15496 df-rlim 15497 df-sum 15695 df-ef 16078 df-sin 16080 df-cos 16081

This theorem is referenced by: sin5t 47425

W3C validator