let a, b be Nat; :: thesis: ( ( a mod 7 = 1 or a mod 7 = 2 or a mod 7 = 4 ) & ( b mod 7 = 1 or b mod 7 = 2 or b mod 7 = 4 ) implies not not (a + b) mod 7 = 1 & ... & not (a + b) mod 7 = 6 )
A1: (a + b) mod 7 = ((a mod 7) + (b mod 7)) mod 7 by NAT_D:66;
assume ( ( a mod 7 = 1 or a mod 7 = 2 or a mod 7 = 4 ) & ( b mod 7 = 1 or b mod 7 = 2 or b mod 7 = 4 ) ) ; :: thesis: not not (a + b) mod 7 = 1 & ... & not (a + b) mod 7 = 6

per cases then ( ( a mod 7 = 1 & b mod 7 = 1 ) or ( a mod 7 = 1 & b mod 7 = 2 ) or ( a mod 7 = 1 & b mod 7 = 4 ) or ( a mod 7 = 2 & b mod 7 = 1 ) or ( a mod 7 = 2 & b mod 7 = 2 ) or ( a mod 7 = 2 & b mod 7 = 4 ) or ( a mod 7 = 4 & b mod 7 = 1 ) or ( a mod 7 = 4 & b mod 7 = 2 ) or ( a mod 7 = 4 & b mod 7 = 4 ) ) ;

suppose ( ( a mod 7 = 1 & b mod 7 = 1 ) or ( a mod 7 = 1 & b mod 7 = 2 ) or ( a mod 7 = 1 & b mod 7 = 4 ) or ( a mod 7 = 2 & b mod 7 = 1 ) or ( a mod 7 = 2 & b mod 7 = 2 ) or ( a mod 7 = 2 & b mod 7 = 4 ) or ( a mod 7 = 4 & b mod 7 = 1 ) or ( a mod 7 = 4 & b mod 7 = 2 ) ) ; :: thesis: not not (a + b) mod 7 = 1 & ... & not (a + b) mod 7 = 6

hence not not (a + b) mod 7 = 1 & ... & not (a + b) mod 7 = 6 by A1, NAT_D:24; :: thesis: verum

end;

suppose A2: ( a mod 7 = 4 & b mod 7 = 4 ) ; :: thesis: not not (a + b) mod 7 = 1 & ... & not (a + b) mod 7 = 6

thus not not (a + b) mod 7 = 1 & ... & not (a + b) mod 7 = 6 :: thesis: verum

proof

take 1 ; :: thesis: ( 1 <= 1 & 1 <= 6 & (a + b) mod 7 = 1 )
(a + b) mod 7 = ((7 * 1) + 1) mod 7 by A1, A2;
hence ( 1 <= 1 & 1 <= 6 & (a + b) mod 7 = 1 ) by Th16; :: thesis: verum

end;

end;

end;