(5steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nonprime
nat
1
1
1
1.
x
:
2.
i
: {2..
x
}
3.
c
:
4.
x
=
i
c
c
{2..
x
}
By:
Inst:
Thm*
k
:
,
i
:{2..
k
},
j
:
.
i
j
=
k
2
j
<
k
&
i
<
k
Using:[
x
|
i
|
c
]
Generated subgoal:
1
5. 2
c
<
x
&
i
<
x
c
{2..
x
}
Auto
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
}
c
c 
{2..x}
}
c
c {2..x}
k:
, i:{2..k}, j:. ij = k 
2 
j < k & i<k Using:[x | i | c] c < x & i<x
c {2..x}
