Theorem xrlenlt

Description: "Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by NM, 14-Oct-2005)

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

Proof

Step	Hyp	Ref	Expression
1		df-br	⊢ ( 𝐴 ≤ 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ≤ )
2		opelxpi	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ℝ* × ℝ* ) )
3		df-le	⊢ ≤ = ( ( ℝ* × ℝ* ) ∖ ◡ < )
4	3	eleq2i	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ≤ ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( ℝ* × ℝ* ) ∖ ◡ < ) )
5		eldif	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( ℝ* × ℝ* ) ∖ ◡ < ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ℝ* × ℝ* ) ∧ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ < ) )
6	4 5	bitri	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ≤ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ℝ* × ℝ* ) ∧ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ < ) )
7	6	baib	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ℝ* × ℝ* ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ≤ ↔ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ < ) )
8	2 7	syl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ≤ ↔ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ < ) )
9	1 8	syl5bb	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ≤ 𝐵 ↔ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ < ) )
10		opelcnvg	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ < ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ < ) )
11		df-br	⊢ ( 𝐵 < 𝐴 ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ < )
12	10 11	syl6rbbr	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐵 < 𝐴 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ < ) )
13	12	notbid	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ¬ 𝐵 < 𝐴 ↔ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ < ) )
14	9 13	bitr4d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) )