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 e. CC -> ( arccos ` -u A ) = ( _pi - ( arccos ` A ) ) )

Proof

Step Hyp Ref Expression
1 picn 
 |-  _pi e. CC
2 halfcl 
 |-  ( _pi e. CC -> ( _pi / 2 ) e. CC )
3 1 2 ax-mp 
 |-  ( _pi / 2 ) e. CC
4 asincl 
 |-  ( A e. CC -> ( arcsin ` A ) e. CC )
5 subneg 
 |-  ( ( ( _pi / 2 ) e. CC /\ ( arcsin ` A ) e. CC ) -> ( ( _pi / 2 ) - -u ( arcsin ` A ) ) = ( ( _pi / 2 ) + ( arcsin ` A ) ) )
6 3 4 5 sylancr 
 |-  ( A e. CC -> ( ( _pi / 2 ) - -u ( arcsin ` A ) ) = ( ( _pi / 2 ) + ( arcsin ` A ) ) )
7 asinneg 
 |-  ( A e. CC -> ( arcsin ` -u A ) = -u ( arcsin ` A ) )
8 7 oveq2d 
 |-  ( A e. CC -> ( ( _pi / 2 ) - ( arcsin ` -u A ) ) = ( ( _pi / 2 ) - -u ( arcsin ` A ) ) )
9 1 a1i 
 |-  ( A e. CC -> _pi e. CC )
10 3 a1i 
 |-  ( A e. CC -> ( _pi / 2 ) e. CC )
11 9 10 4 subsubd 
 |-  ( A e. CC -> ( _pi - ( ( _pi / 2 ) - ( arcsin ` A ) ) ) = ( ( _pi - ( _pi / 2 ) ) + ( arcsin ` A ) ) )
12 pidiv2halves 
 |-  ( ( _pi / 2 ) + ( _pi / 2 ) ) = _pi
13 1 3 3 12 subaddrii 
 |-  ( _pi - ( _pi / 2 ) ) = ( _pi / 2 )
14 13 oveq1i 
 |-  ( ( _pi - ( _pi / 2 ) ) + ( arcsin ` A ) ) = ( ( _pi / 2 ) + ( arcsin ` A ) )
15 11 14 eqtrdi 
 |-  ( A e. CC -> ( _pi - ( ( _pi / 2 ) - ( arcsin ` A ) ) ) = ( ( _pi / 2 ) + ( arcsin ` A ) ) )
16 6 8 15 3eqtr4d 
 |-  ( A e. CC -> ( ( _pi / 2 ) - ( arcsin ` -u A ) ) = ( _pi - ( ( _pi / 2 ) - ( arcsin ` A ) ) ) )
17 negcl 
 |-  ( A e. CC -> -u A e. CC )
18 acosval 
 |-  ( -u A e. CC -> ( arccos ` -u A ) = ( ( _pi / 2 ) - ( arcsin ` -u A ) ) )
19 17 18 syl 
 |-  ( A e. CC -> ( arccos ` -u A ) = ( ( _pi / 2 ) - ( arcsin ` -u A ) ) )
20 acosval 
 |-  ( A e. CC -> ( arccos ` A ) = ( ( _pi / 2 ) - ( arcsin ` A ) ) )
21 20 oveq2d 
 |-  ( A e. CC -> ( _pi - ( arccos ` A ) ) = ( _pi - ( ( _pi / 2 ) - ( arcsin ` A ) ) ) )
22 16 19 21 3eqtr4d 
 |-  ( A e. CC -> ( arccos ` -u A ) = ( _pi - ( arccos ` A ) ) )