let a be Integer; :: thesis: for p being Prime
for b being Integer st p > 2 & a gcd p = 1 & b gcd p = 1 & not a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p holds
a * b is_quadratic_residue_mod p
let p be Prime; :: thesis: for b being Integer st p > 2 & a gcd p = 1 & b gcd p = 1 & not a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p holds
a * b is_quadratic_residue_mod p
let b be Integer; :: thesis: ( p > 2 & a gcd p = 1 & b gcd p = 1 & not a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p implies a * b is_quadratic_residue_mod p )
assume that
A1: p > 2 and
A2: a gcd p = 1 and
A3: b gcd p = 1 and
A4: not a is_quadratic_residue_mod p and
A5: not b is_quadratic_residue_mod p ; :: thesis: a * b is_quadratic_residue_mod p
A6: (a * b) gcd p = 1 by A2, A3, WSIERP_1:6;
set l = (p -' 1) div 2;
((b |^ ((p -' 1) div 2)) + 1) mod p = 0 by A1, A3, A5, Th21;
then A7: p divides (b |^ ((p -' 1) div 2)) + 1 by INT_1:62;
A8: ((a |^ ((p -' 1) div 2)) + 1) * ((b |^ ((p -' 1) div 2)) + 1) = ((((a |^ ((p -' 1) div 2)) * (b |^ ((p -' 1) div 2))) + ((a |^ ((p -' 1) div 2)) * 1)) + (1 * (b |^ ((p -' 1) div 2)))) + (1 * 1)
.= ((((a * b) |^ ((p -' 1) div 2)) + (a |^ ((p -' 1) div 2))) + (b |^ ((p -' 1) div 2))) + 1 by NEWTON:7
.= ((((a * b) |^ ((p -' 1) div 2)) + 1) + ((a |^ ((p -' 1) div 2)) + 1)) - (1 - (b |^ ((p -' 1) div 2))) ;
((a |^ ((p -' 1) div 2)) + 1) mod p = 0 by A1, A2, A4, Th21;
then A9: p divides (a |^ ((p -' 1) div 2)) + 1 by INT_1:62;
then A10: p divides ((a |^ ((p -' 1) div 2)) + 1) * ((b |^ ((p -' 1) div 2)) + 1) by INT_2:2;

now :: thesis: a * b is_quadratic_residue_mod p

assume not a * b is_quadratic_residue_mod p ; :: thesis: contradiction
then (((a * b) |^ ((p -' 1) div 2)) + 1) mod p = 0 by A1, A6, Th21;
then p divides ((a * b) |^ ((p -' 1) div 2)) + 1 by INT_1:62;
then p divides (((a * b) |^ ((p -' 1) div 2)) + 1) + ((a |^ ((p -' 1) div 2)) + 1) by A9, WSIERP_1:4;
then p divides 1 - (b |^ ((p -' 1) div 2)) by A10, A8, Th2;
then p divides ((b |^ ((p -' 1) div 2)) + 1) + (1 - (b |^ ((p -' 1) div 2))) by A7, WSIERP_1:4;
hence contradiction by A1, NAT_D:7; :: thesis: verum

end;

hence a * b is_quadratic_residue_mod p ; :: thesis: verum