Metamath Proof Explorer

Theorem lcmftp

Description: The least common multiple of a triple of integers is the least common multiple of the third integer and the least common multiple of the first two integers. Although there would be a shorter proof using lcmfunsn , this explicit proof (not based on induction) should be kept. (Proof modification is discouraged.) (Contributed by AV, 23-Aug-2020)

Ref Expression
Assertion lcmftp ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → lcm _ ⁡ A B C = A lcm B lcm C

Proof

Step Hyp Ref Expression
1 0z ⊢ 0 ∈ ℤ
2 eltpg ⊢ 0 ∈ ℤ → 0 ∈ A B C ↔ 0 = A ∨ 0 = B ∨ 0 = C
3 1 2 ax-mp ⊢ 0 ∈ A B C ↔ 0 = A ∨ 0 = B ∨ 0 = C
4 3 biimpri ⊢ 0 = A ∨ 0 = B ∨ 0 = C → 0 ∈ A B C
5 tpssi ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A B C ⊆ ℤ
6 4 5 anim12ci ⊢ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A B C ⊆ ℤ ∧ 0 ∈ A B C
7 lcmf0val ⊢ A B C ⊆ ℤ ∧ 0 ∈ A B C → lcm _ ⁡ A B C = 0
8 6 7 syl ⊢ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → lcm _ ⁡ A B C = 0
9 0zd ⊢ C ∈ ℤ → 0 ∈ ℤ
10 lcmcom ⊢ 0 ∈ ℤ ∧ C ∈ ℤ → 0 lcm C = C lcm 0
11 9 10 mpancom ⊢ C ∈ ℤ → 0 lcm C = C lcm 0
12 lcm0val ⊢ C ∈ ℤ → C lcm 0 = 0
13 11 12 eqtrd ⊢ C ∈ ℤ → 0 lcm C = 0
14 13 eqcomd ⊢ C ∈ ℤ → 0 = 0 lcm C
15 14 3ad2ant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → 0 = 0 lcm C
16 15 adantl ⊢ 0 = A ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → 0 = 0 lcm C
17 0zd ⊢ B ∈ ℤ → 0 ∈ ℤ
18 lcmcom ⊢ 0 ∈ ℤ ∧ B ∈ ℤ → 0 lcm B = B lcm 0
19 17 18 mpancom ⊢ B ∈ ℤ → 0 lcm B = B lcm 0
20 lcm0val ⊢ B ∈ ℤ → B lcm 0 = 0
21 19 20 eqtrd ⊢ B ∈ ℤ → 0 lcm B = 0
22 21 eqcomd ⊢ B ∈ ℤ → 0 = 0 lcm B
23 22 3ad2ant2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → 0 = 0 lcm B
24 23 adantl ⊢ 0 = A ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → 0 = 0 lcm B
25 24 oveq1d ⊢ 0 = A ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → 0 lcm C = 0 lcm B lcm C
26 oveq1 ⊢ 0 = A → 0 lcm B = A lcm B
27 26 oveq1d ⊢ 0 = A → 0 lcm B lcm C = A lcm B lcm C
28 27 adantr ⊢ 0 = A ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → 0 lcm B lcm C = A lcm B lcm C
29 16 25 28 3eqtrd ⊢ 0 = A ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → 0 = A lcm B lcm C
30 lcm0val ⊢ A ∈ ℤ → A lcm 0 = 0
31 30 eqcomd ⊢ A ∈ ℤ → 0 = A lcm 0
32 31 3ad2ant1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → 0 = A lcm 0
33 32 adantl ⊢ 0 = B ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → 0 = A lcm 0
34 33 oveq1d ⊢ 0 = B ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → 0 lcm C = A lcm 0 lcm C
35 13 3ad2ant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → 0 lcm C = 0
36 35 adantl ⊢ 0 = B ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → 0 lcm C = 0
37 oveq2 ⊢ 0 = B → A lcm 0 = A lcm B
38 37 adantr ⊢ 0 = B ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A lcm 0 = A lcm B
39 38 oveq1d ⊢ 0 = B ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A lcm 0 lcm C = A lcm B lcm C
40 34 36 39 3eqtr3d ⊢ 0 = B ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → 0 = A lcm B lcm C
41 lcmcl ⊢ A ∈ ℤ ∧ B ∈ ℤ → A lcm B ∈ ℕ 0
42 41 nn0zd ⊢ A ∈ ℤ ∧ B ∈ ℤ → A lcm B ∈ ℤ
43 lcm0val ⊢ A lcm B ∈ ℤ → A lcm B lcm 0 = 0
44 43 eqcomd ⊢ A lcm B ∈ ℤ → 0 = A lcm B lcm 0
45 42 44 syl ⊢ A ∈ ℤ ∧ B ∈ ℤ → 0 = A lcm B lcm 0
46 45 3adant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → 0 = A lcm B lcm 0
47 oveq2 ⊢ 0 = C → A lcm B lcm 0 = A lcm B lcm C
48 46 47 sylan9eqr ⊢ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → 0 = A lcm B lcm C
49 29 40 48 3jaoian ⊢ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → 0 = A lcm B lcm C
50 8 49 eqtrd ⊢ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → lcm _ ⁡ A B C = A lcm B lcm C
51 42 3adant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A lcm B ∈ ℤ
52 simp3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → C ∈ ℤ
53 51 52 jca ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A lcm B ∈ ℤ ∧ C ∈ ℤ
54 53 adantl ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A lcm B ∈ ℤ ∧ C ∈ ℤ
55 dvdslcm ⊢ A lcm B ∈ ℤ ∧ C ∈ ℤ → A lcm B ∥ A lcm B lcm C ∧ C ∥ A lcm B lcm C
56 54 55 syl ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A lcm B ∥ A lcm B lcm C ∧ C ∥ A lcm B lcm C
57 dvdslcm ⊢ A ∈ ℤ ∧ B ∈ ℤ → A ∥ A lcm B ∧ B ∥ A lcm B
58 57 3adant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∥ A lcm B ∧ B ∥ A lcm B
59 simp1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∈ ℤ
60 lcmcl ⊢ A lcm B ∈ ℤ ∧ C ∈ ℤ → A lcm B lcm C ∈ ℕ 0
61 53 60 syl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A lcm B lcm C ∈ ℕ 0
62 61 nn0zd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A lcm B lcm C ∈ ℤ
63 59 51 62 3jca ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∈ ℤ ∧ A lcm B ∈ ℤ ∧ A lcm B lcm C ∈ ℤ
64 dvdstr ⊢ A ∈ ℤ ∧ A lcm B ∈ ℤ ∧ A lcm B lcm C ∈ ℤ → A ∥ A lcm B ∧ A lcm B ∥ A lcm B lcm C → A ∥ A lcm B lcm C
65 63 64 syl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∥ A lcm B ∧ A lcm B ∥ A lcm B lcm C → A ∥ A lcm B lcm C
66 65 expd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∥ A lcm B → A lcm B ∥ A lcm B lcm C → A ∥ A lcm B lcm C
67 66 com12 ⊢ A ∥ A lcm B → A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A lcm B ∥ A lcm B lcm C → A ∥ A lcm B lcm C
68 67 adantr ⊢ A ∥ A lcm B ∧ B ∥ A lcm B → A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A lcm B ∥ A lcm B lcm C → A ∥ A lcm B lcm C
69 58 68 mpcom ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A lcm B ∥ A lcm B lcm C → A ∥ A lcm B lcm C
70 69 adantl ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A lcm B ∥ A lcm B lcm C → A ∥ A lcm B lcm C
71 70 com12 ⊢ A lcm B ∥ A lcm B lcm C → ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∥ A lcm B lcm C
72 71 adantr ⊢ A lcm B ∥ A lcm B lcm C ∧ C ∥ A lcm B lcm C → ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∥ A lcm B lcm C
73 72 impcom ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A lcm B ∥ A lcm B lcm C ∧ C ∥ A lcm B lcm C → A ∥ A lcm B lcm C
74 simpr ⊢ A ∥ A lcm B ∧ B ∥ A lcm B → B ∥ A lcm B
75 57 74 syl ⊢ A ∈ ℤ ∧ B ∈ ℤ → B ∥ A lcm B
76 75 3adant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → B ∥ A lcm B
77 76 adantl ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → B ∥ A lcm B
78 simp2 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → B ∈ ℤ
79 78 51 62 3jca ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → B ∈ ℤ ∧ A lcm B ∈ ℤ ∧ A lcm B lcm C ∈ ℤ
80 79 adantl ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → B ∈ ℤ ∧ A lcm B ∈ ℤ ∧ A lcm B lcm C ∈ ℤ
81 dvdstr ⊢ B ∈ ℤ ∧ A lcm B ∈ ℤ ∧ A lcm B lcm C ∈ ℤ → B ∥ A lcm B ∧ A lcm B ∥ A lcm B lcm C → B ∥ A lcm B lcm C
82 80 81 syl ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → B ∥ A lcm B ∧ A lcm B ∥ A lcm B lcm C → B ∥ A lcm B lcm C
83 77 82 mpand ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A lcm B ∥ A lcm B lcm C → B ∥ A lcm B lcm C
84 83 com12 ⊢ A lcm B ∥ A lcm B lcm C → ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → B ∥ A lcm B lcm C
85 84 adantr ⊢ A lcm B ∥ A lcm B lcm C ∧ C ∥ A lcm B lcm C → ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → B ∥ A lcm B lcm C
86 85 impcom ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A lcm B ∥ A lcm B lcm C ∧ C ∥ A lcm B lcm C → B ∥ A lcm B lcm C
87 simpr ⊢ A lcm B ∥ A lcm B lcm C ∧ C ∥ A lcm B lcm C → C ∥ A lcm B lcm C
88 87 adantl ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A lcm B ∥ A lcm B lcm C ∧ C ∥ A lcm B lcm C → C ∥ A lcm B lcm C
89 73 86 88 3jca ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ A lcm B ∥ A lcm B lcm C ∧ C ∥ A lcm B lcm C → A ∥ A lcm B lcm C ∧ B ∥ A lcm B lcm C ∧ C ∥ A lcm B lcm C
90 56 89 mpdan ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∥ A lcm B lcm C ∧ B ∥ A lcm B lcm C ∧ C ∥ A lcm B lcm C
91 breq1 ⊢ m = A → m ∥ A lcm B lcm C ↔ A ∥ A lcm B lcm C
92 breq1 ⊢ m = B → m ∥ A lcm B lcm C ↔ B ∥ A lcm B lcm C
93 breq1 ⊢ m = C → m ∥ A lcm B lcm C ↔ C ∥ A lcm B lcm C
94 91 92 93 raltpg ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → ∀ m ∈ A B C m ∥ A lcm B lcm C ↔ A ∥ A lcm B lcm C ∧ B ∥ A lcm B lcm C ∧ C ∥ A lcm B lcm C
95 94 adantl ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → ∀ m ∈ A B C m ∥ A lcm B lcm C ↔ A ∥ A lcm B lcm C ∧ B ∥ A lcm B lcm C ∧ C ∥ A lcm B lcm C
96 90 95 mpbird ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → ∀ m ∈ A B C m ∥ A lcm B lcm C
97 breq1 ⊢ m = A → m ∥ k ↔ A ∥ k
98 breq1 ⊢ m = B → m ∥ k ↔ B ∥ k
99 breq1 ⊢ m = C → m ∥ k ↔ C ∥ k
100 97 98 99 raltpg ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → ∀ m ∈ A B C m ∥ k ↔ A ∥ k ∧ B ∥ k ∧ C ∥ k
101 100 ad2antlr ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ k ∈ ℕ → ∀ m ∈ A B C m ∥ k ↔ A ∥ k ∧ B ∥ k ∧ C ∥ k
102 simpr ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ k ∈ ℕ → k ∈ ℕ
103 51 ad2antlr ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ k ∈ ℕ → A lcm B ∈ ℤ
104 52 ad2antlr ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ k ∈ ℕ → C ∈ ℤ
105 102 103 104 3jca ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ k ∈ ℕ → k ∈ ℕ ∧ A lcm B ∈ ℤ ∧ C ∈ ℤ
106 105 adantr ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ k ∈ ℕ ∧ A ∥ k ∧ B ∥ k ∧ C ∥ k → k ∈ ℕ ∧ A lcm B ∈ ℤ ∧ C ∈ ℤ
107 3ioran ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ↔ ¬ 0 = A ∧ ¬ 0 = B ∧ ¬ 0 = C
108 eqcom ⊢ 0 = A ↔ A = 0
109 108 notbii ⊢ ¬ 0 = A ↔ ¬ A = 0
110 eqcom ⊢ 0 = B ↔ B = 0
111 110 notbii ⊢ ¬ 0 = B ↔ ¬ B = 0
112 109 111 anbi12i ⊢ ¬ 0 = A ∧ ¬ 0 = B ↔ ¬ A = 0 ∧ ¬ B = 0
113 112 biimpi ⊢ ¬ 0 = A ∧ ¬ 0 = B → ¬ A = 0 ∧ ¬ B = 0
114 ioran ⊢ ¬ A = 0 ∨ B = 0 ↔ ¬ A = 0 ∧ ¬ B = 0
115 113 114 sylibr ⊢ ¬ 0 = A ∧ ¬ 0 = B → ¬ A = 0 ∨ B = 0
116 115 3adant3 ⊢ ¬ 0 = A ∧ ¬ 0 = B ∧ ¬ 0 = C → ¬ A = 0 ∨ B = 0
117 107 116 sylbi ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C → ¬ A = 0 ∨ B = 0
118 id ⊢ A ∈ ℤ ∧ B ∈ ℤ → A ∈ ℤ ∧ B ∈ ℤ
119 118 3adant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∈ ℤ ∧ B ∈ ℤ
120 117 119 anim12ci ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ A = 0 ∨ B = 0
121 lcmn0cl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ A = 0 ∨ B = 0 → A lcm B ∈ ℕ
122 120 121 syl ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A lcm B ∈ ℕ
123 nnne0 ⊢ A lcm B ∈ ℕ → A lcm B ≠ 0
124 123 neneqd ⊢ A lcm B ∈ ℕ → ¬ A lcm B = 0
125 122 124 syl ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → ¬ A lcm B = 0
126 eqcom ⊢ 0 = C ↔ C = 0
127 126 notbii ⊢ ¬ 0 = C ↔ ¬ C = 0
128 127 biimpi ⊢ ¬ 0 = C → ¬ C = 0
129 128 3ad2ant3 ⊢ ¬ 0 = A ∧ ¬ 0 = B ∧ ¬ 0 = C → ¬ C = 0
130 107 129 sylbi ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C → ¬ C = 0
131 130 adantr ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → ¬ C = 0
132 125 131 jca ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → ¬ A lcm B = 0 ∧ ¬ C = 0
133 132 adantr ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ k ∈ ℕ → ¬ A lcm B = 0 ∧ ¬ C = 0
134 133 adantr ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ k ∈ ℕ ∧ A ∥ k ∧ B ∥ k ∧ C ∥ k → ¬ A lcm B = 0 ∧ ¬ C = 0
135 ioran ⊢ ¬ A lcm B = 0 ∨ C = 0 ↔ ¬ A lcm B = 0 ∧ ¬ C = 0
136 134 135 sylibr ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ k ∈ ℕ ∧ A ∥ k ∧ B ∥ k ∧ C ∥ k → ¬ A lcm B = 0 ∨ C = 0
137 119 adantl ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∈ ℤ ∧ B ∈ ℤ
138 nnz ⊢ k ∈ ℕ → k ∈ ℤ
139 137 138 anim12ci ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ k ∈ ℕ → k ∈ ℤ ∧ A ∈ ℤ ∧ B ∈ ℤ
140 3anass ⊢ k ∈ ℤ ∧ A ∈ ℤ ∧ B ∈ ℤ ↔ k ∈ ℤ ∧ A ∈ ℤ ∧ B ∈ ℤ
141 139 140 sylibr ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ k ∈ ℕ → k ∈ ℤ ∧ A ∈ ℤ ∧ B ∈ ℤ
142 lcmdvds ⊢ k ∈ ℤ ∧ A ∈ ℤ ∧ B ∈ ℤ → A ∥ k ∧ B ∥ k → A lcm B ∥ k
143 141 142 syl ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ k ∈ ℕ → A ∥ k ∧ B ∥ k → A lcm B ∥ k
144 143 com12 ⊢ A ∥ k ∧ B ∥ k → ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ k ∈ ℕ → A lcm B ∥ k
145 144 3adant3 ⊢ A ∥ k ∧ B ∥ k ∧ C ∥ k → ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ k ∈ ℕ → A lcm B ∥ k
146 145 impcom ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ k ∈ ℕ ∧ A ∥ k ∧ B ∥ k ∧ C ∥ k → A lcm B ∥ k
147 simp3 ⊢ A ∥ k ∧ B ∥ k ∧ C ∥ k → C ∥ k
148 147 adantl ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ k ∈ ℕ ∧ A ∥ k ∧ B ∥ k ∧ C ∥ k → C ∥ k
149 lcmledvds ⊢ k ∈ ℕ ∧ A lcm B ∈ ℤ ∧ C ∈ ℤ ∧ ¬ A lcm B = 0 ∨ C = 0 → A lcm B ∥ k ∧ C ∥ k → A lcm B lcm C ≤ k
150 149 imp ⊢ k ∈ ℕ ∧ A lcm B ∈ ℤ ∧ C ∈ ℤ ∧ ¬ A lcm B = 0 ∨ C = 0 ∧ A lcm B ∥ k ∧ C ∥ k → A lcm B lcm C ≤ k
151 106 136 146 148 150 syl22anc ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ k ∈ ℕ ∧ A ∥ k ∧ B ∥ k ∧ C ∥ k → A lcm B lcm C ≤ k
152 151 ex ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ k ∈ ℕ → A ∥ k ∧ B ∥ k ∧ C ∥ k → A lcm B lcm C ≤ k
153 101 152 sylbid ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ k ∈ ℕ → ∀ m ∈ A B C m ∥ k → A lcm B lcm C ≤ k
154 153 ralrimiva ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → ∀ k ∈ ℕ ∀ m ∈ A B C m ∥ k → A lcm B lcm C ≤ k
155 96 154 jca ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → ∀ m ∈ A B C m ∥ A lcm B lcm C ∧ ∀ k ∈ ℕ ∀ m ∈ A B C m ∥ k → A lcm B lcm C ≤ k
156 109 biimpi ⊢ ¬ 0 = A → ¬ A = 0
157 111 biimpi ⊢ ¬ 0 = B → ¬ B = 0
158 156 157 anim12i ⊢ ¬ 0 = A ∧ ¬ 0 = B → ¬ A = 0 ∧ ¬ B = 0
159 158 114 sylibr ⊢ ¬ 0 = A ∧ ¬ 0 = B → ¬ A = 0 ∨ B = 0
160 159 3adant3 ⊢ ¬ 0 = A ∧ ¬ 0 = B ∧ ¬ 0 = C → ¬ A = 0 ∨ B = 0
161 107 160 sylbi ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C → ¬ A = 0 ∨ B = 0
162 161 119 anim12ci ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ A = 0 ∨ B = 0
163 162 121 syl ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A lcm B ∈ ℕ
164 163 124 syl ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → ¬ A lcm B = 0
165 164 131 jca ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → ¬ A lcm B = 0 ∧ ¬ C = 0
166 165 135 sylibr ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → ¬ A lcm B = 0 ∨ C = 0
167 54 166 jca ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A lcm B ∈ ℤ ∧ C ∈ ℤ ∧ ¬ A lcm B = 0 ∨ C = 0
168 lcmn0cl ⊢ A lcm B ∈ ℤ ∧ C ∈ ℤ ∧ ¬ A lcm B = 0 ∨ C = 0 → A lcm B lcm C ∈ ℕ
169 167 168 syl ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A lcm B lcm C ∈ ℕ
170 5 adantl ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A B C ⊆ ℤ
171 tpfi ⊢ A B C ∈ Fin
172 171 a1i ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A B C ∈ Fin
173 3 a1i ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → 0 ∈ A B C ↔ 0 = A ∨ 0 = B ∨ 0 = C
174 173 biimpd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → 0 ∈ A B C → 0 = A ∨ 0 = B ∨ 0 = C
175 174 con3d ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → ¬ 0 = A ∨ 0 = B ∨ 0 = C → ¬ 0 ∈ A B C
176 175 impcom ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → ¬ 0 ∈ A B C
177 df-nel ⊢ 0 ∉ A B C ↔ ¬ 0 ∈ A B C
178 176 177 sylibr ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → 0 ∉ A B C
179 lcmf ⊢ A lcm B lcm C ∈ ℕ ∧ A B C ⊆ ℤ ∧ A B C ∈ Fin ∧ 0 ∉ A B C → A lcm B lcm C = lcm _ ⁡ A B C ↔ ∀ m ∈ A B C m ∥ A lcm B lcm C ∧ ∀ k ∈ ℕ ∀ m ∈ A B C m ∥ k → A lcm B lcm C ≤ k
180 169 170 172 178 179 syl13anc ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A lcm B lcm C = lcm _ ⁡ A B C ↔ ∀ m ∈ A B C m ∥ A lcm B lcm C ∧ ∀ k ∈ ℕ ∀ m ∈ A B C m ∥ k → A lcm B lcm C ≤ k
181 155 180 mpbird ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → A lcm B lcm C = lcm _ ⁡ A B C
182 181 eqcomd ⊢ ¬ 0 = A ∨ 0 = B ∨ 0 = C ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → lcm _ ⁡ A B C = A lcm B lcm C
183 50 182 pm2.61ian ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ → lcm _ ⁡ A B C = A lcm B lcm C