This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐴 ) ∈ ℝ )