let i, j, k be Integer; :: thesis: i gcd (j gcd k) = (i gcd j) gcd k

per cases ( ( i = 0 & j = 0 & k = 0 ) or i <> 0 or j <> 0 or k <> 0 ) ;

suppose ( i = 0 & j = 0 & k = 0 ) ; :: thesis: i gcd (j gcd k) = (i gcd j) gcd k

hence i gcd (j gcd k) = (i gcd j) gcd k ; :: thesis: verum

end;

suppose A1: ( i <> 0 or j <> 0 or k <> 0 ) ; :: thesis: i gcd (j gcd k) = (i gcd j) gcd k

A2: now :: thesis: not i gcd (j gcd k) = - ((i gcd j) gcd k)

assume i gcd (j gcd k) = - ((i gcd j) gcd k) ; :: thesis: contradiction
then (- ((i gcd j) gcd k)) * (- 1) <= 0 * (- 1) ;
then A3: (i gcd j) gcd k = 0 ;
then i gcd j = 0 by INT_2:5;
hence contradiction by A1, A3, INT_2:5; :: thesis: verum

end;

A4: i gcd (j gcd k) divides i by INT_2:21;
A5: (i gcd j) gcd k divides k by INT_2:21;
A6: (i gcd j) gcd k divides i gcd j by INT_2:21;
i gcd j divides j by INT_2:21;
then (i gcd j) gcd k divides j by A6, INT_2:9;
then A7: (i gcd j) gcd k divides j gcd k by A5, INT_2:22;
i gcd j divides i by INT_2:21;
then (i gcd j) gcd k divides i by A6, INT_2:9;
then A8: (i gcd j) gcd k divides i gcd (j gcd k) by A7, INT_2:22;
A9: i gcd (j gcd k) divides j gcd k by INT_2:21;
j gcd k divides j by INT_2:21;
then i gcd (j gcd k) divides j by A9, INT_2:9;
then A10: i gcd (j gcd k) divides i gcd j by A4, INT_2:22;
j gcd k divides k by INT_2:21;
then i gcd (j gcd k) divides k by A9, INT_2:9;
then i gcd (j gcd k) divides (i gcd j) gcd k by A10, INT_2:22;
hence i gcd (j gcd k) = (i gcd j) gcd k by A8, A2, INT_2:11; :: thesis: verum

end;

end;