let a, b be Nat; :: thesis: ( ex k being Nat st
( a = (7 * k) + 1 or a = (7 * k) + 2 or a = (7 * k) + 4 ) & ex k being Nat st
( b = (7 * k) + 1 or b = (7 * k) + 2 or b = (7 * k) + 4 ) implies ex k being Nat st )
given k1 being Nat such that A1: ( a = (7 * k1) + 1 or a = (7 * k1) + 2 or a = (7 * k1) + 4 ) ; :: thesis: ( for k being Nat holds
( not b = (7 * k) + 1 & not b = (7 * k) + 2 & not b = (7 * k) + 4 ) or ex k being Nat st )
given k2 being Nat such that A2: ( b = (7 * k2) + 1 or b = (7 * k2) + 2 or b = (7 * k2) + 4 ) ; :: thesis: not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6
per cases ( ( a = (7 * k1) + 1 & b = (7 * k2) + 1 ) or ( a = (7 * k1) + 1 & b = (7 * k2) + 2 ) or ( a = (7 * k1) + 1 & b = (7 * k2) + 4 ) or ( a = (7 * k1) + 2 & b = (7 * k2) + 1 ) or ( a = (7 * k1) + 2 & b = (7 * k2) + 2 ) or ( a = (7 * k1) + 2 & b = (7 * k2) + 4 ) or ( a = (7 * k1) + 4 & b = (7 * k2) + 1 ) or ( a = (7 * k1) + 4 & b = (7 * k2) + 2 ) or ( a = (7 * k1) + 4 & b = (7 * k2) + 4 ) ) by A1, A2;
suppose A3: ( a = (7 * k1) + 1 & b = (7 * k2) + 1 ) ; :: thesis: not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6
not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6
proof
take k1 + k2 ; :: thesis: not not a + b = (7 * (k1 + k2)) + 1 & ... & not a + b = (7 * (k1 + k2)) + 6
thus not not a + b = (7 * (k1 + k2)) + 1 & ... & not a + b = (7 * (k1 + k2)) + 6 by A3; :: thesis: verum
end;
hence not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6 ; :: thesis: verum
end;
suppose A4: ( a = (7 * k1) + 1 & b = (7 * k2) + 2 ) ; :: thesis: not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6
not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6
proof
take k1 + k2 ; :: thesis: not not a + b = (7 * (k1 + k2)) + 1 & ... & not a + b = (7 * (k1 + k2)) + 6
thus not not a + b = (7 * (k1 + k2)) + 1 & ... & not a + b = (7 * (k1 + k2)) + 6 by A4; :: thesis: verum
end;
hence not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6 ; :: thesis: verum
end;
suppose A5: ( a = (7 * k1) + 1 & b = (7 * k2) + 4 ) ; :: thesis: not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6
not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6
proof
take k1 + k2 ; :: thesis: not not a + b = (7 * (k1 + k2)) + 1 & ... & not a + b = (7 * (k1 + k2)) + 6
thus not not a + b = (7 * (k1 + k2)) + 1 & ... & not a + b = (7 * (k1 + k2)) + 6 by A5; :: thesis: verum
end;
hence not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6 ; :: thesis: verum
end;
suppose A6: ( a = (7 * k1) + 2 & b = (7 * k2) + 1 ) ; :: thesis: not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6
not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6
proof
take k1 + k2 ; :: thesis: not not a + b = (7 * (k1 + k2)) + 1 & ... & not a + b = (7 * (k1 + k2)) + 6
thus not not a + b = (7 * (k1 + k2)) + 1 & ... & not a + b = (7 * (k1 + k2)) + 6 by A6; :: thesis: verum
end;
hence not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6 ; :: thesis: verum
end;
suppose A7: ( a = (7 * k1) + 2 & b = (7 * k2) + 2 ) ; :: thesis: not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6
not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6
proof
take k1 + k2 ; :: thesis: not not a + b = (7 * (k1 + k2)) + 1 & ... & not a + b = (7 * (k1 + k2)) + 6
thus not not a + b = (7 * (k1 + k2)) + 1 & ... & not a + b = (7 * (k1 + k2)) + 6 by A7; :: thesis: verum
end;
hence not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6 ; :: thesis: verum
end;
suppose A8: ( a = (7 * k1) + 2 & b = (7 * k2) + 4 ) ; :: thesis: not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6
not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6
proof
take k1 + k2 ; :: thesis: not not a + b = (7 * (k1 + k2)) + 1 & ... & not a + b = (7 * (k1 + k2)) + 6
thus not not a + b = (7 * (k1 + k2)) + 1 & ... & not a + b = (7 * (k1 + k2)) + 6 by A8; :: thesis: verum
end;
hence not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6 ; :: thesis: verum
end;
suppose A9: ( a = (7 * k1) + 4 & b = (7 * k2) + 1 ) ; :: thesis: not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6
not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6
proof
take k1 + k2 ; :: thesis: not not a + b = (7 * (k1 + k2)) + 1 & ... & not a + b = (7 * (k1 + k2)) + 6
thus not not a + b = (7 * (k1 + k2)) + 1 & ... & not a + b = (7 * (k1 + k2)) + 6 by A9; :: thesis: verum
end;
hence not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6 ; :: thesis: verum
end;
suppose A10: ( a = (7 * k1) + 4 & b = (7 * k2) + 2 ) ; :: thesis: not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6
not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6
proof
take k1 + k2 ; :: thesis: not not a + b = (7 * (k1 + k2)) + 1 & ... & not a + b = (7 * (k1 + k2)) + 6
thus not not a + b = (7 * (k1 + k2)) + 1 & ... & not a + b = (7 * (k1 + k2)) + 6 by A10; :: thesis: verum
end;
hence not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6 ; :: thesis: verum
end;
suppose A11: ( a = (7 * k1) + 4 & b = (7 * k2) + 4 ) ; :: thesis: not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6
not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6
proof
take (k1 + k2) + 1 ; :: thesis: not not a + b = (7 * ((k1 + k2) + 1)) + 1 & ... & not a + b = (7 * ((k1 + k2) + 1)) + 6
thus not not a + b = (7 * ((k1 + k2) + 1)) + 1 & ... & not a + b = (7 * ((k1 + k2) + 1)) + 6 by A11; :: thesis: verum
end;
hence not for k being Nat holds not a + b = (7 * k) + 1 & ... & not a + b = (7 * k) + 6 ; :: thesis: verum
end;
end;