Metamath Proof Explorer

Theorem tan2h

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

Ref Expression
Assertion tan2h 
|- ( A e. ( 0 [,) _pi ) -> ( tan ` ( A / 2 ) ) = ( sqrt ` ( ( 1 - ( cos ` A ) ) / ( 1 + ( cos ` A ) ) ) ) )

Proof

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