Metamath Proof Explorer


Theorem atanord

Description: The arctangent function is strictly increasing. (Contributed by Mario Carneiro, 5-Apr-2015)

Ref Expression
Assertion atanord ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( arctan ‘ 𝐴 ) < ( arctan ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 atanbnd ( 𝐴 ∈ ℝ → ( arctan ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
2 atanbnd ( 𝐵 ∈ ℝ → ( arctan ‘ 𝐵 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
3 tanord ( ( ( arctan ‘ 𝐴 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ ( arctan ‘ 𝐵 ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( arctan ‘ 𝐴 ) < ( arctan ‘ 𝐵 ) ↔ ( tan ‘ ( arctan ‘ 𝐴 ) ) < ( tan ‘ ( arctan ‘ 𝐵 ) ) ) )
4 1 2 3 syl2an ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( arctan ‘ 𝐴 ) < ( arctan ‘ 𝐵 ) ↔ ( tan ‘ ( arctan ‘ 𝐴 ) ) < ( tan ‘ ( arctan ‘ 𝐵 ) ) ) )
5 atanre ( 𝐴 ∈ ℝ → 𝐴 ∈ dom arctan )
6 tanatan ( 𝐴 ∈ dom arctan → ( tan ‘ ( arctan ‘ 𝐴 ) ) = 𝐴 )
7 5 6 syl ( 𝐴 ∈ ℝ → ( tan ‘ ( arctan ‘ 𝐴 ) ) = 𝐴 )
8 atanre ( 𝐵 ∈ ℝ → 𝐵 ∈ dom arctan )
9 tanatan ( 𝐵 ∈ dom arctan → ( tan ‘ ( arctan ‘ 𝐵 ) ) = 𝐵 )
10 8 9 syl ( 𝐵 ∈ ℝ → ( tan ‘ ( arctan ‘ 𝐵 ) ) = 𝐵 )
11 7 10 breqan12d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( tan ‘ ( arctan ‘ 𝐴 ) ) < ( tan ‘ ( arctan ‘ 𝐵 ) ) ↔ 𝐴 < 𝐵 ) )
12 4 11 bitr2d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( arctan ‘ 𝐴 ) < ( arctan ‘ 𝐵 ) ) )