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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( _lcm ` { A , B , C } ) = ( ( A lcm B ) lcm C ) )

Proof

Step Hyp Ref Expression
1 0z 
 |-  0 e. ZZ
2 eltpg 
 |-  ( 0 e. ZZ -> ( 0 e. { A , B , C } <-> ( 0 = A \/ 0 = B \/ 0 = C ) ) )
3 1 2 ax-mp 
 |-  ( 0 e. { A , B , C } <-> ( 0 = A \/ 0 = B \/ 0 = C ) )
4 3 biimpri 
 |-  ( ( 0 = A \/ 0 = B \/ 0 = C ) -> 0 e. { A , B , C } )
5 tpssi 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> { A , B , C } C_ ZZ )
6 4 5 anim12ci 
 |-  ( ( ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( { A , B , C } C_ ZZ /\ 0 e. { A , B , C } ) )
7 lcmf0val 
 |-  ( ( { A , B , C } C_ ZZ /\ 0 e. { A , B , C } ) -> ( _lcm ` { A , B , C } ) = 0 )
8 6 7 syl 
 |-  ( ( ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( _lcm ` { A , B , C } ) = 0 )
9 0zd 
 |-  ( C e. ZZ -> 0 e. ZZ )
10 lcmcom 
 |-  ( ( 0 e. ZZ /\ C e. ZZ ) -> ( 0 lcm C ) = ( C lcm 0 ) )
11 9 10 mpancom 
 |-  ( C e. ZZ -> ( 0 lcm C ) = ( C lcm 0 ) )
12 lcm0val 
 |-  ( C e. ZZ -> ( C lcm 0 ) = 0 )
13 11 12 eqtrd 
 |-  ( C e. ZZ -> ( 0 lcm C ) = 0 )
14 13 eqcomd 
 |-  ( C e. ZZ -> 0 = ( 0 lcm C ) )
15 14 3ad2ant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> 0 = ( 0 lcm C ) )
16 15 adantl 
 |-  ( ( 0 = A /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> 0 = ( 0 lcm C ) )
17 0zd 
 |-  ( B e. ZZ -> 0 e. ZZ )
18 lcmcom 
 |-  ( ( 0 e. ZZ /\ B e. ZZ ) -> ( 0 lcm B ) = ( B lcm 0 ) )
19 17 18 mpancom 
 |-  ( B e. ZZ -> ( 0 lcm B ) = ( B lcm 0 ) )
20 lcm0val 
 |-  ( B e. ZZ -> ( B lcm 0 ) = 0 )
21 19 20 eqtrd 
 |-  ( B e. ZZ -> ( 0 lcm B ) = 0 )
22 21 eqcomd 
 |-  ( B e. ZZ -> 0 = ( 0 lcm B ) )
23 22 3ad2ant2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> 0 = ( 0 lcm B ) )
24 23 adantl 
 |-  ( ( 0 = A /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> 0 = ( 0 lcm B ) )
25 24 oveq1d 
 |-  ( ( 0 = A /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( 0 lcm B ) lcm C ) = ( ( A lcm B ) lcm C ) )
29 16 25 28 3eqtrd 
 |-  ( ( 0 = A /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> 0 = ( ( A lcm B ) lcm C ) )
30 lcm0val 
 |-  ( A e. ZZ -> ( A lcm 0 ) = 0 )
31 30 eqcomd 
 |-  ( A e. ZZ -> 0 = ( A lcm 0 ) )
32 31 3ad2ant1 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> 0 = ( A lcm 0 ) )
33 32 adantl 
 |-  ( ( 0 = B /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> 0 = ( A lcm 0 ) )
34 33 oveq1d 
 |-  ( ( 0 = B /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( 0 lcm C ) = ( ( A lcm 0 ) lcm C ) )
35 13 3ad2ant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( 0 lcm C ) = 0 )
36 35 adantl 
 |-  ( ( 0 = B /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( 0 lcm C ) = 0 )
37 oveq2 
 |-  ( 0 = B -> ( A lcm 0 ) = ( A lcm B ) )
38 37 adantr 
 |-  ( ( 0 = B /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( A lcm 0 ) = ( A lcm B ) )
39 38 oveq1d 
 |-  ( ( 0 = B /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( A lcm 0 ) lcm C ) = ( ( A lcm B ) lcm C ) )
40 34 36 39 3eqtr3d 
 |-  ( ( 0 = B /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> 0 = ( ( A lcm B ) lcm C ) )
41 lcmcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A lcm B ) e. NN0 )
42 41 nn0zd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A lcm B ) e. ZZ )
43 lcm0val 
 |-  ( ( A lcm B ) e. ZZ -> ( ( A lcm B ) lcm 0 ) = 0 )
44 43 eqcomd 
 |-  ( ( A lcm B ) e. ZZ -> 0 = ( ( A lcm B ) lcm 0 ) )
45 42 44 syl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> 0 = ( ( A lcm B ) lcm 0 ) )
46 45 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> 0 = ( ( A lcm B ) lcm C ) )
49 29 40 48 3jaoian 
 |-  ( ( ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> 0 = ( ( A lcm B ) lcm C ) )
50 8 49 eqtrd 
 |-  ( ( ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( _lcm ` { A , B , C } ) = ( ( A lcm B ) lcm C ) )
51 42 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A lcm B ) e. ZZ )
52 simp3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> C e. ZZ )
53 51 52 jca 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( ( A lcm B ) e. ZZ /\ C e. ZZ ) )
54 53 adantl 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( A lcm B ) e. ZZ /\ C e. ZZ ) )
55 dvdslcm 
 |-  ( ( ( A lcm B ) e. ZZ /\ C e. ZZ ) -> ( ( 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( A lcm B ) || ( ( A lcm B ) lcm C ) /\ C || ( ( A lcm B ) lcm C ) ) )
57 dvdslcm 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A || ( A lcm B ) /\ B || ( A lcm B ) ) )
58 57 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A || ( A lcm B ) /\ B || ( A lcm B ) ) )
59 simp1 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> A e. ZZ )
60 lcmcl 
 |-  ( ( ( A lcm B ) e. ZZ /\ C e. ZZ ) -> ( ( A lcm B ) lcm C ) e. NN0 )
61 53 60 syl 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( ( A lcm B ) lcm C ) e. NN0 )
62 61 nn0zd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( ( A lcm B ) lcm C ) e. ZZ )
63 59 51 62 3jca 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A e. ZZ /\ ( A lcm B ) e. ZZ /\ ( ( A lcm B ) lcm C ) e. ZZ ) )
64 dvdstr 
 |-  ( ( A e. ZZ /\ ( A lcm B ) e. ZZ /\ ( ( A lcm B ) lcm C ) e. ZZ ) -> ( ( A || ( A lcm B ) /\ ( A lcm B ) || ( ( A lcm B ) lcm C ) ) -> A || ( ( A lcm B ) lcm C ) ) )
65 63 64 syl 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( ( A || ( A lcm B ) /\ ( A lcm B ) || ( ( A lcm B ) lcm C ) ) -> A || ( ( A lcm B ) lcm C ) ) )
66 65 expd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( ( 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( ( A lcm B ) || ( ( A lcm B ) lcm C ) -> A || ( ( A lcm B ) lcm C ) ) ) )
69 58 68 mpcom 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( ( A lcm B ) || ( ( A lcm B ) lcm C ) -> A || ( ( A lcm B ) lcm C ) ) )
70 69 adantl 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> A || ( ( A lcm B ) lcm C ) ) )
73 72 impcom 
 |-  ( ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ ( ( 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 e. ZZ /\ B e. ZZ ) -> B || ( A lcm B ) )
76 75 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> B || ( A lcm B ) )
77 76 adantl 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> B || ( A lcm B ) )
78 simp2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> B e. ZZ )
79 78 51 62 3jca 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( B e. ZZ /\ ( A lcm B ) e. ZZ /\ ( ( A lcm B ) lcm C ) e. ZZ ) )
80 79 adantl 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( B e. ZZ /\ ( A lcm B ) e. ZZ /\ ( ( A lcm B ) lcm C ) e. ZZ ) )
81 dvdstr 
 |-  ( ( B e. ZZ /\ ( A lcm B ) e. ZZ /\ ( ( A lcm B ) lcm C ) e. ZZ ) -> ( ( 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> B || ( ( A lcm B ) lcm C ) ) )
86 85 impcom 
 |-  ( ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ ( ( 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ ( ( 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ ( ( 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A. m e. { 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( A. m e. { 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> A. m e. { 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A. m e. { A , B , C } m || k <-> ( A || k /\ B || k /\ C || k ) ) )
101 100 ad2antlr 
 |-  ( ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ k e. NN ) -> ( A. m e. { A , B , C } m || k <-> ( A || k /\ B || k /\ C || k ) ) )
102 simpr 
 |-  ( ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ k e. NN ) -> k e. NN )
103 51 ad2antlr 
 |-  ( ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ k e. NN ) -> ( A lcm B ) e. ZZ )
104 52 ad2antlr 
 |-  ( ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ k e. NN ) -> C e. ZZ )
105 102 103 104 3jca 
 |-  ( ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ k e. NN ) -> ( k e. NN /\ ( A lcm B ) e. ZZ /\ C e. ZZ ) )
106 105 adantr 
 |-  ( ( ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ k e. NN ) /\ ( A || k /\ B || k /\ C || k ) ) -> ( k e. NN /\ ( A lcm B ) e. ZZ /\ C e. ZZ ) )
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 e. ZZ /\ B e. ZZ ) -> ( A e. ZZ /\ B e. ZZ ) )
119 118 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A e. ZZ /\ B e. ZZ ) )
120 117 119 anim12ci 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( A e. ZZ /\ B e. ZZ ) /\ -. ( A = 0 \/ B = 0 ) ) )
121 lcmn0cl 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ -. ( A = 0 \/ B = 0 ) ) -> ( A lcm B ) e. NN )
122 120 121 syl 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( A lcm B ) e. NN )
123 nnne0 
 |-  ( ( A lcm B ) e. NN -> ( A lcm B ) =/= 0 )
124 123 neneqd 
 |-  ( ( A lcm B ) e. NN -> -. ( A lcm B ) = 0 )
125 122 124 syl 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> -. ( 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> -. C = 0 )
132 125 131 jca 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( -. ( A lcm B ) = 0 /\ -. C = 0 ) )
133 132 adantr 
 |-  ( ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ k e. NN ) -> ( -. ( A lcm B ) = 0 /\ -. C = 0 ) )
134 133 adantr 
 |-  ( ( ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ k e. NN ) /\ ( 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ k e. NN ) /\ ( A || k /\ B || k /\ C || k ) ) -> -. ( ( A lcm B ) = 0 \/ C = 0 ) )
137 119 adantl 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( A e. ZZ /\ B e. ZZ ) )
138 nnz 
 |-  ( k e. NN -> k e. ZZ )
139 137 138 anim12ci 
 |-  ( ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ k e. NN ) -> ( k e. ZZ /\ ( A e. ZZ /\ B e. ZZ ) ) )
140 3anass 
 |-  ( ( k e. ZZ /\ A e. ZZ /\ B e. ZZ ) <-> ( k e. ZZ /\ ( A e. ZZ /\ B e. ZZ ) ) )
141 139 140 sylibr 
 |-  ( ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ k e. NN ) -> ( k e. ZZ /\ A e. ZZ /\ B e. ZZ ) )
142 lcmdvds 
 |-  ( ( k e. ZZ /\ A e. ZZ /\ B e. ZZ ) -> ( ( A || k /\ B || k ) -> ( A lcm B ) || k ) )
143 141 142 syl 
 |-  ( ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ k e. NN ) -> ( ( A || k /\ B || k ) -> ( A lcm B ) || k ) )
144 143 com12 
 |-  ( ( A || k /\ B || k ) -> ( ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ k e. NN ) -> ( A lcm B ) || k ) )
145 144 3adant3 
 |-  ( ( A || k /\ B || k /\ C || k ) -> ( ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ k e. NN ) -> ( A lcm B ) || k ) )
146 145 impcom 
 |-  ( ( ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ k e. NN ) /\ ( 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ k e. NN ) /\ ( A || k /\ B || k /\ C || k ) ) -> C || k )
149 lcmledvds 
 |-  ( ( ( k e. NN /\ ( A lcm B ) e. ZZ /\ C e. ZZ ) /\ -. ( ( A lcm B ) = 0 \/ C = 0 ) ) -> ( ( ( A lcm B ) || k /\ C || k ) -> ( ( A lcm B ) lcm C ) <_ k ) )
150 149 imp 
 |-  ( ( ( ( k e. NN /\ ( A lcm B ) e. ZZ /\ C e. ZZ ) /\ -. ( ( 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ k e. NN ) /\ ( A || k /\ B || k /\ C || k ) ) -> ( ( A lcm B ) lcm C ) <_ k )
152 151 ex 
 |-  ( ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ k e. NN ) -> ( ( A || k /\ B || k /\ C || k ) -> ( ( A lcm B ) lcm C ) <_ k ) )
153 101 152 sylbid 
 |-  ( ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) /\ k e. NN ) -> ( A. m e. { A , B , C } m || k -> ( ( A lcm B ) lcm C ) <_ k ) )
154 153 ralrimiva 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> A. k e. NN ( A. m e. { A , B , C } m || k -> ( ( A lcm B ) lcm C ) <_ k ) )
155 96 154 jca 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( A. m e. { A , B , C } m || ( ( A lcm B ) lcm C ) /\ A. k e. NN ( A. m e. { 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( A e. ZZ /\ B e. ZZ ) /\ -. ( A = 0 \/ B = 0 ) ) )
163 162 121 syl 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( A lcm B ) e. NN )
164 163 124 syl 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> -. ( A lcm B ) = 0 )
165 164 131 jca 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( -. ( A lcm B ) = 0 /\ -. C = 0 ) )
166 165 135 sylibr 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> -. ( ( A lcm B ) = 0 \/ C = 0 ) )
167 54 166 jca 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( ( A lcm B ) e. ZZ /\ C e. ZZ ) /\ -. ( ( A lcm B ) = 0 \/ C = 0 ) ) )
168 lcmn0cl 
 |-  ( ( ( ( A lcm B ) e. ZZ /\ C e. ZZ ) /\ -. ( ( A lcm B ) = 0 \/ C = 0 ) ) -> ( ( A lcm B ) lcm C ) e. NN )
169 167 168 syl 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( A lcm B ) lcm C ) e. NN )
170 5 adantl 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> { A , B , C } C_ ZZ )
171 tpfi 
 |-  { A , B , C } e. Fin
172 171 a1i 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> { A , B , C } e. Fin )
173 3 a1i 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( 0 e. { A , B , C } <-> ( 0 = A \/ 0 = B \/ 0 = C ) ) )
174 173 biimpd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( 0 e. { A , B , C } -> ( 0 = A \/ 0 = B \/ 0 = C ) ) )
175 174 con3d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( -. ( 0 = A \/ 0 = B \/ 0 = C ) -> -. 0 e. { A , B , C } ) )
176 175 impcom 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> -. 0 e. { A , B , C } )
177 df-nel 
 |-  ( 0 e/ { A , B , C } <-> -. 0 e. { A , B , C } )
178 176 177 sylibr 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> 0 e/ { A , B , C } )
179 lcmf 
 |-  ( ( ( ( A lcm B ) lcm C ) e. NN /\ ( { A , B , C } C_ ZZ /\ { A , B , C } e. Fin /\ 0 e/ { A , B , C } ) ) -> ( ( ( A lcm B ) lcm C ) = ( _lcm ` { A , B , C } ) <-> ( A. m e. { A , B , C } m || ( ( A lcm B ) lcm C ) /\ A. k e. NN ( A. m e. { 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 e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( ( A lcm B ) lcm C ) = ( _lcm ` { A , B , C } ) <-> ( A. m e. { A , B , C } m || ( ( A lcm B ) lcm C ) /\ A. k e. NN ( A. m e. { A , B , C } m || k -> ( ( A lcm B ) lcm C ) <_ k ) ) ) )
181 155 180 mpbird 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( A lcm B ) lcm C ) = ( _lcm ` { A , B , C } ) )
182 181 eqcomd 
 |-  ( ( -. ( 0 = A \/ 0 = B \/ 0 = C ) /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( _lcm ` { A , B , C } ) = ( ( A lcm B ) lcm C ) )
183 50 182 pm2.61ian 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( _lcm ` { A , B , C } ) = ( ( A lcm B ) lcm C ) )