Nuprl - FTA LEMMAs for prime_factorization_includes_prime

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

Rank	Theorem	Name
19	Thm* a:, b:, f:({a..b}), p:. Thm* is_prime_factorization(a; b; f) Thm* Thm* prime(p) p \| {a..b}(f) p {a..b} & 0<f(p)	[prime_factorization_includes_prime_divisors]
cites the following:
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]
0	Thm* f:(AAA), u:A, a,b:, e:({a..b}A). Thm* ba (Iter(f;u) i:{a..b}. e(i)) = u	[iter_via_intseg_null]
11	Thm* b:. b \| 1 prime(b)	[no_nat_prime_divs_one]
18	Thm* p:. prime(p) (b,z:. p \| zb b 0 & p \| z)	[prime_divs_exp]
11	Thm* x:{2...}, y:. prime(y) x \| y x = y	[prime_nat_divby_self_only]
10	Thm* x:. prime(x) 2x & (i:{2..x}. i \| x)	[prime_nat]

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