Nuprl - Pf div_4_to

(11steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

1. a:
2. b: {...-1}
3. a = (a (-b))(-b)+(a rem -b)
4. 0(a rem -b)
5. (a rem -b) < -b
6. a = (a b)b+(a rem b)
7. 0(a rem b)
8. (a rem b) < -b

(a b) = -(a (-b))

By: Using [`n',(b(a (-b)))] (FwdThru Thm* a,b,n:. a = b a+n = b+n [3]) THEN Using [`n',((-b)(a b))] (FwdThru Thm* a,b,n:. a = b a+n = b+n [6]) THEN OnMHyps [-1;-2] ArithSimp THEN OnHyps [6;3] Thin

Generated subgoal:

1 3. 0(a rem -b)
4. (a rem -b) < -b
5. 0(a rem b)
6. (a rem b) < -b
7. a+b(a (-b)) = (a rem -b)
8. a+-b(a b) = (a rem b)
(a b) = -(a (-b))

About:

(11steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc