let a, n be Nat; :: thesis: a - 1 divides (a |^ n) - 1
A1: (2 |^ n) - 1 is Nat by NAT_1:21, PREPOWER:11;

per cases ( a <= 1 or a > 1 ) ;

suppose a <= 1 ; :: thesis: a - 1 divides (a |^ n) - 1

then ( a = 0 or a = 1 ) by NAT_1:25;
hence a - 1 divides (a |^ n) - 1 by INT_2:12; :: thesis: verum

end;

suppose a > 1 ; :: thesis: a - 1 divides (a |^ n) - 1

then A2: a >= 1 + 1 by NAT_1:13;

per cases ( a = 2 or a > 2 ) by A2, XXREAL_0:1;

suppose A3: a = 2 ; :: thesis: a - 1 divides (a |^ n) - 1

then ((a |^ n) - 1) mod (a - 1) = 0 by A1, RADIX_2:1;
hence a - 1 divides (a |^ n) - 1 by A3, INT_1:62; :: thesis: verum

end;

suppose A4: a > 2 ; :: thesis: a - 1 divides (a |^ n) - 1

then A5: a - 1 > 2 - 1 by XREAL_1:9;
A6: a - 1 is Nat by A4, NAT_1:20;
a mod (a - 1) = (a + ((a - 1) * (- 1))) mod (a - 1) by NAT_D:61
.= 1 by A5, PEPIN:5 ;
then A7: (a |^ n) mod (a - 1) = 1 by A5, A6, PEPIN:35;
((a |^ n) - 1) mod (a - 1) = (((a |^ n) mod (a - 1)) - (1 mod (a - 1))) mod (a - 1) by INT_6:7
.= (1 - 1) mod (a - 1) by A5, A7, PEPIN:5
.= 0 by A6, NAT_D:26 ;
hence a - 1 divides (a |^ n) - 1 by A5, INT_1:62; :: thesis: verum

end;

end;

end;

end;