Nuprl - Pf div_3_to_1 1 1 1 1 1 1 1 1

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

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

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

By: FwdThru Thm* a,b:, n:. na < nb a < b [5] THEN FwdThru Thm* a,b:, n:. na < nb a < b [6] THEN OnHyps [6;5;4;3] Thin

Generated subgoal:

1 3. -((a b)+1) < -((-a) (-b))
4. -(1+((-a) (-b))) < -(a b)
(a b) = ((-a) (-b))

About:

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