let t be Integer; :: thesis: for n being prime Nat
for a, b being positive Nat st (n * a) * b divides ((a + t) |^ n) - ((a |^ n) + (b |^ n)) holds
(n * a) * b divides ((a + b) |^ n) - ((a + t) |^ n)
let n be prime Nat; :: thesis: for a, b being positive Nat st (n * a) * b divides ((a + t) |^ n) - ((a |^ n) + (b |^ n)) holds
(n * a) * b divides ((a + b) |^ n) - ((a + t) |^ n)
let a, b be positive Nat; :: thesis: ( (n * a) * b divides ((a + t) |^ n) - ((a |^ n) + (b |^ n)) implies (n * a) * b divides ((a + b) |^ n) - ((a + t) |^ n) )
assume A1: (n * a) * b divides ((a + t) |^ n) - ((a |^ n) + (b |^ n)) ; :: thesis: (n * a) * b divides ((a + b) |^ n) - ((a + t) |^ n)
(n * a) * b divides - (((a + b) |^ n) - ((a |^ n) + (b |^ n))) by INT_2:10, Th55;
then (n * a) * b divides (((a |^ n) + (b |^ n)) - ((a + b) |^ n)) + (((a + t) |^ n) - ((a |^ n) + (b |^ n))) by A1, WSIERP_1:4;
then (n * a) * b divides - (((a + b) |^ n) - ((a + t) |^ n)) ;
hence (n * a) * b divides ((a + b) |^ n) - ((a + t) |^ n) by INT_2:10; :: thesis: verum