(9steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
prime
among
factors
1
1.
a
:
2.
b
:
3. prime(
a
b
)
a
b
=
a
a
b
=
b
By:
Guarding (<prop> & <prop>)
FwdThru:
Thm*
x
:
. prime(
x
)
2
x
&
(
i
:{2..
x
}.
i
|
x
)
on [ prime(
a
b
) ] ...
Generated subgoal:
1
4. 2
a
b
5.
(
i
:{2..(
a
b
)
}.
i
|
a
b
)
a
b
=
a
a
b
=
b
7
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(9steps total)
PrintForm
Definitions
Lemmas
SimpleMulFacts
Sections
DiscrMathExt
Doc
b)
ab = a 
ab = b
b)
ab = a ab = b
x:. prime(x) 
2
x & 
(
i:{2..x
}. i | x)
b) ] ...ab
(i:{2..(ab)}. i | ab)
ab = a ab = b
