(8steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
At:
sum
arith
1
1
1
1
1
1
1.
z:
2.
0
z
((z
2) rem 2) = 0
By:
Inst
Thm*
a,b:
, n:
. ((a+b
n) rem n) = (a rem n) [0;z;2]
THEN
Reduce -1
Generated subgoals:
None
About:
(8steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
z
((z
2) rem 2) = 0
a,b:
, n:
. ((a+bn) rem n) = (a rem n)
[0;z;2]