acos1

Description: The arccosine of 1 is 0 . (Contributed by Mario Carneiro, 2-Apr-2015)

		Ref	Expression
	Assertion	acos1	$⊢ arccos (1) = 0$

Step	Hyp	Ref	Expression
1		ax-1cn	$⊢ 1 \in ℂ$
2		acosval	$⊢ 1 \in ℂ \to arccos (1) = (\frac{π}{2}) - arcsin (1)$
3	1 2	ax-mp	$⊢ arccos (1) = (\frac{π}{2}) - arcsin (1)$
4		asin1	$⊢ arcsin (1) = \frac{π}{2}$
5	4	oveq2i	$⊢ (\frac{π}{2}) - arcsin (1) = (\frac{π}{2}) - (\frac{π}{2})$
6		picn	$⊢ π \in ℂ$
7		halfcl	$⊢ π \in ℂ \to \frac{π}{2} \in ℂ$
8	6 7	ax-mp	$⊢ \frac{π}{2} \in ℂ$
9	8	subidi	$⊢ (\frac{π}{2}) - (\frac{π}{2}) = 0$
10	3 5 9	3eqtri	$⊢ arccos (1) = 0$

Metamath Proof Explorer