let n be integer Number ; :: thesis: ( - 1,1 are_congruent_mod n iff ( n = 2 or n = 1 or n = - 2 or n = - 1 ) )
hereby :: thesis: ( ( n = 2 or n = 1 or n = - 2 or n = - 1 ) implies - 1,1 are_congruent_mod n )
assume A1: - 1,1 are_congruent_mod n ; :: thesis: ( n = 2 or n = 1 or n = - 2 or n = - 1 )
then consider k being Integer such that
A2: n * k = - 2 ;
now :: thesis: ( ( n >= 0 & ( n = 2 or n = 1 or n = - 2 or n = - 1 ) ) or ( n < 0 & ( n = 2 or n = 1 or n = - 2 or n = - 1 ) ) )
per cases ( n >= 0 or n < 0 ) ;
case n >= 0 ; :: thesis: ( n = 2 or n = 1 or n = - 2 or n = - 1 )
then n in NAT by INT_1:3;
then reconsider m = n as natural number ;
( m = 1 or m = 2 ) by A1, Th19;
hence ( n = 2 or n = 1 or n = - 2 or n = - 1 ) ; :: thesis: verum
end;
case A3: n < 0 ; :: thesis: ( n = 2 or n = 1 or n = - 2 or n = - 1 )
then A4: k > 0 by A2;
then A5: k >= 0 + 1 by INT_1:7;
now :: thesis: ( n <> - 2 implies n = - 1 )
assume A6: n <> - 2 ; :: thesis: n = - 1
now :: thesis: not n <> - 1
assume A7: n <> - 1 ; :: thesis: contradiction
n <= - 1 by A3, INT_1:8;
then n < - 1 by A7, XXREAL_0:1;
then n + 1 <= - 1 by INT_1:7;
then (n + 1) - 1 <= (- 1) - 1 by XREAL_1:9;
then n < - 2 by A6, XXREAL_0:1;
then n + 1 <= - 2 by INT_1:7;
then (n + 1) - 1 <= (- 2) - 1 by XREAL_1:9;
then A8: n * k <= (- 3) * k by A4, XREAL_1:64;
(- 3) * k <= (- 3) * 1 by A5, XREAL_1:65;
hence contradiction by A2, A8, XXREAL_0:2; :: thesis: verum
end;
hence n = - 1 ; :: thesis: verum
end;
hence ( n = 2 or n = 1 or n = - 2 or n = - 1 ) ; :: thesis: verum
end;
end;
end;
hence ( n = 2 or n = 1 or n = - 2 or n = - 1 ) ; :: thesis: verum
end;
assume A9: ( n = 2 or n = 1 or n = - 2 or n = - 1 ) ; :: thesis: - 1,1 are_congruent_mod n
per cases ( n = 2 or n = 1 or n = - 2 or n = - 1 ) by A9;
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;
suppose n = - 2 ; :: thesis: - 1,1 are_congruent_mod n
hence - 1,1 are_congruent_mod n ; :: thesis: verum
end;
suppose n = - 1 ; :: thesis: - 1,1 are_congruent_mod n
then n * (- 1) = 1 ;
hence - 1,1 are_congruent_mod n by INT_1:20, INT_1:13; :: thesis: verum
end;
end;