(8steps total)
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
prime
factorization
exists
1
1
1.
n
: {1...}
g
:({2..(
n
+1)
}
).
n
=
{2..
n
+1
}(
g
)
By:
Decide:
n
= 1
Generated subgoals:
1
2.
n
= 1
g
:({2..(
n
+1)
}
).
n
=
{2..
n
+1
}(
g
)
1
step
2
2.
n
= 1
g
:({2..(
n
+1)
}
).
n
=
{2..
n
+1
}(
g
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(8steps total)
PrintForm
Definitions
Lemmas
FTA
Sections
DiscrMathExt
Doc
g:({2..(n+1)
}
). n = 
{2..n+1}(g) g:({2..(n+1)}). n = {2..n+1}(g) g:({2..(n+1)}). n = {2..n+1}(g)
n = 1
g:({2..(n+1)}). n = {2..n+1}(g)
