Nuprl - Proof: prime divs exp 1 2

(7steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: prime divs exp 1 2

1. p :

2. prime(p)
3. b :

4. z :

5. p | z

b
6. b

0

p | z

By:	Auto THEN Inst: Thm* p:. Thm* prime(p) Thm* Thm* (a,b:, e:({a..b}). Thm* (a<b p \| ( i:{a..b}. e(i)) (i:{a..b}. p \| e(i))) Using:[p \| 0 \| b \| e(i):= z] ...

Generated subgoal:

1 7. i:b. p | z
p | z
1 step

About:

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

(7steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc