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