Metamath Proof Explorer


Theorem acoscosb

Description: Relationship between cosine and arccosine. (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Assertion acoscosb A B B 0 π arccos A = B cos B = A

Proof

Step Hyp Ref Expression
1 cosacos A cos arccos A = A
2 1 3ad2ant1 A B B 0 π cos arccos A = A
3 fveqeq2 arccos A = B cos arccos A = A cos B = A
4 2 3 syl5ibcom A B B 0 π arccos A = B cos B = A
5 acoscos B B 0 π arccos cos B = B
6 5 3adant1 A B B 0 π arccos cos B = B
7 fveqeq2 cos B = A arccos cos B = B arccos A = B
8 6 7 syl5ibcom A B B 0 π cos B = A arccos A = B
9 4 8 impbid A B B 0 π arccos A = B cos B = A