Nuprl - Pf div_2_to_1 1 1 1

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

At: div 2 to 1 1 1 1

1. a: {...0}
2. b:
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',(((-a) b)(-b))] (FwdThru Thm* a,b,n:. a = b a+n = b+n [3]) THEN Using [`n',((a b)(-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:

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