A3:
2 to_power n > 0
by POWER:34;
then A4:
(2 to_power n) + 1 > 0 + 1
by XREAL_1:6;
then
((2 to_power n) + 1) - 1 >= (1 + 1) - 1
by NAT_1:13;
then
(((2 to_power n) + 1) - 1) - 1 >= ((1 + 1) - 1) - 1
by XREAL_1:9;
then reconsider n3 = (((2 to_power n) + 1) - 1) - 1 as Element of NAT by INT_1:3;
reconsider nn = (2 to_power n) + 1 as Nat ;
reconsider n2 = ((2 to_power n) + 1) - 1 as Nat ;
A5:
2 to_power n <> 1
by POWER:35;
n2 * n2 = (nn * n3) + 1
;
then A6: (n2 * n2) mod nn =
1 mod nn
by NAT_D:21
.=
1
by A4, NAT_D:24
;
per cases
( i = 0 or i <> 0 )
;
suppose A7:
i = 0
;
ex b1 being Nat st
( MUL_MOD (i,b1,n) = 1 & b1 is_expressible_by n )consider j being
Nat such that A8:
j = 0
;
take
j
;
( MUL_MOD (i,j,n) = 1 & j is_expressible_by n )A9:
j is_expressible_by n
by A3, A8;
MUL_MOD (
i,
j,
n) =
ChangeVal_2 (
(((2 to_power n) * (ChangeVal_1 (0,n))) mod nn),
n)
by A7, A8, Def7
.=
ChangeVal_2 (
((n2 * n2) mod nn),
n)
by Def7
.=
1
by A5, A6, Def8
;
hence
(
MUL_MOD (
i,
j,
n)
= 1 &
j is_expressible_by n )
by A9;
verum end; suppose A10:
i <> 0
;
ex b1 being Nat st
( MUL_MOD (i,b1,n) = 1 & b1 is_expressible_by n )
i < 2
to_power n
by A1;
then
i < (2 to_power n) + 1
by NAT_1:13;
then consider a being
Nat such that A11:
(a * i) mod ((2 to_power n) + 1) = 1
and A12:
a < (2 to_power n) + 1
by A2, A4, A10, Th1;
take k =
ChangeVal_2 (
a,
n);
( MUL_MOD (i,k,n) = 1 & k is_expressible_by n )A13:
a <> 0
by A11, NAT_D:24;
now ( MUL_MOD (i,k,n) = 1 & k is_expressible_by n )per cases
( a <> 2 to_power n or a = 2 to_power n )
;
suppose A14:
a <> 2
to_power n
;
( MUL_MOD (i,k,n) = 1 & k is_expressible_by n )then A15:
k = a
by Def8;
then
k <= 2
to_power n
by A12, NAT_1:13;
then
k < 2
to_power n
by A14, A15, XXREAL_0:1;
then A16:
k is_expressible_by n
;
MUL_MOD (
i,
k,
n) =
ChangeVal_2 (
((i * (ChangeVal_1 (k,n))) mod ((2 to_power n) + 1)),
n)
by A10, Def7
.=
ChangeVal_2 (
((i * a) mod ((2 to_power n) + 1)),
n)
by A13, A15, Def7
.=
1
by A5, A11, Def8
;
hence
(
MUL_MOD (
i,
k,
n)
= 1 &
k is_expressible_by n )
by A16;
verum end; suppose A17:
a = 2
to_power n
;
( MUL_MOD (i,k,n) = 1 & k is_expressible_by n )then A18:
k = 0
by Def8;
then A19:
k is_expressible_by n
by A3;
MUL_MOD (
i,
k,
n) =
ChangeVal_2 (
((i * (ChangeVal_1 (k,n))) mod ((2 to_power n) + 1)),
n)
by A10, Def7
.=
ChangeVal_2 (
((i * a) mod ((2 to_power n) + 1)),
n)
by A17, A18, Def7
.=
1
by A5, A11, Def8
;
hence
(
MUL_MOD (
i,
k,
n)
= 1 &
k is_expressible_by n )
by A19;
verum end; end; end; hence
(
MUL_MOD (
i,
k,
n)
= 1 &
k is_expressible_by n )
;
verum end; end;