let p be natural prime number ; :: thesis: for a being integer number holds
( ( Leg (a,p) = 1 implies ( a gcd p = 1 & a is_quadratic_residue_mod p ) ) & ( a gcd p = 1 & a is_quadratic_residue_mod p implies Leg (a,p) = 1 ) & ( Leg (a,p) = 0 implies p divides a ) & ( p divides a implies Leg (a,p) = 0 ) & ( Leg (a,p) = - 1 implies ( a gcd p = 1 & a is_quadratic_non_residue_mod p ) ) & ( a gcd p = 1 & a is_quadratic_non_residue_mod p implies Leg (a,p) = - 1 ) )
let a be integer number ; :: thesis: ( ( Leg (a,p) = 1 implies ( a gcd p = 1 & a is_quadratic_residue_mod p ) ) & ( a gcd p = 1 & a is_quadratic_residue_mod p implies Leg (a,p) = 1 ) & ( Leg (a,p) = 0 implies p divides a ) & ( p divides a implies Leg (a,p) = 0 ) & ( Leg (a,p) = - 1 implies ( a gcd p = 1 & a is_quadratic_non_residue_mod p ) ) & ( a gcd p = 1 & a is_quadratic_non_residue_mod p implies Leg (a,p) = - 1 ) )
A1: now :: thesis: ( Leg (a,p) = 0 implies p divides a )
assume A2: Leg (a,p) = 0 ; :: thesis: p divides a
now :: thesis: p divides a
assume not p divides a ; :: thesis: contradiction
then a gcd p = 1 by Th6;
hence contradiction by A2, Def4; :: thesis: verum
end;
hence p divides a ; :: thesis: verum
end;
now :: thesis: ( Leg (a,p) = 1 implies ( a gcd p = 1 & a is_quadratic_residue_mod p ) )
assume A3: Leg (a,p) = 1 ; :: thesis: ( a gcd p = 1 & a is_quadratic_residue_mod p )
then a gcd p = 1 by Th6, Def4;
hence ( a gcd p = 1 & a is_quadratic_residue_mod p ) by A3, Def4; :: thesis: verum
end;
hence ( Leg (a,p) = 1 iff ( a gcd p = 1 & a is_quadratic_residue_mod p ) ) by Def4; :: thesis: ( ( Leg (a,p) = 0 implies p divides a ) & ( p divides a implies Leg (a,p) = 0 ) & ( Leg (a,p) = - 1 implies ( a gcd p = 1 & a is_quadratic_non_residue_mod p ) ) & ( a gcd p = 1 & a is_quadratic_non_residue_mod p implies Leg (a,p) = - 1 ) )
now :: thesis: ( Leg (a,p) = - 1 implies ( a gcd p = 1 & a is_quadratic_non_residue_mod p ) )
assume A4: Leg (a,p) = - 1 ; :: thesis: ( a gcd p = 1 & a is_quadratic_non_residue_mod p )
then a gcd p = 1 by Th6, Def4;
hence ( a gcd p = 1 & a is_quadratic_non_residue_mod p ) by A4, Def4; :: thesis: verum
end;
hence ( ( Leg (a,p) = 0 implies p divides a ) & ( p divides a implies Leg (a,p) = 0 ) & ( Leg (a,p) = - 1 implies ( a gcd p = 1 & a is_quadratic_non_residue_mod p ) ) & ( a gcd p = 1 & a is_quadratic_non_residue_mod p implies Leg (a,p) = - 1 ) ) by A1, Def4; :: thesis: verum