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

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 ‘ 𝐵 ) ) )