Nuprl - Proof: prime factorization exists 1

(8steps 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 exists 1

1. n : {1...}

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

}

). n =

{2..n+1

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

By:	g:({2..(n+1)}). n = {2..n+1}(g) Asserted

Generated subgoals:

1 g:({2..(n+1)}). n = {2..n+1}(g)
3 steps

2 2. g:({2..(n+1)}). n = {2..n+1}(g)
h:({2..(n+1)}). n = {2..n+1}(h) & is_prime_factorization(2; (n+1); h)
3 steps

About:

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

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

1	g:({2..(n+1)}). n = {2..n+1}(g)	3 steps
2	2. g:({2..(n+1)}). n = {2..n+1}(g) h:({2..(n+1)}). n = {2..n+1}(h) & is_prime_factorization(2; (n+1); h)	3 steps