let a be Integer; :: thesis: for p being Prime
for b being Integer st p > 2 & a gcd p = 1 & a,b are_congruent_mod p holds
Lege a,p = Lege b,p
let p be Prime; :: thesis: for b being Integer st p > 2 & a gcd p = 1 & a,b are_congruent_mod p holds
Lege a,p = Lege b,p
let b be Integer; :: thesis: ( p > 2 & a gcd p = 1 & a,b are_congruent_mod p implies Lege a,p = Lege b,p )
assume that
A1: p > 2 and
A2: a gcd p = 1 and
A3: a,b are_congruent_mod p ; :: thesis: Lege a,p = Lege b,p
Lege a,p,a |^ ((p -' 1) div 2) are_congruent_mod p by A1, A2, Th28;
then A4: (Lege a,p) mod p = (a |^ ((p -' 1) div 2)) mod p by INT_3:12;
b gcd p = 1 by A2, A3, INT_4:14;
then Lege b,p,b |^ ((p -' 1) div 2) are_congruent_mod p by A1, Th28;
then A5: (Lege b,p) mod p = (b |^ ((p -' 1) div 2)) mod p by INT_3:12;
a mod p = b mod p by A3, INT_3:12;
then (Lege a,p) mod p = (Lege b,p) mod p by A4, A5, Th13;
then Lege a,p, Lege b,p are_congruent_mod p by INT_3:12;
then A6: p divides (Lege a,p) - (Lege b,p) by INT_2:19;

per cases ( Lege a,p = 1 or Lege a,p = - 1 ) by Th25;

suppose A7: Lege a,p = 1 ; :: thesis: Lege a,p = Lege b,p

then Lege b,p <> - 1 by A1, A6, NAT_D:7;
hence Lege a,p = Lege b,p by A7, Th25; :: thesis: verum

end;

suppose A8: Lege a,p = - 1 ; :: thesis: Lege a,p = Lege b,p

now

assume Lege b,p = 1 ; :: thesis: contradiction
then p divides - 2 by A6, A8;
then p divides 2 by INT_2:14;
hence contradiction by A1, NAT_D:7; :: thesis: verum

end;

hence Lege a,p = Lege b,p by A8, Th25; :: thesis: verum

end;

end;