Theorem sin2h

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

	Ref	Expression
Assertion	sin2h	⊢ ( 𝐴 ∈ ( 0 [,] ( 2 · π ) ) → ( sin ‘ ( 𝐴 / 2 ) ) = ( √ ‘ ( ( 1 − ( cos ‘ 𝐴 ) ) / 2 ) ) )

Proof

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