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