let p, q be Prime; :: thesis: ( p is odd & q divides Mersenne p implies ex k being Nat st q = ((2 * k) * p) + 1 )
assume A1: p is odd ; :: thesis: ( not q divides Mersenne p or ex k being Nat st q = ((2 * k) * p) + 1 )
assume A2: q divides Mersenne p ; :: thesis: ex k being Nat st q = ((2 * k) * p) + 1
then 2 |^ p,1 are_congruent_mod q ;
then A3: (2 |^ p) mod q = 1 mod q by NAT_D:64;
A4: q > 1 by INT_2:def 4;

A5: now :: thesis: not q <= 2

assume q <= 2 ; :: thesis: contradiction
then not not q = 0 & ... & not q = 2 ;
hence contradiction by A2, INT_2:def 4; :: thesis: verum

end;

then A6: 2,q are_coprime by XPRIMES1:2, INT_2:30;

A7: now :: thesis: not order (2,q) = 1

assume order (2,q) = 1 ; :: thesis: contradiction
then (2 |^ 1) mod q = 1 by A4, A6, PEPIN:def 2;
hence contradiction by A5, NAT_D:24; :: thesis: verum

end;

order (2,q) divides p by A3, A4, A6, PEPIN:47, NAT_D:24;
then A8: p = order (2,q) by A7, INT_2:def 4;
A9: Euler q = q - 1 by EULER_1:20;
(2 |^ (Euler q)) mod q = 1 by A6, EULER_2:18, INT_2:def 4;
then p divides q - 1 by A4, A6, A8, A9, PEPIN:47;
then consider w being Nat such that
A10: q - 1 = p * w ;
A11: q = (p * w) + 1 by A10;
then w is even by A1, A5, PEPIN:17;
then consider e being Nat such that
A12: w = 2 * e ;
take e ; :: thesis: q = ((2 * e) * p) + 1
thus q = ((2 * e) * p) + 1 by A11, A12; :: thesis: verum