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 A1, A2, Def13; :: thesis: verum
end;
suppose A3: x = 1 ; :: thesis: x + (- x) = a
then - x = 2 by Def12;
hence x + (- x) = a by A1, A3, Def13; :: thesis: verum
end;
suppose A4: x = 2 ; :: thesis: x + (- x) = a
then - x = 1 by Def12;
hence x + (- x) = a by A1, A4, Def13; :: thesis: verum
end;
end;
end;
hence x + (- x) = a ; :: thesis: verum
end;
thus x + a = x by A1, Def13; :: 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 A5, Def13 ;
:: 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 A6, Def13; :: 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 A7, Def13; :: thesis: verum
end;
suppose A8: ( x = 1 & y = 1 & z = 1 ) ; :: thesis: (x + y) + z = x + (y + z)
thus (x + y) + z = 0 by A8, Def13
.= x + (y + z) by A8, Def13 ; :: 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 A9, Def13;
hence (x + y) + z = 1 by A9, Def13
.= x + (y + z) by A9, A10, Def13 ;
:: 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 A11, Def13;
hence (x + y) + z = 1 by A11, Def13
.= x + (y + z) by A11, A12, Def13 ;
:: 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 A13, Def13;
hence (x + y) + z = 2 by A13, Def13
.= x + (y + z) by A13, A14, Def13 ;
:: 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 A15, Def13;
hence (x + y) + z = 1 by A15, Def13
.= x + (y + z) by A15, A16, Def13 ;
:: 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 A17, Def13;
hence (x + y) + z = 2 by A17, Def13
.= x + (y + z) by A17, A18, Def13 ;
:: 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 A19, Def13;
hence (x + y) + z = 2 by A19, Def13
.= x + (y + z) by A19, A20, Def13 ;
:: thesis: verum
end;
suppose A21: ( x = 2 & y = 2 & z = 2 ) ; :: thesis: (x + y) + z = x + (y + z)
thus (x + y) + z = 0 by A21, Def13
.= x + (y + z) by A21, Def13 ; :: thesis: verum
end;
end;
end;
hence (x + y) + z = x + (y + z) ; :: thesis: verum
end;