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

Metamath Proof Explorer

Theorem xrmineq

Description: The minimum of two extended reals is equal to the second if the first is bigger. (Contributed by Mario Carneiro, 25-Mar-2015)

Ref Expression
Assertion xrmineq ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ B ≤ A → if A ≤ B A B = B

Proof

Step Hyp Ref Expression
1 xrletri3 ⊢ B ∈ ℝ * ∧ A ∈ ℝ * → B = A ↔ B ≤ A ∧ A ≤ B
2 1 ancoms ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → B = A ↔ B ≤ A ∧ A ≤ B
3 2 biimpar ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ B ≤ A ∧ A ≤ B → B = A
4 3 anassrs ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ B ≤ A ∧ A ≤ B → B = A
5 4 ifeq1da ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ B ≤ A → if A ≤ B B B = if A ≤ B A B
6 5 3impa ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ B ≤ A → if A ≤ B B B = if A ≤ B A B
7 ifid ⊢ if A ≤ B B B = B
8 6 7 eqtr3di ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ B ≤ A → if A ≤ B A B = B