theorem :: GR_CY_3:23

for p being Prime st p <> 2 holds
(Mersenne p) mod (2 * p) = 1