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

Metamath Proof Explorer

Theorem xrmin1

Description: The minimum of two extended reals is less than or equal to one of them. (Contributed by NM, 7-Feb-2007)

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

Proof

Step Hyp Ref Expression
1 iftrue ⊢ A ≤ B → if A ≤ B A B = A
2 1 adantl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A ≤ B → if A ≤ B A B = A
3 xrleid ⊢ A ∈ ℝ * → A ≤ A
4 3 ad2antrr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A ≤ B → A ≤ A
5 2 4 eqbrtrd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A ≤ B → if A ≤ B A B ≤ A
6 iffalse ⊢ ¬ A ≤ B → if A ≤ B A B = B
7 6 adantl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ ¬ A ≤ B → if A ≤ B A B = B
8 xrletri ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ B ∨ B ≤ A
9 8 orcanai ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ ¬ A ≤ B → B ≤ A
10 7 9 eqbrtrd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ ¬ A ≤ B → if A ≤ B A B ≤ A
11 5 10 pm2.61dan ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → if A ≤ B A B ≤ A