Description: A number is less than or equal to the maximum of it and another. This version of max1 omits the B e. RR antecedent. Although it doesn't exploit undefined behavior, it is still considered poor style, and the use of max1 is preferred. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by NM, 3-Apr-2005)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | max1ALT | ⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | leid | ⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ 𝐴 ) | |
| 2 | iffalse | ⊢ ( ¬ 𝐴 ≤ 𝐵 → if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) = 𝐴 ) | |
| 3 | 2 | breq2d | ⊢ ( ¬ 𝐴 ≤ 𝐵 → ( 𝐴 ≤ if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) ↔ 𝐴 ≤ 𝐴 ) ) |
| 4 | 1 3 | syl5ibrcom | ⊢ ( 𝐴 ∈ ℝ → ( ¬ 𝐴 ≤ 𝐵 → 𝐴 ≤ if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) ) ) |
| 5 | id | ⊢ ( 𝐴 ≤ 𝐵 → 𝐴 ≤ 𝐵 ) | |
| 6 | iftrue | ⊢ ( 𝐴 ≤ 𝐵 → if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) = 𝐵 ) | |
| 7 | 5 6 | breqtrrd | ⊢ ( 𝐴 ≤ 𝐵 → 𝐴 ≤ if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) ) |
| 8 | 4 7 | pm2.61d2 | ⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ if ( 𝐴 ≤ 𝐵 , 𝐵 , 𝐴 ) ) |