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 that
A1: a,p are_relative_prime and
A2: a,x * x are_congruent_mod p ; :: thesis: x,p are_relative_prime
assume not x,p are_relative_prime ; :: thesis: contradiction
then x gcd p = p by PEPIN:2;
then p divides x by NAT_D:def 5;
then A3: p divides x * x by NAT_D:9;
x * x,p are_relative_prime by A1, A2, Th31;
then (x * x) gcd p = 1 by INT_2:def 3;
then p divides 1 by A3, NAT_D:def 5;
then p = 1 by INT_2:13;
hence contradiction by INT_2:def 4; :: thesis: verum