let a be Integer; :: thesis: for p being Prime st p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p holds
ex x, y being Integer st
( ((x ^2) - a) mod p = 0 & ((y ^2) - a) mod p = 0 & not x,y are_congruent_mod p )
let p be Prime; :: thesis: ( p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p implies ex x, y being Integer st
( ((x ^2) - a) mod p = 0 & ((y ^2) - a) mod p = 0 & not x,y are_congruent_mod p ) )
assume that
A1: p > 2 and
A2: a gcd p = 1 and
A3: a is_quadratic_residue_mod p ; :: thesis: ex x, y being Integer st
( ((x ^2) - a) mod p = 0 & ((y ^2) - a) mod p = 0 & not x,y are_congruent_mod p )
consider x being Integer such that
A4: ((x ^2) - a) mod p = 0 by A3, Def2;
take x ; :: thesis: ex y being Integer st
( ((x ^2) - a) mod p = 0 & ((y ^2) - a) mod p = 0 & not x,y are_congruent_mod p )
take - x ; :: thesis: ( ((x ^2) - a) mod p = 0 & (((- x) ^2) - a) mod p = 0 & not x, - x are_congruent_mod p )
not x, - x are_congruent_mod p

proof

assume x, - x are_congruent_mod p ; :: thesis: contradiction
then p divides x - (- x) by INT_2:15;
then A5: p divides 2 * x ;
2,p are_relative_prime by A1, INT_2:28, INT_2:30;
then 2 gcd p = 1 by INT_2:def 3;
then p divides x by A5, WSIERP_1:29;
then consider i being Integer such that
A6: x = p * i by INT_1:def 3;
x gcd p = (p * i) gcd (p * 1) by A6
.= p * (i gcd 1) by EULER_1:15
.= p * 1 by WSIERP_1:8 ;
then x gcd p <> 1 by INT_2:def 4;
then not x,p are_relative_prime by INT_2:def 3;
hence contradiction by A2, A4, Th14; :: thesis: verum

end;

hence ( ((x ^2) - a) mod p = 0 & (((- x) ^2) - a) mod p = 0 & not x, - x are_congruent_mod p ) by A4; :: thesis: verum