Nuprl - FTA LEMMAs for prime_divs_mul_via

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

Rank	Theorem	Name
17	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)))	[prime_divs_mul_via_intseg]
cites the following:
1	Thm* a,b:, e:({a..b}). a+1 = b ( i:{a..b}. e(i)) = e(a)	[mul_via_intseg_singleton]
2	Thm* a,b:, e:({a..b}). Thm* a<b ( i:{a..b}. e(i)) = ( i:{a..b-1}. e(i))e(b-1)	[mul_via_intseg_split_last]
16	Thm* X:. prime(X) (a,b:. X \| ab X \| a X \| b)	[nat_prime_div_each_factor]

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