Nuprl - Proof: prime factorization exists 1 2 1 1

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

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

}

3. n =

{2..n+1

}(g)
4.

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

}

).
4.

{2..n+1

}(g) =

{2..n+1

}(h) & is_prime_factorization(2; (n+1); h)

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

}

). n =

{2..n+1

}(h) & is_prime_factorization(2; (n+1); h)

By:	SimilarTo: Hyp:-1

Generated subgoals:

None

About:

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