let a, b be Nat; :: thesis: ( not a,b are_coprime or ((a |^ 4) + (b |^ 4)) mod 5 = 1 or ((a |^ 4) + (b |^ 4)) mod 5 = 2 )
assume A1: a,b are_coprime ; :: thesis: ( ((a |^ 4) + (b |^ 4)) mod 5 = 1 or ((a |^ 4) + (b |^ 4)) mod 5 = 2 )
A3: ( not 5 divides a or not 5 divides b ) by A1, PEPIN:59, PYTHTRIP:def 2;
( ( (a |^ (5 - 1)) mod 5 = 0 or (a |^ (5 - 1)) mod 5 = 1 ) & ( (b |^ (5 - 1)) mod 5 = 0 or (b |^ (5 - 1)) mod 5 = 1 ) ) by PEPIN:59, MOP;

per cases then ( ( (a |^ 4) mod 5 = 0 & (b |^ 4) mod 5 = 0 ) or ( (a |^ 4) mod 5 = 0 & (b |^ 4) mod 5 = 1 ) or ( (a |^ 4) mod 5 = 1 & (b |^ 4) mod 5 = 0 ) or ( (a |^ 4) mod 5 = 1 & (b |^ 4) mod 5 = 1 ) ) ;

suppose ( (a |^ 4) mod 5 = 0 & (b |^ 4) mod 5 = 0 ) ; :: thesis: ( ((a |^ 4) + (b |^ 4)) mod 5 = 1 or ((a |^ 4) + (b |^ 4)) mod 5 = 2 )

then B1: ( 5 divides a |^ 4 & 5 divides b |^ 4 ) by INT_1:62;
( a |^ 4 divides a |^ (4 + 1) & b |^ 4 divides b |^ (4 + 1) ) by NEWTON:89;
then ( 5 divides a |^ 5 & 5 divides b |^ 5 ) by B1, INT_2:9;
hence ( ((a |^ 4) + (b |^ 4)) mod 5 = 1 or ((a |^ 4) + (b |^ 4)) mod 5 = 2 ) by A3, PEPIN:59, NEWTON02:160; :: thesis: verum

end;

suppose ( (a |^ 4) mod 5 = 0 & (b |^ 4) mod 5 = 1 ) ; :: thesis: ( ((a |^ 4) + (b |^ 4)) mod 5 = 1 or ((a |^ 4) + (b |^ 4)) mod 5 = 2 )

then ((a |^ 4) + (b |^ 4)) mod 5 = (0 + 1) mod (1 + 4) by NAT_D:66;
hence ( ((a |^ 4) + (b |^ 4)) mod 5 = 1 or ((a |^ 4) + (b |^ 4)) mod 5 = 2 ) ; :: thesis: verum

end;

suppose ( (a |^ 4) mod 5 = 1 & (b |^ 4) mod 5 = 0 ) ; :: thesis: ( ((a |^ 4) + (b |^ 4)) mod 5 = 1 or ((a |^ 4) + (b |^ 4)) mod 5 = 2 )

then ((a |^ 4) + (b |^ 4)) mod 5 = (1 + 0) mod (1 + 4) by NAT_D:66;
hence ( ((a |^ 4) + (b |^ 4)) mod 5 = 1 or ((a |^ 4) + (b |^ 4)) mod 5 = 2 ) ; :: thesis: verum

end;

suppose ( (a |^ 4) mod 5 = 1 & (b |^ 4) mod 5 = 1 ) ; :: thesis: ( ((a |^ 4) + (b |^ 4)) mod 5 = 1 or ((a |^ 4) + (b |^ 4)) mod 5 = 2 )

then ((a |^ 4) + (b |^ 4)) mod 5 = (1 + 1) mod (2 + 3) by NAT_D:66;
hence ( ((a |^ 4) + (b |^ 4)) mod 5 = 1 or ((a |^ 4) + (b |^ 4)) mod 5 = 2 ) ; :: thesis: verum

end;

end;