atanord

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

		Ref	Expression
	Assertion	atanord	$⊢ (A \in ℝ \land B \in ℝ) \to (A < B \leftrightarrow arctan (A) < arctan (B))$

Step	Hyp	Ref	Expression
1		atanbnd	$⊢ A \in ℝ \to arctan (A) \in (- \frac{π}{2}, \frac{π}{2})$
2		atanbnd	$⊢ B \in ℝ \to arctan (B) \in (- \frac{π}{2}, \frac{π}{2})$
3		tanord	$⊢ (arctan (A) \in (- \frac{π}{2}, \frac{π}{2}) \land arctan (B) \in (- \frac{π}{2}, \frac{π}{2})) \to (arctan (A) < arctan (B) \leftrightarrow \tan arctan (A) < \tan arctan (B))$
4	1 2 3	syl2an	$⊢ (A \in ℝ \land B \in ℝ) \to (arctan (A) < arctan (B) \leftrightarrow \tan arctan (A) < \tan arctan (B))$
5		atanre	$⊢ A \in ℝ \to A \in dom arctan$
6		tanatan	$⊢ A \in dom arctan \to \tan arctan (A) = A$
7	5 6	syl	$⊢ A \in ℝ \to \tan arctan (A) = A$
8		atanre	$⊢ B \in ℝ \to B \in dom arctan$
9		tanatan	$⊢ B \in dom arctan \to \tan arctan (B) = B$
10	8 9	syl	$⊢ B \in ℝ \to \tan arctan (B) = B$
11	7 10	breqan12d	$⊢ (A \in ℝ \land B \in ℝ) \to (\tan arctan (A) < \tan arctan (B) \leftrightarrow A < B)$
12	4 11	bitr2d	$⊢ (A \in ℝ \land B \in ℝ) \to (A < B \leftrightarrow arctan (A) < arctan (B))$

Metamath Proof Explorer