let a, b be Nat; :: thesis: for n being prime Nat holds
( n divides a + b iff n divides (a |^ n) + (b |^ n) )
let n be prime Nat; :: thesis: ( n divides a + b iff n divides (a |^ n) + (b |^ n) )
( n divides (a |^ n) - a & n divides (b |^ n) - b ) by Th58;
then A1: n divides ((a |^ n) - a) + ((b |^ n) - b) by WSIERP_1:4;
A2: (a |^ n) + (b |^ n) = (a + b) + (((a |^ n) + (b |^ n)) - (a + b)) ;
hence ( n divides a + b implies n divides (a |^ n) + (b |^ n) ) by A1, WSIERP_1:4; :: thesis: ( n divides (a |^ n) + (b |^ n) implies n divides a + b )
assume n divides (a |^ n) + (b |^ n) ; :: thesis: n divides a + b
hence n divides a + b by A1, A2, INT_2:1; :: thesis: verum