This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐴 ) ∈ ℝ )