Theorem tan2h

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

	Ref	Expression
Assertion	tan2h	⊢ ( 𝐴 ∈ ( 0 [,) π ) → ( tan ‘ ( 𝐴 / 2 ) ) = ( √ ‘ ( ( 1 − ( cos ‘ 𝐴 ) ) / ( 1 + ( cos ‘ 𝐴 ) ) ) ) )

Proof

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