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

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 ↔ -𝑒 𝐵 < -𝑒 𝐴 ) )