This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	bitrid	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝐴 ≤ 𝐵 ↔ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ^◡ < ) )
10		df-br	⊢ ( 𝐵 < 𝐴 ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ < )
11		opelcnvg	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ^◡ < ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ < ) )
12	10 11	bitr4id	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝐵 < 𝐴 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ^◡ < ) )
13	12	notbid	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( ¬ 𝐵 < 𝐴 ↔ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ^◡ < ) )
14	9 13	bitr4d	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) )