sin2h

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

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

Proof

Step	Hyp	Ref	Expression
1		0re	$⊢ 0 \in ℝ$
2		2re	$⊢ 2 \in ℝ$
3		pire	$⊢ π \in ℝ$
4	2 3	remulcli	$⊢ 2 π \in ℝ$
5		iccssre	$⊢ (0 \in ℝ \land 2 π \in ℝ) \to [0, 2 π] \subseteq ℝ$
6	1 4 5	mp2an	$⊢ [0, 2 π] \subseteq ℝ$
7	6	sseli	$⊢ A \in [0, 2 π] \to A \in ℝ$
8	7	rehalfcld	$⊢ A \in [0, 2 π] \to \frac{A}{2} \in ℝ$
9	8	resincld	$⊢ A \in [0, 2 π] \to \sin (\frac{A}{2}) \in ℝ$
10		1re	$⊢ 1 \in ℝ$
11		recoscl	$⊢ A \in ℝ \to \cos A \in ℝ$
12		resubcl	$⊢ (1 \in ℝ \land \cos A \in ℝ) \to 1 - \cos A \in ℝ$
13	10 11 12	sylancr	$⊢ A \in ℝ \to 1 - \cos A \in ℝ$
14	13	rehalfcld	$⊢ A \in ℝ \to \frac{1 - \cos A}{2} \in ℝ$
15		cosbnd	$⊢ A \in ℝ \to (- 1 \leq \cos A \land \cos A \leq 1)$
16	15	simprd	$⊢ A \in ℝ \to \cos A \leq 1$
17		subge0	$⊢ (1 \in ℝ \land \cos A \in ℝ) \to (0 \leq 1 - \cos A \leftrightarrow \cos A \leq 1)$
18	10 11 17	sylancr	$⊢ A \in ℝ \to (0 \leq 1 - \cos A \leftrightarrow \cos A \leq 1)$
19		halfnneg2	$⊢ 1 - \cos A \in ℝ \to (0 \leq 1 - \cos A \leftrightarrow 0 \leq \frac{1 - \cos A}{2})$
20	13 19	syl	$⊢ A \in ℝ \to (0 \leq 1 - \cos A \leftrightarrow 0 \leq \frac{1 - \cos A}{2})$
21	18 20	bitr3d	$⊢ A \in ℝ \to (\cos A \leq 1 \leftrightarrow 0 \leq \frac{1 - \cos A}{2})$
22	16 21	mpbid	$⊢ A \in ℝ \to 0 \leq \frac{1 - \cos A}{2}$
23	14 22	resqrtcld	$⊢ A \in ℝ \to \sqrt{\frac{1 - \cos A}{2}} \in ℝ$
24	7 23	syl	$⊢ A \in [0, 2 π] \to \sqrt{\frac{1 - \cos A}{2}} \in ℝ$
25	1 4	elicc2i	$⊢ A \in [0, 2 π] \leftrightarrow (A \in ℝ \land 0 \leq A \land A \leq 2 π)$
26		halfnneg2	$⊢ A \in ℝ \to (0 \leq A \leftrightarrow 0 \leq \frac{A}{2})$
27		2pos	$⊢ 0 < 2$
28	2 27	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
29		ledivmul	$⊢ (A \in ℝ \land π \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (\frac{A}{2} \leq π \leftrightarrow A \leq 2 π)$
30	3 28 29	mp3an23	$⊢ A \in ℝ \to (\frac{A}{2} \leq π \leftrightarrow A \leq 2 π)$
31	30	bicomd	$⊢ A \in ℝ \to (A \leq 2 π \leftrightarrow \frac{A}{2} \leq π)$
32	26 31	anbi12d	$⊢ A \in ℝ \to ((0 \leq A \land A \leq 2 π) \leftrightarrow (0 \leq \frac{A}{2} \land \frac{A}{2} \leq π))$
33		rehalfcl	$⊢ A \in ℝ \to \frac{A}{2} \in ℝ$
34	33	rexrd	$⊢ A \in ℝ \to \frac{A}{2} \in ℝ^{*}$
35		0xr	$⊢ 0 \in ℝ^{*}$
36	3	rexri	$⊢ π \in ℝ^{*}$
37		elicc4	$⊢ (0 \in ℝ^{} \land π \in ℝ^{} \land \frac{A}{2} \in ℝ^{*}) \to (\frac{A}{2} \in [0, π] \leftrightarrow (0 \leq \frac{A}{2} \land \frac{A}{2} \leq π))$
38	35 36 37	mp3an12	$⊢ \frac{A}{2} \in ℝ^{*} \to (\frac{A}{2} \in [0, π] \leftrightarrow (0 \leq \frac{A}{2} \land \frac{A}{2} \leq π))$
39	34 38	syl	$⊢ A \in ℝ \to (\frac{A}{2} \in [0, π] \leftrightarrow (0 \leq \frac{A}{2} \land \frac{A}{2} \leq π))$
40	32 39	bitr4d	$⊢ A \in ℝ \to ((0 \leq A \land A \leq 2 π) \leftrightarrow \frac{A}{2} \in [0, π])$
41	40	biimpd	$⊢ A \in ℝ \to ((0 \leq A \land A \leq 2 π) \to \frac{A}{2} \in [0, π])$
42	41	3impib	$⊢ (A \in ℝ \land 0 \leq A \land A \leq 2 π) \to \frac{A}{2} \in [0, π]$
43	25 42	sylbi	$⊢ A \in [0, 2 π] \to \frac{A}{2} \in [0, π]$
44		sinq12ge0	$⊢ \frac{A}{2} \in [0, π] \to 0 \leq \sin (\frac{A}{2})$
45	43 44	syl	$⊢ A \in [0, 2 π] \to 0 \leq \sin (\frac{A}{2})$
46	14 22	sqrtge0d	$⊢ A \in ℝ \to 0 \leq \sqrt{\frac{1 - \cos A}{2}}$
47	7 46	syl	$⊢ A \in [0, 2 π] \to 0 \leq \sqrt{\frac{1 - \cos A}{2}}$
48	7	recnd	$⊢ A \in [0, 2 π] \to A \in ℂ$
49		ax-1cn	$⊢ 1 \in ℂ$
50		coscl	$⊢ A \in ℂ \to \cos A \in ℂ$
51		subcl	$⊢ (1 \in ℂ \land \cos A \in ℂ) \to 1 - \cos A \in ℂ$
52	49 50 51	sylancr	$⊢ A \in ℂ \to 1 - \cos A \in ℂ$
53	52	halfcld	$⊢ A \in ℂ \to \frac{1 - \cos A}{2} \in ℂ$
54	53	sqsqrtd	$⊢ A \in ℂ \to {\sqrt{\frac{1 - \cos A}{2}}}^{2} = \frac{1 - \cos A}{2}$
55		halfcl	$⊢ A \in ℂ \to \frac{A}{2} \in ℂ$
56		coscl	$⊢ \frac{A}{2} \in ℂ \to \cos (\frac{A}{2}) \in ℂ$
57	56	sqcld	$⊢ \frac{A}{2} \in ℂ \to {\cos (\frac{A}{2})}^{2} \in ℂ$
58		2cn	$⊢ 2 \in ℂ$
59		mulcom	$⊢ ({\cos (\frac{A}{2})}^{2} \in ℂ \land 2 \in ℂ) \to {\cos (\frac{A}{2})}^{2} \cdot 2 = 2 {\cos (\frac{A}{2})}^{2}$
60	57 58 59	sylancl	$⊢ \frac{A}{2} \in ℂ \to {\cos (\frac{A}{2})}^{2} \cdot 2 = 2 {\cos (\frac{A}{2})}^{2}$
61	60	oveq2d	$⊢ \frac{A}{2} \in ℂ \to 1 \cdot 2 - {\cos (\frac{A}{2})}^{2} \cdot 2 = 1 \cdot 2 - 2 {\cos (\frac{A}{2})}^{2}$
62	58	mullidi	$⊢ 1 \cdot 2 = 2$
63		df-2	$⊢ 2 = 1 + 1$
64	62 63	eqtri	$⊢ 1 \cdot 2 = 1 + 1$
65	64	oveq1i	$⊢ 1 \cdot 2 - 2 {\cos (\frac{A}{2})}^{2} = 1 + 1 - 2 {\cos (\frac{A}{2})}^{2}$
66	61 65	eqtrdi	$⊢ \frac{A}{2} \in ℂ \to 1 \cdot 2 - {\cos (\frac{A}{2})}^{2} \cdot 2 = 1 + 1 - 2 {\cos (\frac{A}{2})}^{2}$
67		subdir	$⊢ (1 \in ℂ \land {\cos (\frac{A}{2})}^{2} \in ℂ \land 2 \in ℂ) \to (1 - {\cos (\frac{A}{2})}^{2}) \cdot 2 = 1 \cdot 2 - {\cos (\frac{A}{2})}^{2} \cdot 2$
68	49 58 67	mp3an13	$⊢ {\cos (\frac{A}{2})}^{2} \in ℂ \to (1 - {\cos (\frac{A}{2})}^{2}) \cdot 2 = 1 \cdot 2 - {\cos (\frac{A}{2})}^{2} \cdot 2$
69	57 68	syl	$⊢ \frac{A}{2} \in ℂ \to (1 - {\cos (\frac{A}{2})}^{2}) \cdot 2 = 1 \cdot 2 - {\cos (\frac{A}{2})}^{2} \cdot 2$
70		mulcl	$⊢ (2 \in ℂ \land {\cos (\frac{A}{2})}^{2} \in ℂ) \to 2 {\cos (\frac{A}{2})}^{2} \in ℂ$
71	58 57 70	sylancr	$⊢ \frac{A}{2} \in ℂ \to 2 {\cos (\frac{A}{2})}^{2} \in ℂ$
72		subsub3	$⊢ (1 \in ℂ \land 2 {\cos (\frac{A}{2})}^{2} \in ℂ \land 1 \in ℂ) \to 1 - (2 {\cos (\frac{A}{2})}^{2} - 1) = 1 + 1 - 2 {\cos (\frac{A}{2})}^{2}$
73	49 49 72	mp3an13	$⊢ 2 {\cos (\frac{A}{2})}^{2} \in ℂ \to 1 - (2 {\cos (\frac{A}{2})}^{2} - 1) = 1 + 1 - 2 {\cos (\frac{A}{2})}^{2}$
74	71 73	syl	$⊢ \frac{A}{2} \in ℂ \to 1 - (2 {\cos (\frac{A}{2})}^{2} - 1) = 1 + 1 - 2 {\cos (\frac{A}{2})}^{2}$
75	66 69 74	3eqtr4d	$⊢ \frac{A}{2} \in ℂ \to (1 - {\cos (\frac{A}{2})}^{2}) \cdot 2 = 1 - (2 {\cos (\frac{A}{2})}^{2} - 1)$
76		sincl	$⊢ \frac{A}{2} \in ℂ \to \sin (\frac{A}{2}) \in ℂ$
77	76	sqcld	$⊢ \frac{A}{2} \in ℂ \to {\sin (\frac{A}{2})}^{2} \in ℂ$
78	77 57	pncand	$⊢ \frac{A}{2} \in ℂ \to {\sin (\frac{A}{2})}^{2} + {\cos (\frac{A}{2})}^{2} - {\cos (\frac{A}{2})}^{2} = {\sin (\frac{A}{2})}^{2}$
79		sincossq	$⊢ \frac{A}{2} \in ℂ \to {\sin (\frac{A}{2})}^{2} + {\cos (\frac{A}{2})}^{2} = 1$
80	79	oveq1d	$⊢ \frac{A}{2} \in ℂ \to {\sin (\frac{A}{2})}^{2} + {\cos (\frac{A}{2})}^{2} - {\cos (\frac{A}{2})}^{2} = 1 - {\cos (\frac{A}{2})}^{2}$
81	78 80	eqtr3d	$⊢ \frac{A}{2} \in ℂ \to {\sin (\frac{A}{2})}^{2} = 1 - {\cos (\frac{A}{2})}^{2}$
82	81	oveq1d	$⊢ \frac{A}{2} \in ℂ \to {\sin (\frac{A}{2})}^{2} \cdot 2 = (1 - {\cos (\frac{A}{2})}^{2}) \cdot 2$
83		cos2t	$⊢ \frac{A}{2} \in ℂ \to \cos 2 (\frac{A}{2}) = 2 {\cos (\frac{A}{2})}^{2} - 1$
84	83	oveq2d	$⊢ \frac{A}{2} \in ℂ \to 1 - \cos 2 (\frac{A}{2}) = 1 - (2 {\cos (\frac{A}{2})}^{2} - 1)$
85	75 82 84	3eqtr4d	$⊢ \frac{A}{2} \in ℂ \to {\sin (\frac{A}{2})}^{2} \cdot 2 = 1 - \cos 2 (\frac{A}{2})$
86	55 85	syl	$⊢ A \in ℂ \to {\sin (\frac{A}{2})}^{2} \cdot 2 = 1 - \cos 2 (\frac{A}{2})$
87		2ne0	$⊢ 2 \neq 0$
88		divcan2	$⊢ (A \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to 2 (\frac{A}{2}) = A$
89	58 87 88	mp3an23	$⊢ A \in ℂ \to 2 (\frac{A}{2}) = A$
90	89	fveq2d	$⊢ A \in ℂ \to \cos 2 (\frac{A}{2}) = \cos A$
91	90	oveq2d	$⊢ A \in ℂ \to 1 - \cos 2 (\frac{A}{2}) = 1 - \cos A$
92	86 91	eqtrd	$⊢ A \in ℂ \to {\sin (\frac{A}{2})}^{2} \cdot 2 = 1 - \cos A$
93	92	oveq1d	$⊢ A \in ℂ \to \frac{{\sin (\frac{A}{2})}^{2} \cdot 2}{2} = \frac{1 - \cos A}{2}$
94	55	sincld	$⊢ A \in ℂ \to \sin (\frac{A}{2}) \in ℂ$
95	94	sqcld	$⊢ A \in ℂ \to {\sin (\frac{A}{2})}^{2} \in ℂ$
96		divcan4	$⊢ ({\sin (\frac{A}{2})}^{2} \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to \frac{{\sin (\frac{A}{2})}^{2} \cdot 2}{2} = {\sin (\frac{A}{2})}^{2}$
97	58 87 96	mp3an23	$⊢ {\sin (\frac{A}{2})}^{2} \in ℂ \to \frac{{\sin (\frac{A}{2})}^{2} \cdot 2}{2} = {\sin (\frac{A}{2})}^{2}$
98	95 97	syl	$⊢ A \in ℂ \to \frac{{\sin (\frac{A}{2})}^{2} \cdot 2}{2} = {\sin (\frac{A}{2})}^{2}$
99	54 93 98	3eqtr2rd	$⊢ A \in ℂ \to {\sin (\frac{A}{2})}^{2} = {\sqrt{\frac{1 - \cos A}{2}}}^{2}$
100	48 99	syl	$⊢ A \in [0, 2 π] \to {\sin (\frac{A}{2})}^{2} = {\sqrt{\frac{1 - \cos A}{2}}}^{2}$
101	9 24 45 47 100	sq11d	$⊢ A \in [0, 2 π] \to \sin (\frac{A}{2}) = \sqrt{\frac{1 - \cos A}{2}}$

Metamath Proof Explorer

Theorem sin2h

Proof