let a be Integer; :: thesis: for p being Prime
for b being Integer st p > 2 & a gcd p = 1 & b gcd p = 1 & a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p holds
not 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 & a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p holds
not a * b is_quadratic_residue_mod p
let b be Integer; :: thesis: ( p > 2 & a gcd p = 1 & b gcd p = 1 & a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p implies not a * b is_quadratic_residue_mod p )
assume A1: ( p > 2 & a gcd p = 1 & b gcd p = 1 & a is_quadratic_residue_mod p & not b is_quadratic_residue_mod p ) ; :: thesis: not 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, Th20, 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)) * 1)) - (1 * (b |^ ((p -' 1) div 2)))) - (1 * 1) by NEWTON:12
.= ((((a * b) |^ ((p -' 1) div 2)) - 1) + ((a |^ ((p -' 1) div 2)) - 1)) - ((b |^ ((p -' 1) div 2)) - 1) ;

now

assume a * b is_quadratic_residue_mod p ; :: thesis: contradiction
then (((a * b) |^ ((p -' 1) div 2)) - 1) mod p = 0 by A1, A2, Th20;
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 (b |^ ((p -' 1) div 2)) - 1 by A4, A5, Th2;
then p divides ((b |^ ((p -' 1) div 2)) + 1) - ((b |^ ((p -' 1) div 2)) - 1) by A3, Th1;
hence contradiction by A1, NAT_D:7; :: thesis: verum

end;

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