Metamath Proof Explorer


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