(8steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: sum arith 1 1

1. n:
2. a:
3. b:
4. sum(a+bi | i < n)2 = n(a+a+b(n-1))
2sum(a+bi | i < n) = 2((n(a+a+b(n-1))) 2)

By:
Inst Thm* a:, n:. a = (a n)n+(a rem n) [n(a+a+b(n-1));2]
THEN
Assert (((n(a+a+b(n-1))) rem 2) = 0)


Generated subgoal:

15. n(a+a+b(n-1)) = ((n(a+a+b(n-1))) 2)2+((n(a+a+b(n-1))) rem 2)
((n(a+a+b(n-1))) rem 2) = 0
5 steps

About:
intnatural_numberaddsubtractmultiplydivideremainderequalall

(8steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc