Nuprl - Pf div_4_to_1 1 1 1 1 1 1 1 1

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

1. a:
2. b: {...-1}
3. -b(a (-b)) < -b+b(a b)
4. b(a b) < -b+-b(a (-b))
5. (-b)(a (-b)) < (-b)(1+-(a b))
6. (-b)(-(a b)) < (-b)(1+(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. -(a b) < 1+(a (-b))
(a b) = -(a (-b))

About:

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