let i, n be Nat; :: thesis: 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 being Element of NAT st d in dom fn holds
((fn . d) |^ (order (i,n))) mod n = 1
let fn be FinSequence of NAT ; :: thesis: ( 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 being Element of NAT st d in dom fn holds
((fn . d) |^ (order (i,n))) mod n = 1 )
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) ) ) ; :: thesis: for d being Element of NAT st d in dom fn holds
((fn . d) |^ (order (i,n))) mod n = 1
set K = order (i,n);
let d be Element of NAT ; :: thesis: ( d in dom fn implies ((fn . d) |^ (order (i,n))) mod n = 1 )
assume d in dom fn ; :: thesis: ((fn . d) |^ (order (i,n))) mod n = 1
then A2: fn . d = i |^ (d -' 1) by A1;
A3: ((fn . d) |^ (order (i,n))) mod n = (i |^ ((order (i,n)) * (d -' 1))) mod n by NEWTON:9, A2
.= ((i |^ (order (i,n))) |^ (d -' 1)) mod n by NEWTON:9 ;
(i |^ (order (i,n))) mod n = 1 by A1, PEPIN:def 2
.= 1 mod n by A1, PEPIN:5 ;
then ((i |^ (order (i,n))) |^ (d -' 1)) mod n = (1 |^ (d -' 1)) mod n by INT_4:8
.= 1 mod n
.= 1 by A1, PEPIN:5 ;
hence ((fn . d) |^ (order (i,n))) mod n = 1 by A3; :: thesis: verum