Nuprl - Proof: reduce fac pres isprimefac 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: reduce fac pres isprimefac 1 1

1. a :

2. b :

3. f : {a..b

}

4. j : {a..b

}
5. 0<f(j)
6. i : {a..b

}
7. 0<reduce_factorization(f; j)(i)

0<f(i)

By:	FwdThru: Thm* a,b:, f:({a..b}), j:{a..b}. Thm* 0<f(j) (i:{a..b}. reduce_factorization(f; j)(i)f(i)) on [ 0<f(j) ] Using:[i]

Generated subgoals:

None

About:

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