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

Metamath Proof Explorer

Theorem xleneg

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

Ref Expression
Assertion xleneg ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ B ↔ − B ≤ − A

Proof

Step Hyp Ref Expression
1 xltneg ⊢ B ∈ ℝ * ∧ A ∈ ℝ * → B < A ↔ − A < − B
2 1 ancoms ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → B < A ↔ − A < − B
3 2 notbid ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → ¬ B < A ↔ ¬ − A < − B
4 xrlenlt ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ B ↔ ¬ B < A
5 xnegcl ⊢ B ∈ ℝ * → − B ∈ ℝ *
6 xnegcl ⊢ A ∈ ℝ * → − A ∈ ℝ *
7 xrlenlt ⊢ − B ∈ ℝ * ∧ − A ∈ ℝ * → − B ≤ − A ↔ ¬ − A < − B
8 5 6 7 syl2anr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → − B ≤ − A ↔ ¬ − A < − B
9 3 4 8 3bitr4d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ B ↔ − B ≤ − A