Step |
Hyp |
Ref |
Expression |
1 |
|
xrlttri3 |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 = 𝐵 ↔ ( ¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴 ) ) ) |
2 |
|
simpl |
⊢ ( ( ¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴 ) → ¬ 𝐴 < 𝐵 ) |
3 |
1 2
|
syl6bi |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 = 𝐵 → ¬ 𝐴 < 𝐵 ) ) |
4 |
3
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 = 𝐵 → ¬ 𝐴 < 𝐵 ) ) |
5 |
|
xrleloe |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ) ) ) |
6 |
5
|
biimpa |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ) ) |
7 |
6
|
ord |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 ≤ 𝐵 ) → ( ¬ 𝐴 < 𝐵 → 𝐴 = 𝐵 ) ) |
8 |
4 7
|
impbid |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 = 𝐵 ↔ ¬ 𝐴 < 𝐵 ) ) |
9 |
8
|
necon2abid |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 < 𝐵 ↔ 𝐴 ≠ 𝐵 ) ) |
10 |
|
necom |
⊢ ( 𝐵 ≠ 𝐴 ↔ 𝐴 ≠ 𝐵 ) |
11 |
9 10
|
bitr4di |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 < 𝐵 ↔ 𝐵 ≠ 𝐴 ) ) |
12 |
11
|
3impa |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 < 𝐵 ↔ 𝐵 ≠ 𝐴 ) ) |