let a, m be Nat; :: thesis: ( a <> 0 & m > 1 & a,m are_relative_prime implies (a |^ (Euler m)) mod m = 1 )
assume that
A1: a <> 0 and
A2: m > 1 and
A3: a,m are_relative_prime ; :: thesis: (a |^ (Euler m)) mod m = 1
set X = { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ;
A4: a |^ (Euler m) <> 0 by A1, PREPOWER:12;
set Y = { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } ;
A5: for x being Nat st x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } holds
(a * x) mod m in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) }

proof

let x be Nat; :: thesis: ( x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } implies (a * x) mod m in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } )
assume x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ; :: thesis: (a * x) mod m in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) }
then consider t being Element of NAT such that
A6: t = x and
A7: m,t are_relative_prime and
A8: t >= 1 and
t <= m ;
A9: a * t,m are_relative_prime by A1, A2, A3, A7, EULER_1:15;
(a * t) mod m <> 0

proof

assume (a * t) mod m = 0 ; :: thesis: contradiction
then consider s being Nat such that
A10: a * t = (m * s) + 0 and
0 < m by A2, NAT_D:def 2;
s gcd 1 = 1 by NEWTON:64;
then (m * s) gcd (m * 1) = m by EULER_1:6;
hence contradiction by A2, A9, A10, INT_2:def 4; :: thesis: verum

end;

then A11: (a * t) mod m >= 1 by NAT_1:14;
A12: (a * t) mod m <= m by A2, NAT_D:1;
m,(a * t) mod m are_relative_prime by A1, A2, A3, A7, A8, Th5;
hence (a * x) mod m in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } by A6, A11, A12; :: thesis: verum

end;

A13: { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } = { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) }

proof

thus { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } c= { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } :: according to XBOOLE_0:def 10 :: thesis: { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } c= { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } or x in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } )
assume x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ; :: thesis: x in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) }
then consider xx being Element of NAT such that
A14: x = xx and
A15: m,xx are_relative_prime and
xx >= 1 and
A16: xx <= m ;
consider i, j being Integer such that
A17: (i * a) + (j * m) = xx by A3, EULER_1:11;
xx <> m by A2, A15, EULER_1:2;
then xx < m by A16, XXREAL_0:1;
then A18: xx mod m = xx by NAT_D:24;
reconsider im = i mod m as Element of NAT by INT_1:16, NEWTON:78;
i mod m <> 0

proof

assume i mod m = 0 ; :: thesis: contradiction
then 0 = i - ((i div m) * m) by A2, INT_1:def 8;
then m gcd xx = (m * 1) gcd (m * (((i div m) * a) + j)) by A17
.= m * (1 gcd (((i div m) * a) + j)) by A2, EULER_1:16
.= m * 1 by Lm3
.= m ;
hence contradiction by A2, A15, INT_2:def 4; :: thesis: verum

end;

then A19: im >= 1 by NAT_1:14;
A20: i = ((i div m) * m) + (i mod m) by A2, NEWTON:80;
then reconsider ij = ((i mod m) * a) + ((((i div m) * a) + j) * m) as Element of NAT by A17;
A21: im <= m by A2, NEWTON:79;
A22: ij mod m = (im * a) mod m by EULER_1:13;
then m,im are_relative_prime by A2, A15, A18, A17, A20, Th6;
then im in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } by A19, A21;
hence x in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } by A14, A18, A17, A20, A22; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } or y in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } )
assume y in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } ; :: thesis: y in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) }
then ex yy being Element of NAT st
( y = yy & ex u being Element of NAT st
( yy = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) ) ;
hence y in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } by A5; :: thesis: verum

end;

A23: for xi, xj being Nat st xi in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } & xj in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } & xi <> xj holds
(a * xi) mod m <> (a * xj) mod m

proof

let xi, xj be Nat; :: thesis: ( xi in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } & xj in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } & xi <> xj implies (a * xi) mod m <> (a * xj) mod m )
assume that
A24: xi in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } and
A25: xj in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } and
A26: xi <> xj ; :: thesis: (a * xi) mod m <> (a * xj) mod m
set tm = (a * xi) mod m;
set sm = (a * xj) mod m;
assume A27: (a * xi) mod m = (a * xj) mod m ; :: thesis: contradiction
consider s being Element of NAT such that
A28: s = xj and
m,s are_relative_prime and
A29: ( s >= 1 & s <= m ) by A25;
A30: (a * xj) mod m = (a * s) - (m * ((a * s) div m)) by A2, A28, NEWTON:77;
consider t being Element of NAT such that
A31: t = xi and
m,t are_relative_prime and
A32: ( t >= 1 & t <= m ) by A24;
(a * xi) mod m = (a * t) - (m * ((a * t) div m)) by A2, A31, NEWTON:77;
then 0 = (a * (t - s)) - (m * (((a * t) div m) - ((a * s) div m))) by A27, A30;
then A33: m divides a * (t - s) by INT_1:def 9;
reconsider m = m, c = t - s as Integer ;
( 1 - m <= c & c <= m - 1 ) by A32, A29, XREAL_1:15;
then t - s = 0 by A3, A33, Lm4, INT_2:40;
hence contradiction by A26, A31, A28; :: thesis: verum

end;

reconsider FX = Sgm { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } as FinSequence of NAT ;
reconsider FYY = a * FX as FinSequence of NAT ;
reconsider FY = FYY mod m as FinSequence of NAT ;
A34: { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } c= Seg m

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } or x in Seg m )
assume x in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ; :: thesis: x in Seg m
then ex xx being Element of NAT st
( x = xx & m,xx are_relative_prime & xx >= 1 & xx <= m ) ;
hence x in Seg m by FINSEQ_1:3; :: thesis: verum

end;

then reconsider X = { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } as finite set ;
dom FYY = Seg (len FYY) by FINSEQ_1:def 3
.= Seg (len FX) by NEWTON:6 ;
then A35: dom FX = dom FYY by FINSEQ_1:def 3;
A36: dom FY = Seg (len FY) by FINSEQ_1:def 3
.= Seg (len FYY) by Def1
.= Seg (len FX) by NEWTON:6 ;
then A37: dom FX = dom FY by FINSEQ_1:def 3;
A38: rng FY = { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) }

proof

thus rng FY c= { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } :: according to XBOOLE_0:def 10 :: thesis: { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } c= rng FY

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng FY or x in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } )
assume x in rng FY ; :: thesis: x in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) }
then consider y being set such that
A39: y in dom FY and
A40: x = FY . y by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A39;
FX . y in rng FX by A37, A39, FUNCT_1:def 5;
then A41: FX . y in X by A34, FINSEQ_1:def 13;
y in dom FX by A36, A39, FINSEQ_1:def 3;
then FY . y = (FYY . y) mod m by A35, Def1
.= (a * (FX . y)) mod m by RVSUM_1:66 ;
hence x in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } by A40, A41; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } or y in rng FY )
assume y in { l where l is Element of NAT : ex u being Element of NAT st
( l = (a * u) mod m & u in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } ) } ; :: thesis: y in rng FY
then consider yy being Element of NAT such that
A42: y = yy and
A43: ex u being Element of NAT st
( yy = (a * u) mod m & u in X ) ;
consider uu being Element of NAT such that
A44: yy = (a * uu) mod m and
A45: uu in X by A43;
uu in rng FX by A34, A45, FINSEQ_1:def 13;
then consider xx being set such that
A46: xx in dom FX and
A47: uu = FX . xx by FUNCT_1:def 5;
reconsider xx = xx as Element of NAT by A46;
FY . xx = (FYY . xx) mod m by A35, A46, Def1
.= y by A42, A44, A47, RVSUM_1:66 ;
hence y in rng FY by A37, A46, FUNCT_1:def 5; :: thesis: verum

end;

A48: FY is one-to-one

proof

A49: FX is one-to-one by A34, FINSEQ_3:99;
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 FY or not x2 in proj1 FY or not FY . x1 = FY . x2 or x1 = x2 )
assume that
A50: x1 in dom FY and
A51: x2 in dom FY and
A52: FY . x1 = FY . x2 ; :: thesis: x1 = x2
A53: x2 in dom FX by A36, A51, FINSEQ_1:def 3;
reconsider x2 = x2 as Element of NAT by A51;
A54: x1 in dom FX by A36, A50, FINSEQ_1:def 3;
reconsider x1 = x1 as Element of NAT by A50;
A55: ( FX . x1 in rng FX & FX . x2 in rng FX ) by A37, A50, A51, FUNCT_1:def 5;
A56: FY . x2 = (FYY . x2) mod m by A35, A53, Def1
.= (a * (FX . x2)) mod m by RVSUM_1:66 ;
FY . x1 = (FYY . x1) mod m by A35, A54, Def1
.= (a * (FX . x1)) mod m by RVSUM_1:66 ;
then ( not FX . x1 in X or not FX . x2 in X or not FX . x1 <> FX . x2 ) by A23, A52, A56;
hence x1 = x2 by A34, A54, A53, A55, A49, FINSEQ_1:def 13, FUNCT_1:def 8; :: thesis: verum

end;

for x being set holds card (Coim FX,x) = card (Coim FY,x)

proof

let x be set ; :: thesis: card (Coim FX,x) = card (Coim FY,x)

now

per cases ( x in X or not x in X ) ;

suppose A57: x in X ; :: thesis: card (Coim FX,x) = card (Coim FY,x)

A58: FX is one-to-one by A34, FINSEQ_3:99;
x in rng FX by A34, A57, FINSEQ_1:def 13;
then A59: len (FX - {x}) = (len FX) - 1 by A58, FINSEQ_3:97;
A60: ( (len (FX - {x})) - (len (FX - {x})) = ((len FX) - (card (FX " {x}))) - (len (FX - {x})) & len (FY - {x}) = (len FY) - (card (FY " {x})) ) by FINSEQ_3:66;
len (FY - {x}) = (len FY) - 1 by A13, A38, A48, A57, FINSEQ_3:97;
hence card (Coim FX,x) = card (Coim FY,x) by A59, A60; :: thesis: verum

end;

suppose not x in X ; :: thesis: card (Coim FX,x) = card (Coim FY,x)

then ( not x in rng FX & FY " {x} = {} ) by A13, A34, A38, FINSEQ_1:def 13, FUNCT_1:142;
hence card (Coim FX,x) = card (Coim FY,x) by FUNCT_1:142; :: thesis: verum

end;

end;

end;

hence card (Coim FX,x) = card (Coim FY,x) ; :: thesis: verum

end;

then A61: FX,FY are_fiberwise_equipotent by CLASSES1:def 9;
then A62: len FX = len FY by RFINSEQ:16;
A63: (Product FY) mod m = ((a |^ (len FY)) * (Product FX)) mod m

proof

defpred S₁[ Nat] means ( $1 <= len FY implies (Product (FY | $1)) mod m = ((a |^ (len (FY | $1))) * (Product (FX | $1))) mod m );
FY | (len FY) = FY | (Seg (len FY)) by FINSEQ_1:def 15;
then A64: FY = FY | (len FY) by FINSEQ_2:23;
A65: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )

now

per cases ( n + 1 <= len FY or n + 1 > len FY ) ;

suppose A66: n + 1 <= len FY ; :: thesis: ( S₁[n] implies S₁[n + 1] )

then len (FX | (n + 1)) = n + 1 by A62, FINSEQ_1:80;
then A67: FX | (n + 1) = ((FX | (n + 1)) | n) ^ <*((FX | (n + 1)) . (n + 1))*> by RFINSEQ:20;
assume A68: S₁[n] ; :: thesis: S₁[n + 1]
0 + 1 <= n + 1 by NAT_1:13;
then A69: n + 1 in dom FY by A66, FINSEQ_3:27;
A70: (FY | (n + 1)) . (n + 1) = FY . (n + 1) by FINSEQ_3:121;
A71: (FX | (n + 1)) . (n + 1) = FX . (n + 1) by FINSEQ_3:121;
A72: n <= n + 1 by NAT_1:11;
then A73: len (FY | n) = n by A66, FINSEQ_1:80, XXREAL_0:2;
A74: (FX | (n + 1)) | n = FX | n by A72, FINSEQ_5:80;
A75: (FY | (n + 1)) | n = FY | n by A72, FINSEQ_5:80;
A76: len (FY | (n + 1)) = n + 1 by A66, FINSEQ_1:80;
then FY | (n + 1) = ((FY | (n + 1)) | n) ^ <*((FY | (n + 1)) . (n + 1))*> by RFINSEQ:20;
then (Product (FY | (n + 1))) mod m = ((Product (FY | n)) * (FY . (n + 1))) mod m by A75, A70, RVSUM_1:126
.= ((((a |^ (len (FY | n))) * (Product (FX | n))) mod m) * ((FY . (n + 1)) mod m)) mod m by A66, A68, A72, Th11, XXREAL_0:2
.= ((((a |^ (len (FY | n))) * (Product (FX | n))) mod m) * (((FYY . (n + 1)) mod m) mod m)) mod m by A37, A35, A69, Def1
.= ((((a |^ (len (FY | n))) * (Product (FX | n))) mod m) * (((a * FX) . (n + 1)) mod m)) mod m by Th7
.= (((a |^ (len (FY | n))) * (Product (FX | n))) * ((a * FX) . (n + 1))) mod m by Th11
.= (((a |^ n) * (Product (FX | n))) * (a * (FX . (n + 1)))) mod m by A73, RVSUM_1:66
.= (((a |^ n) * a) * ((Product (FX | n)) * (FX . (n + 1)))) mod m
.= ((a |^ (len (FY | (n + 1)))) * ((Product (FX | n)) * (FX . (n + 1)))) mod m by A76, NEWTON:11
.= ((a |^ (len (FY | (n + 1)))) * (Product (FX | (n + 1)))) mod m by A67, A74, A71, RVSUM_1:126 ;
hence S₁[n + 1] ; :: thesis: verum

end;

suppose n + 1 > len FY ; :: thesis: ( S₁[n] implies S₁[n + 1] )

hence ( S₁[n] implies S₁[n + 1] ) ; :: thesis: verum

end;

end;

end;

hence ( S₁[n] implies S₁[n + 1] ) ; :: thesis: verum

end;

FX | (len FX) = FX | (Seg (len FX)) by FINSEQ_1:def 15;
then A77: FX = FX | (len FY) by A62, FINSEQ_2:23;
A78: S₁[ 0 ] by NEWTON:9, RVSUM_1:124;
for n being Nat holds S₁[n] from NAT_1:sch 2(A78, A65);
hence (Product FY) mod m = ((a |^ (len FY)) * (Product FX)) mod m by A64, A77; :: thesis: verum

end;

A79: Product FX,m are_relative_prime

proof

defpred S₁[ Nat] means ( $1 <= len FX implies Product (FX | $1),m are_relative_prime );
A80: FX | (len FX) = FX by FINSEQ_1:79;
A81: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )

now

per cases ( len FX >= n + 1 or len FX < n + 1 ) ;

suppose A82: len FX >= n + 1 ; :: thesis: ( S₁[n] implies S₁[n + 1] )

reconsider FF = FX | (n + 1) as FinSequence of NAT ;
reconsider ff = FF . (n + 1) as Element of NAT ;
len FF = n + 1 by A82, FINSEQ_1:80;
then A83: FF = (FF | n) ^ <*ff*> by RFINSEQ:20;
reconsider a = Product (FF | n), b = ff, m9 = m as Integer ;
A84: n <= n + 1 by NAT_1:11;
0 + 1 <= n + 1 by XREAL_1:8;
then ( (FX | (n + 1)) . (n + 1) = FX . (n + 1) & n + 1 in dom FX ) by A82, FINSEQ_3:27, FINSEQ_3:121;
then A85: (FX | (n + 1)) . (n + 1) in rng FX by FUNCT_1:def 5;
rng FX = X by A34, FINSEQ_1:def 13;
then A86: ex p being Element of NAT st
( ff = p & m,p are_relative_prime & p >= 1 & p <= m ) by A85;
assume S₁[n] ; :: thesis: S₁[n + 1]
then a,m9 are_relative_prime by A82, A84, FINSEQ_5:80, XXREAL_0:2;
then a * b,m9 are_relative_prime by A86, INT_2:41;
hence S₁[n + 1] by A83, RVSUM_1:126; :: thesis: verum

end;

suppose len FX < n + 1 ; :: thesis: ( S₁[n] implies S₁[n + 1] )

hence ( S₁[n] implies S₁[n + 1] ) ; :: thesis: verum

end;

end;

end;

hence ( S₁[n] implies S₁[n + 1] ) ; :: thesis: verum

end;

(Product (FX | 0 )) gcd m = 1 by NEWTON:64, RVSUM_1:124;
then A87: S₁[ 0 ] by INT_2:def 4;
for n being Nat holds S₁[n] from NAT_1:sch 2(A87, A81);
hence Product FX,m are_relative_prime by A80; :: thesis: verum

end;

len FX = card X by A34, FINSEQ_3:44
.= Euler m by EULER_1:def 1 ;
then A88: len FY = Euler m by A61, RFINSEQ:16;
(Product FX) mod m = (Product FY) mod m by A61, Th25;
hence (a |^ (Euler m)) mod m = 1 by A2, A63, A88, A4, A79, Th27; :: thesis: verum