Theorem acosf

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

	Ref	Expression
Assertion	acosf	⊢ arccos : ℂ ⟶ ℂ

Proof

Step	Hyp	Ref	Expression
1		df-acos	⊢ arccos = ( 𝑥 ∈ ℂ ↦ ( ( π / 2 ) − ( arcsin ‘ 𝑥 ) ) )
2		picn	⊢ π ∈ ℂ
3		halfcl	⊢ ( π ∈ ℂ → ( π / 2 ) ∈ ℂ )
4	2 3	ax-mp	⊢ ( π / 2 ) ∈ ℂ
5		asincl	⊢ ( 𝑥 ∈ ℂ → ( arcsin ‘ 𝑥 ) ∈ ℂ )
6		subcl	⊢ ( ( ( π / 2 ) ∈ ℂ ∧ ( arcsin ‘ 𝑥 ) ∈ ℂ ) → ( ( π / 2 ) − ( arcsin ‘ 𝑥 ) ) ∈ ℂ )
7	4 5 6	sylancr	⊢ ( 𝑥 ∈ ℂ → ( ( π / 2 ) − ( arcsin ‘ 𝑥 ) ) ∈ ℂ )
8	1 7	fmpti	⊢ arccos : ℂ ⟶ ℂ