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 NAT_D:64;
b gcd p = 1 by ;
then Lege (b,p),b |^ ((p -' 1) div 2) are_congruent_mod p by ;
then A5: (Lege (b,p)) mod p = (b |^ ((p -' 1) div 2)) mod p by NAT_D:64;
a mod p = b mod p by ;
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 NAT_D:64;
then A6: p divides (Lege (a,p)) - (Lege (b,p)) ;
per cases ( Lege (a,p) = 1 or Lege (a,p) = 0 or Lege (a,p) = - 1 ) by Th25;
suppose A7: Lege (a,p) = 1 ; :: thesis: Lege (a,p) = Lege (b,p)
A8: now :: thesis: not Lege (b,p) = 0
assume Lege (b,p) = 0 ; :: thesis: contradiction
then p = 1 by ;
hence contradiction by A1; :: thesis: verum
end;
Lege (b,p) <> - 1 by ;
hence Lege (a,p) = Lege (b,p) by A7, A8, Th25; :: thesis: verum
end;
suppose A9: Lege (a,p) = 0 ; :: thesis: Lege (a,p) = Lege (b,p)
A10: now :: thesis: not Lege (b,p) = 1
assume Lege (b,p) = 1 ; :: thesis: contradiction
then p = 1 by ;
hence contradiction by A1; :: thesis: verum
end;
now :: thesis: not Lege (b,p) = - 1
assume Lege (b,p) = - 1 ; :: thesis: contradiction
then p = 1 by ;
hence contradiction by A1; :: thesis: verum
end;
hence Lege (a,p) = Lege (b,p) by ; :: thesis: verum
end;
suppose A11: Lege (a,p) = - 1 ; :: thesis: Lege (a,p) = Lege (b,p)
A12: now :: thesis: not Lege (b,p) = 1end;
now :: thesis: not Lege (b,p) = 0
assume Lege (b,p) = 0 ; :: thesis: contradiction
then p = 1 by ;
hence contradiction by A1; :: thesis: verum
end;
hence Lege (a,p) = Lege (b,p) by ; :: thesis: verum
end;
end;