let a, x be Nat; 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; ( 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
; x,p are_coprime
assume
not x,p are_coprime
; 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_coprime
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; verum