tan2h

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

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

Proof

Step	Hyp	Ref	Expression
1		0re	$⊢ 0 \in ℝ$
2		pire	$⊢ π \in ℝ$
3	2	rexri	$⊢ π \in ℝ^{*}$
4		icossre	$⊢ (0 \in ℝ \land π \in ℝ^{*}) \to [0, π) \subseteq ℝ$
5	1 3 4	mp2an	$⊢ [0, π) \subseteq ℝ$
6	5	sseli	$⊢ A \in [0, π) \to A \in ℝ$
7	6	recnd	$⊢ A \in [0, π) \to A \in ℂ$
8	7	halfcld	$⊢ A \in [0, π) \to \frac{A}{2} \in ℂ$
9	6	rehalfcld	$⊢ A \in [0, π) \to \frac{A}{2} \in ℝ$
10	9	rered	$⊢ A \in [0, π) \to ℜ (\frac{A}{2}) = \frac{A}{2}$
11		elico2	$⊢ (0 \in ℝ \land π \in ℝ^{*}) \to (A \in [0, π) \leftrightarrow (A \in ℝ \land 0 \leq A \land A < π))$
12	1 3 11	mp2an	$⊢ A \in [0, π) \leftrightarrow (A \in ℝ \land 0 \leq A \land A < π)$
13		pipos	$⊢ 0 < π$
14		lt0neg2	$⊢ π \in ℝ \to (0 < π \leftrightarrow - π < 0)$
15	2 14	ax-mp	$⊢ 0 < π \leftrightarrow - π < 0$
16	13 15	mpbi	$⊢ - π < 0$
17	2	renegcli	$⊢ - π \in ℝ$
18		ltletr	$⊢ (- π \in ℝ \land 0 \in ℝ \land A \in ℝ) \to ((- π < 0 \land 0 \leq A) \to - π < A)$
19	17 1 18	mp3an12	$⊢ A \in ℝ \to ((- π < 0 \land 0 \leq A) \to - π < A)$
20	16 19	mpani	$⊢ A \in ℝ \to (0 \leq A \to - π < A)$
21		2re	$⊢ 2 \in ℝ$
22		2pos	$⊢ 0 < 2$
23	21 22	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
24		ltdiv1	$⊢ (- π \in ℝ \land A \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (- π < A \leftrightarrow \frac{- π}{2} < \frac{A}{2})$
25	17 23 24	mp3an13	$⊢ A \in ℝ \to (- π < A \leftrightarrow \frac{- π}{2} < \frac{A}{2})$
26		picn	$⊢ π \in ℂ$
27		2cn	$⊢ 2 \in ℂ$
28		2ne0	$⊢ 2 \neq 0$
29		divneg	$⊢ (π \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to - \frac{π}{2} = \frac{- π}{2}$
30	26 27 28 29	mp3an	$⊢ - \frac{π}{2} = \frac{- π}{2}$
31	30	breq1i	$⊢ - \frac{π}{2} < \frac{A}{2} \leftrightarrow \frac{- π}{2} < \frac{A}{2}$
32	25 31	bitr4di	$⊢ A \in ℝ \to (- π < A \leftrightarrow - \frac{π}{2} < \frac{A}{2})$
33	20 32	sylibd	$⊢ A \in ℝ \to (0 \leq A \to - \frac{π}{2} < \frac{A}{2})$
34		ltdiv1	$⊢ (A \in ℝ \land π \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (A < π \leftrightarrow \frac{A}{2} < \frac{π}{2})$
35	2 23 34	mp3an23	$⊢ A \in ℝ \to (A < π \leftrightarrow \frac{A}{2} < \frac{π}{2})$
36	35	biimpd	$⊢ A \in ℝ \to (A < π \to \frac{A}{2} < \frac{π}{2})$
37	33 36	anim12d	$⊢ A \in ℝ \to ((0 \leq A \land A < π) \to (- \frac{π}{2} < \frac{A}{2} \land \frac{A}{2} < \frac{π}{2}))$
38		rehalfcl	$⊢ A \in ℝ \to \frac{A}{2} \in ℝ$
39	38	rexrd	$⊢ A \in ℝ \to \frac{A}{2} \in ℝ^{*}$
40		halfpire	$⊢ \frac{π}{2} \in ℝ$
41	40	renegcli	$⊢ - \frac{π}{2} \in ℝ$
42	41	rexri	$⊢ - \frac{π}{2} \in ℝ^{*}$
43	40	rexri	$⊢ \frac{π}{2} \in ℝ^{*}$
44		elioo5	$⊢ (- \frac{π}{2} \in ℝ^{} \land \frac{π}{2} \in ℝ^{} \land \frac{A}{2} \in ℝ^{*}) \to (\frac{A}{2} \in (- \frac{π}{2}, \frac{π}{2}) \leftrightarrow (- \frac{π}{2} < \frac{A}{2} \land \frac{A}{2} < \frac{π}{2}))$
45	42 43 44	mp3an12	$⊢ \frac{A}{2} \in ℝ^{*} \to (\frac{A}{2} \in (- \frac{π}{2}, \frac{π}{2}) \leftrightarrow (- \frac{π}{2} < \frac{A}{2} \land \frac{A}{2} < \frac{π}{2}))$
46	39 45	syl	$⊢ A \in ℝ \to (\frac{A}{2} \in (- \frac{π}{2}, \frac{π}{2}) \leftrightarrow (- \frac{π}{2} < \frac{A}{2} \land \frac{A}{2} < \frac{π}{2}))$
47	37 46	sylibrd	$⊢ A \in ℝ \to ((0 \leq A \land A < π) \to \frac{A}{2} \in (- \frac{π}{2}, \frac{π}{2}))$
48	47	3impib	$⊢ (A \in ℝ \land 0 \leq A \land A < π) \to \frac{A}{2} \in (- \frac{π}{2}, \frac{π}{2})$
49	12 48	sylbi	$⊢ A \in [0, π) \to \frac{A}{2} \in (- \frac{π}{2}, \frac{π}{2})$
50	10 49	eqeltrd	$⊢ A \in [0, π) \to ℜ (\frac{A}{2}) \in (- \frac{π}{2}, \frac{π}{2})$
51		cosne0	$⊢ (\frac{A}{2} \in ℂ \land ℜ (\frac{A}{2}) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos (\frac{A}{2}) \neq 0$
52	8 50 51	syl2anc	$⊢ A \in [0, π) \to \cos (\frac{A}{2}) \neq 0$
53		tanval	$⊢ (\frac{A}{2} \in ℂ \land \cos (\frac{A}{2}) \neq 0) \to \tan (\frac{A}{2}) = \frac{\sin (\frac{A}{2})}{\cos (\frac{A}{2})}$
54	8 52 53	syl2anc	$⊢ A \in [0, π) \to \tan (\frac{A}{2}) = \frac{\sin (\frac{A}{2})}{\cos (\frac{A}{2})}$
55		0xr	$⊢ 0 \in ℝ^{*}$
56		elico1	$⊢ (0 \in ℝ^{} \land π \in ℝ^{}) \to (A \in [0, π) \leftrightarrow (A \in ℝ^{*} \land 0 \leq A \land A < π))$
57	55 3 56	mp2an	$⊢ A \in [0, π) \leftrightarrow (A \in ℝ^{*} \land 0 \leq A \land A < π)$
58	21 2	remulcli	$⊢ 2 π \in ℝ$
59	58	rexri	$⊢ 2 π \in ℝ^{*}$
60		1lt2	$⊢ 1 < 2$
61		ltmulgt12	$⊢ (π \in ℝ \land 2 \in ℝ \land 0 < π) \to (1 < 2 \leftrightarrow π < 2 π)$
62	2 21 13 61	mp3an	$⊢ 1 < 2 \leftrightarrow π < 2 π$
63	60 62	mpbi	$⊢ π < 2 π$
64		xrlttr	$⊢ (A \in ℝ^{} \land π \in ℝ^{} \land 2 π \in ℝ^{*}) \to ((A < π \land π < 2 π) \to A < 2 π)$
65	3 64	mp3an2	$⊢ (A \in ℝ^{} \land 2 π \in ℝ^{}) \to ((A < π \land π < 2 π) \to A < 2 π)$
66	63 65	mpan2i	$⊢ (A \in ℝ^{} \land 2 π \in ℝ^{}) \to (A < π \to A < 2 π)$
67		xrltle	$⊢ (A \in ℝ^{} \land 2 π \in ℝ^{}) \to (A < 2 π \to A \leq 2 π)$
68	66 67	syld	$⊢ (A \in ℝ^{} \land 2 π \in ℝ^{}) \to (A < π \to A \leq 2 π)$
69	59 68	mpan2	$⊢ A \in ℝ^{*} \to (A < π \to A \leq 2 π)$
70	69	anim2d	$⊢ A \in ℝ^{*} \to ((0 \leq A \land A < π) \to (0 \leq A \land A \leq 2 π))$
71		elicc4	$⊢ (0 \in ℝ^{} \land 2 π \in ℝ^{} \land A \in ℝ^{*}) \to (A \in [0, 2 π] \leftrightarrow (0 \leq A \land A \leq 2 π))$
72	55 59 71	mp3an12	$⊢ A \in ℝ^{*} \to (A \in [0, 2 π] \leftrightarrow (0 \leq A \land A \leq 2 π))$
73	70 72	sylibrd	$⊢ A \in ℝ^{*} \to ((0 \leq A \land A < π) \to A \in [0, 2 π])$
74	73	3impib	$⊢ (A \in ℝ^{*} \land 0 \leq A \land A < π) \to A \in [0, 2 π]$
75	57 74	sylbi	$⊢ A \in [0, π) \to A \in [0, 2 π]$
76		sin2h	$⊢ A \in [0, 2 π] \to \sin (\frac{A}{2}) = \sqrt{\frac{1 - \cos A}{2}}$
77	75 76	syl	$⊢ A \in [0, π) \to \sin (\frac{A}{2}) = \sqrt{\frac{1 - \cos A}{2}}$
78	1 2 13	ltleii	$⊢ 0 \leq π$
79		le0neg2	$⊢ π \in ℝ \to (0 \leq π \leftrightarrow - π \leq 0)$
80	2 79	ax-mp	$⊢ 0 \leq π \leftrightarrow - π \leq 0$
81	78 80	mpbi	$⊢ - π \leq 0$
82	17	rexri	$⊢ - π \in ℝ^{*}$
83		xrletr	$⊢ (- π \in ℝ^{} \land 0 \in ℝ^{} \land A \in ℝ^{*}) \to ((- π \leq 0 \land 0 \leq A) \to - π \leq A)$
84	82 55 83	mp3an12	$⊢ A \in ℝ^{*} \to ((- π \leq 0 \land 0 \leq A) \to - π \leq A)$
85	81 84	mpani	$⊢ A \in ℝ^{*} \to (0 \leq A \to - π \leq A)$
86		xrltle	$⊢ (A \in ℝ^{} \land π \in ℝ^{}) \to (A < π \to A \leq π)$
87	3 86	mpan2	$⊢ A \in ℝ^{*} \to (A < π \to A \leq π)$
88	85 87	anim12d	$⊢ A \in ℝ^{*} \to ((0 \leq A \land A < π) \to (- π \leq A \land A \leq π))$
89		elicc4	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land A \in ℝ^{*}) \to (A \in [- π, π] \leftrightarrow (- π \leq A \land A \leq π))$
90	82 3 89	mp3an12	$⊢ A \in ℝ^{*} \to (A \in [- π, π] \leftrightarrow (- π \leq A \land A \leq π))$
91	88 90	sylibrd	$⊢ A \in ℝ^{*} \to ((0 \leq A \land A < π) \to A \in [- π, π])$
92	91	3impib	$⊢ (A \in ℝ^{*} \land 0 \leq A \land A < π) \to A \in [- π, π]$
93	57 92	sylbi	$⊢ A \in [0, π) \to A \in [- π, π]$
94		cos2h	$⊢ A \in [- π, π] \to \cos (\frac{A}{2}) = \sqrt{\frac{1 + \cos A}{2}}$
95	93 94	syl	$⊢ A \in [0, π) \to \cos (\frac{A}{2}) = \sqrt{\frac{1 + \cos A}{2}}$
96	77 95	oveq12d	$⊢ A \in [0, π) \to \frac{\sin (\frac{A}{2})}{\cos (\frac{A}{2})} = \frac{\sqrt{\frac{1 - \cos A}{2}}}{\sqrt{\frac{1 + \cos A}{2}}}$
97	54 96	eqtrd	$⊢ A \in [0, π) \to \tan (\frac{A}{2}) = \frac{\sqrt{\frac{1 - \cos A}{2}}}{\sqrt{\frac{1 + \cos A}{2}}}$
98		1re	$⊢ 1 \in ℝ$
99	6	recoscld	$⊢ A \in [0, π) \to \cos A \in ℝ$
100		resubcl	$⊢ (1 \in ℝ \land \cos A \in ℝ) \to 1 - \cos A \in ℝ$
101	98 99 100	sylancr	$⊢ A \in [0, π) \to 1 - \cos A \in ℝ$
102	101	rehalfcld	$⊢ A \in [0, π) \to \frac{1 - \cos A}{2} \in ℝ$
103		cosbnd	$⊢ A \in ℝ \to (- 1 \leq \cos A \land \cos A \leq 1)$
104	103	simprd	$⊢ A \in ℝ \to \cos A \leq 1$
105		recoscl	$⊢ A \in ℝ \to \cos A \in ℝ$
106		subge0	$⊢ (1 \in ℝ \land \cos A \in ℝ) \to (0 \leq 1 - \cos A \leftrightarrow \cos A \leq 1)$
107		halfnneg2	$⊢ 1 - \cos A \in ℝ \to (0 \leq 1 - \cos A \leftrightarrow 0 \leq \frac{1 - \cos A}{2})$
108	100 107	syl	$⊢ (1 \in ℝ \land \cos A \in ℝ) \to (0 \leq 1 - \cos A \leftrightarrow 0 \leq \frac{1 - \cos A}{2})$
109	106 108	bitr3d	$⊢ (1 \in ℝ \land \cos A \in ℝ) \to (\cos A \leq 1 \leftrightarrow 0 \leq \frac{1 - \cos A}{2})$
110	98 105 109	sylancr	$⊢ A \in ℝ \to (\cos A \leq 1 \leftrightarrow 0 \leq \frac{1 - \cos A}{2})$
111	104 110	mpbid	$⊢ A \in ℝ \to 0 \leq \frac{1 - \cos A}{2}$
112	6 111	syl	$⊢ A \in [0, π) \to 0 \leq \frac{1 - \cos A}{2}$
113		readdcl	$⊢ (1 \in ℝ \land \cos A \in ℝ) \to 1 + \cos A \in ℝ$
114	98 99 113	sylancr	$⊢ A \in [0, π) \to 1 + \cos A \in ℝ$
115	103	simpld	$⊢ A \in ℝ \to - 1 \leq \cos A$
116	98	renegcli	$⊢ - 1 \in ℝ$
117		subge0	$⊢ (\cos A \in ℝ \land - 1 \in ℝ) \to (0 \leq \cos A - -1 \leftrightarrow - 1 \leq \cos A)$
118	105 116 117	sylancl	$⊢ A \in ℝ \to (0 \leq \cos A - -1 \leftrightarrow - 1 \leq \cos A)$
119		recn	$⊢ A \in ℝ \to A \in ℂ$
120	119	coscld	$⊢ A \in ℝ \to \cos A \in ℂ$
121		ax-1cn	$⊢ 1 \in ℂ$
122		subneg	$⊢ (\cos A \in ℂ \land 1 \in ℂ) \to \cos A - -1 = \cos A + 1$
123		addcom	$⊢ (\cos A \in ℂ \land 1 \in ℂ) \to \cos A + 1 = 1 + \cos A$
124	122 123	eqtrd	$⊢ (\cos A \in ℂ \land 1 \in ℂ) \to \cos A - -1 = 1 + \cos A$
125	120 121 124	sylancl	$⊢ A \in ℝ \to \cos A - -1 = 1 + \cos A$
126	125	breq2d	$⊢ A \in ℝ \to (0 \leq \cos A - -1 \leftrightarrow 0 \leq 1 + \cos A)$
127	118 126	bitr3d	$⊢ A \in ℝ \to (- 1 \leq \cos A \leftrightarrow 0 \leq 1 + \cos A)$
128	115 127	mpbid	$⊢ A \in ℝ \to 0 \leq 1 + \cos A$
129	6 128	syl	$⊢ A \in [0, π) \to 0 \leq 1 + \cos A$
130		snunioo	$⊢ (0 \in ℝ^{} \land π \in ℝ^{} \land 0 < π) \to \{0\} \cup (0, π) = [0, π)$
131	55 3 13 130	mp3an	$⊢ \{0\} \cup (0, π) = [0, π)$
132	131	eleq2i	$⊢ A \in (\{0\} \cup (0, π)) \leftrightarrow A \in [0, π)$
133		elun	$⊢ A \in (\{0\} \cup (0, π)) \leftrightarrow (A \in \{0\} \lor A \in (0, π))$
134	132 133	bitr3i	$⊢ A \in [0, π) \leftrightarrow (A \in \{0\} \lor A \in (0, π))$
135		elsni	$⊢ A \in \{0\} \to A = 0$
136		fveq2	$⊢ A = 0 \to \cos A = \cos 0$
137		cos0	$⊢ \cos 0 = 1$
138	136 137	eqtrdi	$⊢ A = 0 \to \cos A = 1$
139	138	oveq2d	$⊢ A = 0 \to 1 + \cos A = 1 + 1$
140		df-2	$⊢ 2 = 1 + 1$
141	139 140	eqtr4di	$⊢ A = 0 \to 1 + \cos A = 2$
142	28	a1i	$⊢ A = 0 \to 2 \neq 0$
143	141 142	eqnetrd	$⊢ A = 0 \to 1 + \cos A \neq 0$
144	135 143	syl	$⊢ A \in \{0\} \to 1 + \cos A \neq 0$
145		sinq12gt0	$⊢ A \in (0, π) \to 0 < \sin A$
146		ltne	$⊢ (0 \in ℝ \land 0 < \sin A) \to \sin A \neq 0$
147	1 146	mpan	$⊢ 0 < \sin A \to \sin A \neq 0$
148		elioore	$⊢ A \in (0, π) \to A \in ℝ$
149	148	recnd	$⊢ A \in (0, π) \to A \in ℂ$
150		oveq1	$⊢ - 1 = \cos A \to {(- 1)}^{2} = {\cos A}^{2}$
151	150	a1i	$⊢ A \in ℂ \to (- 1 = \cos A \to {(- 1)}^{2} = {\cos A}^{2})$
152		df-neg	$⊢ - 1 = 0 - 1$
153	152	eqeq1i	$⊢ - 1 = \cos A \leftrightarrow 0 - 1 = \cos A$
154		coscl	$⊢ A \in ℂ \to \cos A \in ℂ$
155		0cn	$⊢ 0 \in ℂ$
156		subadd	$⊢ (0 \in ℂ \land 1 \in ℂ \land \cos A \in ℂ) \to (0 - 1 = \cos A \leftrightarrow 1 + \cos A = 0)$
157	155 121 156	mp3an12	$⊢ \cos A \in ℂ \to (0 - 1 = \cos A \leftrightarrow 1 + \cos A = 0)$
158	154 157	syl	$⊢ A \in ℂ \to (0 - 1 = \cos A \leftrightarrow 1 + \cos A = 0)$
159	153 158	bitrid	$⊢ A \in ℂ \to (- 1 = \cos A \leftrightarrow 1 + \cos A = 0)$
160		sincl	$⊢ A \in ℂ \to \sin A \in ℂ$
161	160	sqcld	$⊢ A \in ℂ \to {\sin A}^{2} \in ℂ$
162		0cnd	$⊢ A \in ℂ \to 0 \in ℂ$
163	154	sqcld	$⊢ A \in ℂ \to {\cos A}^{2} \in ℂ$
164	161 162 163	addcan2d	$⊢ A \in ℂ \to ({\sin A}^{2} + {\cos A}^{2} = 0 + {\cos A}^{2} \leftrightarrow {\sin A}^{2} = 0)$
165		sincossq	$⊢ A \in ℂ \to {\sin A}^{2} + {\cos A}^{2} = 1$
166		neg1sqe1	$⊢ {(- 1)}^{2} = 1$
167	165 166	eqtr4di	$⊢ A \in ℂ \to {\sin A}^{2} + {\cos A}^{2} = {(- 1)}^{2}$
168	163	addlidd	$⊢ A \in ℂ \to 0 + {\cos A}^{2} = {\cos A}^{2}$
169	167 168	eqeq12d	$⊢ A \in ℂ \to ({\sin A}^{2} + {\cos A}^{2} = 0 + {\cos A}^{2} \leftrightarrow {(- 1)}^{2} = {\cos A}^{2})$
170		sqeq0	$⊢ \sin A \in ℂ \to ({\sin A}^{2} = 0 \leftrightarrow \sin A = 0)$
171	160 170	syl	$⊢ A \in ℂ \to ({\sin A}^{2} = 0 \leftrightarrow \sin A = 0)$
172	164 169 171	3bitr3d	$⊢ A \in ℂ \to ({(- 1)}^{2} = {\cos A}^{2} \leftrightarrow \sin A = 0)$
173	151 159 172	3imtr3d	$⊢ A \in ℂ \to (1 + \cos A = 0 \to \sin A = 0)$
174	149 173	syl	$⊢ A \in (0, π) \to (1 + \cos A = 0 \to \sin A = 0)$
175	174	necon3d	$⊢ A \in (0, π) \to (\sin A \neq 0 \to 1 + \cos A \neq 0)$
176	147 175	syl5	$⊢ A \in (0, π) \to (0 < \sin A \to 1 + \cos A \neq 0)$
177	145 176	mpd	$⊢ A \in (0, π) \to 1 + \cos A \neq 0$
178	144 177	jaoi	$⊢ (A \in \{0\} \lor A \in (0, π)) \to 1 + \cos A \neq 0$
179	134 178	sylbi	$⊢ A \in [0, π) \to 1 + \cos A \neq 0$
180	114 129 179	ne0gt0d	$⊢ A \in [0, π) \to 0 < 1 + \cos A$
181	114 180	elrpd	$⊢ A \in [0, π) \to 1 + \cos A \in ℝ^{+}$
182	181	rphalfcld	$⊢ A \in [0, π) \to \frac{1 + \cos A}{2} \in ℝ^{+}$
183	102 112 182	sqrtdivd	$⊢ A \in [0, π) \to \sqrt{\frac{\frac{1 - \cos A}{2}}{\frac{1 + \cos A}{2}}} = \frac{\sqrt{\frac{1 - \cos A}{2}}}{\sqrt{\frac{1 + \cos A}{2}}}$
184	7	coscld	$⊢ A \in [0, π) \to \cos A \in ℂ$
185		subcl	$⊢ (1 \in ℂ \land \cos A \in ℂ) \to 1 - \cos A \in ℂ$
186	121 184 185	sylancr	$⊢ A \in [0, π) \to 1 - \cos A \in ℂ$
187		addcl	$⊢ (1 \in ℂ \land \cos A \in ℂ) \to 1 + \cos A \in ℂ$
188	121 184 187	sylancr	$⊢ A \in [0, π) \to 1 + \cos A \in ℂ$
189		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
190		divcan7	$⊢ (1 - \cos A \in ℂ \land (1 + \cos A \in ℂ \land 1 + \cos A \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to \frac{\frac{1 - \cos A}{2}}{\frac{1 + \cos A}{2}} = \frac{1 - \cos A}{1 + \cos A}$
191	189 190	mp3an3	$⊢ (1 - \cos A \in ℂ \land (1 + \cos A \in ℂ \land 1 + \cos A \neq 0)) \to \frac{\frac{1 - \cos A}{2}}{\frac{1 + \cos A}{2}} = \frac{1 - \cos A}{1 + \cos A}$
192	186 188 179 191	syl12anc	$⊢ A \in [0, π) \to \frac{\frac{1 - \cos A}{2}}{\frac{1 + \cos A}{2}} = \frac{1 - \cos A}{1 + \cos A}$
193	192	fveq2d	$⊢ A \in [0, π) \to \sqrt{\frac{\frac{1 - \cos A}{2}}{\frac{1 + \cos A}{2}}} = \sqrt{\frac{1 - \cos A}{1 + \cos A}}$
194	97 183 193	3eqtr2d	$⊢ A \in [0, π) \to \tan (\frac{A}{2}) = \sqrt{\frac{1 - \cos A}{1 + \cos A}}$

Metamath Proof Explorer

Theorem tan2h

Proof