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:18;

then (Lege (a,p)) * (Lege (b,p)),(a * b) |^ ((p -' 1) div 2) are_congruent_mod p by NEWTON:7;

then A5: (a * b) |^ ((p -' 1) div 2),(Lege (a,p)) * (Lege (b,p)) are_congruent_mod p by INT_1:14;

(a * b) gcd p = 1 by A2, A3, WSIERP_1:6;

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:15;

then A6: p divides (Lege ((a * b),p)) - ((Lege (a,p)) * (Lege (b,p))) ;

A7: ( Lege (b,p) = 1 or Lege (b,p) = - 1 or Lege (b,p) = 0 ) by Th25;

A8: ( Lege (a,p) = 1 or Lege (a,p) = - 1 or Lege (a,p) = 0 ) by Th25;

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:18;

then (Lege (a,p)) * (Lege (b,p)),(a * b) |^ ((p -' 1) div 2) are_congruent_mod p by NEWTON:7;

then A5: (a * b) |^ ((p -' 1) div 2),(Lege (a,p)) * (Lege (b,p)) are_congruent_mod p by INT_1:14;

(a * b) gcd p = 1 by A2, A3, WSIERP_1:6;

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:15;

then A6: p divides (Lege ((a * b),p)) - ((Lege (a,p)) * (Lege (b,p))) ;

A7: ( Lege (b,p) = 1 or Lege (b,p) = - 1 or Lege (b,p) = 0 ) by Th25;

A8: ( Lege (a,p) = 1 or Lege (a,p) = - 1 or Lege (a,p) = 0 ) by Th25;

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

end;

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

end;

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

hence
Lege ((a * b),p) = (Lege (a,p)) * (Lege (b,p))
by A8, A7, A1, A6, A9, NAT_D:7; :: thesis: verumassume
( Lege (a,p) = 0 or Lege (b,p) = 0 )
; :: 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 A10:
Lege ((a * b),p) = 0
; :: thesis: Lege ((a * b),p) = (Lege (a,p)) * (Lege (b,p))

end;

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

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

then p <= 1 by A6, A10, NAT_D:7;

then p < 1 + 1 by NAT_1:13;

hence contradiction by A1; :: thesis: verum

end;then p <= 1 by A6, A10, NAT_D:7;

then p < 1 + 1 by NAT_1:13;

hence contradiction by A1; :: thesis: verum

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

hence
Lege ((a * b),p) = (Lege (a,p)) * (Lege (b,p))
by A8, A7, A11, A10; :: thesis: verumassume
(Lege (a,p)) * (Lege (b,p)) = 1
; :: thesis: contradiction

then p divides 1 by A6, A10, INT_2:10;

then p <= 1 by NAT_D:7;

then p < 1 + 1 by NAT_1:13;

hence contradiction by A1; :: thesis: verum

end;then p divides 1 by A6, A10, INT_2:10;

then p <= 1 by NAT_D:7;

then p < 1 + 1 by NAT_1:13;

hence contradiction by A1; :: thesis: verum

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

end;

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

assume
( Lege (a,p) = 0 or Lege (b,p) = 0 )
; :: thesis: contradiction

then ( p = 1 or p = - 1 ) by A6, A12, INT_2:13;

hence contradiction by INT_2:def 4; :: thesis: verum

end;then ( p = 1 or p = - 1 ) by A6, A12, INT_2:13;

hence contradiction by INT_2:def 4; :: thesis: verum

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

hence
Lege ((a * b),p) = (Lege (a,p)) * (Lege (b,p))
by A12, A13, A7, A8; :: thesis: verumassume
(Lege (a,p)) * (Lege (b,p)) = 1
; :: thesis: contradiction

then p divides - 2 by A6, A12;

then p divides 2 by INT_2:10;

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

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

then p divides 2 by INT_2:10;

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