Theorem atanrecl

Description: The arctangent function is real for all real inputs. (Contributed by Mario Carneiro, 31-Mar-2015)

	Ref	Expression
Assertion	atanrecl	⊢ ( 𝐴 ∈ ℝ → ( arctan ‘ 𝐴 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 0 ) → 𝐴 = 0 )
2	1	fveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 0 ) → ( arctan ‘ 𝐴 ) = ( arctan ‘ 0 ) )
3		atan0	⊢ ( arctan ‘ 0 ) = 0
4		0re	⊢ 0 ∈ ℝ
5	3 4	eqeltri	⊢ ( arctan ‘ 0 ) ∈ ℝ
6	2 5	eqeltrdi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 0 ) → ( arctan ‘ 𝐴 ) ∈ ℝ )
7		atanre	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ dom arctan )
8	7	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ dom arctan )
9		atancl	⊢ ( 𝐴 ∈ dom arctan → ( arctan ‘ 𝐴 ) ∈ ℂ )
10	8 9	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( arctan ‘ 𝐴 ) ∈ ℂ )
11		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℝ )
12	11	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℂ )
13		rere	⊢ ( 𝐴 ∈ ℝ → ( ℜ ‘ 𝐴 ) = 𝐴 )
14	13	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ 𝐴 ) = 𝐴 )
15		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 𝐴 ≠ 0 )
16	14 15	eqnetrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ 𝐴 ) ≠ 0 )
17		atancj	⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 𝐴 ∈ dom arctan ∧ ( ∗ ‘ ( arctan ‘ 𝐴 ) ) = ( arctan ‘ ( ∗ ‘ 𝐴 ) ) ) )
18	12 16 17	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐴 ∈ dom arctan ∧ ( ∗ ‘ ( arctan ‘ 𝐴 ) ) = ( arctan ‘ ( ∗ ‘ 𝐴 ) ) ) )
19	18	simprd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ ( arctan ‘ 𝐴 ) ) = ( arctan ‘ ( ∗ ‘ 𝐴 ) ) )
20		cjre	⊢ ( 𝐴 ∈ ℝ → ( ∗ ‘ 𝐴 ) = 𝐴 )
21	20	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ 𝐴 ) = 𝐴 )
22	21	fveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( arctan ‘ ( ∗ ‘ 𝐴 ) ) = ( arctan ‘ 𝐴 ) )
23	19 22	eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ ( arctan ‘ 𝐴 ) ) = ( arctan ‘ 𝐴 ) )
24	10 23	cjrebd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( arctan ‘ 𝐴 ) ∈ ℝ )
25	6 24	pm2.61dane	⊢ ( 𝐴 ∈ ℝ → ( arctan ‘ 𝐴 ) ∈ ℝ )