acosneg

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

		Ref	Expression
	Assertion	acosneg	$⊢ A \in ℂ \to arccos (- A) = π - arccos (A)$

Proof

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

Metamath Proof Explorer

Theorem acosneg

Proof