A1: ( a gcd p = 1 & a is_quadratic_residue_mod p & p divides a implies for z being integer number holds
( z = 1 iff z = 0 ) )
proof
assume A2: ( a gcd p = 1 & a is_quadratic_residue_mod p & p divides a ) ; :: thesis: for z being integer number holds
( z = 1 iff z = 0 )
then a gcd p = p by Lm3;
hence for z being integer number holds
( z = 1 iff z = 0 ) by A2, INT_2:def 4; :: thesis: verum
end;
( a gcd p = 1 & a is_quadratic_non_residue_mod p & p divides a implies for z being integer number holds
( z = - 1 iff z = 0 ) )
proof
assume A3: ( a gcd p = 1 & a is_quadratic_non_residue_mod p & p divides a ) ; :: thesis: for z being integer number holds
( z = - 1 iff z = 0 )
then a gcd p = p by Lm3;
hence for z being integer number holds
( z = - 1 iff z = 0 ) by A3, INT_2:def 4; :: thesis: verum
end;
hence for b1 being integer Number holds
( ( a gcd p = 1 & a is_quadratic_residue_mod p & p divides a implies ( b1 = 1 iff b1 = 0 ) ) & ( a gcd p = 1 & a is_quadratic_residue_mod p & a gcd p = 1 & a is_quadratic_non_residue_mod p implies ( b1 = 1 iff b1 = - 1 ) ) & ( p divides a & a gcd p = 1 & a is_quadratic_non_residue_mod p implies ( b1 = 0 iff b1 = - 1 ) ) ) by A1; :: thesis: verum