let x, y, z, a be Element of {0,1,2}; :: thesis: ( a = 0 implies ( x + (- x) = a & x + a = x & (x + y) + z = x + (y + z) ) )
assume A1: a = 0 ; :: thesis: ( x + (- x) = a & x + a = x & (x + y) + z = x + (y + z) )
thus x + (- x) = a :: thesis: ( x + a = x & (x + y) + z = x + (y + z) )
proof
now :: thesis: x + (- x) = a
per cases ( x = 0 or x = 1 or x = 2 ) by ENUMSET1:def 1;
suppose A2: x = 0 ; :: thesis: x + (- x) = a
then - x = 0 by Def12;
hence x + (- x) = a by ; :: thesis: verum
end;
suppose A3: x = 1 ; :: thesis: x + (- x) = a
then - x = 2 by Def12;
hence x + (- x) = a by ; :: thesis: verum
end;
suppose A4: x = 2 ; :: thesis: x + (- x) = a
then - x = 1 by Def12;
hence x + (- x) = a by ; :: thesis: verum
end;
end;
end;
hence x + (- x) = a ; :: thesis: verum
end;
thus x + a = x by ; :: thesis: (x + y) + z = x + (y + z)
thus (x + y) + z = x + (y + z) :: thesis: verum
proof
now :: thesis: (x + y) + z = x + (y + z)
per cases ( x = 0 or y = 0 or z = 0 or ( x = 1 & y = 1 & z = 1 ) or ( x = 1 & y = 1 & z = 2 ) or ( x = 1 & y = 2 & z = 1 ) or ( x = 1 & y = 2 & z = 2 ) or ( x = 2 & y = 1 & z = 1 ) or ( x = 2 & y = 1 & z = 2 ) or ( x = 2 & y = 2 & z = 1 ) or ( x = 2 & y = 2 & z = 2 ) ) by ENUMSET1:def 1;
suppose A5: x = 0 ; :: thesis: (x + y) + z = x + (y + z)
hence (x + y) + z = y + z by Def13
.= x + (y + z) by ;
:: thesis: verum
end;
suppose A6: y = 0 ; :: thesis: (x + y) + z = x + (y + z)
then x + y = x by Def13;
hence (x + y) + z = x + (y + z) by ; :: thesis: verum
end;
suppose A7: z = 0 ; :: thesis: (x + y) + z = x + (y + z)
then y + z = y by Def13;
hence (x + y) + z = x + (y + z) by ; :: thesis: verum
end;
suppose A8: ( x = 1 & y = 1 & z = 1 ) ; :: thesis: (x + y) + z = x + (y + z)
thus (x + y) + z = 0 by
.= x + (y + z) by ; :: thesis: verum
end;
suppose A9: ( x = 1 & y = 1 & z = 2 ) ; :: thesis: (x + y) + z = x + (y + z)
then A10: y + z = 0 by Def13;
x + y = 2 by ;
hence (x + y) + z = 1 by
.= x + (y + z) by ;
:: thesis: verum
end;
suppose A11: ( x = 1 & y = 2 & z = 1 ) ; :: thesis: (x + y) + z = x + (y + z)
then A12: y + z = 0 by Def13;
x + y = 0 by ;
hence (x + y) + z = 1 by
.= x + (y + z) by ;
:: thesis: verum
end;
suppose A13: ( x = 1 & y = 2 & z = 2 ) ; :: thesis: (x + y) + z = x + (y + z)
then A14: y + z = 1 by Def13;
x + y = 0 by ;
hence (x + y) + z = 2 by
.= x + (y + z) by ;
:: thesis: verum
end;
suppose A15: ( x = 2 & y = 1 & z = 1 ) ; :: thesis: (x + y) + z = x + (y + z)
then A16: y + z = 2 by Def13;
x + y = 0 by ;
hence (x + y) + z = 1 by
.= x + (y + z) by ;
:: thesis: verum
end;
suppose A17: ( x = 2 & y = 1 & z = 2 ) ; :: thesis: (x + y) + z = x + (y + z)
then A18: y + z = 0 by Def13;
x + y = 0 by ;
hence (x + y) + z = 2 by
.= x + (y + z) by ;
:: thesis: verum
end;
suppose A19: ( x = 2 & y = 2 & z = 1 ) ; :: thesis: (x + y) + z = x + (y + z)
then A20: y + z = 0 by Def13;
x + y = 1 by ;
hence (x + y) + z = 2 by
.= x + (y + z) by ;
:: thesis: verum
end;
suppose A21: ( x = 2 & y = 2 & z = 2 ) ; :: thesis: (x + y) + z = x + (y + z)
thus (x + y) + z = 0 by
.= x + (y + z) by ; :: thesis: verum
end;
end;
end;
hence (x + y) + z = x + (y + z) ; :: thesis: verum
end;