let a, m be Nat; :: thesis: ( a <> 0 & m > 1 & a,m are_relative_prime implies (a |^ (Euler m)) mod m = 1 )
assume A1: ( a <> 0 & m > 1 & 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 ) } ;
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 ) } ) } ;
A2: 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
A3: t = x and
A4: m,t are_relative_prime and
A5: ( t >= 1 & t <= m ) ;
A6: a * t,m are_relative_prime by A1, A4, A5, EULER_1:15;
A7: m,(a * t) mod m are_relative_prime by A1, A4, A5, Th5;
(a * t) mod m <> 0

proof

assume (a * t) mod m = 0 ; :: thesis: contradiction
then consider s being Nat such that
A8: a * t = (m * s) + 0 and
0 < m by A1, 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 A1, A6, A8, INT_2:def 4; :: thesis: verum

end;

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

end;

A10: 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 A11: ( 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 ) ; :: thesis: (a * xi) mod m <> (a * xj) mod m
assume A12: (a * xi) mod m = (a * xj) mod m ; :: thesis: contradiction
set tm = (a * xi) mod m;
set sm = (a * xj) mod m;
consider t being Element of NAT such that
A13: t = xi and
m,t are_relative_prime and
A14: ( t >= 1 & t <= m ) by A11;
A15: (a * xi) mod m = (a * t) - (m * ((a * t) div m)) by A1, A13, NEWTON:77;
consider s being Element of NAT such that
A16: s = xj and
m,s are_relative_prime and
A17: ( s >= 1 & s <= m ) by A11;
(a * xj) mod m = (a * s) - (m * ((a * s) div m)) by A1, A16, NEWTON:77;
then 0 = (a * (t - s)) - (m * (((a * t) div m) - ((a * s) div m))) by A12, A15;
then A18: 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 A14, A17, XREAL_1:15;
then t - s = 0 by A1, A18, Lm4, INT_2:40;
hence contradiction by A11, A13, A16; :: thesis: verum

end;

A19: { 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
A20: x = xx and
A21: m,xx are_relative_prime and
A22: ( xx >= 1 & xx <= m ) ;
xx <> m by A1, A21, EULER_1:2;
then xx < m by A22, XXREAL_0:1;
then A23: xx mod m = xx by NAT_D:24;
consider i, j being Integer such that
A24: (i * a) + (j * m) = xx by A1, EULER_1:11;
A25: i = ((i div m) * m) + (i mod m) by A1, NEWTON:80;
A26: i mod m <> 0

proof

assume i mod m = 0 ; :: thesis: contradiction
then A27: 0 = i - ((i div m) * m) by A1, INT_1:def 8;
then xx = m * (((i div m) * a) + j) by A24;
then A28: ( ((i div m) * a) + j <> 0 & 1 <> 0 ) by A22;
m gcd xx = (m * 1) gcd (m * (((i div m) * a) + j)) by A24, A27
.= m * (1 gcd (((i div m) * a) + j)) by A1, A28, EULER_1:16
.= m * 1 by Lm3
.= m ;
hence contradiction by A1, A21, INT_2:def 4; :: thesis: verum

end;

reconsider im = i mod m as Element of NAT by INT_1:16, NEWTON:78;
A29: im >= 1 by A26, NAT_1:14;
A30: im <= m by A1, NEWTON:79;
reconsider ij = ((i mod m) * a) + ((((i div m) * a) + j) * m) as Element of NAT by A24, A25;
A31: ij mod m = (im * a) mod m by EULER_1:13;
then m,im are_relative_prime by A1, A21, A23, A24, A25, A26, Th6;
then im in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } by A29, A30;
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 A20, A23, A24, A25, A31; :: 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 consider yy being Element of NAT such that
A32: y = yy and
A33: 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 ) } ) ;
consider uu being Element of NAT such that
A34: yy = (a * uu) mod m and
A35: uu in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } by A33;
thus y in { k where k is Element of NAT : ( m,k are_relative_prime & k >= 1 & k <= m ) } by A2, A32, A34, A35; :: 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 ;
A36: { 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 consider xx being Element of NAT such that
A37: x = xx and
m,xx are_relative_prime and
A38: ( xx >= 1 & xx <= m ) ;
thus x in Seg m by A37, A38, 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 ;
A39: len FX = card X by A36, FINSEQ_3:44
.= Euler m by EULER_1:def 1 ;
A40: dom FY = Seg (len FY) by FINSEQ_1:def 3
.= Seg (len FYY) by Def1
.= Seg (len FX) by NEWTON:6 ;
then A41: dom FX = dom FY by FINSEQ_1:def 3;
dom FYY = Seg (len FYY) by FINSEQ_1:def 3
.= Seg (len FX) by NEWTON:6 ;
then A42: dom FX = dom FYY by FINSEQ_1:def 3;
A43: 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
A44: ( y in dom FY & x = FY . y ) by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A44;
y in dom FX by A40, A44, FINSEQ_1:def 3;
then A45: FY . y = (FYY . y) mod m by A42, Def1
.= (a * (FX . y)) mod m by RVSUM_1:66 ;
FX . y in rng FX by A41, A44, FUNCT_1:def 5;
then FX . y in X by A36, FINSEQ_1:def 13;
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 A44, A45; :: 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
A46: y = yy and
A47: ex u being Element of NAT st
( yy = (a * u) mod m & u in X ) ;
consider uu being Element of NAT such that
A48: yy = (a * uu) mod m and
A49: uu in X by A47;
uu in rng FX by A36, A49, FINSEQ_1:def 13;
then consider xx being set such that
A50: ( xx in dom FX & uu = FX . xx ) by FUNCT_1:def 5;
reconsider xx = xx as Element of NAT by A50;
FY . xx = (FYY . xx) mod m by A42, A50, Def1
.= y by A46, A48, A50, RVSUM_1:66 ;
hence y in rng FY by A41, A50, FUNCT_1:def 5; :: thesis: verum

end;

A51: FY is one-to-one

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom FY or not x2 in dom FY or not FY . x1 = FY . x2 or x1 = x2 )
assume A52: ( x1 in dom FY & x2 in dom FY & FY . x1 = FY . x2 ) ; :: thesis: x1 = x2
then A53: ( x1 in dom FX & x2 in dom FX & FY . x1 = FY . x2 ) by A40, FINSEQ_1:def 3;
reconsider x1 = x1 as Element of NAT by A52;
reconsider x2 = x2 as Element of NAT by A52;
A54: FY . x1 = (FYY . x1) mod m by A42, A53, Def1
.= (a * (FX . x1)) mod m by RVSUM_1:66 ;
A55: FY . x2 = (FYY . x2) mod m by A42, A53, Def1
.= (a * (FX . x2)) mod m by RVSUM_1:66 ;
A56: FX . x1 in rng FX by A41, A52, FUNCT_1:def 5;
A57: FX . x2 in rng FX by A41, A52, FUNCT_1:def 5;
A58: FX is one-to-one by A36, FINSEQ_3:99;
( not FX . x1 in X or not FX . x2 in X or not FX . x1 <> FX . x2 ) by A10, A52, A54, A55;
hence x1 = x2 by A36, A53, A56, A57, A58, 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 A59: x in X ; :: thesis: card (Coim FX,x) = card (Coim FY,x)

then A60: x in rng FX by A36, FINSEQ_1:def 13;
FX is one-to-one by A36, FINSEQ_3:99;
then A61: len (FX - {x}) = (len FX) - 1 by A60, FINSEQ_3:97;
A62: (len (FX - {x})) - (len (FX - {x})) = ((len FX) - (card (FX " {x}))) - (len (FX - {x})) by FINSEQ_3:66;
A63: len (FY - {x}) = (len FY) - 1 by A19, A43, A51, A59, FINSEQ_3:97;
len (FY - {x}) = (len FY) - (card (FY " {x})) by FINSEQ_3:66;
hence card (Coim FX,x) = card (Coim FY,x) by A61, A62, A63; :: thesis: verum

end;

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

then A65: not x in rng FX by A36, FINSEQ_1:def 13;
FY " {x} = {} by A19, A43, A64, FUNCT_1:142;
hence card (Coim FX,x) = card (Coim FY,x) by A65, FUNCT_1:142; :: thesis: verum

end;

end;

end;

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

end;

then A66: FX,FY are_fiberwise_equipotent by CLASSES1:def 9;
then A67: (Product FX) mod m = (Product FY) mod m by Th25;
A68: len FX = len FY by A66, RFINSEQ:16;
A69: (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 );
A70: S₁[ 0 ]

proof

0 <= len FY ;
then len (FY | 0 ) = 0 by FINSEQ_1:80;
hence S₁[ 0 ] by NEWTON:9, RVSUM_1:124; :: thesis: verum

end;

A71: 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 A72: n + 1 <= len FY ; :: thesis: ( S₁[n] implies S₁[n + 1] )

assume A73: S₁[n] ; :: thesis: S₁[n + 1]
A74: n <= n + 1 by NAT_1:11;
then A75: len (FY | n) = n by A72, FINSEQ_1:80, XXREAL_0:2;
A76: len (FY | (n + 1)) = n + 1 by A72, FINSEQ_1:80;
then A77: FY | (n + 1) = ((FY | (n + 1)) | n) ^ <*((FY | (n + 1)) . (n + 1))*> by RFINSEQ:20;
0 + 1 <= n + 1 by NAT_1:13;
then A78: n + 1 in dom FY by A72, FINSEQ_3:27;
A79: (FY | (n + 1)) | n = FY | n by A74, FINSEQ_5:80;
A80: (FY | (n + 1)) . (n + 1) = FY . (n + 1) by FINSEQ_3:121;
len (FX | (n + 1)) = n + 1 by A68, A72, FINSEQ_1:80;
then A81: FX | (n + 1) = ((FX | (n + 1)) | n) ^ <*((FX | (n + 1)) . (n + 1))*> by RFINSEQ:20;
A82: (FX | (n + 1)) | n = FX | n by A74, FINSEQ_5:80;
A83: (FX | (n + 1)) . (n + 1) = FX . (n + 1) by FINSEQ_3:121;
(Product (FY | (n + 1))) mod m = ((Product (FY | n)) * (FY . (n + 1))) mod m by A77, A79, A80, RVSUM_1:126
.= ((((a |^ (len (FY | n))) * (Product (FX | n))) mod m) * ((FY . (n + 1)) mod m)) mod m by A72, A73, A74, Th11, XXREAL_0:2
.= ((((a |^ (len (FY | n))) * (Product (FX | n))) mod m) * (((FYY . (n + 1)) mod m) mod m)) mod m by A41, A42, A78, 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 A75, 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 A81, A82, A83, 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;

A84: for n being Nat holds S₁[n] from NAT_1:sch 2(A70, A71);
FY | (len FY) = FY | (Seg (len FY)) by FINSEQ_1:def 15;
then A85: FY = FY | (len FY) by FINSEQ_2:23;
FX | (len FX) = FX | (Seg (len FX)) by FINSEQ_1:def 15;
then FX = FX | (len FY) by A68, FINSEQ_2:23;
hence (Product FY) mod m = ((a |^ (len FY)) * (Product FX)) mod m by A84, A85; :: thesis: verum

end;

A86: len FY = Euler m by A39, A66, RFINSEQ:16;
A87: a |^ (Euler m) <> 0 by A1, PREPOWER:12;
A88: Product FX <> 0

proof

assume Product FX = 0 ; :: thesis: contradiction
then consider k being Nat such that
A89: k in dom FX and
A90: FX . k = 0 by RVSUM_1:133;
A91: rng FX = X by A36, FINSEQ_1:def 13;
FX . k in rng FX by A89, FUNCT_1:def 5;
then consider p being Element of NAT such that
A92: FX . k = p and
m,p are_relative_prime and
A93: ( p >= 1 & p <= m ) by A91;
thus contradiction by A90, A92, A93; :: thesis: verum

end;

Product FX,m are_relative_prime

proof

defpred S₁[ Nat] means ( $1 <= len FX implies Product (FX | $1),m are_relative_prime );
A94: S₁[ 0 ]

proof

(Product (FX | 0 )) gcd m = 1 by NEWTON:64, RVSUM_1:124;
hence S₁[ 0 ] by INT_2:def 4; :: thesis: verum

end;

A95: 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 A96: len FX >= n + 1 ; :: thesis: ( S₁[n] implies S₁[n + 1] )

assume A97: S₁[n] ; :: thesis: S₁[n + 1]
A98: n <= n + 1 by NAT_1:11;
reconsider FF = FX | (n + 1) as FinSequence of NAT ;
reconsider ff = FF . (n + 1) as Element of NAT ;
len FF = n + 1 by A96, FINSEQ_1:80;
then A99: FF = (FF | n) ^ <*ff*> by RFINSEQ:20;
A100: rng FX = X by A36, FINSEQ_1:def 13;
A101: (FX | (n + 1)) . (n + 1) = FX . (n + 1) by FINSEQ_3:121;
0 + 1 <= n + 1 by XREAL_1:8;
then n + 1 in dom FX by A96, FINSEQ_3:27;
then (FX | (n + 1)) . (n + 1) in rng FX by A101, FUNCT_1:def 5;
then consider p being Element of NAT such that
A102: ff = p and
A103: m,p are_relative_prime and
( p >= 1 & p <= m ) by A100;
reconsider a = Product (FF | n), b = ff, m' = m as Integer ;
a,m' are_relative_prime by A96, A97, A98, FINSEQ_5:80, XXREAL_0:2;
then a * b,m' are_relative_prime by A102, A103, INT_2:41;
hence S₁[n + 1] by A99, 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;

A104: for n being Nat holds S₁[n] from NAT_1:sch 2(A94, A95);
FX | (len FX) = FX by FINSEQ_1:79;
hence Product FX,m are_relative_prime by A104; :: thesis: verum

end;

hence (a |^ (Euler m)) mod m = 1 by A1, A67, A69, A86, A87, A88, Th27; :: thesis: verum