Theorem xltneg

Description: Extended real version of ltneg . (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	xltneg	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 ↔ -e 𝐵 < -e 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		xltnegi	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → -e 𝐵 < -e 𝐴 )
2	1	3expia	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 → -e 𝐵 < -e 𝐴 ) )
3		xnegcl	⊢ ( 𝐵 ∈ ℝ* → -e 𝐵 ∈ ℝ* )
4		xnegcl	⊢ ( 𝐴 ∈ ℝ* → -e 𝐴 ∈ ℝ* )
5		xltnegi	⊢ ( ( -e 𝐵 ∈ ℝ* ∧ -e 𝐴 ∈ ℝ* ∧ -e 𝐵 < -e 𝐴 ) → -e -e 𝐴 < -e -e 𝐵 )
6	5	3expia	⊢ ( ( -e 𝐵 ∈ ℝ* ∧ -e 𝐴 ∈ ℝ* ) → ( -e 𝐵 < -e 𝐴 → -e -e 𝐴 < -e -e 𝐵 ) )
7	3 4 6	syl2anr	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( -e 𝐵 < -e 𝐴 → -e -e 𝐴 < -e -e 𝐵 ) )
8		xnegneg	⊢ ( 𝐴 ∈ ℝ* → -e -e 𝐴 = 𝐴 )
9		xnegneg	⊢ ( 𝐵 ∈ ℝ* → -e -e 𝐵 = 𝐵 )
10	8 9	breqan12d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( -e -e 𝐴 < -e -e 𝐵 ↔ 𝐴 < 𝐵 ) )
11	7 10	sylibd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( -e 𝐵 < -e 𝐴 → 𝐴 < 𝐵 ) )
12	2 11	impbid	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 ↔ -e 𝐵 < -e 𝐴 ) )