IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
prime factorization existsLEMMA
1
2
2
1
2
1. k : {2...}
2. n :
3. n1:.
3. n1<n
3.
3. (g:({2..k}).
3. (2 n1 < k+1
3. (
3. ((i:{2..k}. n1i 0<g(i) prime(i))
3. (
3. ((h:({2..k}).
3. (({2..k}(g) = {2..k}(h) & is_prime_factorization(2; k; h)))
4. g : {2..k}
5. 2n
6. n<k+1
7. i:{2..k}. ni 0<g(i) prime(i)
8. n = 2
9. prime(n-1)
10. g' : {2..k}
11. {2..k}(g) = {2..k}(g')
12. g'(n-1) = 0
13. u:{2..k}. n-1<u g'(u) = g(u)
14. h:({2..k}).
14. {2..k}(g') = {2..k}(h) & is_prime_factorization(2; k; h)
h:({2..k}).
{2..k}(g) = {2..k}(h) & is_prime_factorization(2; k; h)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html