Nuprl - Proof: prime factorization existsLEMMA 1 1 1 1

(13steps 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 existsLEMMA 1 1 1 1

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. i : {2..k

}
10. 0<g(i)

prime(i)

By:	BackThru: Hyp:7 ...

Generated subgoals:

None

About:

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

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