let p be natural prime number ; 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 ; ( ( 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 ) )
hence
( Leg (a,p) = 1 iff ( a gcd p = 1 & a is_quadratic_residue_mod p ) )
by Def4; ( ( 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 ) )
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; verum