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