let a, x be Integer; :: thesis: for p being Prime st a,p are_coprime & a,x * x are_congruent_mod p holds
x,p are_coprime
let p be Prime; :: thesis: ( a,p are_coprime & a,x * x are_congruent_mod p implies x,p are_coprime )
assume that
A1: a,p are_coprime and
A2: a,x * x are_congruent_mod p ; :: thesis: x,p are_coprime
x * x,p are_coprime by A1, A2, Th31;
then A3: (x * x) gcd p = 1 by INT_2:def 3;
assume A4: not x,p are_coprime ; :: thesis: contradiction
A5: x gcd p divides p by INT_2:21;
A6: x gcd p >= 0 ;
x gcd p divides x * x by INT_2:2, INT_2:21;
then ( x gcd p = 1 or x gcd p = - 1 ) by A3, A5, INT_2:13, INT_2:22;
hence contradiction by A4, A6, INT_2:def 3; :: thesis: verum