let a, n be Nat; :: thesis: ( a > 1 implies a - 1 divides (a |^ n) - 1 )

A1: (2 |^ n) - 1 is Nat by NAT_1:21, PREPOWER:11;

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

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

A1: (2 |^ n) - 1 is Nat by NAT_1:21, PREPOWER:11;

assume 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;

end;

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;hence a - 1 divides (a |^ n) - 1 by A3, INT_1:62; :: thesis: verum

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;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