Metamath Proof Explorer

Theorem lemaxle

Description: A real number which is less than or equal to a second real number is less than or equal to the maximum/supremum of the second real number and a third real number. (Contributed by AV, 8-Jun-2021)

Ref Expression
Assertion lemaxle ⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ A ∈ ℝ ∧ A ≤ B → A ≤ if C ≤ B B C

Proof

Step Hyp Ref Expression
1 max2 ⊢ C ∈ ℝ ∧ B ∈ ℝ → B ≤ if C ≤ B B C
2 1 ancoms ⊢ B ∈ ℝ ∧ C ∈ ℝ → B ≤ if C ≤ B B C
3 2 adantr ⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ A ∈ ℝ → B ≤ if C ≤ B B C
4 simpr ⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ A ∈ ℝ → A ∈ ℝ
5 simpll ⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ A ∈ ℝ → B ∈ ℝ
6 ifcl ⊢ B ∈ ℝ ∧ C ∈ ℝ → if C ≤ B B C ∈ ℝ
7 6 adantr ⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ A ∈ ℝ → if C ≤ B B C ∈ ℝ
8 letr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ if C ≤ B B C ∈ ℝ → A ≤ B ∧ B ≤ if C ≤ B B C → A ≤ if C ≤ B B C
9 4 5 7 8 syl3anc ⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ A ∈ ℝ → A ≤ B ∧ B ≤ if C ≤ B B C → A ≤ if C ≤ B B C
10 3 9 mpan2d ⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ A ∈ ℝ → A ≤ B → A ≤ if C ≤ B B C
11 10 3impia ⊢ B ∈ ℝ ∧ C ∈ ℝ ∧ A ∈ ℝ ∧ A ≤ B → A ≤ if C ≤ B B C