let p be Prime; :: thesis: ( p <> 2 implies (Mersenne p) mod 8 = 7 )
A1: p > 1 by INT_2:def 4;
then A2: p >= 1 + 1 by NAT_1:13;
assume p <> 2 ; :: thesis: (Mersenne p) mod 8 = 7
then p > 2 + 0 by A2, XXREAL_0:1;
then p - 2 > 2 - 2 by XREAL_1:14;
then A3: p -' 2 > 0 by A2, XREAL_1:233;
A4: p -' 1 > 0 by A1, NAT_D:49;
(Mersenne p) mod 8 = ((2 * (2 |^ (p -' 1))) - 1) mod 8 by PEPIN:26
.= (((2 * (2 |^ (p -' 1))) mod (2 * 4)) - (1 mod 8)) mod 8 by INT_6:7
.= ((2 * ((2 |^ (p -' 1)) mod 4)) - (1 mod 8)) mod 8 by INT_4:20
.= ((2 * ((2 * (2 |^ ((p -' 1) -' 1))) mod (2 * 2))) - (1 mod 8)) mod 8 by A4, PEPIN:26
.= ((2 * ((2 * (2 |^ (p -' 2))) mod (2 * 2))) - (1 mod 8)) mod 8 by NAT_D:45
.= ((2 * (2 * ((2 |^ (p -' 2)) mod 2))) - (1 mod 8)) mod 8 by INT_4:20
.= ((4 * ((2 |^ (p -' 2)) mod 2)) - 1) mod 8 by PEPIN:5
.= ((4 * 0) - 1) mod 8 by A3, PEPIN:36
.= ((- 1) + (8 * 1)) mod 8 by NAT_D:61
.= 7 by NAT_D:24 ;
hence (Mersenne p) mod 8 = 7 ; :: thesis: verum