Nuprl - FTA LEMMAs for nat_prime_div_each

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

Rank	Theorem	Name
15	Thm* X:. Thm* prime(X) Thm* Thm* (X1:. X1<X prime(X1) (a,b:. X1 \| ab X1 \| a X1 \| b)) Thm* Thm* (W:. 0<W W<X (t:. X \| tW X \| t))	[nat_prime_div_each_factorLEMMA]
cites the following:
14	Thm* x:{2...}. p:{2...}. px & prime(p) & p \| x	[prime_or_smaller_prime_factor]
0	Thm* P Q P Q	[disjunct_elim]
11	Thm* x:. prime(x) (i:{2..x}. i \| x)	[natprime_nondivs]
2	Thm* a,b:. a \| b (c:. b = ac)	[divides_def_on_nat]
4	Thm* a,b:. 0<ab 0<a & 0<b	[pos_mul_arg_boundsNat]
2	Thm* i:{2...}, j:{1...}. j<ij	[factor_smaller]

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