let a be Integer; 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; 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; ( 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
; not 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)) * 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
; 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 A9, WSIERP_1:4;
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 A7, Th1;
hence
contradiction
by A1, NAT_D:7; verum