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;

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

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;

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

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

then A5: p divides 2 * x ;

2,p are_coprime 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 ;

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_coprime by INT_2:def 3;

hence contradiction by A2, A4, Th14; :: thesis: verum

end;then A5: p divides 2 * x ;

2,p are_coprime 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 ;

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_coprime by INT_2:def 3;

hence contradiction by A2, A4, Th14; :: thesis: verum