let p be positive Nat; :: thesis: for a being Integer holds
( a is_quadratic_residue_mod p iff ex x being Integer st x |^ 2,a are_congruent_mod p )
let a be Integer; :: thesis: ( a is_quadratic_residue_mod p iff ex x being Integer st x |^ 2,a are_congruent_mod p )
thus ( a is_quadratic_residue_mod p implies ex x being Integer st x |^ 2,a are_congruent_mod p ) :: thesis: ( ex x being Integer st x |^ 2,a are_congruent_mod p implies a is_quadratic_residue_mod p )

proof

assume a is_quadratic_residue_mod p ; :: thesis: ex x being Integer st x |^ 2,a are_congruent_mod p
then consider x being Integer such that
A1: ((x ^2) - a) mod p = 0 by INT_5:def 2;
A2: (x ^2) - a = ((((x ^2) - a) div p) * p) + 0 by A1, INT_1:59;
take x ; :: thesis: x |^ 2,a are_congruent_mod p
x ^2 = x |^ 2 by NEWTON:81;
hence x |^ 2,a are_congruent_mod p by A2; :: thesis: verum

end;

assume ex x being Integer st x |^ 2,a are_congruent_mod p ; :: thesis: a is_quadratic_residue_mod p
then consider x being Integer such that
A3: x |^ 2,a are_congruent_mod p ;
x ^2 = (x |^ 1) * x
.= x |^ (1 + 1) by NEWTON:6 ;
then ((x ^2) - a) mod p = 0 by A3, INT_1:62;
hence a is_quadratic_residue_mod p by INT_5:def 2; :: thesis: verum