Metamath Proof Explorer


Theorem acosneg

Description: The negative symmetry relation of the arccosine. (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Assertion acosneg A arccos A = π arccos A

Proof

Step Hyp Ref Expression
1 picn π
2 halfcl π π 2
3 1 2 ax-mp π 2
4 asincl A arcsin A
5 subneg π 2 arcsin A π 2 arcsin A = π 2 + arcsin A
6 3 4 5 sylancr A π 2 arcsin A = π 2 + arcsin A
7 asinneg A arcsin A = arcsin A
8 7 oveq2d A π 2 arcsin A = π 2 arcsin A
9 1 a1i A π
10 3 a1i A π 2
11 9 10 4 subsubd A π π 2 arcsin A = π - π 2 + arcsin A
12 pidiv2halves π 2 + π 2 = π
13 1 3 3 12 subaddrii π π 2 = π 2
14 13 oveq1i π - π 2 + arcsin A = π 2 + arcsin A
15 11 14 eqtrdi A π π 2 arcsin A = π 2 + arcsin A
16 6 8 15 3eqtr4d A π 2 arcsin A = π π 2 arcsin A
17 negcl A A
18 acosval A arccos A = π 2 arcsin A
19 17 18 syl A arccos A = π 2 arcsin A
20 acosval A arccos A = π 2 arcsin A
21 20 oveq2d A π arccos A = π π 2 arcsin A
22 16 19 21 3eqtr4d A arccos A = π arccos A