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