Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Brendan Leahy
tan2h
Next ⟩
lindsadd
Metamath Proof Explorer
Ascii
Unicode
Theorem
tan2h
Description:
Half-angle rule for tangent.
(Contributed by
Brendan Leahy
, 4-Aug-2018)
Ref
Expression
Assertion
tan2h
π
⊢
A
∈
0
π
→
tan
A
2
=
1
−
cos
A
1
+
cos
A
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
π
⊢
A
∈
0
π
→
A
∈
ℝ
7
6
recnd
π
⊢
A
∈
0
π
→
A
∈
ℂ
8
7
halfcld
π
⊢
A
∈
0
π
→
A
2
∈
ℂ
9
6
rehalfcld
π
⊢
A
∈
0
π
→
A
2
∈
ℝ
10
9
rered
π
⊢
A
∈
0
π
→
ℜ
A
2
=
A
2
11
elico2
π
π
π
⊢
0
∈
ℝ
∧
π
∈
ℝ
*
→
A
∈
0
π
↔
A
∈
ℝ
∧
0
≤
A
∧
A
<
π
12
1
3
11
mp2an
π
π
⊢
A
∈
0
π
↔
A
∈
ℝ
∧
0
≤
A
∧
A
<
π
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
∈
ℝ
∧
A
∈
ℝ
→
−
π
<
0
∧
0
≤
A
→
−
π
<
A
19
17
1
18
mp3an12
π
π
⊢
A
∈
ℝ
→
−
π
<
0
∧
0
≤
A
→
−
π
<
A
20
16
19
mpani
π
⊢
A
∈
ℝ
→
0
≤
A
→
−
π
<
A
21
2re
⊢
2
∈
ℝ
22
2pos
⊢
0
<
2
23
21
22
pm3.2i
⊢
2
∈
ℝ
∧
0
<
2
24
ltdiv1
π
π
π
⊢
−
π
∈
ℝ
∧
A
∈
ℝ
∧
2
∈
ℝ
∧
0
<
2
→
−
π
<
A
↔
−
π
2
<
A
2
25
17
23
24
mp3an13
π
π
⊢
A
∈
ℝ
→
−
π
<
A
↔
−
π
2
<
A
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
<
A
2
↔
−
π
2
<
A
2
32
25
31
bitr4di
π
π
⊢
A
∈
ℝ
→
−
π
<
A
↔
−
π
2
<
A
2
33
20
32
sylibd
π
⊢
A
∈
ℝ
→
0
≤
A
→
−
π
2
<
A
2
34
ltdiv1
π
π
π
⊢
A
∈
ℝ
∧
π
∈
ℝ
∧
2
∈
ℝ
∧
0
<
2
→
A
<
π
↔
A
2
<
π
2
35
2
23
34
mp3an23
π
π
⊢
A
∈
ℝ
→
A
<
π
↔
A
2
<
π
2
36
35
biimpd
π
π
⊢
A
∈
ℝ
→
A
<
π
→
A
2
<
π
2
37
33
36
anim12d
π
π
π
⊢
A
∈
ℝ
→
0
≤
A
∧
A
<
π
→
−
π
2
<
A
2
∧
A
2
<
π
2
38
rehalfcl
⊢
A
∈
ℝ
→
A
2
∈
ℝ
39
38
rexrd
⊢
A
∈
ℝ
→
A
2
∈
ℝ
*
40
halfpire
π
⊢
π
2
∈
ℝ
41
40
renegcli
π
⊢
−
π
2
∈
ℝ
42
41
rexri
π
⊢
−
π
2
∈
ℝ
*
43
40
rexri
π
⊢
π
2
∈
ℝ
*
44
elioo5
π
π
π
π
π
π
⊢
−
π
2
∈
ℝ
*
∧
π
2
∈
ℝ
*
∧
A
2
∈
ℝ
*
→
A
2
∈
−
π
2
π
2
↔
−
π
2
<
A
2
∧
A
2
<
π
2
45
42
43
44
mp3an12
π
π
π
π
⊢
A
2
∈
ℝ
*
→
A
2
∈
−
π
2
π
2
↔
−
π
2
<
A
2
∧
A
2
<
π
2
46
39
45
syl
π
π
π
π
⊢
A
∈
ℝ
→
A
2
∈
−
π
2
π
2
↔
−
π
2
<
A
2
∧
A
2
<
π
2
47
37
46
sylibrd
π
π
π
⊢
A
∈
ℝ
→
0
≤
A
∧
A
<
π
→
A
2
∈
−
π
2
π
2
48
47
3impib
π
π
π
⊢
A
∈
ℝ
∧
0
≤
A
∧
A
<
π
→
A
2
∈
−
π
2
π
2
49
12
48
sylbi
π
π
π
⊢
A
∈
0
π
→
A
2
∈
−
π
2
π
2
50
10
49
eqeltrd
π
π
π
⊢
A
∈
0
π
→
ℜ
A
2
∈
−
π
2
π
2
51
cosne0
π
π
⊢
A
2
∈
ℂ
∧
ℜ
A
2
∈
−
π
2
π
2
→
cos
A
2
≠
0
52
8
50
51
syl2anc
π
⊢
A
∈
0
π
→
cos
A
2
≠
0
53
tanval
⊢
A
2
∈
ℂ
∧
cos
A
2
≠
0
→
tan
A
2
=
sin
A
2
cos
A
2
54
8
52
53
syl2anc
π
⊢
A
∈
0
π
→
tan
A
2
=
sin
A
2
cos
A
2
55
0xr
⊢
0
∈
ℝ
*
56
elico1
π
π
π
⊢
0
∈
ℝ
*
∧
π
∈
ℝ
*
→
A
∈
0
π
↔
A
∈
ℝ
*
∧
0
≤
A
∧
A
<
π
57
55
3
56
mp2an
π
π
⊢
A
∈
0
π
↔
A
∈
ℝ
*
∧
0
≤
A
∧
A
<
π
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
π
π
π
π
π
π
⊢
A
∈
ℝ
*
∧
π
∈
ℝ
*
∧
2
π
∈
ℝ
*
→
A
<
π
∧
π
<
2
π
→
A
<
2
π
65
3
64
mp3an2
π
π
π
π
π
⊢
A
∈
ℝ
*
∧
2
π
∈
ℝ
*
→
A
<
π
∧
π
<
2
π
→
A
<
2
π
66
63
65
mpan2i
π
π
π
⊢
A
∈
ℝ
*
∧
2
π
∈
ℝ
*
→
A
<
π
→
A
<
2
π
67
xrltle
π
π
π
⊢
A
∈
ℝ
*
∧
2
π
∈
ℝ
*
→
A
<
2
π
→
A
≤
2
π
68
66
67
syld
π
π
π
⊢
A
∈
ℝ
*
∧
2
π
∈
ℝ
*
→
A
<
π
→
A
≤
2
π
69
59
68
mpan2
π
π
⊢
A
∈
ℝ
*
→
A
<
π
→
A
≤
2
π
70
69
anim2d
π
π
⊢
A
∈
ℝ
*
→
0
≤
A
∧
A
<
π
→
0
≤
A
∧
A
≤
2
π
71
elicc4
π
π
π
⊢
0
∈
ℝ
*
∧
2
π
∈
ℝ
*
∧
A
∈
ℝ
*
→
A
∈
0
2
π
↔
0
≤
A
∧
A
≤
2
π
72
55
59
71
mp3an12
π
π
⊢
A
∈
ℝ
*
→
A
∈
0
2
π
↔
0
≤
A
∧
A
≤
2
π
73
70
72
sylibrd
π
π
⊢
A
∈
ℝ
*
→
0
≤
A
∧
A
<
π
→
A
∈
0
2
π
74
73
3impib
π
π
⊢
A
∈
ℝ
*
∧
0
≤
A
∧
A
<
π
→
A
∈
0
2
π
75
57
74
sylbi
π
π
⊢
A
∈
0
π
→
A
∈
0
2
π
76
sin2h
π
⊢
A
∈
0
2
π
→
sin
A
2
=
1
−
cos
A
2
77
75
76
syl
π
⊢
A
∈
0
π
→
sin
A
2
=
1
−
cos
A
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
∈
ℝ
*
∧
A
∈
ℝ
*
→
−
π
≤
0
∧
0
≤
A
→
−
π
≤
A
84
82
55
83
mp3an12
π
π
⊢
A
∈
ℝ
*
→
−
π
≤
0
∧
0
≤
A
→
−
π
≤
A
85
81
84
mpani
π
⊢
A
∈
ℝ
*
→
0
≤
A
→
−
π
≤
A
86
xrltle
π
π
π
⊢
A
∈
ℝ
*
∧
π
∈
ℝ
*
→
A
<
π
→
A
≤
π
87
3
86
mpan2
π
π
⊢
A
∈
ℝ
*
→
A
<
π
→
A
≤
π
88
85
87
anim12d
π
π
π
⊢
A
∈
ℝ
*
→
0
≤
A
∧
A
<
π
→
−
π
≤
A
∧
A
≤
π
89
elicc4
π
π
π
π
π
π
⊢
−
π
∈
ℝ
*
∧
π
∈
ℝ
*
∧
A
∈
ℝ
*
→
A
∈
−
π
π
↔
−
π
≤
A
∧
A
≤
π
90
82
3
89
mp3an12
π
π
π
π
⊢
A
∈
ℝ
*
→
A
∈
−
π
π
↔
−
π
≤
A
∧
A
≤
π
91
88
90
sylibrd
π
π
π
⊢
A
∈
ℝ
*
→
0
≤
A
∧
A
<
π
→
A
∈
−
π
π
92
91
3impib
π
π
π
⊢
A
∈
ℝ
*
∧
0
≤
A
∧
A
<
π
→
A
∈
−
π
π
93
57
92
sylbi
π
π
π
⊢
A
∈
0
π
→
A
∈
−
π
π
94
cos2h
π
π
⊢
A
∈
−
π
π
→
cos
A
2
=
1
+
cos
A
2
95
93
94
syl
π
⊢
A
∈
0
π
→
cos
A
2
=
1
+
cos
A
2
96
77
95
oveq12d
π
⊢
A
∈
0
π
→
sin
A
2
cos
A
2
=
1
−
cos
A
2
1
+
cos
A
2
97
54
96
eqtrd
π
⊢
A
∈
0
π
→
tan
A
2
=
1
−
cos
A
2
1
+
cos
A
2
98
1re
⊢
1
∈
ℝ
99
6
recoscld
π
⊢
A
∈
0
π
→
cos
A
∈
ℝ
100
resubcl
⊢
1
∈
ℝ
∧
cos
A
∈
ℝ
→
1
−
cos
A
∈
ℝ
101
98
99
100
sylancr
π
⊢
A
∈
0
π
→
1
−
cos
A
∈
ℝ
102
101
rehalfcld
π
⊢
A
∈
0
π
→
1
−
cos
A
2
∈
ℝ
103
cosbnd
⊢
A
∈
ℝ
→
−
1
≤
cos
A
∧
cos
A
≤
1
104
103
simprd
⊢
A
∈
ℝ
→
cos
A
≤
1
105
recoscl
⊢
A
∈
ℝ
→
cos
A
∈
ℝ
106
subge0
⊢
1
∈
ℝ
∧
cos
A
∈
ℝ
→
0
≤
1
−
cos
A
↔
cos
A
≤
1
107
halfnneg2
⊢
1
−
cos
A
∈
ℝ
→
0
≤
1
−
cos
A
↔
0
≤
1
−
cos
A
2
108
100
107
syl
⊢
1
∈
ℝ
∧
cos
A
∈
ℝ
→
0
≤
1
−
cos
A
↔
0
≤
1
−
cos
A
2
109
106
108
bitr3d
⊢
1
∈
ℝ
∧
cos
A
∈
ℝ
→
cos
A
≤
1
↔
0
≤
1
−
cos
A
2
110
98
105
109
sylancr
⊢
A
∈
ℝ
→
cos
A
≤
1
↔
0
≤
1
−
cos
A
2
111
104
110
mpbid
⊢
A
∈
ℝ
→
0
≤
1
−
cos
A
2
112
6
111
syl
π
⊢
A
∈
0
π
→
0
≤
1
−
cos
A
2
113
readdcl
⊢
1
∈
ℝ
∧
cos
A
∈
ℝ
→
1
+
cos
A
∈
ℝ
114
98
99
113
sylancr
π
⊢
A
∈
0
π
→
1
+
cos
A
∈
ℝ
115
103
simpld
⊢
A
∈
ℝ
→
−
1
≤
cos
A
116
98
renegcli
⊢
−
1
∈
ℝ
117
subge0
⊢
cos
A
∈
ℝ
∧
−
1
∈
ℝ
→
0
≤
cos
A
−
-1
↔
−
1
≤
cos
A
118
105
116
117
sylancl
⊢
A
∈
ℝ
→
0
≤
cos
A
−
-1
↔
−
1
≤
cos
A
119
recn
⊢
A
∈
ℝ
→
A
∈
ℂ
120
119
coscld
⊢
A
∈
ℝ
→
cos
A
∈
ℂ
121
ax-1cn
⊢
1
∈
ℂ
122
subneg
⊢
cos
A
∈
ℂ
∧
1
∈
ℂ
→
cos
A
−
-1
=
cos
A
+
1
123
addcom
⊢
cos
A
∈
ℂ
∧
1
∈
ℂ
→
cos
A
+
1
=
1
+
cos
A
124
122
123
eqtrd
⊢
cos
A
∈
ℂ
∧
1
∈
ℂ
→
cos
A
−
-1
=
1
+
cos
A
125
120
121
124
sylancl
⊢
A
∈
ℝ
→
cos
A
−
-1
=
1
+
cos
A
126
125
breq2d
⊢
A
∈
ℝ
→
0
≤
cos
A
−
-1
↔
0
≤
1
+
cos
A
127
118
126
bitr3d
⊢
A
∈
ℝ
→
−
1
≤
cos
A
↔
0
≤
1
+
cos
A
128
115
127
mpbid
⊢
A
∈
ℝ
→
0
≤
1
+
cos
A
129
6
128
syl
π
⊢
A
∈
0
π
→
0
≤
1
+
cos
A
130
snunioo
π
π
π
π
⊢
0
∈
ℝ
*
∧
π
∈
ℝ
*
∧
0
<
π
→
0
∪
0
π
=
0
π
131
55
3
13
130
mp3an
π
π
⊢
0
∪
0
π
=
0
π
132
131
eleq2i
π
π
⊢
A
∈
0
∪
0
π
↔
A
∈
0
π
133
elun
π
π
⊢
A
∈
0
∪
0
π
↔
A
∈
0
∨
A
∈
0
π
134
132
133
bitr3i
π
π
⊢
A
∈
0
π
↔
A
∈
0
∨
A
∈
0
π
135
elsni
⊢
A
∈
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
∈
0
→
1
+
cos
A
≠
0
145
sinq12gt0
π
⊢
A
∈
0
π
→
0
<
sin
A
146
ltne
⊢
0
∈
ℝ
∧
0
<
sin
A
→
sin
A
≠
0
147
1
146
mpan
⊢
0
<
sin
A
→
sin
A
≠
0
148
elioore
π
⊢
A
∈
0
π
→
A
∈
ℝ
149
148
recnd
π
⊢
A
∈
0
π
→
A
∈
ℂ
150
oveq1
⊢
−
1
=
cos
A
→
−
1
2
=
cos
A
2
151
150
a1i
⊢
A
∈
ℂ
→
−
1
=
cos
A
→
−
1
2
=
cos
A
2
152
df-neg
⊢
−
1
=
0
−
1
153
152
eqeq1i
⊢
−
1
=
cos
A
↔
0
−
1
=
cos
A
154
coscl
⊢
A
∈
ℂ
→
cos
A
∈
ℂ
155
0cn
⊢
0
∈
ℂ
156
subadd
⊢
0
∈
ℂ
∧
1
∈
ℂ
∧
cos
A
∈
ℂ
→
0
−
1
=
cos
A
↔
1
+
cos
A
=
0
157
155
121
156
mp3an12
⊢
cos
A
∈
ℂ
→
0
−
1
=
cos
A
↔
1
+
cos
A
=
0
158
154
157
syl
⊢
A
∈
ℂ
→
0
−
1
=
cos
A
↔
1
+
cos
A
=
0
159
153
158
syl5bb
⊢
A
∈
ℂ
→
−
1
=
cos
A
↔
1
+
cos
A
=
0
160
sincl
⊢
A
∈
ℂ
→
sin
A
∈
ℂ
161
160
sqcld
⊢
A
∈
ℂ
→
sin
A
2
∈
ℂ
162
0cnd
⊢
A
∈
ℂ
→
0
∈
ℂ
163
154
sqcld
⊢
A
∈
ℂ
→
cos
A
2
∈
ℂ
164
161
162
163
addcan2d
⊢
A
∈
ℂ
→
sin
A
2
+
cos
A
2
=
0
+
cos
A
2
↔
sin
A
2
=
0
165
sincossq
⊢
A
∈
ℂ
→
sin
A
2
+
cos
A
2
=
1
166
neg1sqe1
⊢
−
1
2
=
1
167
165
166
eqtr4di
⊢
A
∈
ℂ
→
sin
A
2
+
cos
A
2
=
−
1
2
168
163
addid2d
⊢
A
∈
ℂ
→
0
+
cos
A
2
=
cos
A
2
169
167
168
eqeq12d
⊢
A
∈
ℂ
→
sin
A
2
+
cos
A
2
=
0
+
cos
A
2
↔
−
1
2
=
cos
A
2
170
sqeq0
⊢
sin
A
∈
ℂ
→
sin
A
2
=
0
↔
sin
A
=
0
171
160
170
syl
⊢
A
∈
ℂ
→
sin
A
2
=
0
↔
sin
A
=
0
172
164
169
171
3bitr3d
⊢
A
∈
ℂ
→
−
1
2
=
cos
A
2
↔
sin
A
=
0
173
151
159
172
3imtr3d
⊢
A
∈
ℂ
→
1
+
cos
A
=
0
→
sin
A
=
0
174
149
173
syl
π
⊢
A
∈
0
π
→
1
+
cos
A
=
0
→
sin
A
=
0
175
174
necon3d
π
⊢
A
∈
0
π
→
sin
A
≠
0
→
1
+
cos
A
≠
0
176
147
175
syl5
π
⊢
A
∈
0
π
→
0
<
sin
A
→
1
+
cos
A
≠
0
177
145
176
mpd
π
⊢
A
∈
0
π
→
1
+
cos
A
≠
0
178
144
177
jaoi
π
⊢
A
∈
0
∨
A
∈
0
π
→
1
+
cos
A
≠
0
179
134
178
sylbi
π
⊢
A
∈
0
π
→
1
+
cos
A
≠
0
180
114
129
179
ne0gt0d
π
⊢
A
∈
0
π
→
0
<
1
+
cos
A
181
114
180
elrpd
π
⊢
A
∈
0
π
→
1
+
cos
A
∈
ℝ
+
182
181
rphalfcld
π
⊢
A
∈
0
π
→
1
+
cos
A
2
∈
ℝ
+
183
102
112
182
sqrtdivd
π
⊢
A
∈
0
π
→
1
−
cos
A
2
1
+
cos
A
2
=
1
−
cos
A
2
1
+
cos
A
2
184
7
coscld
π
⊢
A
∈
0
π
→
cos
A
∈
ℂ
185
subcl
⊢
1
∈
ℂ
∧
cos
A
∈
ℂ
→
1
−
cos
A
∈
ℂ
186
121
184
185
sylancr
π
⊢
A
∈
0
π
→
1
−
cos
A
∈
ℂ
187
addcl
⊢
1
∈
ℂ
∧
cos
A
∈
ℂ
→
1
+
cos
A
∈
ℂ
188
121
184
187
sylancr
π
⊢
A
∈
0
π
→
1
+
cos
A
∈
ℂ
189
2cnne0
⊢
2
∈
ℂ
∧
2
≠
0
190
divcan7
⊢
1
−
cos
A
∈
ℂ
∧
1
+
cos
A
∈
ℂ
∧
1
+
cos
A
≠
0
∧
2
∈
ℂ
∧
2
≠
0
→
1
−
cos
A
2
1
+
cos
A
2
=
1
−
cos
A
1
+
cos
A
191
189
190
mp3an3
⊢
1
−
cos
A
∈
ℂ
∧
1
+
cos
A
∈
ℂ
∧
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
∈
0
π
→
1
−
cos
A
2
1
+
cos
A
2
=
1
−
cos
A
1
+
cos
A
193
192
fveq2d
π
⊢
A
∈
0
π
→
1
−
cos
A
2
1
+
cos
A
2
=
1
−
cos
A
1
+
cos
A
194
97
183
193
3eqtr2d
π
⊢
A
∈
0
π
→
tan
A
2
=
1
−
cos
A
1
+
cos
A