Nuprl - Proof: prime factorization exists2 1 1 1 2 1

(11steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc

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

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

}

3. n =

{2..n+1

}(h)
4. is_prime_factorization(2; (n+1); h)
5. x : {2..(n+1)

}

h(x) = prime_mset_complete(complete_intseg_mset(2; (n+1); h))(x)

By:	Decide: prime(x)

Generated subgoals:

1 6. prime(x)
h(x) = prime_mset_complete(complete_intseg_mset(2; (n+1); h))(x)
2 steps

2 6. prime(x)
h(x) = prime_mset_complete(complete_intseg_mset(2; (n+1); h))(x)
2 steps

About:

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

(11steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc

1	6. prime(x) h(x) = prime_mset_complete(complete_intseg_mset(2; (n+1); h))(x)	2 steps
2	6. prime(x) h(x) = prime_mset_complete(complete_intseg_mset(2; (n+1); h))(x)	2 steps