(18steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
composite
with
prime
factor
1
1
1
1.
x
:
2.
x1
:
.
x1
<
x
2
x1
prime(
x1
)
(
i
,
j
:{2..
x1
}.
x1
=
i
j
& prime(
i
))
3. 2
x
4.
prime(
x
)
5.
i
,
j
:{2..
x
}.
x
=
i
j
i
,
j
:{2..
x
}.
x
=
i
j
& prime(
i
)
By:
ExistHD Hyp:-1
Generated subgoal:
1
5.
i
: {2..
x
}
6.
j
: {2..
x
}
7.
x
=
i
j
i
,
j
:{2..
x
}.
x
=
i
j
& prime(
i
)
10
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(18steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc