let a, b be Nat; :: thesis: ( a,b are_coprime implies ((a |^ 4) - (b |^ 4)) mod 5 is square )
assume A1: a,b are_coprime ; :: thesis: ((a |^ 4) - (b |^ 4)) mod 5 is square
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 is square

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 is square by A3, PEPIN:59, NEWTON02:160; :: thesis: verum

end;

suppose B1: ( (a |^ 4) mod 5 = 0 & (b |^ 4) mod 5 = 1 ) ; :: thesis: ((a |^ 4) - (b |^ 4)) mod 5 is square

then (- (b |^ 4)) mod 5 = ((1 * 5) - (1 mod (1 + 4))) mod (4 + 1) by NEWTON02:86
.= 4 ;
then ((a |^ 4) + (- (b |^ 4))) mod 5 = (0 + 4) mod (4 + 1) by B1, NAT_D:66
.= 2 * 2 ;
hence ((a |^ 4) - (b |^ 4)) mod 5 is square ; :: thesis: verum

end;

suppose B1: ( (a |^ 4) mod 5 = 1 & (b |^ 4) mod 5 = 0 ) ; :: thesis: ((a |^ 4) - (b |^ 4)) mod 5 is square

then (- (b |^ 4)) mod 5 = ((1 * 5) - (0 mod 5)) mod 5 by NEWTON02:86
.= 0 ;
then ((a |^ 4) + (- (b |^ 4))) mod 5 = (1 + 0) mod (1 + 4) by B1, NAT_D:66
.= 1 * 1 ;
hence ((a |^ 4) - (b |^ 4)) mod 5 is square ; :: thesis: verum

end;

suppose B1: ( (a |^ 4) mod 5 = 1 & (b |^ 4) mod 5 = 1 ) ; :: thesis: ((a |^ 4) - (b |^ 4)) mod 5 is square

then (- (b |^ 4)) mod 5 = ((1 * 5) - (1 mod (1 + 4))) mod (4 + 1) by NEWTON02:86
.= 4 ;
then ((a |^ 4) + (- (b |^ 4))) mod 5 = (1 + 4) mod 5 by B1, NAT_D:66;
hence ((a |^ 4) - (b |^ 4)) mod 5 is square ; :: thesis: verum

end;

end;