Metamath Proof Explorer

Theorem acosneg

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

Ref Expression
Assertion acosneg ( 𝐴 ∈ ℂ → ( arccos ‘ - 𝐴 ) = ( π − ( arccos ‘ 𝐴 ) ) )

Proof

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