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 ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → 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 ∈ ℕ | N ∥ x ∧ M ∥ x ∧ P ∥ x = x ∈ ℕ | N ∥ x ∧ M ∥ x ∧ P ∥ x
4 3 infeq1i ⊢ inf x ∈ ℕ | N ∥ x ∧ M ∥ x ∧ P ∥ x ℝ < = inf x ∈ ℕ | N ∥ x ∧ M ∥ x ∧ P ∥ x ℝ <
5 1 4 ifbieq2i ⊢ if N = 0 ∨ M = 0 ∨ P = 0 0 inf x ∈ ℕ | N ∥ x ∧ M ∥ x ∧ P ∥ x ℝ < = if N = 0 ∨ M = 0 ∨ P = 0 0 inf x ∈ ℕ | N ∥ x ∧ M ∥ x ∧ P ∥ x ℝ <
6 lcmcl ⊢ N ∈ ℤ ∧ M ∈ ℤ → N lcm M ∈ ℕ 0
7 6 3adant3 ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → N lcm M ∈ ℕ 0
8 7 nn0zd ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → N lcm M ∈ ℤ
9 simp3 ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → P ∈ ℤ
10 lcmval ⊢ N lcm M ∈ ℤ ∧ P ∈ ℤ → N lcm M lcm P = if N lcm M = 0 ∨ P = 0 0 inf x ∈ ℕ | N lcm M ∥ x ∧ P ∥ x ℝ <
11 8 9 10 syl2anc ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → N lcm M lcm P = if N lcm M = 0 ∨ P = 0 0 inf x ∈ ℕ | N lcm M ∥ x ∧ P ∥ x ℝ <
12 lcmeq0 ⊢ N ∈ ℤ ∧ M ∈ ℤ → N lcm M = 0 ↔ N = 0 ∨ M = 0
13 12 3adant3 ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → N lcm M = 0 ↔ N = 0 ∨ M = 0
14 13 orbi1d ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → N lcm M = 0 ∨ P = 0 ↔ N = 0 ∨ M = 0 ∨ P = 0
15 14 bicomd ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → N = 0 ∨ M = 0 ∨ P = 0 ↔ N lcm M = 0 ∨ P = 0
16 nnz ⊢ x ∈ ℕ → x ∈ ℤ
17 16 adantl ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ ∧ x ∈ ℕ → x ∈ ℤ
18 simp1 ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → N ∈ ℤ
19 18 adantr ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ ∧ x ∈ ℕ → N ∈ ℤ
20 simpl2 ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ ∧ x ∈ ℕ → M ∈ ℤ
21 lcmdvdsb ⊢ x ∈ ℤ ∧ N ∈ ℤ ∧ M ∈ ℤ → N ∥ x ∧ M ∥ x ↔ N lcm M ∥ x
22 17 19 20 21 syl3anc ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ ∧ x ∈ ℕ → N ∥ x ∧ M ∥ x ↔ N lcm M ∥ x
23 22 anbi1d ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ ∧ x ∈ ℕ → N ∥ x ∧ M ∥ x ∧ P ∥ x ↔ N lcm M ∥ x ∧ P ∥ x
24 23 rabbidva ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → x ∈ ℕ | N ∥ x ∧ M ∥ x ∧ P ∥ x = x ∈ ℕ | N lcm M ∥ x ∧ P ∥ x
25 24 infeq1d ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → inf x ∈ ℕ | N ∥ x ∧ M ∥ x ∧ P ∥ x ℝ < = inf x ∈ ℕ | N lcm M ∥ x ∧ P ∥ x ℝ <
26 15 25 ifbieq2d ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → if N = 0 ∨ M = 0 ∨ P = 0 0 inf x ∈ ℕ | N ∥ x ∧ M ∥ x ∧ P ∥ x ℝ < = if N lcm M = 0 ∨ P = 0 0 inf x ∈ ℕ | N lcm M ∥ x ∧ P ∥ x ℝ <
27 11 26 eqtr4d ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → N lcm M lcm P = if N = 0 ∨ M = 0 ∨ P = 0 0 inf x ∈ ℕ | N ∥ x ∧ M ∥ x ∧ P ∥ x ℝ <
28 lcmcl ⊢ M ∈ ℤ ∧ P ∈ ℤ → M lcm P ∈ ℕ 0
29 28 3adant1 ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → M lcm P ∈ ℕ 0
30 29 nn0zd ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → M lcm P ∈ ℤ
31 lcmval ⊢ N ∈ ℤ ∧ M lcm P ∈ ℤ → N lcm M lcm P = if N = 0 ∨ M lcm P = 0 0 inf x ∈ ℕ | N ∥ x ∧ M lcm P ∥ x ℝ <
32 18 30 31 syl2anc ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → N lcm M lcm P = if N = 0 ∨ M lcm P = 0 0 inf x ∈ ℕ | N ∥ x ∧ M lcm P ∥ x ℝ <
33 lcmeq0 ⊢ M ∈ ℤ ∧ P ∈ ℤ → M lcm P = 0 ↔ M = 0 ∨ P = 0
34 33 3adant1 ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → M lcm P = 0 ↔ M = 0 ∨ P = 0
35 34 orbi2d ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → N = 0 ∨ M lcm P = 0 ↔ N = 0 ∨ M = 0 ∨ P = 0
36 35 bicomd ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → N = 0 ∨ M = 0 ∨ P = 0 ↔ N = 0 ∨ M lcm P = 0
37 9 adantr ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ ∧ x ∈ ℕ → P ∈ ℤ
38 lcmdvdsb ⊢ x ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → M ∥ x ∧ P ∥ x ↔ M lcm P ∥ x
39 17 20 37 38 syl3anc ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ ∧ x ∈ ℕ → M ∥ x ∧ P ∥ x ↔ M lcm P ∥ x
40 39 anbi2d ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ ∧ x ∈ ℕ → N ∥ x ∧ M ∥ x ∧ P ∥ x ↔ N ∥ x ∧ M lcm P ∥ x
41 40 rabbidva ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → x ∈ ℕ | N ∥ x ∧ M ∥ x ∧ P ∥ x = x ∈ ℕ | N ∥ x ∧ M lcm P ∥ x
42 41 infeq1d ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → inf x ∈ ℕ | N ∥ x ∧ M ∥ x ∧ P ∥ x ℝ < = inf x ∈ ℕ | N ∥ x ∧ M lcm P ∥ x ℝ <
43 36 42 ifbieq2d ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → if N = 0 ∨ M = 0 ∨ P = 0 0 inf x ∈ ℕ | N ∥ x ∧ M ∥ x ∧ P ∥ x ℝ < = if N = 0 ∨ M lcm P = 0 0 inf x ∈ ℕ | N ∥ x ∧ M lcm P ∥ x ℝ <
44 32 43 eqtr4d ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → N lcm M lcm P = if N = 0 ∨ M = 0 ∨ P = 0 0 inf x ∈ ℕ | N ∥ x ∧ M ∥ x ∧ P ∥ x ℝ <
45 5 27 44 3eqtr4a ⊢ N ∈ ℤ ∧ M ∈ ℤ ∧ P ∈ ℤ → N lcm M lcm P = N lcm M lcm P