Nuprl - Proof: div rem properties 1 2

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

At: div rem properties 1 2

1. a:
2. n:
3. a = (a n)n+(a rem n)
4. (0 n) = 0

|a rem n| < |n| & ((a rem n) < 0 a < 0) & ((a rem n) > 0 a > 0)

By: ((Decide (0a)) THEN (Decide (0n))) THENL [Inst Thm* a:, n:. 0(a rem n) & (a rem n) < n [a;n] ;Inst Thm* a:, n:{...-1}. 0(a rem n) & (a rem n) < -n [a;n] ;Inst Thm* a:{...0}, n:. 0(a rem n) & (a rem n) > -n [a;n] ;Inst Thm* a:{...0}, n:{...-1}. 0(a rem n) & (a rem n) > n [a;n]] THEN Unfold `absval` 0 THEN Repeat SplitOnConclITE THEN MoveToConcl 3 THEN MoveToConcl -1 THEN CaseNat 0 `a' THEN Subst ((0 n) = 0) -1

Generated subgoals:

None

About:

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