(3steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
natprime
nondivs
1
1.
x
:
2. prime(
x
)
3.
i
: {2..
x
}
4. 2
x
5.
(
i
:{2..
x
}.
i
|
x
)
i
|
x
By:
SimilarTo Hyp:-1 ...
Generated subgoal:
1
5.
i
|
x
i
:{2..
x
}.
i
|
x
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc