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 A2, A3, WSIERP_1:43;

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 NAT_D:64;

a mod p = b mod p by A3, NAT_D:64;

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)) ;

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 A2, A3, WSIERP_1:43;

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 NAT_D:64;

a mod p = b mod p by A3, NAT_D:64;

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;

end;

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

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

end;

A8: now :: thesis: not Lege (b,p) = 0

Lege (b,p) <> - 1
by A7, A1, A6, NAT_D:7;assume
Lege (b,p) = 0
; :: thesis: contradiction

then p = 1 by A6, A7, WSIERP_1:15;

hence contradiction by A1; :: thesis: verum

end;then p = 1 by A6, A7, WSIERP_1:15;

hence contradiction by A1; :: thesis: verum

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

suppose A9:
Lege (a,p) = 0
; :: thesis: Lege (a,p) = Lege (b,p)

end;

A10: now :: thesis: not Lege (b,p) = 1

assume
Lege (b,p) = 1
; :: thesis: contradiction

then p = 1 by WSIERP_1:15, A6, A9, INT_2:10;

hence contradiction by A1; :: thesis: verum

end;then p = 1 by WSIERP_1:15, A6, A9, INT_2:10;

hence contradiction by A1; :: thesis: verum

now :: thesis: not Lege (b,p) = - 1

hence
Lege (a,p) = Lege (b,p)
by A9, Th25, A10; :: thesis: verumassume
Lege (b,p) = - 1
; :: thesis: contradiction

then p = 1 by A6, A9, WSIERP_1:15;

hence contradiction by A1; :: thesis: verum

end;then p = 1 by A6, A9, WSIERP_1:15;

hence contradiction by A1; :: thesis: verum

suppose A11:
Lege (a,p) = - 1
; :: thesis: Lege (a,p) = Lege (b,p)

end;

A12: now :: thesis: not Lege (b,p) = 1

assume
Lege (b,p) = 1
; :: thesis: contradiction

then p divides - 2 by A6, A11;

then p divides 2 by INT_2:10;

hence contradiction by A1, NAT_D:7; :: thesis: verum

end;then p divides - 2 by A6, A11;

then p divides 2 by INT_2:10;

hence contradiction by A1, NAT_D:7; :: thesis: verum

now :: thesis: not Lege (b,p) = 0

hence
Lege (a,p) = Lege (b,p)
by A11, Th25, A12; :: thesis: verumassume
Lege (b,p) = 0
; :: thesis: contradiction

then p = 1 by WSIERP_1:15, A6, A11, INT_2:10;

hence contradiction by A1; :: thesis: verum

end;then p = 1 by WSIERP_1:15, A6, A11, INT_2:10;

hence contradiction by A1; :: thesis: verum