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
}. n1
i 
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. 2
n
6. n<k+1
7.
i:{2..k
}. n
i 
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