let n be triangular number ; not n,4 are_congruent_mod 10
consider k being Nat such that
A1:
n = Triangle k
by Def2;
A2:
4 * 5 = 20
;
A3:
n = (k * (k + 1)) / 2
by A1, Th19;
assume
n,4 are_congruent_mod 10
; contradiction
then
((k * (k + 1)) / 2) * 2,4 * 2 are_congruent_mod 10 * 2
by A3, INT_4:10;
then
k * (k + 1),8 are_congruent_mod 5
by A2, INT_1:20;
then
8,k * (k + 1) are_congruent_mod 5
by INT_1:14;
then
8 - 5,k * (k + 1) are_congruent_mod 5
by INT_1:22;
then
3,(k * k) + k are_congruent_mod 5
;
hence
contradiction
by Th7, INT_1:14; verum