Description: The value of the lcm operator when both operands are nonzero. (Contributed by Steve Rodriguez, 20-Jan-2020) (Revised by AV, 16-Sep-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | lcmn0val | |- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) = inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lcmval | |- ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) = if ( ( M = 0 \/ N = 0 ) , 0 , inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) ) ) |
|
| 2 | iffalse | |- ( -. ( M = 0 \/ N = 0 ) -> if ( ( M = 0 \/ N = 0 ) , 0 , inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) ) = inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) ) |
|
| 3 | 1 2 | sylan9eq | |- ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) = inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) ) |