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 A1: ( a,p are_relative_prime & a,x * x are_congruent_mod p ) ; :: thesis: x,p are_relative_prime
assume A2: not x,p are_relative_prime ; :: thesis: contradiction
x * x,p are_relative_prime by A1, THP;
then A4: (x * x) gcd p = 1 by INT_2:def 4;
A5: ( x gcd p <> 1 & x gcd p >= 0 ) by A2, INT_2:def 4;
( x gcd p divides x * x & x gcd p divides p ) by INT_2:31, INT_2:12;
then ( x gcd p = 1 or x gcd p = - 1 ) by INT_2:33, INT_2:17, A4;
hence contradiction by A5; :: thesis: verum