Theorem xlenegcon2

Description: Extended real version of lenegcon2 . (Contributed by Glauco Siliprandi, 23-Apr-2023)

	Ref	Expression
Assertion	xlenegcon2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ≤ -𝑒 𝐵 ↔ 𝐵 ≤ -𝑒 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		xnegcl	⊢ ( 𝐵 ∈ ℝ* → -𝑒 𝐵 ∈ ℝ* )
2		xleneg	⊢ ( ( 𝐴 ∈ ℝ* ∧ -𝑒 𝐵 ∈ ℝ* ) → ( 𝐴 ≤ -𝑒 𝐵 ↔ -𝑒 -𝑒 𝐵 ≤ -𝑒 𝐴 ) )
3	1 2	sylan2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ≤ -𝑒 𝐵 ↔ -𝑒 -𝑒 𝐵 ≤ -𝑒 𝐴 ) )
4		xnegneg	⊢ ( 𝐵 ∈ ℝ* → -𝑒 -𝑒 𝐵 = 𝐵 )
5	4	breq1d	⊢ ( 𝐵 ∈ ℝ* → ( -𝑒 -𝑒 𝐵 ≤ -𝑒 𝐴 ↔ 𝐵 ≤ -𝑒 𝐴 ) )
6	5	adantl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( -𝑒 -𝑒 𝐵 ≤ -𝑒 𝐴 ↔ 𝐵 ≤ -𝑒 𝐴 ) )
7	3 6	bitrd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ≤ -𝑒 𝐵 ↔ 𝐵 ≤ -𝑒 𝐴 ) )