Theorem xlenegcon1

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

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

Proof

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