Metamath Proof Explorer


Theorem lcmval

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 MNMlcmN=ifM=0N=00supn|MnNn<

Proof

Step Hyp Ref Expression
1 eqeq1 x=Mx=0M=0
2 1 orbi1d x=Mx=0y=0M=0y=0
3 breq1 x=MxnMn
4 3 anbi1d x=MxnynMnyn
5 4 rabbidv x=Mn|xnyn=n|Mnyn
6 5 infeq1d x=Msupn|xnyn<=supn|Mnyn<
7 2 6 ifbieq2d x=Mifx=0y=00supn|xnyn<=ifM=0y=00supn|Mnyn<
8 eqeq1 y=Ny=0N=0
9 8 orbi2d y=NM=0y=0M=0N=0
10 breq1 y=NynNn
11 10 anbi2d y=NMnynMnNn
12 11 rabbidv y=Nn|Mnyn=n|MnNn
13 12 infeq1d y=Nsupn|Mnyn<=supn|MnNn<
14 9 13 ifbieq2d y=NifM=0y=00supn|Mnyn<=ifM=0N=00supn|MnNn<
15 df-lcm lcm=x,yifx=0y=00supn|xnyn<
16 c0ex 0V
17 ltso <Or
18 17 infex supn|MnNn<V
19 16 18 ifex ifM=0N=00supn|MnNn<V
20 7 14 15 19 ovmpo MNMlcmN=ifM=0N=00supn|MnNn<