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;
consider j being Integer such that
A4: ((j ^2) - b) mod p = 0 by A2;
A5: j ^2 ,b are_congruent_mod p by A4, INT_1:62;
i ^2 ,a are_congruent_mod p by A3, INT_1:62;
then (i ^2) * (j ^2),a * b are_congruent_mod p by A5, INT_1:18;
then (((i * j) ^2) - (a * b)) mod p = 0 by INT_1:62;
hence a * b is_quadratic_residue_mod p ; :: thesis: verum