let a, x be Integer; :: thesis: for p being Prime st a gcd p = 1 & ((x ^2) - a) mod p = 0 holds

x,p are_coprime

let p be Prime; :: thesis: ( a gcd p = 1 & ((x ^2) - a) mod p = 0 implies x,p are_coprime )

assume that

A1: a gcd p = 1 and

A2: ((x ^2) - a) mod p = 0 ; :: thesis: x,p are_coprime

assume not x,p are_coprime ; :: thesis: contradiction

then A3: p divides x ^2 by Lm2, INT_2:2;

p divides (x ^2) - a by A2, Lm1;

then p divides (x ^2) - ((x ^2) - a) by A3, Th1;

then p gcd a = |.p.| by Th12

.= p by ABSVALUE:def 1 ;

hence contradiction by A1, INT_2:def 4; :: thesis: verum

x,p are_coprime

let p be Prime; :: thesis: ( a gcd p = 1 & ((x ^2) - a) mod p = 0 implies x,p are_coprime )

assume that

A1: a gcd p = 1 and

A2: ((x ^2) - a) mod p = 0 ; :: thesis: x,p are_coprime

assume not x,p are_coprime ; :: thesis: contradiction

then A3: p divides x ^2 by Lm2, INT_2:2;

p divides (x ^2) - a by A2, Lm1;

then p divides (x ^2) - ((x ^2) - a) by A3, Th1;

then p gcd a = |.p.| by Th12

.= p by ABSVALUE:def 1 ;

hence contradiction by A1, INT_2:def 4; :: thesis: verum