let p be Prime; :: thesis: for x being Integer holds
( x |^ 2,1 are_congruent_mod p iff ( x,1 are_congruent_mod p or x, - 1 are_congruent_mod p ) )
let x be Integer; :: thesis: ( x |^ 2,1 are_congruent_mod p iff ( x,1 are_congruent_mod p or x, - 1 are_congruent_mod p ) )

A1: now :: thesis: ( not x |^ 2,1 are_congruent_mod p or x,1 are_congruent_mod p or x, - 1 are_congruent_mod p )

assume x |^ 2,1 are_congruent_mod p ; :: thesis: ( x,1 are_congruent_mod p or x, - 1 are_congruent_mod p )
then p divides (x ^2) - (1 ^2) by NEWTON:81;
then A2: p divides (x + 1) * (x - 1) ;

now :: thesis: ( ( p divides x + 1 & x, - 1 are_congruent_mod p ) or ( p divides x - 1 & x,1 are_congruent_mod p ) )

per cases ( p divides x + 1 or p divides x - 1 ) by A2, Th7;

case p divides x + 1 ; :: thesis: x, - 1 are_congruent_mod p

then consider l being Integer such that
A3: p * l = x + 1 ;
thus x, - 1 are_congruent_mod p by A3; :: thesis: verum

end;

case p divides x - 1 ; :: thesis: x,1 are_congruent_mod p

then consider l being Integer such that
A4: p * l = x - 1 ;
thus x,1 are_congruent_mod p by A4; :: thesis: verum

end;

end;

end;

hence ( x,1 are_congruent_mod p or x, - 1 are_congruent_mod p ) ; :: thesis: verum

end;

now :: thesis: ( ( x,1 are_congruent_mod p or x, - 1 are_congruent_mod p ) implies x |^ 2,1 are_congruent_mod p )

assume A5: ( x,1 are_congruent_mod p or x, - 1 are_congruent_mod p ) ; :: thesis: x |^ 2,1 are_congruent_mod p

now :: thesis: ( ( x,1 are_congruent_mod p & x |^ 2,1 are_congruent_mod p ) or ( x, - 1 are_congruent_mod p & x |^ 2,1 are_congruent_mod p ) )

per cases ( x,1 are_congruent_mod p or x, - 1 are_congruent_mod p ) by A5;

case x,1 are_congruent_mod p ; :: thesis: x |^ 2,1 are_congruent_mod p

then x * x,1 * 1 are_congruent_mod p by INT_1:18;
hence x |^ 2,1 are_congruent_mod p by NEWTON:81; :: thesis: verum

end;

case x, - 1 are_congruent_mod p ; :: thesis: x |^ 2,1 are_congruent_mod p

then x * x,(- 1) * (- 1) are_congruent_mod p by INT_1:18;
hence x |^ 2,1 are_congruent_mod p by NEWTON:81; :: thesis: verum

end;

end;

end;

hence x |^ 2,1 are_congruent_mod p ; :: thesis: verum

end;

hence ( x |^ 2,1 are_congruent_mod p iff ( x,1 are_congruent_mod p or x, - 1 are_congruent_mod p ) ) by A1; :: thesis: verum