let a, m be Nat; :: thesis: ( a <> 0 & m > 1 & a,m are_coprime implies (a |^ (Euler m)) mod m = 1 )
assume that
A1: a <> 0 and
A2: m > 1 and
A3: a,m are_coprime ; :: thesis: (a |^ (Euler m)) mod m = 1
set X = { k where k is Element of NAT : ( m,k are_coprime & k >= 1 & k <= m ) } ;
A4: a |^ (Euler m) <> 0 by A1, PREPOWER:5;
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_coprime & k >= 1 & k <= m ) } ) } ;
A5: for x being Nat st x in { k where k is Element of NAT : ( m,k are_coprime & k >= 1 & k <= m ) } holds
(a * x) mod m in { k where k is Element of NAT : ( m,k are_coprime & k >= 1 & k <= m ) }

proof

let x be Nat; :: thesis: ( x in { k where k is Element of NAT : ( m,k are_coprime & k >= 1 & k <= m ) } implies (a * x) mod m in { k where k is Element of NAT : ( m,k are_coprime & k >= 1 & k <= m ) } )
assume x in { k where k is Element of NAT : ( m,k are_coprime & k >= 1 & k <= m ) } ; :: thesis: (a * x) mod m in { k where k is Element of NAT : ( m,k are_coprime & k >= 1 & k <= m ) }
then consider t being Element of NAT such that
A6: t = x and
A7: m,t are_coprime and
A8: t >= 1 and
t <= m ;
A9: a * t,m are_coprime by A1, A2, A3, A7, EULER_1:14;
(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:51;
then (m * s) gcd (m * 1) = m by EULER_1:5;
hence contradiction by A2, A9, A10; :: 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_coprime by A1, A2, A3, A7, A8, Th3;
hence (a * x) mod m in { k where k is Element of NAT : ( m,k are_coprime & k >= 1 & k <= m ) } by A6, A11, A12; :: thesis: verum

end;

A13: { k where k is Element of NAT : ( m,k are_coprime & 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_coprime & k >= 1 & k <= m ) } ) }

proof

thus { k where k is Element of NAT : ( m,k are_coprime & 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_coprime & 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_coprime & k >= 1 & k <= m ) } ) } c= { k where k is Element of NAT : ( m,k are_coprime & k >= 1 & k <= m ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : ( m,k are_coprime & 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_coprime & k >= 1 & k <= m ) } ) } )
assume x in { k where k is Element of NAT : ( m,k are_coprime & 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_coprime & k >= 1 & k <= m ) } ) }
then consider xx being Element of NAT such that
A14: x = xx and
A15: m,xx are_coprime and
xx >= 1 and
A16: xx <= m ;
consider i, j being Integer such that
A17: (i * a) + (j * m) = xx by A3, EULER_1:10;
xx <> m by A2, A15, EULER_1:1;
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:3, NEWTON:64;
i mod m <> 0

proof

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

end;

then A19: im >= 1 by NAT_1:14;
A20: i = ((i div m) * m) + (i mod m) by A2, NEWTON:66;
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:65;
A22: ij mod m = (im * a) mod m by NAT_D:61;
then m,im are_coprime by A2, A15, A18, A17, A20, Th4;
then im in { k where k is Element of NAT : ( m,k are_coprime & 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_coprime & k >= 1 & k <= m ) } ) } by A14, A18, A17, A20, A22; :: thesis: verum

end;

let y be object ; :: 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_coprime & k >= 1 & k <= m ) } ) } or y in { k where k is Element of NAT : ( m,k are_coprime & 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_coprime & k >= 1 & k <= m ) } ) } ; :: thesis: y in { k where k is Element of NAT : ( m,k are_coprime & 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_coprime & k >= 1 & k <= m ) } ) ) ;
hence y in { k where k is Element of NAT : ( m,k are_coprime & 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_coprime & k >= 1 & k <= m ) } & xj in { k where k is Element of NAT : ( m,k are_coprime & 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_coprime & k >= 1 & k <= m ) } & xj in { k where k is Element of NAT : ( m,k are_coprime & 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_coprime & k >= 1 & k <= m ) } and
A25: xj in { k where k is Element of NAT : ( m,k are_coprime & 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_coprime and
A29: ( s >= 1 & s <= m ) by A25;
A30: (a * xj) mod m = (a * s) - (m * ((a * s) div m)) by A2, A28, NEWTON:63;
consider t being Element of NAT such that
A31: t = xi and
m,t are_coprime and
A32: ( t >= 1 & t <= m ) by A24;
(a * xi) mod m = (a * t) - (m * ((a * t) div m)) by A2, A31, NEWTON:63;
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 3;
reconsider m = m, c = t - s as Integer ;
( 1 - m <= c & c <= m - 1 ) by A32, A29, XREAL_1:13;
then t - s = 0 by A3, A33, Lm4, INT_2:25;
hence contradiction by A26, A31, A28; :: thesis: verum

end;

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

proof

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

end;

then reconsider X = { k where k is Element of NAT : ( m,k are_coprime & k >= 1 & k <= m ) } as finite set ;
a35: X is included_in_Seg by A35, FINSEQ_1:def 13;
dom FYY = Seg (len FYY) by FINSEQ_1:def 3
.= Seg (len FX) by NEWTON:2 ;
then A36: dom FX = dom FYY by FINSEQ_1:def 3;
A37: dom FY = Seg (len FY) by FINSEQ_1:def 3
.= Seg (len FYY) by Def2
.= Seg (len FX) by NEWTON:2 ;
then A38: dom FX = dom FY by FINSEQ_1:def 3;
A39: 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_coprime & 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_coprime & 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_coprime & k >= 1 & k <= m ) } ) } c= rng FY

proof

let x be object ; :: 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_coprime & 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_coprime & k >= 1 & k <= m ) } ) }
then consider y being object such that
A40: y in dom FY and
A41: x = FY . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A40;
FX . y in rng FX by A38, A40, FUNCT_1:def 3;
then A42: FX . y in X by a35, FINSEQ_1:def 14;
y in dom FX by A37, A40, FINSEQ_1:def 3;
then FY . y = (FYY . y) mod m by A36, Def1
.= (a * (FX . y)) mod m by RVSUM_1:44 ;
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_coprime & k >= 1 & k <= m ) } ) } by A41, A42; :: thesis: verum

end;

let y be object ; :: 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_coprime & 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_coprime & k >= 1 & k <= m ) } ) } ; :: thesis: y in rng FY
then consider yy being Element of NAT such that
A43: y = yy and
A44: ex u being Element of NAT st
( yy = (a * u) mod m & u in X ) ;
consider uu being Element of NAT such that
A45: yy = (a * uu) mod m and
A46: uu in X by A44;
uu in rng FX by a35, A46, FINSEQ_1:def 14;
then consider xx being object such that
A47: xx in dom FX and
A48: uu = FX . xx by FUNCT_1:def 3;
reconsider xx = xx as Element of NAT by A47;
FY . xx = (FYY . xx) mod m by A36, A47, Def1
.= y by A43, A45, A48, RVSUM_1:44 ;
hence y in rng FY by A38, A47, FUNCT_1:def 3; :: thesis: verum

end;

A49: FY is one-to-one

proof

A50: FX is one-to-one by a35, FINSEQ_3:92;
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom FY or not x2 in dom FY or not FY . x1 = FY . x2 or x1 = x2 )
assume that
A51: x1 in dom FY and
A52: x2 in dom FY and
A53: FY . x1 = FY . x2 ; :: thesis: x1 = x2
A54: x2 in dom FX by A37, A52, FINSEQ_1:def 3;
reconsider x2 = x2 as Element of NAT by A52;
A55: x1 in dom FX by A37, A51, FINSEQ_1:def 3;
reconsider x1 = x1 as Element of NAT by A51;
A56: ( FX . x1 in rng FX & FX . x2 in rng FX ) by A38, A51, A52, FUNCT_1:def 3;
A57: FY . x2 = (FYY . x2) mod m by A36, A54, Def1
.= (a * (FX . x2)) mod m by RVSUM_1:44 ;
FY . x1 = (FYY . x1) mod m by A36, A55, Def1
.= (a * (FX . x1)) mod m by RVSUM_1:44 ;
then ( not FX . x1 in X or not FX . x2 in X or not FX . x1 <> FX . x2 ) by A23, A53, A57;
hence x1 = x2 by a35, A55, A54, A56, A50, FINSEQ_1:def 14; :: thesis: verum

end;

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

proof

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

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

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

A59: FX is one-to-one by a35, FINSEQ_3:92;
x in rng FX by a35, A58, FINSEQ_1:def 14;
then A60: len (FX - {x}) = (len FX) - 1 by A59, FINSEQ_3:90;
A61: ( (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:59;
len (FY - {x}) = (len FY) - 1 by A13, A39, A49, A58, FINSEQ_3:90;
hence card (Coim (FX,x)) = card (Coim (FY,x)) by A60, A61; :: 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, a35, A39, FINSEQ_1:def 14, FUNCT_1:72;
hence card (Coim (FX,x)) = card (Coim (FY,x)) by FUNCT_1:72; :: thesis: verum

end;

end;

end;

then A62: FX,FY are_fiberwise_equipotent by CLASSES1:def 10;
then A63: len FX = len FY by RFINSEQ:3;
A64: (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 16;
then A65: FY = FY | (len FY) by FINSEQ_2:20;
A66: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

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

now :: thesis: ( S₁[n] implies S₁[n + 1] )

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

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

then len (FX | (n + 1)) = n + 1 by A63, FINSEQ_1:59;
then A68: FX | (n + 1) = ((FX | (n + 1)) | n) ^ <*((FX | (n + 1)) . (n + 1))*> by RFINSEQ:7;
assume A69: S₁[n] ; :: thesis: S₁[n + 1]
0 + 1 <= n + 1 by NAT_1:13;
then A70: n + 1 in dom FY by A67, FINSEQ_3:25;
A71: (FY | (n + 1)) . (n + 1) = FY . (n + 1) by FINSEQ_3:112;
A72: (FX | (n + 1)) . (n + 1) = FX . (n + 1) by FINSEQ_3:112;
A73: n <= n + 1 by NAT_1:11;
then A74: len (FY | n) = n by A67, FINSEQ_1:59, XXREAL_0:2;
A75: (FX | (n + 1)) | n = FX | n by A73, FINSEQ_5:77;
A76: (FY | (n + 1)) | n = FY | n by A73, FINSEQ_5:77;
A77: len (FY | (n + 1)) = n + 1 by A67, FINSEQ_1:59;
then FY | (n + 1) = ((FY | (n + 1)) | n) ^ <*((FY | (n + 1)) . (n + 1))*> by RFINSEQ:7;
then (Product (FY | (n + 1))) mod m = ((Product (FY | n)) * (FY . (n + 1))) mod m by A76, A71, RVSUM_1:96
.= ((((a |^ (len (FY | n))) * (Product (FX | n))) mod m) * ((FY . (n + 1)) mod m)) mod m by A67, A69, A73, NAT_D:67, XXREAL_0:2
.= ((((a |^ (len (FY | n))) * (Product (FX | n))) mod m) * (((FYY . (n + 1)) mod m) mod m)) mod m by A38, A36, A70, Def1
.= ((((a |^ (len (FY | n))) * (Product (FX | n))) mod m) * (((a * FX) . (n + 1)) mod m)) mod m by NAT_D:73
.= (((a |^ (len (FY | n))) * (Product (FX | n))) * ((a * FX) . (n + 1))) mod m by NAT_D:67
.= (((a |^ n) * (Product (FX | n))) * (a * (FX . (n + 1)))) mod m by A74, RVSUM_1:44
.= (((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 A77, NEWTON:6
.= ((a |^ (len (FY | (n + 1)))) * (Product (FX | (n + 1)))) mod m by A68, A75, A72, RVSUM_1:96 ;
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 16;
then A78: FX = FX | (len FY) by A63, FINSEQ_2:20;
A79: S₁[ 0 ] by NEWTON:4, RVSUM_1:94;
for n being Nat holds S₁[n] from NAT_1:sch 2(A79, A66);
hence (Product FY) mod m = ((a |^ (len FY)) * (Product FX)) mod m by A65, A78; :: thesis: verum

end;

A80: Product FX,m are_coprime

proof

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

proof

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

now :: thesis: ( S₁[n] implies S₁[n + 1] )

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

suppose A83: 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 A83, FINSEQ_1:59;
then A84: FF = (FF | n) ^ <*ff*> by RFINSEQ:7;
reconsider a = Product (FF | n), b = ff, m9 = m as Integer ;
A85: n <= n + 1 by NAT_1:11;
0 + 1 <= n + 1 by XREAL_1:6;
then ( (FX | (n + 1)) . (n + 1) = FX . (n + 1) & n + 1 in dom FX ) by A83, FINSEQ_3:25, FINSEQ_3:112;
then A86: (FX | (n + 1)) . (n + 1) in rng FX by FUNCT_1:def 3;
rng FX = X by a35, FINSEQ_1:def 14;
then A87: ex p being Element of NAT st
( ff = p & m,p are_coprime & p >= 1 & p <= m ) by A86;
assume S₁[n] ; :: thesis: S₁[n + 1]
then a,m9 are_coprime by A83, A85, FINSEQ_5:77, XXREAL_0:2;
then a * b,m9 are_coprime by A87, INT_2:26;
hence S₁[n + 1] by A84, RVSUM_1:96; :: 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:51, RVSUM_1:94;
then A88: S₁[ 0 ] by INT_2:def 3;
for n being Nat holds S₁[n] from NAT_1:sch 2(A88, A82);
hence Product FX,m are_coprime by A81; :: thesis: verum

end;

len FX = card X by a35, FINSEQ_3:39
.= Euler m by EULER_1:def 1 ;
then A89: len FY = Euler m by A62, RFINSEQ:3;
(Product FX) mod m = (Product FY) mod m by A62, Th10;
hence (a |^ (Euler m)) mod m = 1 by A2, A4, A64, A89, A80, Th12; :: thesis: verum