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 | |- ( A e. RR -> A <_ if ( A <_ B , B , A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | leid | |- ( A e. RR -> A <_ A ) |
|
| 2 | iffalse | |- ( -. A <_ B -> if ( A <_ B , B , A ) = A ) |
|
| 3 | 2 | breq2d | |- ( -. A <_ B -> ( A <_ if ( A <_ B , B , A ) <-> A <_ A ) ) |
| 4 | 1 3 | syl5ibrcom | |- ( A e. RR -> ( -. A <_ B -> A <_ if ( A <_ B , B , A ) ) ) |
| 5 | id | |- ( A <_ B -> A <_ B ) |
|
| 6 | iftrue | |- ( A <_ B -> if ( A <_ B , B , A ) = B ) |
|
| 7 | 5 6 | breqtrrd | |- ( A <_ B -> A <_ if ( A <_ B , B , A ) ) |
| 8 | 4 7 | pm2.61d2 | |- ( A e. RR -> A <_ if ( A <_ B , B , A ) ) |