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