let m, n be non zero Nat; :: thesis: for A being set st A = { i where i is Nat : (ArProg (m,n)) . i is square } holds
( A is infinite iff m is_quadratic_residue_mod n )
let A be set ; :: thesis: ( A = { i where i is Nat : (ArProg (m,n)) . i is square } implies ( A is infinite iff m is_quadratic_residue_mod n ) )
assume A1: A = { i where i is Nat : (ArProg (m,n)) . i is square } ; :: thesis: ( A is infinite iff m is_quadratic_residue_mod n )

hereby :: thesis: ( m is_quadratic_residue_mod n implies A is infinite )

assume A is infinite ; :: thesis: m is_quadratic_residue_mod n
then consider i being object such that
A2: i in A by XBOOLE_0:7;
consider ii being Nat such that
A3: ( ii = i & (ArProg (m,n)) . ii is square ) by A1, A2;
consider x being Nat such that
A4: (ArProg (m,n)) . ii = x ^2 by A3, PYTHTRIP:def 3;
A8: x ^2 = m + (n * ii) by A4, NUMBER06:7;
then x ^2 ,m are_congruent_mod n ;
then ((x ^2) - m) mod n = 0 by A8, PEPIN:6;
hence m is_quadratic_residue_mod n by INT_5:def 2; :: thesis: verum

end;

assume m is_quadratic_residue_mod n ; :: thesis: A is infinite
then consider i being Nat such that
D3: (ArProg (m,n)) . i is square by LemmaTo57;
consider x being Nat such that
D2: (ArProg (m,n)) . i = x ^2 by D3, PYTHTRIP:def 3;
for j being Nat ex k being Nat st
( k >= j & k in A )

proof

let j be Nat; :: thesis: ex k being Nat st
( k >= j & k in A )
Z2: (((j ^2) * n) + ((2 * j) * x)) + i = (((j ^2) * n) + i) + ((2 * j) * x) ;
hh: x <> 0

proof

assume x = 0 ; :: thesis: contradiction
then m + (n * i) = 0 by D2, NUMBER06:7;
hence contradiction ; :: thesis: verum

end;

(2 * j) * x = j * (2 * x) ;
then U3: (2 * j) * x >= 1 * j by hh, XREAL_1:64, NAT_1:14;
set ww = (((j ^2) * n) + ((2 * j) * x)) + i;
(ArProg (m,n)) . ((((j ^2) * n) + ((2 * j) * x)) + i) is square by D2, Lemma2To57;
then (((j ^2) * n) + ((2 * j) * x)) + i in A by A1;
hence ex k being Nat st
( k >= j & k in A ) by U3, Z2, NAT_1:12; :: thesis: verum

end;

hence A is infinite by PYTHTRIP:9; :: thesis: verum