(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+b
i | i < n)
2 = n
(a+a+b
(n-1))
2
sum(a+b
i | 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:
1
5.
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:
(8steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc