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 ⊢ A ∈ − 1 1 → arccos ⁡ A ∈ ℝ

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 ⊢ A ∈ − 1 1 → A ∈ ℝ
6 5 recnd ⊢ A ∈ − 1 1 → A ∈ ℂ
7 acosval ⊢ A ∈ ℂ → arccos ⁡ A = π 2 − arcsin ⁡ A
8 6 7 syl ⊢ A ∈ − 1 1 → arccos ⁡ A = π 2 − arcsin ⁡ A
9 halfpire ⊢ π 2 ∈ ℝ
10 asinrecl ⊢ A ∈ − 1 1 → arcsin ⁡ A ∈ ℝ
11 resubcl ⊢ π 2 ∈ ℝ ∧ arcsin ⁡ A ∈ ℝ → π 2 − arcsin ⁡ A ∈ ℝ
12 9 10 11 sylancr ⊢ A ∈ − 1 1 → π 2 − arcsin ⁡ A ∈ ℝ
13 8 12 eqeltrd ⊢ A ∈ − 1 1 → arccos ⁡ A ∈ ℝ