let a, b be odd Nat; :: thesis: ( not a,b are_coprime or (((a |^ 4) + (b |^ 4)) / 2) mod 5 = 3 or (((a |^ 4) + (b |^ 4)) / 2) mod 5 = 1 )
assume A1: a,b are_coprime ; :: thesis: ( (((a |^ 4) + (b |^ 4)) / 2) mod 5 = 3 or (((a |^ 4) + (b |^ 4)) / 2) mod 5 = 1 )
reconsider n = ((a |^ 4) + (b |^ 4)) / 2 as Nat ;
A2: ((a |^ 4) + (b |^ 4)) mod 5 = (2 * n) mod (4 + 1)
.= ((2 mod (2 + 3)) * (n mod 5)) mod 5 by NAT_D:67
.= (2 * (n mod 5)) mod 5 ;
not not n mod (4 + 1) = 0 & ... & not n mod (4 + 1) = 4 by NUMBER03:11;

per cases then ( n mod (4 + 1) = 0 or n mod (4 + 1) = 1 or n mod (4 + 1) = 2 or n mod (4 + 1) = 3 or n mod (4 + 1) = 4 ) ;

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

hence ( (((a |^ 4) + (b |^ 4)) / 2) mod 5 = 3 or (((a |^ 4) + (b |^ 4)) / 2) mod 5 = 1 ) by A1, A2, MO5; :: thesis: verum

end;

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

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

end;

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

hence ( (((a |^ 4) + (b |^ 4)) / 2) mod 5 = 3 or (((a |^ 4) + (b |^ 4)) / 2) mod 5 = 1 ) by A1, A2, MO5; :: thesis: verum

end;

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

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

end;

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

then ((a |^ 4) + (b |^ 4)) mod 5 = ((1 * 5) + 3) mod 5 by A2
.= 3 mod (3 + 2) by NAT_D:21
.= 3 ;
hence ( (((a |^ 4) + (b |^ 4)) / 2) mod 5 = 3 or (((a |^ 4) + (b |^ 4)) / 2) mod 5 = 1 ) by A1, MO5; :: thesis: verum

end;

end;