acosf

Description: Domain and codoamin of the arccos function. (Contributed by Mario Carneiro, 31-Mar-2015)

		Ref	Expression
	Assertion	acosf	$⊢ arccos : ℂ ⟶ ℂ$

Step	Hyp	Ref	Expression
1		df-acos	$⊢ arccos = (x \in ℂ ⟼ (\frac{π}{2}) - arcsin (x))$
2		picn	$⊢ π \in ℂ$
3		halfcl	$⊢ π \in ℂ \to \frac{π}{2} \in ℂ$
4	2 3	ax-mp	$⊢ \frac{π}{2} \in ℂ$
5		asincl	$⊢ x \in ℂ \to arcsin (x) \in ℂ$
6		subcl	$⊢ (\frac{π}{2} \in ℂ \land arcsin (x) \in ℂ) \to (\frac{π}{2}) - arcsin (x) \in ℂ$
7	4 5 6	sylancr	$⊢ x \in ℂ \to (\frac{π}{2}) - arcsin (x) \in ℂ$
8	1 7	fmpti	$⊢ arccos : ℂ ⟶ ℂ$

Metamath Proof Explorer