let p be Prime; :: thesis: for a, b being Element of (GF p) holds Lege_p (a * b) = (Lege_p a) * (Lege_p b)
let a, b be Element of (GF p); :: thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)

per cases ( a is quadratic_residue or not a is quadratic_residue ) ;

suppose A1: a is quadratic_residue ; :: thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)

then A2: Lege_p a = 1 by Th33;

per cases ( b is quadratic_residue or b = 0 or ( b <> 0 & not b is quadratic_residue ) ) ;

suppose A3: b is quadratic_residue ; :: thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)

then A4: Lege_p b = 1 by Th33;
A5: ( a <> 0 & ex x being Element of (GF p) st x |^ 2 = a ) by A1;
( b <> 0 & ex x being Element of (GF p) st x |^ 2 = b ) by A3;
then A6: a * b <> 0 by A5, Th20;
ex x being Element of (GF p) st x |^ 2 = a * b

proof

consider a1 being Element of (GF p) such that
A7: a1 |^ 2 = a by A1;
consider b1 being Element of (GF p) such that
A8: b1 |^ 2 = b by A3;
(a1 |^ 2) * (b1 |^ 2) = (a1 * b1) |^ 2 by BINOM:9;
hence ex x being Element of (GF p) st x |^ 2 = a * b by A7, A8; :: thesis: verum

end;

then a * b is quadratic_residue by A6;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A2, A4, Th33; :: thesis: verum

end;

suppose A9: b = 0 ; :: thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)

then Lege_p b = 0 by Def5;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A9, Th20; :: thesis: verum

end;

suppose A10: ( b <> 0 & not b is quadratic_residue ) ; :: thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)

then A11: Lege_p b = - 1 by Def5;
A12: ( a <> 0 & ex x being Element of (GF p) st x |^ 2 = a ) by A1;
A13: a * b <> 0 by A10, A12, Th20;
for x being Element of (GF p) holds not x |^ 2 = a * b

proof

given xab being Element of (GF p) such that A14: xab |^ 2 = a * b ; :: thesis: contradiction
consider xa being Element of (GF p) such that
A15: xa |^ 2 = a by A1;
A16: xa |^ 2 <> 0. (GF p) by A12, A15, Th11;
A17: xa <> 0

proof

assume xa = 0 ; :: thesis: contradiction
then xa = 0. (GF p) ;
then xa * xa = 0. (GF p) ;
then xa |^ 2 = 0. (GF p) by Lm2;
hence contradiction by A15, A12, Th11; :: thesis: verum

end;

((xa ") * xab) |^ 2 = ((xa ") |^ 2) * (a * b) by A14, BINOM:9
.= (((xa ") |^ 2) * (xa |^ 2)) * b by A15, GROUP_1:def 3
.= (((xa |^ 2) ") * (xa |^ 2)) * b by Th28, A17
.= (1. (GF p)) * b by A16, VECTSP_1:def 10
.= b ;
hence contradiction by A10; :: thesis: verum

end;

then a * b is not_quadratic_residue by A13;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A2, A11, Th32; :: thesis: verum

end;

end;

end;

suppose A18: not a is quadratic_residue ; :: thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)

now :: thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)

per cases ( a = 0 or a <> 0 ) ;

suppose A19: a = 0 ; :: thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)

then Lege_p a = 0 by Th34;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A19, Th20; :: thesis: verum

end;

suppose A20: a <> 0 ; :: thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)

then A21: Lege_p a = - 1 by A18, Def5;

per cases ( b is quadratic_residue or b = 0 or ( b <> 0 & not b is quadratic_residue ) ) ;

suppose A22: b is quadratic_residue ; :: thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)

then A23: Lege_p b = 1 by Th33;
A24: ( b <> 0 & ex x being Element of (GF p) st x |^ 2 = b ) by A22;
then A25: a * b <> 0 by A20, Th20;
for x being Element of (GF p) holds not x |^ 2 = a * b

proof

given xab being Element of (GF p) such that A26: xab |^ 2 = a * b ; :: thesis: contradiction
consider xb being Element of (GF p) such that
A27: xb |^ 2 = b by A22;
A28: xb |^ 2 <> 0. (GF p) by A24, A27, Th11;
A29: xb <> 0

proof

assume xb = 0 ; :: thesis: contradiction
then xb = 0. (GF p) ;
then xb * xb = 0. (GF p) ;
then xb |^ 2 = 0. (GF p) by Lm2;
hence contradiction by A27, A24, Th11; :: thesis: verum

end;

(xab * (xb ")) |^ 2 = (a * b) * ((xb ") |^ 2) by A26, BINOM:9
.= a * ((xb |^ 2) * ((xb ") |^ 2)) by A27, GROUP_1:def 3
.= a * ((xb |^ 2) * ((xb |^ 2) ")) by Th28, A29
.= a * (1. (GF p)) by A28, VECTSP_1:def 10
.= a ;
hence contradiction by A18, A20; :: thesis: verum

end;

then a * b is not_quadratic_residue by A25;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A21, A23, Th32; :: thesis: verum

end;

suppose A30: b = 0 ; :: thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)

then Lege_p b = 0 by Th34;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A30, Th20; :: thesis: verum

end;

suppose A31: ( b <> 0 & not b is quadratic_residue ) ; :: thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)

then A32: Lege_p b = - 1 by Def5;
A33: a * b <> 0 by A20, A31, Th20;
ex x being Element of (GF p) st x |^ 2 = a * b

proof

consider g being Element of (GF p) such that
A34: for a being Element of (GF p) st a <> 0. (GF p) holds
ex n being Nat st a = g |^ n by Th30;
a <> 0. (GF p) by A20, Th11;
then consider na being Nat such that
A35: a = g |^ na by A34;
b <> 0. (GF p) by A31, Th11;
then consider nb being Nat such that
A36: b = g |^ nb by A34;
A37: na = ((na div 2) * 2) + (na mod 2) by NAT_D:2;
A38: nb = ((nb div 2) * 2) + (nb mod 2) by NAT_D:2;
na mod 2 <> 0

proof

assume A39: na mod 2 = 0 ; :: thesis: contradiction
reconsider nn = na div 2 as Element of NAT ;
a = (g |^ nn) |^ 2 by A35, A37, A39, Lm4;
hence contradiction by A18, A20; :: thesis: verum

end;

then A40: na mod 2 = 1 by NAT_D:12;
nb mod 2 <> 0

proof

assume A41: nb mod 2 = 0 ; :: thesis: contradiction
reconsider nn = nb div 2 as Element of NAT ;
b = (g |^ nn) |^ 2 by A36, A38, A41, Lm4;
hence contradiction by A31; :: thesis: verum

end;

then A42: nb mod 2 = 1 by NAT_D:12;
reconsider nc = ((na div 2) + (nb div 2)) + 1 as Nat ;
A43: na + nb = (((na div 2) * 2) + 1) + nb by A40, NAT_D:2
.= (((na div 2) * 2) + 1) + (((nb div 2) * 2) + 1) by A42, NAT_D:2
.= nc * 2 ;
a * b = g |^ (na + nb) by A35, A36, Lm3
.= (g |^ nc) |^ 2 by A43, Lm4 ;
hence ex x being Element of (GF p) st x |^ 2 = a * b ; :: thesis: verum

end;

then a * b is quadratic_residue by A33;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A21, A32, Th33; :: thesis: verum

end;

end;

end;

end;

end;

hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) ; :: thesis: verum

end;

end;