let n be Nat; :: thesis: not (n * n) + n,3 are_congruent_mod 5
assume (n * n) + n,3 are_congruent_mod 5 ; :: thesis: contradiction
then A1: 3,(n * n) + n are_congruent_mod 5 by INT_1:14;
not not n, 0 are_congruent_mod 5 & ... & not n,4 are_congruent_mod 5 by Th5;
per cases then ( n, 0 are_congruent_mod 5 or n,1 are_congruent_mod 5 or n,2 are_congruent_mod 5 or n,3 are_congruent_mod 5 or n,4 are_congruent_mod 5 ) ;
suppose A2: n, 0 are_congruent_mod 5 ; :: thesis: contradiction
then n * n,0 * 0 are_congruent_mod 5 by INT_1:18;
then (n * n) + n,0 + 0 are_congruent_mod 5 by A2, INT_1:16;
then 5 divides 3 - 0 by INT_1:def 4, A1, INT_1:15;
hence contradiction by NAT_D:7; :: thesis: verum
end;
suppose A3: n,1 are_congruent_mod 5 ; :: thesis: contradiction
then n * n,1 * 1 are_congruent_mod 5 by INT_1:18;
then (n * n) + n,1 + 1 are_congruent_mod 5 by A3, INT_1:16;
then 5 divides 3 - 2 by INT_1:def 4, A1, INT_1:15;
then 5 <= 1 by NAT_D:7;
hence contradiction ; :: thesis: verum
end;
suppose A4: n,2 are_congruent_mod 5 ; :: thesis: contradiction
then n * n,2 * 2 are_congruent_mod 5 by INT_1:18;
then (n * n) + n,4 + 2 are_congruent_mod 5 by A4, INT_1:16;
then 6,(n * n) + n are_congruent_mod 5 by INT_1:14;
then 6 - 5,(n * n) + n are_congruent_mod 5 by INT_1:22;
then (n * n) + n,1 are_congruent_mod 5 by INT_1:14;
then 5 divides 3 - 1 by INT_1:def 4, A1, INT_1:15;
then 5 <= 2 by NAT_D:7;
hence contradiction ; :: thesis: verum
end;
suppose A5: n,3 are_congruent_mod 5 ; :: thesis: contradiction
then n * n,3 * 3 are_congruent_mod 5 by INT_1:18;
then (n * n) + n,9 + 3 are_congruent_mod 5 by A5, INT_1:16;
then 12,(n * n) + n are_congruent_mod 5 by INT_1:14;
then 12 - 5,(n * n) + n are_congruent_mod 5 by INT_1:22;
then 7 - 5,(n * n) + n are_congruent_mod 5 by INT_1:22;
then (n * n) + n,2 are_congruent_mod 5 by INT_1:14;
then 5 divides 3 - 2 by INT_1:def 4, A1, INT_1:15;
then 5 <= 1 by NAT_D:7;
hence contradiction ; :: thesis: verum
end;
suppose A6: n,4 are_congruent_mod 5 ; :: thesis: contradiction
then n * n,4 * 4 are_congruent_mod 5 by INT_1:18;
then (n * n) + n,16 + 4 are_congruent_mod 5 by A6, INT_1:16;
then 20,(n * n) + n are_congruent_mod 5 by INT_1:14;
then 20 - 5,(n * n) + n are_congruent_mod 5 by INT_1:22;
then 15 - 5,(n * n) + n are_congruent_mod 5 by INT_1:22;
then 10 - 5,(n * n) + n are_congruent_mod 5 by INT_1:22;
then 5 - 5,(n * n) + n are_congruent_mod 5 by INT_1:22;
then (n * n) + n, 0 are_congruent_mod 5 by INT_1:14;
then 5 divides 3 - 0 by INT_1:def 4, A1, INT_1:15;
hence contradiction by NAT_D:7; :: thesis: verum
end;
end;