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