Theorem ltnltne

Description: Variant of trichotomy law for 'less than'. (Contributed by Alexander van der Vekens, 8-Jun-2018)

	Ref	Expression
Assertion	ltnltne	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( ¬ 𝐵 < 𝐴 ∧ ¬ 𝐵 = 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ltnle	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴 ) )
2		leloe	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 ≤ 𝐴 ↔ ( 𝐵 < 𝐴 ∨ 𝐵 = 𝐴 ) ) )
3	2	ancoms	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 ≤ 𝐴 ↔ ( 𝐵 < 𝐴 ∨ 𝐵 = 𝐴 ) ) )
4	3	notbid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ¬ 𝐵 ≤ 𝐴 ↔ ¬ ( 𝐵 < 𝐴 ∨ 𝐵 = 𝐴 ) ) )
5		ioran	⊢ ( ¬ ( 𝐵 < 𝐴 ∨ 𝐵 = 𝐴 ) ↔ ( ¬ 𝐵 < 𝐴 ∧ ¬ 𝐵 = 𝐴 ) )
6	5	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ¬ ( 𝐵 < 𝐴 ∨ 𝐵 = 𝐴 ) ↔ ( ¬ 𝐵 < 𝐴 ∧ ¬ 𝐵 = 𝐴 ) ) )
7	1 4 6	3bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( ¬ 𝐵 < 𝐴 ∧ ¬ 𝐵 = 𝐴 ) ) )