Metamath Proof Explorer

Theorem atanord

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

Ref Expression
Assertion atanord ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ arctan ⁡ A < arctan ⁡ B

Proof

Step Hyp Ref Expression
1 atanbnd ⊢ A ∈ ℝ → arctan ⁡ A ∈ − π 2 π 2
2 atanbnd ⊢ B ∈ ℝ → arctan ⁡ B ∈ − π 2 π 2
3 tanord ⊢ arctan ⁡ A ∈ − π 2 π 2 ∧ arctan ⁡ B ∈ − π 2 π 2 → arctan ⁡ A < arctan ⁡ B ↔ tan ⁡ arctan ⁡ A < tan ⁡ arctan ⁡ B
4 1 2 3 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → arctan ⁡ A < arctan ⁡ B ↔ tan ⁡ arctan ⁡ A < tan ⁡ arctan ⁡ B
5 atanre ⊢ A ∈ ℝ → A ∈ dom ⁡ arctan
6 tanatan ⊢ A ∈ dom ⁡ arctan → tan ⁡ arctan ⁡ A = A
7 5 6 syl ⊢ A ∈ ℝ → tan ⁡ arctan ⁡ A = A
8 atanre ⊢ B ∈ ℝ → B ∈ dom ⁡ arctan
9 tanatan ⊢ B ∈ dom ⁡ arctan → tan ⁡ arctan ⁡ B = B
10 8 9 syl ⊢ B ∈ ℝ → tan ⁡ arctan ⁡ B = B
11 7 10 breqan12d ⊢ A ∈ ℝ ∧ B ∈ ℝ → tan ⁡ arctan ⁡ A < tan ⁡ arctan ⁡ B ↔ A < B
12 4 11 bitr2d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ arctan ⁡ A < arctan ⁡ B