(2steps total)
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
only
positives
prime
fed
f
:(Prime
),
n
:
.
f
is a factorization of
n
0<
n
By:
Def of
f
is a factorization of
n
Generated subgoal:
1
1.
f
: Prime
2.
n
:
3.
x
:Prime
.
n
<
x
f
(
x
) = 0
4.
n
=
{2..
n
+1
}(prime_mset_complete(
f
))
0<
n
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
f:(Prime
), n:. f is a factorization of n 
0<n f:(Prime), n:. f is a factorization of n 0<n
x:Prime. n<x f(x) = 0
{2..n+1
}(prime_mset_complete(f))
0<n
