let x be odd Integer; :: thesis: for k being Nat st k >= 3 holds
(x |^ (2 |^ (k -' 2))) mod (2 |^ k) = 1
let k be Nat; :: thesis: ( k >= 3 implies (x |^ (2 |^ (k -' 2))) mod (2 |^ k) = 1 )
assume A1: k >= 3 ; :: thesis: (x |^ (2 |^ (k -' 2))) mod (2 |^ k) = 1
defpred S₁[ Nat] means (x |^ (2 |^ ($1 -' 2))) mod (2 |^ $1) = 1;
consider y being Integer such that
A2: x = (2 * y) + 1 by ABIAN:1;
A3: S₁[3]

proof

3 -' 2 = 3 - 2 by XREAL_1:233
.= 1 ;
then A4: (x |^ (2 |^ (3 -' 2))) mod (2 |^ 3) = (x |^ 2) mod (2 |^ 3)
.= (x ^2) mod (2 |^ 3) by NEWTON:81 ;
A5: (x ^2) - 1 = (2 ^2) * (y * (y + 1)) by A2;
2 divides y * (y + 1) by Lm1;
then (2 ^2) * 2 divides (x ^2) - 1 by A5, INT_4:7;
then (2 |^ 2) * 2 divides (x ^2) - 1 by NEWTON:81;
then 2 |^ (2 + 1) divides (x ^2) - 1 by NEWTON:6;
then A6: x ^2 ,1 are_congruent_mod 2 |^ 3 by INT_2:15;
(2 * 2) * 2 > 1 ;
then (2 |^ 2) * 2 > 1 by NEWTON:81;
then 2 |^ (2 + 1) > 1 by NEWTON:6;
hence S₁[3] by A4, A6, PEPIN:39; :: thesis: verum

end;

A7: for k being Nat st k >= 3 & S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( k >= 3 & S₁[k] implies S₁[k + 1] )
assume A8: ( k >= 3 & S₁[k] ) ; :: thesis: S₁[k + 1]
A9: ( k > 0 & k > 1 & k > 2 ) by A8, XXREAL_0:2;
A10: (k -' 3) + 1 = (k + 1) -' 3 by A8, NAT_D:38
.= (k + 1) - 3 by A8, NAT_D:37
.= k - 2 ;
k -' 2 = k - 2 by A9, XREAL_1:233;
then A11: x |^ (2 |^ (k -' 2)) = x |^ ((2 |^ (k -' 3)) * 2) by A10, NEWTON:6
.= (x |^ 2) |^ (2 |^ (k -' 3)) by NEWTON:9
.= (x ^2) |^ (2 |^ (k -' 3)) by NEWTON:81 ;
2 |^ k > 1 by A8, PEPIN:25;
then x |^ (2 |^ (k -' 2)),1 are_congruent_mod 2 |^ k by A8, A11, PEPIN:39;
then consider t being Integer such that
A12: (x |^ (2 |^ (k -' 2))) - 1 = (2 |^ k) * t by INT_1:def 3, INT_2:15;
(x |^ (2 |^ (k -' 2))) ^2 = (x |^ (2 |^ (k -' 2))) |^ 2 by NEWTON:81
.= x |^ ((2 |^ (k -' 2)) * 2) by NEWTON:9
.= x |^ (2 |^ ((k -' 2) + 1)) by NEWTON:6 ;
then A13: x |^ (2 |^ ((k -' 2) + 1)) = ((t * (2 |^ k)) + 1) ^2 by A12
.= (((t ^2) * ((2 |^ k) ^2)) + (2 * (t * (2 |^ k)))) + 1
.= (((t ^2) * ((2 |^ k) |^ 2)) + (2 * (t * (2 |^ k)))) + 1 by NEWTON:81
.= (((t ^2) * (2 |^ (2 * k))) + ((2 * (2 |^ k)) * t)) + 1 by NEWTON:9
.= (((t ^2) * (2 |^ (2 * k))) + ((2 |^ (k + 1)) * t)) + 1 by NEWTON:6 ;
k + k > k + 1 by A9, XREAL_1:8;
then A14: 2 |^ (k + 1) divides (t ^2) * (2 |^ (2 * k)) by NAT_D:9, PEPIN:31;
2 |^ (k + 1) divides (2 |^ (k + 1)) * t by INT_2:2;
then A15: 2 |^ (k + 1) divides ((t ^2) * (2 |^ (2 * k))) + ((2 |^ (k + 1)) * t) by A14, WSIERP_1:4;
A16: (((t ^2) * (2 |^ (2 * k))) + ((2 |^ (k + 1)) * t)) mod (2 |^ (k + 1)) = 0 by A15, INT_1:62;
(x |^ (2 |^ ((k + 1) -' 2))) mod (2 |^ (k + 1)) = (x |^ (2 |^ ((k -' 2) + 1))) mod (2 |^ (k + 1)) by NAT_D:38, A9
.= (((((t ^2) * (2 |^ (2 * k))) + ((2 |^ (k + 1)) * t)) mod (2 |^ (k + 1))) + (1 mod (2 |^ (k + 1)))) mod (2 |^ (k + 1)) by A13, NAT_D:66
.= 1 mod (2 |^ (k + 1)) by A16, NAT_D:65
.= 1 by PEPIN:5, PEPIN:25 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat st k >= 3 holds
S₁[k] from NAT_1:sch 8(A3, A7);
hence (x |^ (2 |^ (k -' 2))) mod (2 |^ k) = 1 by A1; :: thesis: verum