Theorem 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 \mathrm{dom}arctan$$

Proof

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\le A^2$$
9	3 4 5 7 8	ltletrd	$$⊢A\in ℝ\to -1<A^2$$
10	3 9	gtned	$$⊢A\in ℝ\to A^2\ne -1$$
11		atandm3	$$⊢A\in \mathrm{dom}arctan\leftrightarrow \left(A\in ℂ\wedge A^2\ne -1\right)$$
12	1 10 11	sylanbrc	$$⊢A\in ℝ\to A\in \mathrm{dom}arctan$$