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

At: sum arith 1 1 1 1 1 2
1. z:
2. 0z
((z2) rem 2) = 0
By:
RWO Thm* a:{...0}, n:. (a rem n) = -((-a) rem n) 0
THEN
Inst Thm* a,b:, n:. ((a+bn) rem n) = (a rem n) [0;-z;2]
THEN
Reduce -1
Generated subgoals:

None

About:
intnatural_numberminusaddmultiplyremainderequalall

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