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_relative_prime
let p be Prime; :: thesis: ( a gcd p = 1 & ((x ^2 ) - a) mod p = 0 implies x,p are_relative_prime )
assume A1: ( a gcd p = 1 & ((x ^2 ) - a) mod p = 0 ) ; :: thesis: x,p are_relative_prime
then A2: p divides (x ^2 ) - a by Lm1;
assume not x,p are_relative_prime ; :: thesis: contradiction
then p divides x ^2 by Lm2, INT_2:12;
then p divides (x ^2 ) - ((x ^2 ) - a) by A2, Th1;
then p gcd a = abs p by Th12
.= p by ABSVALUE:def 1 ;
hence contradiction by A1, INT_2:def 5; :: thesis: verum