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 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A < B ↔ − B < − A

Proof

Step Hyp Ref Expression
1 xltnegi ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A < B → − B < − A
2 1 3expia ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A < B → − B < − A
3 xnegcl ⊢ B ∈ ℝ * → − B ∈ ℝ *
4 xnegcl ⊢ A ∈ ℝ * → − A ∈ ℝ *
5 xltnegi ⊢ − B ∈ ℝ * ∧ − A ∈ ℝ * ∧ − B < − A → − − A < − − B
6 5 3expia ⊢ − B ∈ ℝ * ∧ − A ∈ ℝ * → − B < − A → − − A < − − B
7 3 4 6 syl2anr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → − B < − A → − − A < − − B
8 xnegneg ⊢ A ∈ ℝ * → − − A = A
9 xnegneg ⊢ B ∈ ℝ * → − − B = B
10 8 9 breqan12d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → − − A < − − B ↔ A < B
11 7 10 sylibd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → − B < − A → A < B
12 2 11 impbid ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A < B ↔ − B < − A