Theorem ltlen

Description: 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 27-Oct-1999)

	Ref	Expression
Assertion	ltlen	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ltle	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 → 𝐴 ≤ 𝐵 ) )
2		ltne	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐵 ≠ 𝐴 )
3	2	ex	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < 𝐵 → 𝐵 ≠ 𝐴 ) )
4	3	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 → 𝐵 ≠ 𝐴 ) )
5	1 4	jcad	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 → ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴 ) ) )
6		leloe	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ) ) )
7		df-ne	⊢ ( 𝐵 ≠ 𝐴 ↔ ¬ 𝐵 = 𝐴 )
8		pm2.24	⊢ ( 𝐵 = 𝐴 → ( ¬ 𝐵 = 𝐴 → 𝐴 < 𝐵 ) )
9	8	eqcoms	⊢ ( 𝐴 = 𝐵 → ( ¬ 𝐵 = 𝐴 → 𝐴 < 𝐵 ) )
10	7 9	syl5bi	⊢ ( 𝐴 = 𝐵 → ( 𝐵 ≠ 𝐴 → 𝐴 < 𝐵 ) )
11	10	jao1i	⊢ ( ( 𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ) → ( 𝐵 ≠ 𝐴 → 𝐴 < 𝐵 ) )
12	6 11	syl6bi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 → ( 𝐵 ≠ 𝐴 → 𝐴 < 𝐵 ) ) )
13	12	impd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴 ) → 𝐴 < 𝐵 ) )
14	5 13	impbid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴 ) ) )