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_⁡ABC=AlcmBlcmC

Proof

Step Hyp Ref Expression
1 0z ⊢0∈ℤ
2 eltpg ⊢0∈ℤ→0∈ABC↔0=A∨0=B∨0=C
3 1 2 ax-mp ⊢0∈ABC↔0=A∨0=B∨0=C
4 3 biimpri ⊢0=A∨0=B∨0=C→0∈ABC
5 tpssi ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→ABC⊆ℤ
6 4 5 anim12ci ⊢0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→ABC⊆ℤ∧0∈ABC
7 lcmf0val ⊢ABC⊆ℤ∧0∈ABC→lcm_⁡ABC=0
8 6 7 syl ⊢0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→lcm_⁡ABC=0
9 0zd ⊢C∈ℤ→0∈ℤ
10 lcmcom ⊢0∈ℤ∧C∈ℤ→0lcmC=Clcm0
11 9 10 mpancom ⊢C∈ℤ→0lcmC=Clcm0
12 lcm0val ⊢C∈ℤ→Clcm0=0
13 11 12 eqtrd ⊢C∈ℤ→0lcmC=0
14 13 eqcomd ⊢C∈ℤ→0=0lcmC
15 14 3ad2ant3 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→0=0lcmC
16 15 adantl ⊢0=A∧A∈ℤ∧B∈ℤ∧C∈ℤ→0=0lcmC
17 0zd ⊢B∈ℤ→0∈ℤ
18 lcmcom ⊢0∈ℤ∧B∈ℤ→0lcmB=Blcm0
19 17 18 mpancom ⊢B∈ℤ→0lcmB=Blcm0
20 lcm0val ⊢B∈ℤ→Blcm0=0
21 19 20 eqtrd ⊢B∈ℤ→0lcmB=0
22 21 eqcomd ⊢B∈ℤ→0=0lcmB
23 22 3ad2ant2 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→0=0lcmB
24 23 adantl ⊢0=A∧A∈ℤ∧B∈ℤ∧C∈ℤ→0=0lcmB
25 24 oveq1d ⊢0=A∧A∈ℤ∧B∈ℤ∧C∈ℤ→0lcmC=0lcmBlcmC
26 oveq1 ⊢0=A→0lcmB=AlcmB
27 26 oveq1d ⊢0=A→0lcmBlcmC=AlcmBlcmC
28 27 adantr ⊢0=A∧A∈ℤ∧B∈ℤ∧C∈ℤ→0lcmBlcmC=AlcmBlcmC
29 16 25 28 3eqtrd ⊢0=A∧A∈ℤ∧B∈ℤ∧C∈ℤ→0=AlcmBlcmC
30 lcm0val ⊢A∈ℤ→Alcm0=0
31 30 eqcomd ⊢A∈ℤ→0=Alcm0
32 31 3ad2ant1 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→0=Alcm0
33 32 adantl ⊢0=B∧A∈ℤ∧B∈ℤ∧C∈ℤ→0=Alcm0
34 33 oveq1d ⊢0=B∧A∈ℤ∧B∈ℤ∧C∈ℤ→0lcmC=Alcm0lcmC
35 13 3ad2ant3 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→0lcmC=0
36 35 adantl ⊢0=B∧A∈ℤ∧B∈ℤ∧C∈ℤ→0lcmC=0
37 oveq2 ⊢0=B→Alcm0=AlcmB
38 37 adantr ⊢0=B∧A∈ℤ∧B∈ℤ∧C∈ℤ→Alcm0=AlcmB
39 38 oveq1d ⊢0=B∧A∈ℤ∧B∈ℤ∧C∈ℤ→Alcm0lcmC=AlcmBlcmC
40 34 36 39 3eqtr3d ⊢0=B∧A∈ℤ∧B∈ℤ∧C∈ℤ→0=AlcmBlcmC
41 lcmcl ⊢A∈ℤ∧B∈ℤ→AlcmB∈ℕ0
42 41 nn0zd ⊢A∈ℤ∧B∈ℤ→AlcmB∈ℤ
43 lcm0val ⊢AlcmB∈ℤ→AlcmBlcm0=0
44 43 eqcomd ⊢AlcmB∈ℤ→0=AlcmBlcm0
45 42 44 syl ⊢A∈ℤ∧B∈ℤ→0=AlcmBlcm0
46 45 3adant3 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→0=AlcmBlcm0
47 oveq2 ⊢0=C→AlcmBlcm0=AlcmBlcmC
48 46 47 sylan9eqr ⊢0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→0=AlcmBlcmC
49 29 40 48 3jaoian ⊢0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→0=AlcmBlcmC
50 8 49 eqtrd ⊢0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→lcm_⁡ABC=AlcmBlcmC
51 42 3adant3 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→AlcmB∈ℤ
52 simp3 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→C∈ℤ
53 51 52 jca ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→AlcmB∈ℤ∧C∈ℤ
54 53 adantl ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→AlcmB∈ℤ∧C∈ℤ
55 dvdslcm ⊢AlcmB∈ℤ∧C∈ℤ→AlcmB∥AlcmBlcmC∧C∥AlcmBlcmC
56 54 55 syl ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→AlcmB∥AlcmBlcmC∧C∥AlcmBlcmC
57 dvdslcm ⊢A∈ℤ∧B∈ℤ→A∥AlcmB∧B∥AlcmB
58 57 3adant3 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→A∥AlcmB∧B∥AlcmB
59 simp1 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→A∈ℤ
60 lcmcl ⊢AlcmB∈ℤ∧C∈ℤ→AlcmBlcmC∈ℕ0
61 53 60 syl ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→AlcmBlcmC∈ℕ0
62 61 nn0zd ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→AlcmBlcmC∈ℤ
63 59 51 62 3jca ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→A∈ℤ∧AlcmB∈ℤ∧AlcmBlcmC∈ℤ
64 dvdstr ⊢A∈ℤ∧AlcmB∈ℤ∧AlcmBlcmC∈ℤ→A∥AlcmB∧AlcmB∥AlcmBlcmC→A∥AlcmBlcmC
65 63 64 syl ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→A∥AlcmB∧AlcmB∥AlcmBlcmC→A∥AlcmBlcmC
66 65 expd ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→A∥AlcmB→AlcmB∥AlcmBlcmC→A∥AlcmBlcmC
67 66 com12 ⊢A∥AlcmB→A∈ℤ∧B∈ℤ∧C∈ℤ→AlcmB∥AlcmBlcmC→A∥AlcmBlcmC
68 67 adantr ⊢A∥AlcmB∧B∥AlcmB→A∈ℤ∧B∈ℤ∧C∈ℤ→AlcmB∥AlcmBlcmC→A∥AlcmBlcmC
69 58 68 mpcom ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→AlcmB∥AlcmBlcmC→A∥AlcmBlcmC
70 69 adantl ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→AlcmB∥AlcmBlcmC→A∥AlcmBlcmC
71 70 com12 ⊢AlcmB∥AlcmBlcmC→¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→A∥AlcmBlcmC
72 71 adantr ⊢AlcmB∥AlcmBlcmC∧C∥AlcmBlcmC→¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→A∥AlcmBlcmC
73 72 impcom ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ∧AlcmB∥AlcmBlcmC∧C∥AlcmBlcmC→A∥AlcmBlcmC
74 simpr ⊢A∥AlcmB∧B∥AlcmB→B∥AlcmB
75 57 74 syl ⊢A∈ℤ∧B∈ℤ→B∥AlcmB
76 75 3adant3 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→B∥AlcmB
77 76 adantl ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→B∥AlcmB
78 simp2 ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→B∈ℤ
79 78 51 62 3jca ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→B∈ℤ∧AlcmB∈ℤ∧AlcmBlcmC∈ℤ
80 79 adantl ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→B∈ℤ∧AlcmB∈ℤ∧AlcmBlcmC∈ℤ
81 dvdstr ⊢B∈ℤ∧AlcmB∈ℤ∧AlcmBlcmC∈ℤ→B∥AlcmB∧AlcmB∥AlcmBlcmC→B∥AlcmBlcmC
82 80 81 syl ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→B∥AlcmB∧AlcmB∥AlcmBlcmC→B∥AlcmBlcmC
83 77 82 mpand ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→AlcmB∥AlcmBlcmC→B∥AlcmBlcmC
84 83 com12 ⊢AlcmB∥AlcmBlcmC→¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→B∥AlcmBlcmC
85 84 adantr ⊢AlcmB∥AlcmBlcmC∧C∥AlcmBlcmC→¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→B∥AlcmBlcmC
86 85 impcom ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ∧AlcmB∥AlcmBlcmC∧C∥AlcmBlcmC→B∥AlcmBlcmC
87 simpr ⊢AlcmB∥AlcmBlcmC∧C∥AlcmBlcmC→C∥AlcmBlcmC
88 87 adantl ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ∧AlcmB∥AlcmBlcmC∧C∥AlcmBlcmC→C∥AlcmBlcmC
89 73 86 88 3jca ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ∧AlcmB∥AlcmBlcmC∧C∥AlcmBlcmC→A∥AlcmBlcmC∧B∥AlcmBlcmC∧C∥AlcmBlcmC
90 56 89 mpdan ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→A∥AlcmBlcmC∧B∥AlcmBlcmC∧C∥AlcmBlcmC
91 breq1 ⊢m=A→m∥AlcmBlcmC↔A∥AlcmBlcmC
92 breq1 ⊢m=B→m∥AlcmBlcmC↔B∥AlcmBlcmC
93 breq1 ⊢m=C→m∥AlcmBlcmC↔C∥AlcmBlcmC
94 91 92 93 raltpg ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→∀m∈ABCm∥AlcmBlcmC↔A∥AlcmBlcmC∧B∥AlcmBlcmC∧C∥AlcmBlcmC
95 94 adantl ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→∀m∈ABCm∥AlcmBlcmC↔A∥AlcmBlcmC∧B∥AlcmBlcmC∧C∥AlcmBlcmC
96 90 95 mpbird ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→∀m∈ABCm∥AlcmBlcmC
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∈ABCm∥k↔A∥k∧B∥k∧C∥k
101 100 ad2antlr ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ∧k∈ℕ→∀m∈ABCm∥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∈ℕ→AlcmB∈ℤ
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∈ℕ∧AlcmB∈ℤ∧C∈ℤ
106 105 adantr ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ∧k∈ℕ∧A∥k∧B∥k∧C∥k→k∈ℕ∧AlcmB∈ℤ∧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→AlcmB∈ℕ
122 120 121 syl ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→AlcmB∈ℕ
123 nnne0 ⊢AlcmB∈ℕ→AlcmB≠0
124 123 neneqd ⊢AlcmB∈ℕ→¬AlcmB=0
125 122 124 syl ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→¬AlcmB=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∈ℤ→¬AlcmB=0∧¬C=0
133 132 adantr ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ∧k∈ℕ→¬AlcmB=0∧¬C=0
134 133 adantr ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ∧k∈ℕ∧A∥k∧B∥k∧C∥k→¬AlcmB=0∧¬C=0
135 ioran ⊢¬AlcmB=0∨C=0↔¬AlcmB=0∧¬C=0
136 134 135 sylibr ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ∧k∈ℕ∧A∥k∧B∥k∧C∥k→¬AlcmB=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→AlcmB∥k
143 141 142 syl ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ∧k∈ℕ→A∥k∧B∥k→AlcmB∥k
144 143 com12 ⊢A∥k∧B∥k→¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ∧k∈ℕ→AlcmB∥k
145 144 3adant3 ⊢A∥k∧B∥k∧C∥k→¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ∧k∈ℕ→AlcmB∥k
146 145 impcom ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ∧k∈ℕ∧A∥k∧B∥k∧C∥k→AlcmB∥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∈ℕ∧AlcmB∈ℤ∧C∈ℤ∧¬AlcmB=0∨C=0→AlcmB∥k∧C∥k→AlcmBlcmC≤k
150 149 imp ⊢k∈ℕ∧AlcmB∈ℤ∧C∈ℤ∧¬AlcmB=0∨C=0∧AlcmB∥k∧C∥k→AlcmBlcmC≤k
151 106 136 146 148 150 syl22anc ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ∧k∈ℕ∧A∥k∧B∥k∧C∥k→AlcmBlcmC≤k
152 151 ex ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ∧k∈ℕ→A∥k∧B∥k∧C∥k→AlcmBlcmC≤k
153 101 152 sylbid ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ∧k∈ℕ→∀m∈ABCm∥k→AlcmBlcmC≤k
154 153 ralrimiva ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→∀k∈ℕ∀m∈ABCm∥k→AlcmBlcmC≤k
155 96 154 jca ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→∀m∈ABCm∥AlcmBlcmC∧∀k∈ℕ∀m∈ABCm∥k→AlcmBlcmC≤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∈ℤ→AlcmB∈ℕ
164 163 124 syl ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→¬AlcmB=0
165 164 131 jca ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→¬AlcmB=0∧¬C=0
166 165 135 sylibr ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→¬AlcmB=0∨C=0
167 54 166 jca ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→AlcmB∈ℤ∧C∈ℤ∧¬AlcmB=0∨C=0
168 lcmn0cl ⊢AlcmB∈ℤ∧C∈ℤ∧¬AlcmB=0∨C=0→AlcmBlcmC∈ℕ
169 167 168 syl ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→AlcmBlcmC∈ℕ
170 5 adantl ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→ABC⊆ℤ
171 tpfi ⊢ABC∈Fin
172 171 a1i ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→ABC∈Fin
173 3 a1i ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→0∈ABC↔0=A∨0=B∨0=C
174 173 biimpd ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→0∈ABC→0=A∨0=B∨0=C
175 174 con3d ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→¬0=A∨0=B∨0=C→¬0∈ABC
176 175 impcom ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→¬0∈ABC
177 df-nel ⊢0∉ABC↔¬0∈ABC
178 176 177 sylibr ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→0∉ABC
179 lcmf ⊢AlcmBlcmC∈ℕ∧ABC⊆ℤ∧ABC∈Fin∧0∉ABC→AlcmBlcmC=lcm_⁡ABC↔∀m∈ABCm∥AlcmBlcmC∧∀k∈ℕ∀m∈ABCm∥k→AlcmBlcmC≤k
180 169 170 172 178 179 syl13anc ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→AlcmBlcmC=lcm_⁡ABC↔∀m∈ABCm∥AlcmBlcmC∧∀k∈ℕ∀m∈ABCm∥k→AlcmBlcmC≤k
181 155 180 mpbird ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→AlcmBlcmC=lcm_⁡ABC
182 181 eqcomd ⊢¬0=A∨0=B∨0=C∧A∈ℤ∧B∈ℤ∧C∈ℤ→lcm_⁡ABC=AlcmBlcmC
183 50 182 pm2.61ian ⊢A∈ℤ∧B∈ℤ∧C∈ℤ→lcm_⁡ABC=AlcmBlcmC