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 that
A1: p > 2 and
A2: a gcd p = 1 and
A3: b gcd p = 1 ; :: thesis: Lege ((a * b),p) = (Lege (a,p)) * (Lege (b,p))
A4: Lege (b,p),b |^ ((p -' 1) div 2) are_congruent_mod p by A1, A3, Th28;
Lege (a,p),a |^ ((p -' 1) div 2) are_congruent_mod p by A1, A2, Th28;
then (Lege (a,p)) * (Lege (b,p)),(a |^ ((p -' 1) div 2)) * (b |^ ((p -' 1) div 2)) are_congruent_mod p by A4, INT_1:39;
then (Lege (a,p)) * (Lege (b,p)),(a * b) |^ ((p -' 1) div 2) are_congruent_mod p by NEWTON:12;
then A5: (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 A2, A3, 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 A5, INT_1:36;
then A6: p divides (Lege ((a * b),p)) - ((Lege (a,p)) * (Lege (b,p))) by INT_2:19;
A7: ( Lege (b,p) = 1 or Lege (b,p) = - 1 ) by Th25;
A8: ( Lege (a,p) = 1 or Lege (a,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, A6, A8, A7, NAT_D:7; :: thesis: verum

end;

suppose A9: 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 A6, A8, A7, A9;
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 A9; :: thesis: verum

end;

end;