acosrecl

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

		Ref	Expression
	Assertion	acosrecl	$⊢ A \in [- 1, 1] \to arccos (A) \in ℝ$

Step	Hyp	Ref	Expression
1		neg1rr	$⊢ - 1 \in ℝ$
2		1re	$⊢ 1 \in ℝ$
3		iccssre	$⊢ (- 1 \in ℝ \land 1 \in ℝ) \to [- 1, 1] \subseteq ℝ$
4	1 2 3	mp2an	$⊢ [- 1, 1] \subseteq ℝ$
5	4	sseli	$⊢ A \in [- 1, 1] \to A \in ℝ$
6	5	recnd	$⊢ A \in [- 1, 1] \to A \in ℂ$
7		acosval	$⊢ A \in ℂ \to arccos (A) = (\frac{π}{2}) - arcsin (A)$
8	6 7	syl	$⊢ A \in [- 1, 1] \to arccos (A) = (\frac{π}{2}) - arcsin (A)$
9		halfpire	$⊢ \frac{π}{2} \in ℝ$
10		asinrecl	$⊢ A \in [- 1, 1] \to arcsin (A) \in ℝ$
11		resubcl	$⊢ (\frac{π}{2} \in ℝ \land arcsin (A) \in ℝ) \to (\frac{π}{2}) - arcsin (A) \in ℝ$
12	9 10 11	sylancr	$⊢ A \in [- 1, 1] \to (\frac{π}{2}) - arcsin (A) \in ℝ$
13	8 12	eqeltrd	$⊢ A \in [- 1, 1] \to arccos (A) \in ℝ$

Metamath Proof Explorer