let n be triangular number ; :: thesis: ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 )
not not n, 0 are_congruent_mod 10 & ... & not n,9 are_congruent_mod 10 by Th9;
per cases then ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,2 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,4 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,7 are_congruent_mod 10 or n,8 are_congruent_mod 10 or n,9 are_congruent_mod 10 ) ;
suppose n, 0 are_congruent_mod 10 ; :: thesis: ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 )
hence ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 ) ; :: thesis: verum
end;
suppose n,1 are_congruent_mod 10 ; :: thesis: ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 )
hence ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 ) ; :: thesis: verum
end;
suppose n,2 are_congruent_mod 10 ; :: thesis: ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 )
hence ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 ) by Th24; :: thesis: verum
end;
suppose n,3 are_congruent_mod 10 ; :: thesis: ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 )
hence ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 ) ; :: thesis: verum
end;
suppose n,4 are_congruent_mod 10 ; :: thesis: ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 )
hence ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 ) by Th25; :: thesis: verum
end;
suppose n,5 are_congruent_mod 10 ; :: thesis: ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 )
hence ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 ) ; :: thesis: verum
end;
suppose n,6 are_congruent_mod 10 ; :: thesis: ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 )
hence ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 ) ; :: thesis: verum
end;
suppose n,7 are_congruent_mod 10 ; :: thesis: ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 )
hence ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 ) by Th22; :: thesis: verum
end;
suppose n,8 are_congruent_mod 10 ; :: thesis: ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 )
hence ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 ) ; :: thesis: verum
end;
suppose n,9 are_congruent_mod 10 ; :: thesis: ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 )
hence ( n, 0 are_congruent_mod 10 or n,1 are_congruent_mod 10 or n,3 are_congruent_mod 10 or n,5 are_congruent_mod 10 or n,6 are_congruent_mod 10 or n,8 are_congruent_mod 10 ) by Th23; :: thesis: verum
end;
end;