let p be natural positive number ; :: thesis: for a being integer number holds
( a is_quadratic_residue_mod p iff ex x being integer number st x |^ 2,a are_congruent_mod p )
let a be integer number ; :: thesis: ( a is_quadratic_residue_mod p iff ex x being integer number st x |^ 2,a are_congruent_mod p )
thus ( a is_quadratic_residue_mod p implies ex x being integer number st x |^ 2,a are_congruent_mod p ) :: thesis: ( ex x being integer number 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 number 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;
reconsider xx = x as integer number by TARSKI:1;
take xx ; :: thesis: xx |^ 2,a are_congruent_mod p
xx ^2 = xx |^ 2 by NEWTON:81;
hence xx |^ 2,a are_congruent_mod p by A2; :: thesis: verum

end;

assume ex x being integer number st x |^ 2,a are_congruent_mod p ; :: thesis: a is_quadratic_residue_mod p
then consider x being integer number 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