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
)
2
x
[natprimes_lb]
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) 
2
xx:. prime(x) 
2x & 
(
i:{2..x
}. i | x)x:. prime(x) 2xx:. prime(x) 2x & (i:{2..x}. i | x)