let n be Nat; not (n * n) + n,4 are_congruent_mod 5
assume
(n * n) + n,4 are_congruent_mod 5
; contradiction
then A1:
4,(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 A6:
n,4
are_congruent_mod 5
;
contradictionthen
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 4
- 0
by INT_1:def 4, A1, INT_1:15;
hence
contradiction
by NAT_D:7;
verum end; end;