Database
BASIC REAL AND COMPLEX FUNCTIONS
Basic trigonometry
Inverse trigonometric functions
acos1
Next ⟩
reasinsin
Metamath Proof Explorer
Ascii
Unicode
Theorem
acos1
Description:
The arccosine of
1
is
0
.
(Contributed by
Mario Carneiro
, 2-Apr-2015)
Ref
Expression
Assertion
acos1
⊢
arccos
⁡
1
=
0
Proof
Step
Hyp
Ref
Expression
1
ax-1cn
⊢
1
∈
ℂ
2
acosval
⊢
1
∈
ℂ
→
arccos
⁡
1
=
π
2
−
arcsin
⁡
1
3
1
2
ax-mp
⊢
arccos
⁡
1
=
π
2
−
arcsin
⁡
1
4
asin1
⊢
arcsin
⁡
1
=
π
2
5
4
oveq2i
⊢
π
2
−
arcsin
⁡
1
=
π
2
−
π
2
6
picn
⊢
π
∈
ℂ
7
halfcl
⊢
π
∈
ℂ
→
π
2
∈
ℂ
8
6
7
ax-mp
⊢
π
2
∈
ℂ
9
8
subidi
⊢
π
2
−
π
2
=
0
10
3
5
9
3eqtri
⊢
arccos
⁡
1
=
0