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 A1: ( p > 2 & a gcd p = 1 & b gcd p = 1 & not a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p ) ; :: thesis: a * b is_quadratic_residue_mod p
then A2: (a * b) gcd p = 1 by WSIERP_1:11;
set l = (p -' 1) div 2;
( ((a |^ ((p -' 1) div 2)) + 1) mod p = 0 & ((b |^ ((p -' 1) div 2)) + 1) mod p = 0 ) by A1, Th21;
then A3: ( p divides (a |^ ((p -' 1) div 2)) + 1 & p divides (b |^ ((p -' 1) div 2)) + 1 ) by INT_1:89;
then A4: p divides ((a |^ ((p -' 1) div 2)) + 1) * ((b |^ ((p -' 1) div 2)) + 1) by INT_2:12;
A5: ((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:12
.= ((((a * b) |^ ((p -' 1) div 2)) + 1) + ((a |^ ((p -' 1) div 2)) + 1)) - (1 - (b |^ ((p -' 1) div 2))) ;

now

assume not a * b is_quadratic_residue_mod p ; :: thesis: contradiction
then (((a * b) |^ ((p -' 1) div 2)) + 1) mod p = 0 by A1, A2, Th21;
then p divides ((a * b) |^ ((p -' 1) div 2)) + 1 by INT_1:89;
then p divides (((a * b) |^ ((p -' 1) div 2)) + 1) + ((a |^ ((p -' 1) div 2)) + 1) by A3, WSIERP_1:9;
then p divides 1 - (b |^ ((p -' 1) div 2)) by A4, A5, Th2;
then p divides ((b |^ ((p -' 1) div 2)) + 1) + (1 - (b |^ ((p -' 1) div 2))) by A3, WSIERP_1:9;
hence contradiction by A1, NAT_D:7; :: thesis: verum

end;

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