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 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( lcm ‘ { 𝐴 , 𝐵 , 𝐶 } ) = ( ( 𝐴 lcm 𝐵 ) lcm 𝐶 ) )

Proof

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