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	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ dom arctan )

Proof

Step	Hyp	Ref	Expression
1		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
2		neg1rr	⊢ - 1 ∈ ℝ
3	2	a1i	⊢ ( 𝐴 ∈ ℝ → - 1 ∈ ℝ )
4		0red	⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ )
5		resqcl	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ↑ 2 ) ∈ ℝ )
6		neg1lt0	⊢ - 1 < 0
7	6	a1i	⊢ ( 𝐴 ∈ ℝ → - 1 < 0 )
8		sqge0	⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( 𝐴 ↑ 2 ) )
9	3 4 5 7 8	ltletrd	⊢ ( 𝐴 ∈ ℝ → - 1 < ( 𝐴 ↑ 2 ) )
10	3 9	gtned	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ↑ 2 ) ≠ - 1 )
11		atandm3	⊢ ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ≠ - 1 ) )
12	1 10 11	sylanbrc	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ dom arctan )