Theorem acosrecl

Description: The arccosine function is real in its principal domain. (Contributed by Mario Carneiro, 2-Apr-2015)

	Ref	Expression
Assertion	acosrecl	⊢ ( 𝐴 ∈ ( - 1 [,] 1 ) → ( arccos ‘ 𝐴 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		neg1rr	⊢ - 1 ∈ ℝ
2		1re	⊢ 1 ∈ ℝ
3		iccssre	⊢ ( ( - 1 ∈ ℝ ∧ 1 ∈ ℝ ) → ( - 1 [,] 1 ) ⊆ ℝ )
4	1 2 3	mp2an	⊢ ( - 1 [,] 1 ) ⊆ ℝ
5	4	sseli	⊢ ( 𝐴 ∈ ( - 1 [,] 1 ) → 𝐴 ∈ ℝ )
6	5	recnd	⊢ ( 𝐴 ∈ ( - 1 [,] 1 ) → 𝐴 ∈ ℂ )
7		acosval	⊢ ( 𝐴 ∈ ℂ → ( arccos ‘ 𝐴 ) = ( ( π / 2 ) − ( arcsin ‘ 𝐴 ) ) )
8	6 7	syl	⊢ ( 𝐴 ∈ ( - 1 [,] 1 ) → ( arccos ‘ 𝐴 ) = ( ( π / 2 ) − ( arcsin ‘ 𝐴 ) ) )
9		halfpire	⊢ ( π / 2 ) ∈ ℝ
10		asinrecl	⊢ ( 𝐴 ∈ ( - 1 [,] 1 ) → ( arcsin ‘ 𝐴 ) ∈ ℝ )
11		resubcl	⊢ ( ( ( π / 2 ) ∈ ℝ ∧ ( arcsin ‘ 𝐴 ) ∈ ℝ ) → ( ( π / 2 ) − ( arcsin ‘ 𝐴 ) ) ∈ ℝ )
12	9 10 11	sylancr	⊢ ( 𝐴 ∈ ( - 1 [,] 1 ) → ( ( π / 2 ) − ( arcsin ‘ 𝐴 ) ) ∈ ℝ )
13	8 12	eqeltrd	⊢ ( 𝐴 ∈ ( - 1 [,] 1 ) → ( arccos ‘ 𝐴 ) ∈ ℝ )