Description: The value, by convention, of the lcm operator when either operand is 0. (Use lcmcom for a left-hand 0.) (Contributed by Steve Rodriguez, 20-Jan-2020) (Proof shortened by AV, 16-Sep-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | lcm0val | |- ( M e. ZZ -> ( M lcm 0 ) = 0 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0z | |- 0 e. ZZ |
|
| 2 | lcmval | |- ( ( M e. ZZ /\ 0 e. ZZ ) -> ( M lcm 0 ) = if ( ( M = 0 \/ 0 = 0 ) , 0 , inf ( { n e. NN | ( M || n /\ 0 || n ) } , RR , < ) ) ) |
|
| 3 | eqid | |- 0 = 0 |
|
| 4 | 3 | olci | |- ( M = 0 \/ 0 = 0 ) |
| 5 | 4 | iftruei | |- if ( ( M = 0 \/ 0 = 0 ) , 0 , inf ( { n e. NN | ( M || n /\ 0 || n ) } , RR , < ) ) = 0 |
| 6 | 2 5 | eqtrdi | |- ( ( M e. ZZ /\ 0 e. ZZ ) -> ( M lcm 0 ) = 0 ) |
| 7 | 1 6 | mpan2 | |- ( M e. ZZ -> ( M lcm 0 ) = 0 ) |