Nuprl - Proof: prime factorization exists2 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: prime factorization exists2 1 1 1

1. n : {1...}
2. h : {2..(n+1)

}

3. n =

{2..n+1

}(h)
4. is_prime_factorization(2; (n+1); h)

complete_intseg_mset(2; (n+1); h) is a factorization of n

By:

Analyze

Generated subgoals:

1 5. x : Prime
6. n<x
complete_intseg_mset(2; (n+1); h)(x) = 0
1 step

2 n = {2..n+1}(prime_mset_complete(complete_intseg_mset(2; (n+1); h)))
6 steps

About:

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

1	5. x : Prime 6. n<x complete_intseg_mset(2; (n+1); h)(x) = 0	1 step
2	n = {2..n+1}(prime_mset_complete(complete_intseg_mset(2; (n+1); h)))	6 steps