let a be Integer; :: thesis: for p being Prime
for b being Integer st a is_quadratic_residue_mod p & b is_quadratic_residue_mod p holds
a * b is_quadratic_residue_mod p
let p be Prime; :: thesis: for b being Integer st a is_quadratic_residue_mod p & b is_quadratic_residue_mod p holds
a * b is_quadratic_residue_mod p
let b be Integer; :: thesis: ( a is_quadratic_residue_mod p & b is_quadratic_residue_mod p implies a * b is_quadratic_residue_mod p )
assume that
A1: a is_quadratic_residue_mod p and
A2: b is_quadratic_residue_mod p ; :: thesis: a * b is_quadratic_residue_mod p
consider i being Integer such that
A3: ((i ^2) - a) mod p = 0 by A1, Def2;
consider j being Integer such that
A4: ((j ^2) - b) mod p = 0 by A2, Def2;
p divides (j ^2) - b by A4, INT_1:62;
then A5: j ^2 ,b are_congruent_mod p by INT_2:15;
p divides (i ^2) - a by A3, INT_1:62;
then i ^2 ,a are_congruent_mod p by INT_2:15;
then (i ^2) * (j ^2),a * b are_congruent_mod p by A5, INT_1:18;
then p divides ((i * j) ^2) - (a * b) by INT_2:15;
then (((i * j) ^2) - (a * b)) mod p = 0 by INT_1:62;
hence a * b is_quadratic_residue_mod p by Def2; :: thesis: verum