let a, b, n be Nat; :: thesis: ( not 3 divides a & not 3 divides b & not 3 divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) implies 3 divides (a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1)) )
assume ( not 3 divides a & not 3 divides b ) ; :: thesis: ( 3 divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) or 3 divides (a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1)) )
per cases then ( ( 3 divides a + 1 & 3 divides b + 1 ) or ( 3 divides a - 1 & 3 divides b - 1 ) or ( 3 divides a - 1 & 3 divides b + 1 ) or ( 3 divides a + 1 & 3 divides b - 1 ) ) by Th90;
suppose ( 3 divides a + 1 & 3 divides b + 1 ) ; :: thesis: ( 3 divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) or 3 divides (a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1)) )
then ( 3 divides (a + 1) - (b + 1) & a - b divides (a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1)) ) by INT_5:1, NEWTON01:33;
hence ( 3 divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) or 3 divides (a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1)) ) by INT_2:9; :: thesis: verum
end;
suppose ( 3 divides a - 1 & 3 divides b - 1 ) ; :: thesis: ( 3 divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) or 3 divides (a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1)) )
then ( 3 divides (a - 1) - (b - 1) & a - b divides (a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1)) ) by INT_5:1, NEWTON01:33;
hence ( 3 divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) or 3 divides (a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1)) ) by INT_2:9; :: thesis: verum
end;
suppose ( 3 divides a - 1 & 3 divides b + 1 ) ; :: thesis: ( 3 divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) or 3 divides (a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1)) )
then ( 3 divides (a - 1) + (b + 1) & a + b divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) ) by WSIERP_1:4, NEWTON01:35;
hence ( 3 divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) or 3 divides (a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1)) ) by INT_2:9; :: thesis: verum
end;
suppose ( 3 divides a + 1 & 3 divides b - 1 ) ; :: thesis: ( 3 divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) or 3 divides (a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1)) )
then ( 3 divides (a + 1) + (b - 1) & a + b divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) ) by WSIERP_1:4, NEWTON01:35;
hence ( 3 divides (a |^ ((2 * n) + 1)) + (b |^ ((2 * n) + 1)) or 3 divides (a |^ ((2 * n) + 1)) - (b |^ ((2 * n) + 1)) ) by INT_2:9; :: thesis: verum
end;
end;