Metamath Proof Explorer


Theorem cosacos

Description: The arccosine function is an inverse to cos . (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion cosacos A cos arccos A = A

Proof

Step Hyp Ref Expression
1 acosval A arccos A = π 2 arcsin A
2 1 fveq2d A cos arccos A = cos π 2 arcsin A
3 asincl A arcsin A
4 coshalfpim arcsin A cos π 2 arcsin A = sin arcsin A
5 3 4 syl A cos π 2 arcsin A = sin arcsin A
6 sinasin A sin arcsin A = A
7 2 5 6 3eqtrd A cos arccos A = A