Theorem cos2h

Description: Half-angle rule for cosine. (Contributed by Brendan Leahy, 4-Aug-2018)

	Ref	Expression
Assertion	cos2h	⊢ ( 𝐴 ∈ ( - π [,] π ) → ( cos ‘ ( 𝐴 / 2 ) ) = ( √ ‘ ( ( 1 + ( cos ‘ 𝐴 ) ) / 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pire	⊢ π ∈ ℝ
2	1	renegcli	⊢ - π ∈ ℝ
3		iccssre	⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ) → ( - π [,] π ) ⊆ ℝ )
4	2 1 3	mp2an	⊢ ( - π [,] π ) ⊆ ℝ
5	4	sseli	⊢ ( 𝐴 ∈ ( - π [,] π ) → 𝐴 ∈ ℝ )
6	5	rehalfcld	⊢ ( 𝐴 ∈ ( - π [,] π ) → ( 𝐴 / 2 ) ∈ ℝ )
7	6	recoscld	⊢ ( 𝐴 ∈ ( - π [,] π ) → ( cos ‘ ( 𝐴 / 2 ) ) ∈ ℝ )
8		1re	⊢ 1 ∈ ℝ
9	5	recoscld	⊢ ( 𝐴 ∈ ( - π [,] π ) → ( cos ‘ 𝐴 ) ∈ ℝ )
10		readdcl	⊢ ( ( 1 ∈ ℝ ∧ ( cos ‘ 𝐴 ) ∈ ℝ ) → ( 1 + ( cos ‘ 𝐴 ) ) ∈ ℝ )
11	8 9 10	sylancr	⊢ ( 𝐴 ∈ ( - π [,] π ) → ( 1 + ( cos ‘ 𝐴 ) ) ∈ ℝ )
12	11	rehalfcld	⊢ ( 𝐴 ∈ ( - π [,] π ) → ( ( 1 + ( cos ‘ 𝐴 ) ) / 2 ) ∈ ℝ )
13		cosbnd	⊢ ( 𝐴 ∈ ℝ → ( - 1 ≤ ( cos ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) ≤ 1 ) )
14	13	simpld	⊢ ( 𝐴 ∈ ℝ → - 1 ≤ ( cos ‘ 𝐴 ) )
15		recoscl	⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) ∈ ℝ )
16		recn	⊢ ( ( cos ‘ 𝐴 ) ∈ ℝ → ( cos ‘ 𝐴 ) ∈ ℂ )
17		recn	⊢ ( 1 ∈ ℝ → 1 ∈ ℂ )
18		subneg	⊢ ( ( ( cos ‘ 𝐴 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( cos ‘ 𝐴 ) − - 1 ) = ( ( cos ‘ 𝐴 ) + 1 ) )
19		addcom	⊢ ( ( 1 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ∈ ℂ ) → ( 1 + ( cos ‘ 𝐴 ) ) = ( ( cos ‘ 𝐴 ) + 1 ) )
20	19	ancoms	⊢ ( ( ( cos ‘ 𝐴 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( 1 + ( cos ‘ 𝐴 ) ) = ( ( cos ‘ 𝐴 ) + 1 ) )
21	18 20	eqtr4d	⊢ ( ( ( cos ‘ 𝐴 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( cos ‘ 𝐴 ) − - 1 ) = ( 1 + ( cos ‘ 𝐴 ) ) )
22	16 17 21	syl2an	⊢ ( ( ( cos ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( cos ‘ 𝐴 ) − - 1 ) = ( 1 + ( cos ‘ 𝐴 ) ) )
23	22	breq2d	⊢ ( ( ( cos ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( 0 ≤ ( ( cos ‘ 𝐴 ) − - 1 ) ↔ 0 ≤ ( 1 + ( cos ‘ 𝐴 ) ) ) )
24		renegcl	⊢ ( 1 ∈ ℝ → - 1 ∈ ℝ )
25		subge0	⊢ ( ( ( cos ‘ 𝐴 ) ∈ ℝ ∧ - 1 ∈ ℝ ) → ( 0 ≤ ( ( cos ‘ 𝐴 ) − - 1 ) ↔ - 1 ≤ ( cos ‘ 𝐴 ) ) )
26	24 25	sylan2	⊢ ( ( ( cos ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( 0 ≤ ( ( cos ‘ 𝐴 ) − - 1 ) ↔ - 1 ≤ ( cos ‘ 𝐴 ) ) )
27	10	ancoms	⊢ ( ( ( cos ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( 1 + ( cos ‘ 𝐴 ) ) ∈ ℝ )
28		halfnneg2	⊢ ( ( 1 + ( cos ‘ 𝐴 ) ) ∈ ℝ → ( 0 ≤ ( 1 + ( cos ‘ 𝐴 ) ) ↔ 0 ≤ ( ( 1 + ( cos ‘ 𝐴 ) ) / 2 ) ) )
29	27 28	syl	⊢ ( ( ( cos ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( 0 ≤ ( 1 + ( cos ‘ 𝐴 ) ) ↔ 0 ≤ ( ( 1 + ( cos ‘ 𝐴 ) ) / 2 ) ) )
30	23 26 29	3bitr3d	⊢ ( ( ( cos ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( - 1 ≤ ( cos ‘ 𝐴 ) ↔ 0 ≤ ( ( 1 + ( cos ‘ 𝐴 ) ) / 2 ) ) )
31	15 8 30	sylancl	⊢ ( 𝐴 ∈ ℝ → ( - 1 ≤ ( cos ‘ 𝐴 ) ↔ 0 ≤ ( ( 1 + ( cos ‘ 𝐴 ) ) / 2 ) ) )
32	14 31	mpbid	⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( ( 1 + ( cos ‘ 𝐴 ) ) / 2 ) )
33	5 32	syl	⊢ ( 𝐴 ∈ ( - π [,] π ) → 0 ≤ ( ( 1 + ( cos ‘ 𝐴 ) ) / 2 ) )
34	12 33	resqrtcld	⊢ ( 𝐴 ∈ ( - π [,] π ) → ( √ ‘ ( ( 1 + ( cos ‘ 𝐴 ) ) / 2 ) ) ∈ ℝ )
35	2 1	elicc2i	⊢ ( 𝐴 ∈ ( - π [,] π ) ↔ ( 𝐴 ∈ ℝ ∧ - π ≤ 𝐴 ∧ 𝐴 ≤ π ) )
36		2re	⊢ 2 ∈ ℝ
37		2pos	⊢ 0 < 2
38	36 37	pm3.2i	⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
39		lediv1	⊢ ( ( - π ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( - π ≤ 𝐴 ↔ ( - π / 2 ) ≤ ( 𝐴 / 2 ) ) )
40	2 38 39	mp3an13	⊢ ( 𝐴 ∈ ℝ → ( - π ≤ 𝐴 ↔ ( - π / 2 ) ≤ ( 𝐴 / 2 ) ) )
41		picn	⊢ π ∈ ℂ
42		2cn	⊢ 2 ∈ ℂ
43		2ne0	⊢ 2 ≠ 0
44		divneg	⊢ ( ( π ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → - ( π / 2 ) = ( - π / 2 ) )
45	41 42 43 44	mp3an	⊢ - ( π / 2 ) = ( - π / 2 )
46	45	breq1i	⊢ ( - ( π / 2 ) ≤ ( 𝐴 / 2 ) ↔ ( - π / 2 ) ≤ ( 𝐴 / 2 ) )
47	40 46	bitr4di	⊢ ( 𝐴 ∈ ℝ → ( - π ≤ 𝐴 ↔ - ( π / 2 ) ≤ ( 𝐴 / 2 ) ) )
48		lediv1	⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 𝐴 ≤ π ↔ ( 𝐴 / 2 ) ≤ ( π / 2 ) ) )
49	1 38 48	mp3an23	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ≤ π ↔ ( 𝐴 / 2 ) ≤ ( π / 2 ) ) )
50	47 49	anbi12d	⊢ ( 𝐴 ∈ ℝ → ( ( - π ≤ 𝐴 ∧ 𝐴 ≤ π ) ↔ ( - ( π / 2 ) ≤ ( 𝐴 / 2 ) ∧ ( 𝐴 / 2 ) ≤ ( π / 2 ) ) ) )
51		rehalfcl	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 / 2 ) ∈ ℝ )
52	51	rexrd	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 / 2 ) ∈ ℝ* )
53		halfpire	⊢ ( π / 2 ) ∈ ℝ
54	53	renegcli	⊢ - ( π / 2 ) ∈ ℝ
55	54	rexri	⊢ - ( π / 2 ) ∈ ℝ*
56	53	rexri	⊢ ( π / 2 ) ∈ ℝ*
57		elicc4	⊢ ( ( - ( π / 2 ) ∈ ℝ* ∧ ( π / 2 ) ∈ ℝ* ∧ ( 𝐴 / 2 ) ∈ ℝ* ) → ( ( 𝐴 / 2 ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ↔ ( - ( π / 2 ) ≤ ( 𝐴 / 2 ) ∧ ( 𝐴 / 2 ) ≤ ( π / 2 ) ) ) )
58	55 56 57	mp3an12	⊢ ( ( 𝐴 / 2 ) ∈ ℝ* → ( ( 𝐴 / 2 ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ↔ ( - ( π / 2 ) ≤ ( 𝐴 / 2 ) ∧ ( 𝐴 / 2 ) ≤ ( π / 2 ) ) ) )
59	52 58	syl	⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 / 2 ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ↔ ( - ( π / 2 ) ≤ ( 𝐴 / 2 ) ∧ ( 𝐴 / 2 ) ≤ ( π / 2 ) ) ) )
60	50 59	bitr4d	⊢ ( 𝐴 ∈ ℝ → ( ( - π ≤ 𝐴 ∧ 𝐴 ≤ π ) ↔ ( 𝐴 / 2 ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ) )
61	60	biimpd	⊢ ( 𝐴 ∈ ℝ → ( ( - π ≤ 𝐴 ∧ 𝐴 ≤ π ) → ( 𝐴 / 2 ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ) )
62	61	3impib	⊢ ( ( 𝐴 ∈ ℝ ∧ - π ≤ 𝐴 ∧ 𝐴 ≤ π ) → ( 𝐴 / 2 ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
63	35 62	sylbi	⊢ ( 𝐴 ∈ ( - π [,] π ) → ( 𝐴 / 2 ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
64		cosq14ge0	⊢ ( ( 𝐴 / 2 ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → 0 ≤ ( cos ‘ ( 𝐴 / 2 ) ) )
65	63 64	syl	⊢ ( 𝐴 ∈ ( - π [,] π ) → 0 ≤ ( cos ‘ ( 𝐴 / 2 ) ) )
66	12 33	sqrtge0d	⊢ ( 𝐴 ∈ ( - π [,] π ) → 0 ≤ ( √ ‘ ( ( 1 + ( cos ‘ 𝐴 ) ) / 2 ) ) )
67	5	recnd	⊢ ( 𝐴 ∈ ( - π [,] π ) → 𝐴 ∈ ℂ )
68		ax-1cn	⊢ 1 ∈ ℂ
69		coscl	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
70		addcl	⊢ ( ( 1 ∈ ℂ ∧ ( cos ‘ 𝐴 ) ∈ ℂ ) → ( 1 + ( cos ‘ 𝐴 ) ) ∈ ℂ )
71	68 69 70	sylancr	⊢ ( 𝐴 ∈ ℂ → ( 1 + ( cos ‘ 𝐴 ) ) ∈ ℂ )
72	71	halfcld	⊢ ( 𝐴 ∈ ℂ → ( ( 1 + ( cos ‘ 𝐴 ) ) / 2 ) ∈ ℂ )
73	72	sqsqrtd	⊢ ( 𝐴 ∈ ℂ → ( ( √ ‘ ( ( 1 + ( cos ‘ 𝐴 ) ) / 2 ) ) ↑ 2 ) = ( ( 1 + ( cos ‘ 𝐴 ) ) / 2 ) )
74		divcan2	⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 2 · ( 𝐴 / 2 ) ) = 𝐴 )
75	42 43 74	mp3an23	⊢ ( 𝐴 ∈ ℂ → ( 2 · ( 𝐴 / 2 ) ) = 𝐴 )
76	75	fveq2d	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( 2 · ( 𝐴 / 2 ) ) ) = ( cos ‘ 𝐴 ) )
77		halfcl	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 / 2 ) ∈ ℂ )
78		cos2t	⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( cos ‘ ( 2 · ( 𝐴 / 2 ) ) ) = ( ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) − 1 ) )
79	77 78	syl	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( 2 · ( 𝐴 / 2 ) ) ) = ( ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) − 1 ) )
80	76 79	eqtr3d	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) = ( ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) − 1 ) )
81	80	oveq2d	⊢ ( 𝐴 ∈ ℂ → ( 1 + ( cos ‘ 𝐴 ) ) = ( 1 + ( ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) − 1 ) ) )
82	81	oveq1d	⊢ ( 𝐴 ∈ ℂ → ( ( 1 + ( cos ‘ 𝐴 ) ) / 2 ) = ( ( 1 + ( ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) − 1 ) ) / 2 ) )
83	77	coscld	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( 𝐴 / 2 ) ) ∈ ℂ )
84	83	sqcld	⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ∈ ℂ )
85		mulcl	⊢ ( ( 2 ∈ ℂ ∧ ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ∈ ℂ ) → ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ∈ ℂ )
86	42 85	mpan	⊢ ( ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ∈ ℂ → ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ∈ ℂ )
87		pncan3	⊢ ( ( 1 ∈ ℂ ∧ ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ∈ ℂ ) → ( 1 + ( ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) − 1 ) ) = ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) )
88	68 86 87	sylancr	⊢ ( ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ∈ ℂ → ( 1 + ( ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) − 1 ) ) = ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) )
89	88	oveq1d	⊢ ( ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ∈ ℂ → ( ( 1 + ( ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) − 1 ) ) / 2 ) = ( ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) / 2 ) )
90		divcan3	⊢ ( ( ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) / 2 ) = ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) )
91	42 43 90	mp3an23	⊢ ( ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ∈ ℂ → ( ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) / 2 ) = ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) )
92	89 91	eqtrd	⊢ ( ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ∈ ℂ → ( ( 1 + ( ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) − 1 ) ) / 2 ) = ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) )
93	84 92	syl	⊢ ( 𝐴 ∈ ℂ → ( ( 1 + ( ( 2 · ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) − 1 ) ) / 2 ) = ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) )
94	73 82 93	3eqtrrd	⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) = ( ( √ ‘ ( ( 1 + ( cos ‘ 𝐴 ) ) / 2 ) ) ↑ 2 ) )
95	67 94	syl	⊢ ( 𝐴 ∈ ( - π [,] π ) → ( ( cos ‘ ( 𝐴 / 2 ) ) ↑ 2 ) = ( ( √ ‘ ( ( 1 + ( cos ‘ 𝐴 ) ) / 2 ) ) ↑ 2 ) )
96	7 34 65 66 95	sq11d	⊢ ( 𝐴 ∈ ( - π [,] π ) → ( cos ‘ ( 𝐴 / 2 ) ) = ( √ ‘ ( ( 1 + ( cos ‘ 𝐴 ) ) / 2 ) ) )