Step |
Hyp |
Ref |
Expression |
1 |
|
xltneg |
⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 𝐵 < 𝐴 ↔ -𝑒 𝐴 < -𝑒 𝐵 ) ) |
2 |
1
|
ancoms |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐵 < 𝐴 ↔ -𝑒 𝐴 < -𝑒 𝐵 ) ) |
3 |
2
|
notbid |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ¬ 𝐵 < 𝐴 ↔ ¬ -𝑒 𝐴 < -𝑒 𝐵 ) ) |
4 |
|
xrlenlt |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) ) |
5 |
|
xnegcl |
⊢ ( 𝐵 ∈ ℝ* → -𝑒 𝐵 ∈ ℝ* ) |
6 |
|
xnegcl |
⊢ ( 𝐴 ∈ ℝ* → -𝑒 𝐴 ∈ ℝ* ) |
7 |
|
xrlenlt |
⊢ ( ( -𝑒 𝐵 ∈ ℝ* ∧ -𝑒 𝐴 ∈ ℝ* ) → ( -𝑒 𝐵 ≤ -𝑒 𝐴 ↔ ¬ -𝑒 𝐴 < -𝑒 𝐵 ) ) |
8 |
5 6 7
|
syl2anr |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( -𝑒 𝐵 ≤ -𝑒 𝐴 ↔ ¬ -𝑒 𝐴 < -𝑒 𝐵 ) ) |
9 |
3 4 8
|
3bitr4d |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ≤ 𝐵 ↔ -𝑒 𝐵 ≤ -𝑒 𝐴 ) ) |