let a be Integer; :: thesis: for p being Prime
for b being Integer st p > 2 & a gcd p = 1 & b gcd p = 1 holds
Lege (a * b),p = (Lege a,p) * (Lege b,p)
let p be Prime; :: thesis: for b being Integer st p > 2 & a gcd p = 1 & b gcd p = 1 holds
Lege (a * b),p = (Lege a,p) * (Lege b,p)
let b be Integer; :: thesis: ( p > 2 & a gcd p = 1 & b gcd p = 1 implies Lege (a * b),p = (Lege a,p) * (Lege b,p) )
assume A1: ( p > 2 & a gcd p = 1 & b gcd p = 1 ) ; :: thesis: Lege (a * b),p = (Lege a,p) * (Lege b,p)
then ( Lege a,p,a |^ ((p -' 1) div 2) are_congruent_mod p & Lege b,p,b |^ ((p -' 1) div 2) are_congruent_mod p ) by Th28;
then (Lege a,p) * (Lege b,p),(a |^ ((p -' 1) div 2)) * (b |^ ((p -' 1) div 2)) are_congruent_mod p by INT_1:39;
then (Lege a,p) * (Lege b,p),(a * b) |^ ((p -' 1) div 2) are_congruent_mod p by NEWTON:12;
then A2: (a * b) |^ ((p -' 1) div 2),(Lege a,p) * (Lege b,p) are_congruent_mod p by INT_1:35;
(a * b) gcd p = 1 by A1, WSIERP_1:11;
then Lege (a * b),p,(a * b) |^ ((p -' 1) div 2) are_congruent_mod p by A1, Th28;
then Lege (a * b),p,(Lege a,p) * (Lege b,p) are_congruent_mod p by A2, INT_1:36;
then A3: p divides (Lege (a * b),p) - ((Lege a,p) * (Lege b,p)) by INT_2:19;
A4: ( ( Lege a,p = 1 or Lege a,p = - 1 ) & ( Lege b,p = 1 or Lege b,p = - 1 ) ) by Th25;

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

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

hence Lege (a * b),p = (Lege a,p) * (Lege b,p) by A1, A3, A4, NAT_D:7; :: thesis: verum

end;

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

now

assume (Lege a,p) * (Lege b,p) <> - 1 ; :: thesis: contradiction
then p divides - 2 by A3, A4, A5;
then p divides 2 by INT_2:14;
hence contradiction by A1, NAT_D:7; :: thesis: verum

end;

hence Lege (a * b),p = (Lege a,p) * (Lege b,p) by A5; :: thesis: verum

end;

end;