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 & b is_quadratic_residue_mod p holds
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 & b is_quadratic_residue_mod p holds
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 & b is_quadratic_residue_mod p implies 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 & b is_quadratic_residue_mod p ) ; :: thesis: a * b is_quadratic_residue_mod p
then consider i being Integer such that
A2: ((i ^2 ) - a) mod p = 0 by Def2;
consider j being Integer such that
A3: ((j ^2 ) - b) mod p = 0 by A1, Def2;
( p divides (i ^2 ) - a & p divides (j ^2 ) - b ) by A2, A3, INT_1:89;
then ( i ^2 ,a are_congruent_mod p & j ^2 ,b are_congruent_mod p ) by INT_2:19;
then (i ^2 ) * (j ^2 ),a * b are_congruent_mod p by INT_1:39;
then p divides ((i * j) ^2 ) - (a * b) by INT_2:19;
then (((i * j) ^2 ) - (a * b)) mod p = 0 by INT_1:89;
hence a * b is_quadratic_residue_mod p by Def2; :: thesis: verum