Nuprl - Proof: absval mul 2 2

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

1. a:
2. b:
3. a = 0
4. b = 0

|ab| = |a||b|

By: Unfold `absval` 0 THEN Repeat SplitOnConclITE

Generated subgoals:

1 5. 0ab
6. 0a
7. b < 0
ab = a(-b) 1 step

2 5. 0ab
6. a < 0
7. 0b
ab = (-a)b 1 step

3 5. ab < 0
6. 0a
7. 0b
-ab = ab 1 step

4 5. ab < 0
6. a < 0
7. b < 0
-ab = (-a)(-b) 1 step

About:

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

1	5. `0ab` 6. `0a` 7. `b < 0` `ab = a(-b)`	1 step

2	5. `0ab` 6. `a < 0` 7. `0b` `ab = (-a)b`	1 step

3	5. `ab < 0` 6. `0a` 7. `0b` `-ab = ab`	1 step

4	5. `ab < 0` 6. `a < 0` 7. `b < 0` `-ab = (-a)(-b)`	1 step