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 that
A1: a gcd p = 1 and
A2: ((x ^2) - a) mod p = 0 ; :: thesis: x,p are_relative_prime
assume not x,p are_relative_prime ; :: 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 = abs p by Th12
.= p by ABSVALUE:def 1 ;
hence contradiction by A1, INT_2:def 4; :: thesis: verum