Theorem xltneg

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

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

Proof

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