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 P0: a is quadratic_residue ; :: thesis: Lege_p (a * b) = (Lege_p a) * (Lege_p b)

then P1: Lege_p a = 1 by QR11;

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

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

then A1: Lege_p b = 1 by QR11;
A2: ( a <> 0 & ex x being Element of (GF p) st x |^ 2 = a ) by P0, QRDef1;
( b <> 0 & ex x being Element of (GF p) st x |^ 2 = b ) by A0, QRDef1;
then A4: a * b <> 0 by A2, GF8;
ex x being Element of (GF p) st x |^ 2 = a * b

proof

consider a1 being Element of (GF p) such that
B0: a1 |^ 2 = a by P0, QRDef1;
consider b1 being Element of (GF p) such that
B1: b1 |^ 2 = b by A0, QRDef1;
(a1 |^ 2) * (b1 |^ 2) = (a1 * b1) |^ 2 by EX9;
hence ex x being Element of (GF p) st x |^ 2 = a * b by B0, B1; :: thesis: verum

end;

then a * b is quadratic_residue by A4, QRDef1;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by P1, A1, QR11; :: thesis: verum

end;

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

then Lege_p b = 0 by QRDef3;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A0, GF8; :: thesis: verum

end;

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

then A1: Lege_p b = - 1 by QRDef3;
A2: ( a <> 0 & ex x being Element of (GF p) st x |^ 2 = a ) by P0, QRDef1;
A4: a * b <> 0 by A0, A2, GF8;
for x being Element of (GF p) holds not x |^ 2 = a * b

proof

given xab being Element of (GF p) such that L1: xab |^ 2 = a * b ; :: thesis: contradiction
consider xa being Element of (GF p) such that
L2: xa |^ 2 = a by P0, QRDef1;
L3: xa |^ 2 <> 0. (GF p) by A2, L2, XLm2;
L4: xa <> 0

proof

assume xa = 0 ; :: thesis: contradiction
then xa = 0. (GF p) by XLm2;
then xa * xa = 0. (GF p) by VECTSP_1:12;
then xa |^ 2 = 0. (GF p) by EXLm4;
hence contradiction by L2, A2, XLm2; :: thesis: verum

end;

((xa ") * xab) |^ 2 = ((xa ") |^ 2) * (a * b) by L1, EX9
.= (((xa ") |^ 2) * (xa |^ 2)) * b by L2, GROUP_1:def 3
.= (((xa |^ 2) ") * (xa |^ 2)) * b by EX10, L4
.= (1. (GF p)) * b by L3, VECTSP_1:def 10
.= b by VECTSP_1:def 8 ;
hence contradiction by A0, QRDef1; :: thesis: verum

end;

then a * b is not_quadratic_residue by A4, QRDef2;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by P1, A1, QR10; :: thesis: verum

end;

end;

end;

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

now

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

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

then Lege_p a = 0 by QR12;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by P3, GF8; :: thesis: verum

end;

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

then P5: Lege_p a = - 1 by P2, QRDef3;

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

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

then A1: Lege_p b = 1 by QR11;
A3: ( b <> 0 & ex x being Element of (GF p) st x |^ 2 = b ) by A0, QRDef1;
then A4: a * b <> 0 by P4, GF8;
for x being Element of (GF p) holds not x |^ 2 = a * b

proof

given xab being Element of (GF p) such that L1: xab |^ 2 = a * b ; :: thesis: contradiction
consider xb being Element of (GF p) such that
L2: xb |^ 2 = b by A0, QRDef1;
L3: xb |^ 2 <> 0. (GF p) by A3, L2, XLm2;
L4: xb <> 0

proof

assume xb = 0 ; :: thesis: contradiction
then xb = 0. (GF p) by XLm2;
then xb * xb = 0. (GF p) by VECTSP_1:12;
then xb |^ 2 = 0. (GF p) by EXLm4;
hence contradiction by L2, A3, XLm2; :: thesis: verum

end;

(xab * (xb ")) |^ 2 = (a * b) * ((xb ") |^ 2) by L1, EX9
.= a * ((xb |^ 2) * ((xb ") |^ 2)) by L2, GROUP_1:def 3
.= a * ((xb |^ 2) * ((xb |^ 2) ")) by EX10, L4
.= a * (1. (GF p)) by L3, VECTSP_1:def 10
.= a by VECTSP_1:def 8 ;
hence contradiction by P2, P4, QRDef1; :: thesis: verum

end;

then a * b is not_quadratic_residue by A4, QRDef2;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by P5, A1, QR10; :: thesis: verum

end;

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

then Lege_p b = 0 by QR12;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by A0, GF8; :: thesis: verum

end;

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

then A1: Lege_p b = - 1 by QRDef3;
A4: a * b <> 0 by P4, A0, GF8;
ex x being Element of (GF p) st x |^ 2 = a * b

proof

consider g being Element of (GF p) such that
XP1: for a being Element of (GF p) st a <> 0. (GF p) holds
ex n being Nat st a = g |^ n by LMCycle5;
a <> 0. (GF p) by P4, XLm2;
then consider na being Nat such that
XP2: a = g |^ na by XP1;
b <> 0. (GF p) by A0, XLm2;
then consider nb being Nat such that
XP3: b = g |^ nb by XP1;
XP4: na = ((na div 2) * 2) + (na mod 2) by NAT_D:2;
XP5: nb = ((nb div 2) * 2) + (nb mod 2) by NAT_D:2;
na mod 2 <> 0

proof

assume XP61: na mod 2 = 0 ; :: thesis: contradiction
reconsider nn = na div 2 as Element of NAT ;
a = (g |^ nn) |^ 2 by XP2, XP4, XP61, EX12;
hence contradiction by P2, P4, QRDef1; :: thesis: verum

end;

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

proof

assume XP61: nb mod 2 = 0 ; :: thesis: contradiction
reconsider nn = nb div 2 as Element of NAT ;
b = (g |^ nn) |^ 2 by XP3, XP5, XP61, EX12;
hence contradiction by A0, QRDef1; :: thesis: verum

end;

then XP9: nb mod 2 = 1 by NAT_D:12;
reconsider nc = ((na div 2) + (nb div 2)) + 1 as Nat ;
XP10: na + nb = (((na div 2) * 2) + 1) + nb by XP7, NAT_D:2
.= (((na div 2) * 2) + 1) + (((nb div 2) * 2) + 1) by XP9, NAT_D:2
.= nc * 2 ;
a * b = g |^ (na + nb) by XP2, XP3, EX11
.= (g |^ nc) |^ 2 by XP10, EX12 ;
hence ex x being Element of (GF p) st x |^ 2 = a * b ; :: thesis: verum

end;

then a * b is quadratic_residue by A4, QRDef1;
hence Lege_p (a * b) = (Lege_p a) * (Lege_p b) by P5, A1, QR11; :: thesis: verum

end;

end;

end;

end;

end;

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

end;

end;