Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jim Kingdon
Circle constant
taupilem3
Next ⟩
taupilemrplb
Metamath Proof Explorer
Ascii
Unicode
Theorem
taupilem3
Description:
Lemma for tau-related theorems.
(Contributed by
Jim Kingdon
, 16-Feb-2019)
Ref
Expression
Assertion
taupilem3
⊢
A
∈
ℝ
+
∩
cos
-1
1
↔
A
∈
ℝ
+
∧
cos
⁡
A
=
1
Proof
Step
Hyp
Ref
Expression
1
elin
⊢
A
∈
ℝ
+
∩
cos
-1
1
↔
A
∈
ℝ
+
∧
A
∈
cos
-1
1
2
cosf
⊢
cos
:
ℂ
⟶
ℂ
3
ffn
⊢
cos
:
ℂ
⟶
ℂ
→
cos
Fn
ℂ
4
fniniseg
⊢
cos
Fn
ℂ
→
A
∈
cos
-1
1
↔
A
∈
ℂ
∧
cos
⁡
A
=
1
5
2
3
4
mp2b
⊢
A
∈
cos
-1
1
↔
A
∈
ℂ
∧
cos
⁡
A
=
1
6
rpcn
⊢
A
∈
ℝ
+
→
A
∈
ℂ
7
6
biantrurd
⊢
A
∈
ℝ
+
→
cos
⁡
A
=
1
↔
A
∈
ℂ
∧
cos
⁡
A
=
1
8
5
7
bitr4id
⊢
A
∈
ℝ
+
→
A
∈
cos
-1
1
↔
cos
⁡
A
=
1
9
8
pm5.32i
⊢
A
∈
ℝ
+
∧
A
∈
cos
-1
1
↔
A
∈
ℝ
+
∧
cos
⁡
A
=
1
10
1
9
bitri
⊢
A
∈
ℝ
+
∩
cos
-1
1
↔
A
∈
ℝ
+
∧
cos
⁡
A
=
1