let a, x be Nat; :: 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
reconsider ai = a, dpi = p, xx = x * x as Integer ;
x * x,p are_relative_prime by A1, THP;
then A4: (x * x) gcd p = 1 by INT_2:def 4;
x gcd p = p by A2, PEPIN:2;
then p divides x by NAT_D:def 5;
then ( p divides x * x & p divides p ) by NAT_D:9;
then p divides 1 by A4, NAT_D:def 5;
then p = 1 by INT_2:17;
hence contradiction by INT_2:def 5; :: thesis: verum