let i, n be Nat; for fn being FinSequence of NAT st n > 1 & i,n are_coprime & len fn = order (i,n) & ( for d being Element of NAT st d in dom fn holds
fn . d = i |^ (d -' 1) ) holds
for d, e being Element of NAT st d in dom fn & e in dom fn & d <> e holds
not fn . d,fn . e are_congruent_mod n
let fn be FinSequence of NAT ; ( n > 1 & i,n are_coprime & len fn = order (i,n) & ( for d being Element of NAT st d in dom fn holds
fn . d = i |^ (d -' 1) ) implies for d, e being Element of NAT st d in dom fn & e in dom fn & d <> e holds
not fn . d,fn . e are_congruent_mod n )
assume A1:
( n > 1 & i,n are_coprime & len fn = order (i,n) & ( for d being Element of NAT st d in dom fn holds
fn . d = i |^ (d -' 1) ) )
; for d, e being Element of NAT st d in dom fn & e in dom fn & d <> e holds
not fn . d,fn . e are_congruent_mod n
then A2:
( i <> 0 & n <> 0 )
by Th5;
A3:
i gcd n = 1
by A1, INT_2:def 3;
assume
ex d, e being Element of NAT st
( d in dom fn & e in dom fn & d <> e & fn . d,fn . e are_congruent_mod n )
; contradiction
then consider d, e being Element of NAT such that
A4:
( d in dom fn & e in dom fn & d <> e & fn . d,fn . e are_congruent_mod n )
;
A5:
( d >= 1 & d <= order (i,n) & e >= 1 & e <= order (i,n) )
by A4, A1, FINSEQ_3:25;
then (d -' 1) + 1 =
(d + 1) -' 1
by NAT_D:38
.=
(d + 1) - 1
by NAT_D:37
.=
(d - 1) + 1
;
then A6:
d -' 1 = d - 1
;
(e -' 1) + 1 =
(e + 1) -' 1
by NAT_D:38, A5
.=
(e + 1) - 1
by NAT_D:37
.=
(e - 1) + 1
;
then A7:
( d - 1 = d -' 1 & e - 1 = e -' 1 )
by A6;
per cases
( d > e or e > d )
by A4, XXREAL_0:1;
suppose
d > e
;
contradictionthen A8:
e -' 1
< d -' 1
by A7, XREAL_1:9;
then consider k being
Nat such that A9:
d -' 1
= (e -' 1) + k
by NAT_1:10;
reconsider ll =
(i |^ k) - 1 as
Element of
NAT by A2, NAT_1:21, NAT_1:14;
A10:
(i |^ (d -' 1)) - (i |^ (e -' 1)) =
((i |^ (e -' 1)) * (i |^ k)) - ((i |^ (e -' 1)) * 1)
by A9, NEWTON:8
.=
(i |^ (e -' 1)) * ll
;
A11:
(i |^ (e -' 1)) gcd n = 1
by A2, A3, NAT_4:10;
i |^ (d -' 1),
fn . e are_congruent_mod n
by A1, A4;
then
i |^ (d -' 1),
i |^ (e -' 1) are_congruent_mod n
by A1, A4;
then
n divides (i |^ (d -' 1)) - (i |^ (e -' 1))
by INT_2:15;
then
n divides ll
by A10, A11, WSIERP_1:30;
then
i |^ k,1
are_congruent_mod n
by INT_2:15;
then A12:
(i |^ k) mod n =
1
mod n
by NAT_D:64
.=
1
by A1, PEPIN:5
;
A13:
(d -' 1) - (e -' 1) > 0
by A8, XREAL_1:50;
A14:
order (
i,
n)
<= k
by A13, A9, NAT_D:7, A1, A12, PEPIN:47;
d - e <= (order (i,n)) - 1
by A5, XREAL_1:13;
hence
contradiction
by A7, A9, A14, XXREAL_0:2, XREAL_1:146;
verum end; suppose
e > d
;
contradictionthen A15:
e -' 1
> d -' 1
by A7, XREAL_1:9;
then consider k being
Nat such that A16:
e -' 1
= (d -' 1) + k
by NAT_1:10;
reconsider ll =
(i |^ k) - 1 as
Element of
NAT by A2, NAT_1:21, NAT_1:14;
A17:
(i |^ (e -' 1)) - (i |^ (d -' 1)) =
((i |^ (d -' 1)) * (i |^ k)) - ((i |^ (d -' 1)) * 1)
by A16, NEWTON:8
.=
(i |^ (d -' 1)) * ll
;
A18:
(i |^ (d -' 1)) gcd n = 1
by A2, A3, NAT_4:10;
i |^ (d -' 1),
fn . e are_congruent_mod n
by A1, A4;
then
i |^ (d -' 1),
i |^ (e -' 1) are_congruent_mod n
by A1, A4;
then
i |^ (e -' 1),
i |^ (d -' 1) are_congruent_mod n
by INT_1:14;
then
n divides (i |^ (e -' 1)) - (i |^ (d -' 1))
by INT_2:15;
then
n divides ll
by A17, A18, WSIERP_1:30;
then
i |^ k,1
are_congruent_mod n
by INT_2:15;
then A19:
(i |^ k) mod n =
1
mod n
by NAT_D:64
.=
1
by A1, PEPIN:5
;
A20:
(e -' 1) - (d -' 1) > 0
by A15, XREAL_1:50;
A21:
order (
i,
n)
<= k
by A16, A20, NAT_D:7, A1, A19, PEPIN:47;
e - d <= (order (i,n)) - 1
by A5, XREAL_1:13;
hence
contradiction
by A16, A21, A7, XXREAL_0:2, XREAL_1:146;
verum end;