let p be Prime; :: thesis: ( p <> 2 implies (Mersenne p) mod (2 * p) = 1 )
assume A1: p <> 2 ; :: thesis: (Mersenne p) mod (2 * p) = 1
p > 1 by INT_2:def 4;
then 2 * p > 2 * 1 by XREAL_1:68;
then A2: 2 * p > 2 - 1 by XREAL_1:51;
(Mersenne p) mod (2 * p) = ((2 * (2 |^ (p -' 1))) - 1) mod (2 * p) by PEPIN:26
.= (((2 * (2 |^ (p -' 1))) mod (2 * p)) - (1 mod (2 * p))) mod (2 * p) by INT_6:7
.= ((2 * ((2 |^ (p -' 1)) mod p)) - (1 mod (2 * p))) mod (2 * p) by INT_4:20
.= ((2 * 1) - (1 mod (2 * p))) mod (2 * p) by A1, INT_2:28, INT_2:30, PEPIN:37
.= ((2 * 1) - 1) mod (2 * p) by A2, PEPIN:5 ;
hence (Mersenne p) mod (2 * p) = 1 by A2, PEPIN:5; :: thesis: verum