Metamath Proof Explorer

Theorem lcmass

Description: Associative law for lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020) (Proof shortened by AV, 16-Sep-2020)

Ref Expression
Assertion lcmass 
|- ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( N lcm M ) lcm P ) = ( N lcm ( M lcm P ) ) )

Proof

Step Hyp Ref Expression
1 orass 
 |-  ( ( ( N = 0 \/ M = 0 ) \/ P = 0 ) <-> ( N = 0 \/ ( M = 0 \/ P = 0 ) ) )
2 anass 
 |-  ( ( ( N || x /\ M || x ) /\ P || x ) <-> ( N || x /\ ( M || x /\ P || x ) ) )
3 2 rabbii 
 |-  { x e. NN | ( ( N || x /\ M || x ) /\ P || x ) } = { x e. NN | ( N || x /\ ( M || x /\ P || x ) ) }
4 3 infeq1i 
 |-  inf ( { x e. NN | ( ( N || x /\ M || x ) /\ P || x ) } , RR , < ) = inf ( { x e. NN | ( N || x /\ ( M || x /\ P || x ) ) } , RR , < )
5 1 4 ifbieq2i 
 |-  if ( ( ( N = 0 \/ M = 0 ) \/ P = 0 ) , 0 , inf ( { x e. NN | ( ( N || x /\ M || x ) /\ P || x ) } , RR , < ) ) = if ( ( N = 0 \/ ( M = 0 \/ P = 0 ) ) , 0 , inf ( { x e. NN | ( N || x /\ ( M || x /\ P || x ) ) } , RR , < ) )
6 lcmcl 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( N lcm M ) e. NN0 )
7 6 3adant3 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( N lcm M ) e. NN0 )
8 7 nn0zd 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( N lcm M ) e. ZZ )
9 simp3 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> P e. ZZ )
10 lcmval 
 |-  ( ( ( N lcm M ) e. ZZ /\ P e. ZZ ) -> ( ( N lcm M ) lcm P ) = if ( ( ( N lcm M ) = 0 \/ P = 0 ) , 0 , inf ( { x e. NN | ( ( N lcm M ) || x /\ P || x ) } , RR , < ) ) )
11 8 9 10 syl2anc 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( N lcm M ) lcm P ) = if ( ( ( N lcm M ) = 0 \/ P = 0 ) , 0 , inf ( { x e. NN | ( ( N lcm M ) || x /\ P || x ) } , RR , < ) ) )
12 lcmeq0 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( ( N lcm M ) = 0 <-> ( N = 0 \/ M = 0 ) ) )
13 12 3adant3 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( N lcm M ) = 0 <-> ( N = 0 \/ M = 0 ) ) )
14 13 orbi1d 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( ( N lcm M ) = 0 \/ P = 0 ) <-> ( ( N = 0 \/ M = 0 ) \/ P = 0 ) ) )
15 14 bicomd 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( ( N = 0 \/ M = 0 ) \/ P = 0 ) <-> ( ( N lcm M ) = 0 \/ P = 0 ) ) )
16 nnz 
 |-  ( x e. NN -> x e. ZZ )
17 16 adantl 
 |-  ( ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) /\ x e. NN ) -> x e. ZZ )
18 simp1 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> N e. ZZ )
19 18 adantr 
 |-  ( ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) /\ x e. NN ) -> N e. ZZ )
20 simpl2 
 |-  ( ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) /\ x e. NN ) -> M e. ZZ )
21 lcmdvdsb 
 |-  ( ( x e. ZZ /\ N e. ZZ /\ M e. ZZ ) -> ( ( N || x /\ M || x ) <-> ( N lcm M ) || x ) )
22 17 19 20 21 syl3anc 
 |-  ( ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) /\ x e. NN ) -> ( ( N || x /\ M || x ) <-> ( N lcm M ) || x ) )
23 22 anbi1d 
 |-  ( ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) /\ x e. NN ) -> ( ( ( N || x /\ M || x ) /\ P || x ) <-> ( ( N lcm M ) || x /\ P || x ) ) )
24 23 rabbidva 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> { x e. NN | ( ( N || x /\ M || x ) /\ P || x ) } = { x e. NN | ( ( N lcm M ) || x /\ P || x ) } )
25 24 infeq1d 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> inf ( { x e. NN | ( ( N || x /\ M || x ) /\ P || x ) } , RR , < ) = inf ( { x e. NN | ( ( N lcm M ) || x /\ P || x ) } , RR , < ) )
26 15 25 ifbieq2d 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> if ( ( ( N = 0 \/ M = 0 ) \/ P = 0 ) , 0 , inf ( { x e. NN | ( ( N || x /\ M || x ) /\ P || x ) } , RR , < ) ) = if ( ( ( N lcm M ) = 0 \/ P = 0 ) , 0 , inf ( { x e. NN | ( ( N lcm M ) || x /\ P || x ) } , RR , < ) ) )
27 11 26 eqtr4d 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( N lcm M ) lcm P ) = if ( ( ( N = 0 \/ M = 0 ) \/ P = 0 ) , 0 , inf ( { x e. NN | ( ( N || x /\ M || x ) /\ P || x ) } , RR , < ) ) )
28 lcmcl 
 |-  ( ( M e. ZZ /\ P e. ZZ ) -> ( M lcm P ) e. NN0 )
29 28 3adant1 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( M lcm P ) e. NN0 )
30 29 nn0zd 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( M lcm P ) e. ZZ )
31 lcmval 
 |-  ( ( N e. ZZ /\ ( M lcm P ) e. ZZ ) -> ( N lcm ( M lcm P ) ) = if ( ( N = 0 \/ ( M lcm P ) = 0 ) , 0 , inf ( { x e. NN | ( N || x /\ ( M lcm P ) || x ) } , RR , < ) ) )
32 18 30 31 syl2anc 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( N lcm ( M lcm P ) ) = if ( ( N = 0 \/ ( M lcm P ) = 0 ) , 0 , inf ( { x e. NN | ( N || x /\ ( M lcm P ) || x ) } , RR , < ) ) )
33 lcmeq0 
 |-  ( ( M e. ZZ /\ P e. ZZ ) -> ( ( M lcm P ) = 0 <-> ( M = 0 \/ P = 0 ) ) )
34 33 3adant1 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( M lcm P ) = 0 <-> ( M = 0 \/ P = 0 ) ) )
35 34 orbi2d 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( N = 0 \/ ( M lcm P ) = 0 ) <-> ( N = 0 \/ ( M = 0 \/ P = 0 ) ) ) )
36 35 bicomd 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( N = 0 \/ ( M = 0 \/ P = 0 ) ) <-> ( N = 0 \/ ( M lcm P ) = 0 ) ) )
37 9 adantr 
 |-  ( ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) /\ x e. NN ) -> P e. ZZ )
38 lcmdvdsb 
 |-  ( ( x e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( M || x /\ P || x ) <-> ( M lcm P ) || x ) )
39 17 20 37 38 syl3anc 
 |-  ( ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) /\ x e. NN ) -> ( ( M || x /\ P || x ) <-> ( M lcm P ) || x ) )
40 39 anbi2d 
 |-  ( ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) /\ x e. NN ) -> ( ( N || x /\ ( M || x /\ P || x ) ) <-> ( N || x /\ ( M lcm P ) || x ) ) )
41 40 rabbidva 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> { x e. NN | ( N || x /\ ( M || x /\ P || x ) ) } = { x e. NN | ( N || x /\ ( M lcm P ) || x ) } )
42 41 infeq1d 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> inf ( { x e. NN | ( N || x /\ ( M || x /\ P || x ) ) } , RR , < ) = inf ( { x e. NN | ( N || x /\ ( M lcm P ) || x ) } , RR , < ) )
43 36 42 ifbieq2d 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> if ( ( N = 0 \/ ( M = 0 \/ P = 0 ) ) , 0 , inf ( { x e. NN | ( N || x /\ ( M || x /\ P || x ) ) } , RR , < ) ) = if ( ( N = 0 \/ ( M lcm P ) = 0 ) , 0 , inf ( { x e. NN | ( N || x /\ ( M lcm P ) || x ) } , RR , < ) ) )
44 32 43 eqtr4d 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( N lcm ( M lcm P ) ) = if ( ( N = 0 \/ ( M = 0 \/ P = 0 ) ) , 0 , inf ( { x e. NN | ( N || x /\ ( M || x /\ P || x ) ) } , RR , < ) ) )
45 5 27 44 3eqtr4a 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ P e. ZZ ) -> ( ( N lcm M ) lcm P ) = ( N lcm ( M lcm P ) ) )