let n be natural number ; :: thesis: ( - 1,1 are_congruent_mod n iff ( n = 2 or n = 1 ) )
hereby :: thesis: ( ( n = 2 or n = 1 ) implies - 1,1 are_congruent_mod n )
assume - 1,1 are_congruent_mod n ; :: thesis: ( n = 2 or n = 1 )
then consider k being Integer such that
A1: n * k = - 2 ;
( k < 0 & n <> 0 ) by A1;
then A2: k <= - 1 by INT_1:8;
now :: thesis: ( n <> 2 implies n = 1 )
assume A3: n <> 2 ; :: thesis: n = 1
now :: thesis: not n <> 1
assume n <> 1 ; :: thesis: contradiction
then not n = 0 & ... & not n = 2 by A1, A3;
then not n <= 2 ;
then n >= 2 + 1 by NAT_1:13;
then ( n >= 3 & k < 0 ) by A1;
then A4: n * k <= 3 * k by XREAL_1:65;
3 * k <= 3 * (- 1) by A2, XREAL_1:64;
hence contradiction by A1, A4, XXREAL_0:2; :: thesis: verum
end;
hence n = 1 ; :: thesis: verum
end;
hence ( n = 2 or n = 1 ) ; :: thesis: verum
end;
assume A5: ( n = 2 or n = 1 ) ; :: thesis: - 1,1 are_congruent_mod n
per cases ( n = 2 or n = 1 ) by A5;
suppose n = 2 ; :: thesis: - 1,1 are_congruent_mod n
then n * (- 1) = - 2 ;
hence - 1,1 are_congruent_mod n ; :: thesis: verum
end;
suppose n = 1 ; :: thesis: - 1,1 are_congruent_mod n
hence - 1,1 are_congruent_mod n by INT_1:13; :: thesis: verum
end;
end;