atanre

Description: A real number is in the domain of the arctangent function. (Contributed by Mario Carneiro, 31-Mar-2015)

		Ref	Expression
	Assertion	atanre	$⊢ A \in ℝ \to A \in dom arctan$

Step	Hyp	Ref	Expression
1		recn	$⊢ A \in ℝ \to A \in ℂ$
2		neg1rr	$⊢ - 1 \in ℝ$
3	2	a1i	$⊢ A \in ℝ \to - 1 \in ℝ$
4		0red	$⊢ A \in ℝ \to 0 \in ℝ$
5		resqcl	$⊢ A \in ℝ \to A^{2} \in ℝ$
6		neg1lt0	$⊢ - 1 < 0$
7	6	a1i	$⊢ A \in ℝ \to - 1 < 0$
8		sqge0	$⊢ A \in ℝ \to 0 \leq A^{2}$
9	3 4 5 7 8	ltletrd	$⊢ A \in ℝ \to - 1 < A^{2}$
10	3 9	gtned	$⊢ A \in ℝ \to A^{2} \neq - 1$
11		atandm3	$⊢ A \in dom arctan \leftrightarrow (A \in ℂ \land A^{2} \neq - 1)$
12	1 10 11	sylanbrc	$⊢ A \in ℝ \to A \in dom arctan$

Metamath Proof Explorer