let p be natural prime number ; :: thesis: for x being integer number 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 number ; :: 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 ) )
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