Theorem xrltlen

Description: 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 6-Nov-2015)

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

Proof

Step	Hyp	Ref	Expression
1		xrlttri	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) ) )
2		ioran	⊢ ( ¬ ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) ↔ ( ¬ 𝐴 = 𝐵 ∧ ¬ 𝐵 < 𝐴 ) )
3	2	biancomi	⊢ ( ¬ ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) ↔ ( ¬ 𝐵 < 𝐴 ∧ ¬ 𝐴 = 𝐵 ) )
4	1 3	bitrdi	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 ↔ ( ¬ 𝐵 < 𝐴 ∧ ¬ 𝐴 = 𝐵 ) ) )
5		xrlenlt	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) )
6		nesym	⊢ ( 𝐵 ≠ 𝐴 ↔ ¬ 𝐴 = 𝐵 )
7	6	a1i	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐵 ≠ 𝐴 ↔ ¬ 𝐴 = 𝐵 ) )
8	5 7	anbi12d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴 ) ↔ ( ¬ 𝐵 < 𝐴 ∧ ¬ 𝐴 = 𝐵 ) ) )
9	4 8	bitr4d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≠ 𝐴 ) ) )