cos2h

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

		Ref	Expression
	Assertion	cos2h	$⊢ A \in [- π, π] \to \cos (\frac{A}{2}) = \sqrt{\frac{1 + \cos A}{2}}$

Proof

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

Metamath Proof Explorer

Theorem cos2h

Proof