let p be Prime; :: thesis: for a being Integer 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; :: 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