Nuprl - Proof: divides iff rem zero 1 2

(24steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: divides iff rem zero 1 2

1. a :

2. b :

3. b | a
4.

, j:

. j | i

(i rem j) = 0

(a rem b) = 0

By:	(Decide (a0)) THEN (Decide (b0))

Generated subgoals:

1 5. a0
6. b0
  (a rem b) = 0
1 step

2 5. a0
6. b0
  (a rem b) = 0
3 steps

3 5. a0
6. b0
  (a rem b) = 0
3 steps

4 5. a0
6. b0
  (a rem b) = 0
3 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(24steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc

1	5. a0 6. b0 (a rem b) = 0	1 step
2	5. a0 6. b0 (a rem b) = 0	3 steps
3	5. a0 6. b0 (a rem b) = 0	3 steps
4	5. a0 6. b0 (a rem b) = 0	3 steps