Description: Value of the lcm operator. ( M lcm N ) is the least common multiple of M and N . If either M or N is 0 , the result is defined conventionally as 0 . Contrast with df-gcd and gcdval . (Contributed by Steve Rodriguez, 20-Jan-2020) (Revised by AV, 16-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | lcmval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1 | |
|
2 | 1 | orbi1d | |
3 | breq1 | |
|
4 | 3 | anbi1d | |
5 | 4 | rabbidv | |
6 | 5 | infeq1d | |
7 | 2 6 | ifbieq2d | |
8 | eqeq1 | |
|
9 | 8 | orbi2d | |
10 | breq1 | |
|
11 | 10 | anbi2d | |
12 | 11 | rabbidv | |
13 | 12 | infeq1d | |
14 | 9 13 | ifbieq2d | |
15 | df-lcm | |
|
16 | c0ex | |
|
17 | ltso | |
|
18 | 17 | infex | |
19 | 16 18 | ifex | |
20 | 7 14 15 19 | ovmpo | |