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 ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑁 lcm 𝑀 ) lcm 𝑃 ) = ( 𝑁 lcm ( 𝑀 lcm 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 orass ⊢ ( ( ( 𝑁 = 0 ∨ 𝑀 = 0 ) ∨ 𝑃 = 0 ) ↔ ( 𝑁 = 0 ∨ ( 𝑀 = 0 ∨ 𝑃 = 0 ) ) )
2 anass ⊢ ( ( ( 𝑁 ∥ 𝑥 ∧ 𝑀 ∥ 𝑥 ) ∧ 𝑃 ∥ 𝑥 ) ↔ ( 𝑁 ∥ 𝑥 ∧ ( 𝑀 ∥ 𝑥 ∧ 𝑃 ∥ 𝑥 ) ) )
3 2 rabbii ⊢ { 𝑥 ∈ ℕ ∣ ( ( 𝑁 ∥ 𝑥 ∧ 𝑀 ∥ 𝑥 ) ∧ 𝑃 ∥ 𝑥 ) } = { 𝑥 ∈ ℕ ∣ ( 𝑁 ∥ 𝑥 ∧ ( 𝑀 ∥ 𝑥 ∧ 𝑃 ∥ 𝑥 ) ) }
4 3 infeq1i ⊢ inf ( { 𝑥 ∈ ℕ ∣ ( ( 𝑁 ∥ 𝑥 ∧ 𝑀 ∥ 𝑥 ) ∧ 𝑃 ∥ 𝑥 ) } , ℝ , < ) = inf ( { 𝑥 ∈ ℕ ∣ ( 𝑁 ∥ 𝑥 ∧ ( 𝑀 ∥ 𝑥 ∧ 𝑃 ∥ 𝑥 ) ) } , ℝ , < )
5 1 4 ifbieq2i ⊢ if ( ( ( 𝑁 = 0 ∨ 𝑀 = 0 ) ∨ 𝑃 = 0 ) , 0 , inf ( { 𝑥 ∈ ℕ ∣ ( ( 𝑁 ∥ 𝑥 ∧ 𝑀 ∥ 𝑥 ) ∧ 𝑃 ∥ 𝑥 ) } , ℝ , < ) ) = if ( ( 𝑁 = 0 ∨ ( 𝑀 = 0 ∨ 𝑃 = 0 ) ) , 0 , inf ( { 𝑥 ∈ ℕ ∣ ( 𝑁 ∥ 𝑥 ∧ ( 𝑀 ∥ 𝑥 ∧ 𝑃 ∥ 𝑥 ) ) } , ℝ , < ) )
6 lcmcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 lcm 𝑀 ) ∈ ℕ0 )
7 6 3adant3 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑁 lcm 𝑀 ) ∈ ℕ0 )
8 7 nn0zd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑁 lcm 𝑀 ) ∈ ℤ )
9 simp3 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → 𝑃 ∈ ℤ )
10 lcmval ⊢ ( ( ( 𝑁 lcm 𝑀 ) ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑁 lcm 𝑀 ) lcm 𝑃 ) = if ( ( ( 𝑁 lcm 𝑀 ) = 0 ∨ 𝑃 = 0 ) , 0 , inf ( { 𝑥 ∈ ℕ ∣ ( ( 𝑁 lcm 𝑀 ) ∥ 𝑥 ∧ 𝑃 ∥ 𝑥 ) } , ℝ , < ) ) )
11 8 9 10 syl2anc ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑁 lcm 𝑀 ) lcm 𝑃 ) = if ( ( ( 𝑁 lcm 𝑀 ) = 0 ∨ 𝑃 = 0 ) , 0 , inf ( { 𝑥 ∈ ℕ ∣ ( ( 𝑁 lcm 𝑀 ) ∥ 𝑥 ∧ 𝑃 ∥ 𝑥 ) } , ℝ , < ) ) )
12 lcmeq0 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑁 lcm 𝑀 ) = 0 ↔ ( 𝑁 = 0 ∨ 𝑀 = 0 ) ) )
13 12 3adant3 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑁 lcm 𝑀 ) = 0 ↔ ( 𝑁 = 0 ∨ 𝑀 = 0 ) ) )
14 13 orbi1d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( ( 𝑁 lcm 𝑀 ) = 0 ∨ 𝑃 = 0 ) ↔ ( ( 𝑁 = 0 ∨ 𝑀 = 0 ) ∨ 𝑃 = 0 ) ) )
15 14 bicomd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( ( 𝑁 = 0 ∨ 𝑀 = 0 ) ∨ 𝑃 = 0 ) ↔ ( ( 𝑁 lcm 𝑀 ) = 0 ∨ 𝑃 = 0 ) ) )
16 nnz ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℤ )
17 16 adantl ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑥 ∈ ℕ ) → 𝑥 ∈ ℤ )
18 simp1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → 𝑁 ∈ ℤ )
19 18 adantr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑥 ∈ ℕ ) → 𝑁 ∈ ℤ )
20 simpl2 ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑥 ∈ ℕ ) → 𝑀 ∈ ℤ )
21 lcmdvdsb ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑁 ∥ 𝑥 ∧ 𝑀 ∥ 𝑥 ) ↔ ( 𝑁 lcm 𝑀 ) ∥ 𝑥 ) )
22 17 19 20 21 syl3anc ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝑁 ∥ 𝑥 ∧ 𝑀 ∥ 𝑥 ) ↔ ( 𝑁 lcm 𝑀 ) ∥ 𝑥 ) )
23 22 anbi1d ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑥 ∈ ℕ ) → ( ( ( 𝑁 ∥ 𝑥 ∧ 𝑀 ∥ 𝑥 ) ∧ 𝑃 ∥ 𝑥 ) ↔ ( ( 𝑁 lcm 𝑀 ) ∥ 𝑥 ∧ 𝑃 ∥ 𝑥 ) ) )
24 23 rabbidva ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → { 𝑥 ∈ ℕ ∣ ( ( 𝑁 ∥ 𝑥 ∧ 𝑀 ∥ 𝑥 ) ∧ 𝑃 ∥ 𝑥 ) } = { 𝑥 ∈ ℕ ∣ ( ( 𝑁 lcm 𝑀 ) ∥ 𝑥 ∧ 𝑃 ∥ 𝑥 ) } )
25 24 infeq1d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → inf ( { 𝑥 ∈ ℕ ∣ ( ( 𝑁 ∥ 𝑥 ∧ 𝑀 ∥ 𝑥 ) ∧ 𝑃 ∥ 𝑥 ) } , ℝ , < ) = inf ( { 𝑥 ∈ ℕ ∣ ( ( 𝑁 lcm 𝑀 ) ∥ 𝑥 ∧ 𝑃 ∥ 𝑥 ) } , ℝ , < ) )
26 15 25 ifbieq2d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → if ( ( ( 𝑁 = 0 ∨ 𝑀 = 0 ) ∨ 𝑃 = 0 ) , 0 , inf ( { 𝑥 ∈ ℕ ∣ ( ( 𝑁 ∥ 𝑥 ∧ 𝑀 ∥ 𝑥 ) ∧ 𝑃 ∥ 𝑥 ) } , ℝ , < ) ) = if ( ( ( 𝑁 lcm 𝑀 ) = 0 ∨ 𝑃 = 0 ) , 0 , inf ( { 𝑥 ∈ ℕ ∣ ( ( 𝑁 lcm 𝑀 ) ∥ 𝑥 ∧ 𝑃 ∥ 𝑥 ) } , ℝ , < ) ) )
27 11 26 eqtr4d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑁 lcm 𝑀 ) lcm 𝑃 ) = if ( ( ( 𝑁 = 0 ∨ 𝑀 = 0 ) ∨ 𝑃 = 0 ) , 0 , inf ( { 𝑥 ∈ ℕ ∣ ( ( 𝑁 ∥ 𝑥 ∧ 𝑀 ∥ 𝑥 ) ∧ 𝑃 ∥ 𝑥 ) } , ℝ , < ) ) )
28 lcmcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑀 lcm 𝑃 ) ∈ ℕ0 )
29 28 3adant1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑀 lcm 𝑃 ) ∈ ℕ0 )
30 29 nn0zd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑀 lcm 𝑃 ) ∈ ℤ )
31 lcmval ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑀 lcm 𝑃 ) ∈ ℤ ) → ( 𝑁 lcm ( 𝑀 lcm 𝑃 ) ) = if ( ( 𝑁 = 0 ∨ ( 𝑀 lcm 𝑃 ) = 0 ) , 0 , inf ( { 𝑥 ∈ ℕ ∣ ( 𝑁 ∥ 𝑥 ∧ ( 𝑀 lcm 𝑃 ) ∥ 𝑥 ) } , ℝ , < ) ) )
32 18 30 31 syl2anc ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑁 lcm ( 𝑀 lcm 𝑃 ) ) = if ( ( 𝑁 = 0 ∨ ( 𝑀 lcm 𝑃 ) = 0 ) , 0 , inf ( { 𝑥 ∈ ℕ ∣ ( 𝑁 ∥ 𝑥 ∧ ( 𝑀 lcm 𝑃 ) ∥ 𝑥 ) } , ℝ , < ) ) )
33 lcmeq0 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑀 lcm 𝑃 ) = 0 ↔ ( 𝑀 = 0 ∨ 𝑃 = 0 ) ) )
34 33 3adant1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑀 lcm 𝑃 ) = 0 ↔ ( 𝑀 = 0 ∨ 𝑃 = 0 ) ) )
35 34 orbi2d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑁 = 0 ∨ ( 𝑀 lcm 𝑃 ) = 0 ) ↔ ( 𝑁 = 0 ∨ ( 𝑀 = 0 ∨ 𝑃 = 0 ) ) ) )
36 35 bicomd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑁 = 0 ∨ ( 𝑀 = 0 ∨ 𝑃 = 0 ) ) ↔ ( 𝑁 = 0 ∨ ( 𝑀 lcm 𝑃 ) = 0 ) ) )
37 9 adantr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑥 ∈ ℕ ) → 𝑃 ∈ ℤ )
38 lcmdvdsb ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑀 ∥ 𝑥 ∧ 𝑃 ∥ 𝑥 ) ↔ ( 𝑀 lcm 𝑃 ) ∥ 𝑥 ) )
39 17 20 37 38 syl3anc ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝑀 ∥ 𝑥 ∧ 𝑃 ∥ 𝑥 ) ↔ ( 𝑀 lcm 𝑃 ) ∥ 𝑥 ) )
40 39 anbi2d ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝑁 ∥ 𝑥 ∧ ( 𝑀 ∥ 𝑥 ∧ 𝑃 ∥ 𝑥 ) ) ↔ ( 𝑁 ∥ 𝑥 ∧ ( 𝑀 lcm 𝑃 ) ∥ 𝑥 ) ) )
41 40 rabbidva ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → { 𝑥 ∈ ℕ ∣ ( 𝑁 ∥ 𝑥 ∧ ( 𝑀 ∥ 𝑥 ∧ 𝑃 ∥ 𝑥 ) ) } = { 𝑥 ∈ ℕ ∣ ( 𝑁 ∥ 𝑥 ∧ ( 𝑀 lcm 𝑃 ) ∥ 𝑥 ) } )
42 41 infeq1d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → inf ( { 𝑥 ∈ ℕ ∣ ( 𝑁 ∥ 𝑥 ∧ ( 𝑀 ∥ 𝑥 ∧ 𝑃 ∥ 𝑥 ) ) } , ℝ , < ) = inf ( { 𝑥 ∈ ℕ ∣ ( 𝑁 ∥ 𝑥 ∧ ( 𝑀 lcm 𝑃 ) ∥ 𝑥 ) } , ℝ , < ) )
43 36 42 ifbieq2d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → if ( ( 𝑁 = 0 ∨ ( 𝑀 = 0 ∨ 𝑃 = 0 ) ) , 0 , inf ( { 𝑥 ∈ ℕ ∣ ( 𝑁 ∥ 𝑥 ∧ ( 𝑀 ∥ 𝑥 ∧ 𝑃 ∥ 𝑥 ) ) } , ℝ , < ) ) = if ( ( 𝑁 = 0 ∨ ( 𝑀 lcm 𝑃 ) = 0 ) , 0 , inf ( { 𝑥 ∈ ℕ ∣ ( 𝑁 ∥ 𝑥 ∧ ( 𝑀 lcm 𝑃 ) ∥ 𝑥 ) } , ℝ , < ) ) )
44 32 43 eqtr4d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑁 lcm ( 𝑀 lcm 𝑃 ) ) = if ( ( 𝑁 = 0 ∨ ( 𝑀 = 0 ∨ 𝑃 = 0 ) ) , 0 , inf ( { 𝑥 ∈ ℕ ∣ ( 𝑁 ∥ 𝑥 ∧ ( 𝑀 ∥ 𝑥 ∧ 𝑃 ∥ 𝑥 ) ) } , ℝ , < ) ) )
45 5 27 44 3eqtr4a ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝑁 lcm 𝑀 ) lcm 𝑃 ) = ( 𝑁 lcm ( 𝑀 lcm 𝑃 ) ) )