let x be odd Integer; for k being Nat st k >= 3 holds
(x |^ (2 |^ (k -' 2))) mod (2 |^ k) = 1
let k be Nat; ( k >= 3 implies (x |^ (2 |^ (k -' 2))) mod (2 |^ k) = 1 )
assume A1:
k >= 3
; (x |^ (2 |^ (k -' 2))) mod (2 |^ k) = 1
defpred S1[ 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:
S1[3]
A7:
for k being Nat st k >= 3 & S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( k >= 3 & S1[k] implies S1[k + 1] )
assume A8:
(
k >= 3 &
S1[
k] )
;
S1[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
S1[
k + 1]
;
verum
end;
for k being Nat st k >= 3 holds
S1[k]
from NAT_1:sch 8(A3, A7);
hence
(x |^ (2 |^ (k -' 2))) mod (2 |^ k) = 1
by A1; verum