let k, n be Nat; for p being odd Prime st n = (p - 1) * ((k * p) + 1) holds
(2 |^ n) mod p = 1
let p be odd Prime; ( n = (p - 1) * ((k * p) + 1) implies (2 |^ n) mod p = 1 )
assume A1:
n = (p - 1) * ((k * p) + 1)
; (2 |^ n) mod p = 1
A2:
1 < p
by INT_2:def 4;
then A3:
p -' 1 = p - 1
by XREAL_1:233;
A4:
2 |^ n = (2 |^ (p - 1)) |^ ((k * p) + 1)
by A1, NEWTON:9;
2 |^ 1,p are_coprime
by NAT_5:3;
then
(2 |^ (p -' 1)) mod p = 1
by PEPIN:37;
hence
(2 |^ n) mod p = 1
by A2, A3, A4, PEPIN:35; verum