SimpleMulFacts
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
11
Thm*
x
:
. prime(
x
)
(
i
:{2..
x
}.
i
|
x
)
[natprime_nondivs]
cites the following:
10
Thm*
x
:
. prime(
x
)
2
x
&
(
i
:{2..
x
}.
i
|
x
)
[prime_nat]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
SimpleMulFacts
Sections
DiscrMathExt
Doc
x:
. prime(x) 
(i:{2..x
}. 
i | x)x:. prime(x) 
2
x & (
i:{2..x}. i | x)x:. prime(x) (i:{2..x}. i | x)x:. prime(x) 2x & (i:{2..x}. i | x)