This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) = if ( ( M = 0 \/ N = 0 ) , 0 , inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) ) )

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( x = M -> ( x = 0 <-> M = 0 ) )
2 1 orbi1d 
 |-  ( x = M -> ( ( x = 0 \/ y = 0 ) <-> ( M = 0 \/ y = 0 ) ) )
3 breq1 
 |-  ( x = M -> ( x || n <-> M || n ) )
4 3 anbi1d 
 |-  ( x = M -> ( ( x || n /\ y || n ) <-> ( M || n /\ y || n ) ) )
5 4 rabbidv 
 |-  ( x = M -> { n e. NN | ( x || n /\ y || n ) } = { n e. NN | ( M || n /\ y || n ) } )
6 5 infeq1d 
 |-  ( x = M -> inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) = inf ( { n e. NN | ( M || n /\ y || n ) } , RR , < ) )
7 2 6 ifbieq2d 
 |-  ( x = M -> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) = if ( ( M = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( M || n /\ y || n ) } , RR , < ) ) )
8 eqeq1 
 |-  ( y = N -> ( y = 0 <-> N = 0 ) )
9 8 orbi2d 
 |-  ( y = N -> ( ( M = 0 \/ y = 0 ) <-> ( M = 0 \/ N = 0 ) ) )
10 breq1 
 |-  ( y = N -> ( y || n <-> N || n ) )
11 10 anbi2d 
 |-  ( y = N -> ( ( M || n /\ y || n ) <-> ( M || n /\ N || n ) ) )
12 11 rabbidv 
 |-  ( y = N -> { n e. NN | ( M || n /\ y || n ) } = { n e. NN | ( M || n /\ N || n ) } )
13 12 infeq1d 
 |-  ( y = N -> inf ( { n e. NN | ( M || n /\ y || n ) } , RR , < ) = inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) )
14 9 13 ifbieq2d 
 |-  ( y = N -> if ( ( M = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( M || n /\ y || n ) } , RR , < ) ) = if ( ( M = 0 \/ N = 0 ) , 0 , inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) ) )
15 df-lcm 
 |-  lcm = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 \/ y = 0 ) , 0 , inf ( { n e. NN | ( x || n /\ y || n ) } , RR , < ) ) )
16 c0ex 
 |-  0 e. _V
17 ltso 
 |-  < Or RR
18 17 infex 
 |-  inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) e. _V
19 16 18 ifex 
 |-  if ( ( M = 0 \/ N = 0 ) , 0 , inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) ) e. _V
20 7 14 15 19 ovmpo 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) = if ( ( M = 0 \/ N = 0 ) , 0 , inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) ) )