(7steps total)
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
prime
divs
exp
1
1
1
1
1.
p
:
2. prime(
p
)
3.
b
:
4.
z
:
5.
p
|
z
b
6.
b
= 0
7.
p
| 1
False
By:
FwdThru:
Thm*
b
:
.
b
| 1
prime(
b
) on [
p
| 1 ] ...
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc