:: Euler's {T}heorem and Small {F}ermat's Theorem
:: by Yoshinori Fujisawa , Yasushi Fuwa and Hidetaka Shimizu
::
:: Received June 10, 1998
:: Copyright (c) 1998-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, INT_1, FINSEQ_1, ARYTM_3, XXREAL_0, CARD_1,
SUBSET_1, ARYTM_1, INT_2, COMPLEX1, RELAT_1, TARSKI, FUNCT_1, CLASSES1,
CARD_3, ORDINAL4, RFINSEQ, XBOOLE_0, NEWTON, EULER_1, FINSET_1,
VALUED_0, VALUED_1, ORDINAL1, NUMBER09;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
CARD_1, RELAT_1, FUNCT_1, RECDEF_1, INT_1, INT_2, FINSET_1, NAT_1, NAT_D,
VALUED_0, VALUED_1,
NEWTON, EULER_1, CLASSES1, RFINSEQ, FINSEQ_1, FINSEQ_3, RVSUM_1, TREES_4;
constructors REAL_1, SQUARE_1, NAT_1, NAT_D, NEWTON, RFINSEQ, WSIERP_1,
EULER_1, RECDEF_1, CLASSES1, BINOP_2, RELSET_1, NUMBERS, FUNCT_4;
registrations FUNCT_1, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1,
FINSEQ_1, NEWTON, VALUED_0, FINSET_1, CARD_1, WSIERP_1, SEQM_3, RVSUM_1,
VALUED_1, XCMPLX_0;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, FUNCT_1, XBOOLE_0, VALUED_0, INT_2;
equalities RELAT_1;
expansions FUNCT_1, INT_2;
theorems INT_2, FINSEQ_1, NAT_1, ABSVALUE, INT_1, FUNCT_1, EULER_1, PREPOWER,
RFINSEQ, FINSEQ_2, RVSUM_1, FINSEQ_3, NEWTON, RELAT_1, XBOOLE_1,
XREAL_1, FINSEQ_5, XXREAL_0, ORDINAL1, NAT_D, CLASSES1,
VALUED_0, VALUED_1, WSIERP_1;
schemes NAT_1, FUNCT_1;
begin :: Preliminary
reserve a,b,m,x,n,l,xi,xj for Nat,
t,z for Integer;
Lm1: t < 1 iff t <= 0
proof
thus t < 1 implies t <= 0
proof
assume
A1: t < 1;
assume
A2: t > 0;
then reconsider t as Element of NAT by INT_1:3;
t >= 1 by A2,NAT_1:14;
hence contradiction by A1;
end;
thus thesis;
end;
Lm2: for a be natural Number holds a <> 0 implies a-1 >= 0
proof
let a be natural Number;
assume a <> 0;
then a-1 >= 1-1 by XREAL_1:9,NAT_1:14;
hence thesis;
end;
Lm3: 1 gcd z = 1
proof
thus 1 gcd z = |.1.| gcd |.z.| by INT_2:34
.= 1 gcd |.z.| by ABSVALUE:def 1
.= 1 by NEWTON:51;
end;
:: Very useful theorem
::
::$CT
theorem Th2:
m*t >= 1 implies t >= 1
proof
assume
A1: m*t >= 1;
assume t < 1;
then t <= 0 by Lm1;
hence contradiction by A1;
end;
Lm4: 1-m <= z & z <= m-1 & m divides z implies z = 0
proof
assume that
A1: 1-m <= z and
A2: z <= m-1 and
A3: m divides z;
consider t being Integer such that
A4: z = m*t by A3,INT_1:def 3;
assume
A5: z <> 0;
now
per cases by A5,A4;
suppose
A6: t > 0;
then reconsider t as Element of NAT by INT_1:3;
m*t >= m by A6,NAT_1:14,NEWTON:33;
then m*t+1 > m by NAT_1:13;
hence contradiction by A2,A4,XREAL_1:19;
end;
suppose
A7: t < 0;
reconsider r = (t+1) as Integer;
1 <= m*t+m*1 by A1,A4,XREAL_1:20;
then 1 <= m*(t+1);
then 1-1 <= t by Th2,XREAL_1:20;
hence contradiction by A7;
end;
end;
hence contradiction;
end;
theorem Th3:
a <> 0 & b <> 0 & m <> 0 & a,m are_coprime & b,m are_coprime implies
m,a*b mod m are_coprime
proof
assume that
A1: a <> 0 and
A2: b <> 0 and
A3: m <> 0 and
A4: a,m are_coprime & b,m are_coprime;
a*b,m are_coprime by A1,A3,A4,EULER_1:14;
then
A5: a*b gcd m = 1;
consider t being Nat such that
A6: a*b = m*t+(a*b mod m) and
(a*b mod m) < m by A3,NAT_D:def 2;
a*b <> a*0 by A1,A2;
then a*b+(-t)*m gcd m = a*b gcd m by EULER_1:16;
hence thesis by A6,A5;
end;
theorem Th4:
m > 1 & m,n are_coprime & n = a*b mod m implies m,b are_coprime
proof
assume that
A1: m > 1 and
A2: m,n are_coprime and
A3: n = a*b mod m;
set k = m gcd b;
k divides m by NAT_D:def 5;
then consider km being Nat such that
A4: m = k*km by NAT_D:def 3;
A5: k <> 0 & km <> 0 by A1,A4;
reconsider km as Element of NAT by ORDINAL1:def 12;
k divides b by NAT_D:def 5;
then consider kb being Nat such that
A6: b = k*kb by NAT_D:def 3;
consider p being Nat such that
A7: a*(k*kb) = (k*km)*p+(a*(k*kb) mod (k*km)) and
(a*(k*kb) mod (k*km)) < k*km by A1,A4,NAT_D:def 2;
set tm = (a*kb)-(km*p);
A8: (a*(k*kb) mod (k*km)) = k*((a*kb)-(km*p)) by A7;
assume not m,b are_coprime;
then
A9: m gcd b <> 1;
A11: tm <> 0 implies m gcd n <> 1
proof
assume tm <> 0;
m gcd n = k*(km gcd tm) by A3,A4,A5,A6,A8,EULER_1:15;
hence thesis by A9,INT_1:9;
end;
tm = 0 implies m gcd n <> 1 by A1,A3,A4,A6,A8,NEWTON:52;
hence contradiction by A2,A11;
end;
::$CT 2
theorem Th7:
for l,m,n being Integer holds (l*m) mod n = (l*(m mod n)) mod n
proof
let l,m,n be Integer;
thus (l*(m mod n)) mod n = ((l mod n)*((m mod n)mod n)) mod n by NAT_D:67
.= ((l mod n)*(m mod n)) mod n by NAT_D:73
.= (l*m) mod n by NAT_D:67;
end;
theorem
for l,m,n being Integer holds
(l*m) mod n = ((l mod n)*m) mod n by Th7;
::$CT
begin :: Function of Element of NAT*(FinSequence of NAT)
definition
let f be FinSequence of NAT;
let a be Nat;
redefine func a*f -> FinSequence of NAT; :: redefines * (RVSUM_1, synonym) → (#) (VALUED_1, definition)
coherence
proof
rng(a*f) c= NAT
proof
let x be object;
assume x in rng (a*f);
then ex xx being object st xx in dom (a*f) &
x = (a*f).xx by FUNCT_1:def 3;
hence thesis by ORDINAL1:def 12;
end;
hence thesis by FINSEQ_1:def 4;
end;
end;
theorem Th10:
for R1,R2 be complex-valued FinSequence st
R1,R2 are_fiberwise_equipotent holds Product R1 = Product R2
proof
let R1,R2 be complex-valued FinSequence;
rng R1 c= COMPLEX & rng R2 c= COMPLEX by VALUED_0:def 1;
then
A0: R1 is FinSequence of COMPLEX & R2 is FinSequence of COMPLEX
by FINSEQ_1:def 4;
defpred P[Nat] means for f,g be FinSequence of COMPLEX st f,g
are_fiberwise_equipotent & len f = $1 holds Product f = Product g;
A1: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
let f,g be FinSequence of COMPLEX;
assume that
A3: f,g are_fiberwise_equipotent and
A4: len f = n+1;
set a = f.(n+1);
A5: rng f = rng g by A3,CLASSES1:75;
set fn = f|n;
A6: f = fn ^ <*a*> by A4,RFINSEQ:7;
0+1<=n+1 by NAT_1:13;
then n+1 in dom f by A4,FINSEQ_3:25;
then a in rng g by A5,FUNCT_1:def 3;
then consider m being Nat such that
A7: m in dom g and
A8: g.m = a by FINSEQ_2:10;
reconsider m as Element of NAT by ORDINAL1:def 12;
set gg = g/^m, gm = g|m;
m<=len g by A7,FINSEQ_3:25;
then
A9: len gm = m by FINSEQ_1:59;
A10: 1<=m by A7,FINSEQ_3:25;
then max(0,m-1) = m-1 by FINSEQ_2:4;
then reconsider m1 = m-1 as Element of NAT by FINSEQ_2:5;
A11: m = m1+1;
then m1<=m by NAT_1:11;
then
A12: Seg m1 c= Seg m by FINSEQ_1:5;
m in Seg m by A10,FINSEQ_1:1;
then gm.m = a by A7,A8,RFINSEQ:6;
then
A13: gm = (gm|m1)^<*a*> by A9,A11,RFINSEQ:7;
A14: g = (g|m)^(g/^m) by RFINSEQ:8;
A15: gm|m1 = gm|(Seg m1) by FINSEQ_1:def 16
.= (g|(Seg m))|(Seg m1) by FINSEQ_1:def 16
.= g|((Seg m)/\(Seg m1)) by RELAT_1:71
.= g|(Seg m1) by A12,XBOOLE_1:28
.= g|m1 by FINSEQ_1:def 16;
now
let x be object;
card Coim(f,x) = card Coim(g,x) by A3,CLASSES1:def 10;
then card(fn"{x})+card(<*a*>"{x}) = card(((g|m1)^<*a*>^(g/^m))"{x}) by
A14,A13,A15,A6,FINSEQ_3:57
.= card(((g|m1)^<*a*>)"{x})+card((g/^m)"{x}) by FINSEQ_3:57
.= card((g|m1)"{x})+card(<*a*>"{x})+card((g/^m)"{x}) by FINSEQ_3:57
.= card((g|m1)"{x})+card((g/^m)"{x})+card(<*a*>"{x})
.= card(((g|m1)^(g/^m))"{x})+card(<*a*>"{x}) by FINSEQ_3:57;
hence card Coim(fn,x) = card Coim((g|m1)^(g/^m),x);
end;
then
A16: fn, (g|m1)^(g/^m) are_fiberwise_equipotent by CLASSES1:def 10;
len fn = n by A4,FINSEQ_1:59,NAT_1:11;
then Product fn = Product((g|m1)^gg) by A2,A16;
hence Product f = Product(g|m1^gg)*Product <*a*> by A6,RVSUM_1:97
.= Product (g|m1)*(Product gg)*(Product <*a*>) by RVSUM_1:97
.= Product(g|m1)*Product <*a*>*Product gg
.= Product gm*Product gg by A13,A15,RVSUM_1:97
.= Product g by A14,RVSUM_1:97;
end;
assume
A17: R1,R2 are_fiberwise_equipotent;
A18: len R1 = len R1;
A19: P[0]
proof
let f,g be FinSequence of COMPLEX;
assume f,g are_fiberwise_equipotent & len f = 0;
then
A20: len g = 0 & f = <*>NAT by RFINSEQ:3;
then g = <*>NAT;
hence thesis by A20;
end;
for n holds P[n] from NAT_1:sch 2(A19,A1);
hence thesis by A0,A17,A18;
end;
begin :: Modulus for Finite Sequence of Natural
:: Function of (FinSequence of NAT) mod Element of NAT
definition
let f be integer-valued Function, m be Integer;
func f mod m -> Function means
:Def1:
dom(it) = dom(f) & for i being object st i in dom f holds it.i = (f.i) mod m;
existence
proof
deffunc F(object) = (f.$1) mod m;
consider g being Function such that
A1: dom g = dom f and
A2: for x being object st x in dom f holds g.x = F(x) from FUNCT_1:sch 3;
take g;
thus thesis by A1,A2;
end;
uniqueness
proof
let fa,fb be Function such that
A5: dom(f) = dom(fa) and
A6: for i being object st i in dom f holds fa.i = (f.i) mod m and
A7: dom(f) = dom(fb) and
A8: for i being object st i in dom f holds fb.i = (f.i) mod m;
now
let X be set such that
A9: dom f = X;
for i being object st i in X holds fa.i = fb.i
proof
given j being object such that
A11: j in X and
A12: fa.j <> fb.j;
fa.j <> (f.j) mod m by A8,A9,A11,A12;
hence contradiction by A6,A9,A11;
end;
hence thesis by A5,A7,A9;
end;
hence thesis;
end;
end;
registration
let f be integer-valued FinSequence, m be Integer;
cluster f mod m -> FinSequence-like;
coherence
proof
dom (f mod m) = dom f by Def1;
then ex n st dom (f mod m) = Seg n by FINSEQ_1:def 2;
hence thesis by FINSEQ_1:def 2;
end;
end;
registration
let f be integer-valued Function, m be Integer;
cluster f mod m -> integer-valued;
coherence
proof
set g = f mod m;
let y be object;
assume
A1: y in dom g;
dom g = dom f by Def1;
then g.y = (f.y) mod m by A1,Def1;
hence thesis;
end;
end;
registration
let f be natural-valued Function, m be Nat;
cluster f mod m -> natural-valued;
coherence
proof
set g = f mod m;
let x be object such that
A1: x in dom g;
dom g = dom f by Def1;
then g.x = (f.x) mod m by A1,Def1;
hence thesis;
end;
end;
definition
let f be integer-valued FinSequence, m be Nat;
redefine func f mod m -> FinSequence of INT means :Def2: :: redefines mod (EULER_2, definition)
len(it) = len(f) & for i being object st i in dom f holds it.i = (f.i) mod m;
coherence
proof
rng (f mod m) c= INT by RELAT_1:def 19;
hence thesis by FINSEQ_1:def 4;
end;
compatibility
proof
let F be FinSequence of INT;
thus F = f mod m implies
len(F) = len(f) & for i being object st i in dom f holds F.i = (f.i) mod m
proof
assume
A1: F = f mod m;
then dom(F) = dom(f) by Def1;
hence thesis by A1,Def1,FINSEQ_3:29;
end;
thus thesis by Def1,FINSEQ_3:29;
end;
end;
theorem
for f be integer-valued FinSequence st m <> 0 holds
(Product(f mod m)) mod m = (Product f) mod m
proof
defpred P[Nat] means
for f be integer-valued FinSequence st m <> 0 & len f = $1
holds (Product(f mod m)) mod m = (Product f) mod m;
let f be integer-valued FinSequence;
assume
A1: m <> 0;
A2: len f is Element of NAT;
A3: for n st P[n] holds P[n+1]
proof
let n;
assume
A4: P[n];
let f be integer-valued FinSequence;
assume that
A5: m <> 0 and
A6: len f = n+1;
reconsider fn = f|n as integer-valued FinSequence;
A7: len fn = n by A6,FINSEQ_1:59,NAT_1:11;
A8: len (f mod m) = n+1 by A6,Def2;
then
A9: len((f mod m)|n) = n by FINSEQ_1:59,NAT_1:11;
A10: n <= len f by A6,NAT_1:11;
A11: for i being Nat st 1 <= i & i <= len ((f mod m)|n) holds
((f mod m)|n).i = (fn mod m).i
proof
let i be Nat;
assume that
A12: 1 <= i and
A13: i <= len ((f mod m)|n);
A14: (f|n).i = ((f|Seg n).i) by FINSEQ_1:def 16;
A15: i in Seg n by A9,A12,A13,FINSEQ_1:1;
then
A16: ((f mod m)|Seg n).i = (f mod m).i by FUNCT_1:49;
i <= len f by A10,A9,A13,XXREAL_0:2;
then
A17: i in dom f by A12,FINSEQ_3:25;
i in dom fn by A7,A9,A12,A13,FINSEQ_3:25;
then (fn mod m).i = fn.i mod m by Def1
.= f.i mod m by A15,A14,FUNCT_1:49
.= (f mod m).i by A17,Def1;
hence thesis by A16,FINSEQ_1:def 16;
end;
0+1<=n+1 by NAT_1:13;
then n+1 in dom f by A6,FINSEQ_3:25;
then
A18: (f mod m).(n+1) = f.(n+1) mod m by Def1;
reconsider F = fn mod m as integer-valued FinSequence;
len((f mod m)|n) = len(fn mod m) by A7,A9,Def2;
then (f mod m)|n = fn mod m by A11,FINSEQ_1:14;
then f mod m = (fn mod m) ^ <* f.(n+1) mod m *> by A8,A18,RFINSEQ:7;
then
A19: Product (f mod m) mod m = ((Product (fn mod m))*(f.(n+1) mod m)) mod
m by RVSUM_1:96
.= (((Product (fn mod m)) mod m)*((f.(n+1) mod m) mod m)) mod m
by NAT_D:67
.= (((Product fn) mod m)*((f.(n+1) mod m) mod m)) mod m by A4,A5,A7
.= (((Product fn) mod m)*(f.(n+1) mod m)) mod m by NAT_D:73;
(Product f) mod m = (Product (fn^<* f.(n+1) *>)) mod m by A6,RFINSEQ:7
.= ((Product fn)*f.(n+1)) mod m by RVSUM_1:96;
hence thesis by A19,NAT_D:67;
end;
A20: P[0]
proof
let f be integer-valued FinSequence;
assume that
m <> 0 and
A21: len f=0;
A22: f = <*> NAT & len (f mod m) = 0 by A21,Def2;
then f mod m = <*> NAT;
hence thesis by A22;
end;
for n holds P[n] from NAT_1:sch 2(A20,A3);
hence thesis by A1,A2;
end;
theorem Th12:
for a,m,n being natural Number holds
a <> 0 & m > 1 & a*n mod m = n mod m & m,n are_coprime
implies a mod m = 1
proof
let a,m,n be natural Number;
assume that
A1: a <> 0 and
A2: m > 1 and
A3: a*n mod m = n mod m and
A4: m,n are_coprime;
consider k2 be Nat such that
A5: n = m*k2+(n mod m) and
n mod m < m by A2,NAT_D:def 2;
consider k1 be Nat such that
A6: a*n = m*k1+(a*n mod m) and
(a*n mod m) < m by A2,NAT_D:def 2;
(a-1)*n = m*(k1-k2) by A3,A6,A5;
then
A7: m divides (a-1)*n by INT_1:def 3;
reconsider t = (a-1),m as Integer;
m divides t by A4,A7,INT_2:25;
then consider tt be Integer such that
A8: (a-1) = m*tt by INT_1:def 3;
a-1 >= 0 by A1,Lm2;
then
A9: tt >= 0 by A2,A8;
A10: a = m*tt+1 by A8;
reconsider tt,m as Element of NAT by A9,INT_1:3;
a mod m = (((m*tt) mod m)+1) mod m by A10,NAT_D:22
.= (0+1) mod m
.= 1 by A2,NAT_D:24;
hence thesis;
end;
theorem
for F being integer-valued Function holds (F mod m) mod m = F mod m
proof
let F be integer-valued Function;
A1: dom (F mod m) = dom F by Def1;
A2: for x being object st x in dom F holds ((F mod m) mod m).x = (F mod m).x
proof
let x be object;
assume
A3: x in dom F;
((F mod m) mod m).x = ((F mod m).x) mod m by A1,A3,Def1
.= (F.x mod m) mod m by A3,Def1
.= F.x mod m by NAT_D:73
.= (F mod m).x by A3,Def1;
hence thesis;
end;
dom ((F mod m) mod m) = dom (F mod m) by Def1;
hence thesis by A1,A2;
end;
theorem
for F being integer-valued Function holds
(a(#)(F mod m)) mod m = (a(#)F) mod m
proof
let F be integer-valued Function;
A3: dom (a(#)F) = dom F by VALUED_1:def 5;
dom (a(#)(F mod m)) = dom(F mod m) by VALUED_1:def 5;
then
A4: dom (a(#)(F mod m)) = dom F by Def1;
A5: for x being object st x in dom F
holds ((a(#)(F mod m)) mod m).x = ((a(#)F) mod m).x
proof
let x be object;
assume
A6: x in dom F;
A1: (a(#)(F mod m)).x = a*(F mod m).x by VALUED_1:6;
((a(#)(F mod m)) mod m).x = (a(#)(F mod m)).x mod m by A4,A6,Def1
.= (a*(F.x mod m)) mod m by A6,A1,Def1
.= (a*F.x) mod m by Th7
.= (a(#)F).x mod m by VALUED_1:6
.= ((a(#)F) mod m).x by A3,A6,Def1;
hence thesis;
end;
A7: dom ((a(#)F) mod m) = dom F by A3,Def1;
dom ((a(#)(F mod m)) mod m) = dom F by A4,Def1;
hence thesis by A7,A5;
end;
theorem
for F,G being integer-valued FinSequence holds
(F^G) mod m = (F mod m)^(G mod m)
proof
let F,G be integer-valued FinSequence;
A1: dom ((F ^ G) mod m) = dom (F ^ G) by Def1;
A2: dom (G mod m) = dom G by Def1;
A3: dom (F mod m) = dom F by Def1;
A4: for x being object st x in dom (F ^ G)
holds ((F ^ G) mod m).x = ((F mod m) ^ (G mod m)).x
proof
let x be object;
assume
A5: x in dom (F ^ G);
then reconsider x as Element of NAT;
now
per cases by A5,FINSEQ_1:25;
suppose
A6: x in dom F;
A7: ((F ^ G) mod m).x = (F ^ G).x mod m by A5,Def1
.= F.x mod m by A6,FINSEQ_1:def 7;
((F mod m) ^ (G mod m)).x = (F mod m).x by A3,A6,FINSEQ_1:def 7
.= F.x mod m by A6,Def1;
hence ((F ^ G) mod m).x = ((F mod m) ^ (G mod m)).x by A7;
end;
suppose
ex n being Nat st n in dom G & x=len F+n;
then consider n being Element of NAT such that
A8: n in dom G and
A9: x=len F+n;
A10: ((F ^ G) mod m).x = (F ^ G).x mod m by A5,Def1
.= G.n mod m by A8,A9,FINSEQ_1:def 7;
len (F mod m) = len F by Def2;
then ((F mod m) ^ (G mod m)).x = (G mod m).n by A2,A8,A9,FINSEQ_1:def 7
.= G.n mod m by A8,Def1;
hence ((F ^ G) mod m).x = ((F mod m) ^ (G mod m)).x by A10;
end;
end;
hence thesis;
end;
dom ((F mod m) ^ (G mod m)) = Seg(len((F mod m) ^ (G mod m))) by
FINSEQ_1:def 3
.= Seg(len(F mod m)+len(G mod m)) by FINSEQ_1:22
.= Seg(len(F)+len(G mod m)) by Def2
.= Seg(len(F)+len(G)) by Def2
.= Seg(len(F ^ G)) by FINSEQ_1:22
.= dom (F ^ G) by FINSEQ_1:def 3;
hence thesis by A1,A4;
end;
theorem
for F,G being integer-valued FinSequence holds
(a*(F ^ G)) mod m = ((a*F) mod m) ^ ((a*G) mod m)
proof
let F,G be integer-valued FinSequence;
set FG = F^G;
A4: dom (a*(F ^ G)) = dom (F ^ G) by VALUED_1:def 5;
A5: dom (a*G) = dom G by VALUED_1:def 5;
then
A6: dom ((a*G) mod m) = dom G by Def1;
A7: dom (a*F) = dom F by VALUED_1:def 5;
then
A8: dom ((a*F) mod m) = dom F by Def1;
A9: for x being object st x in dom (F ^ G)
holds ((a*(F ^ G)) mod m).x = (((a*F) mod m) ^ ((a*G) mod m)).x
proof
set H = F^G;
let x be object;
assume
A10: x in dom (F ^ G);
now
per cases by A10,FINSEQ_1:25;
suppose
A11: x in dom F;
A12: ((a*(F ^ G)) mod m).x = ((a*(F ^ G)).x) mod m by A4,A10,Def1
.= (a*H.x) mod m by VALUED_1:6
.= (a*(F.x)) mod m by A11,FINSEQ_1:def 7;
(((a*F) mod m) ^ ((a*G) mod m)).x = ((a*F) mod m).x by A8,A11,
FINSEQ_1:def 7
.= ((a*F).x) mod m by A7,A11,Def1
.= (a*(F.x)) mod m by VALUED_1:6;
hence ((a*(F ^ G)) mod m).x = (((a*F) mod m) ^ ((a*G) mod m)).x by A12;
end;
suppose
ex n being Nat st n in dom G & x=len F+n;
then consider n being Element of NAT such that
A13: n in dom G and
A14: x=len F+n;
A15: ((a*(F ^ G)) mod m).x = ((a*(F ^ G)).x) mod m by A4,A10,Def1
.= (a*H.x) mod m by VALUED_1:6
.= (a*G.n) mod m by A13,A14,FINSEQ_1:def 7;
len ((a*F) mod m) = len(a*F) by Def2
.= len F by NEWTON:2;
then
(((a*F) mod m) ^ ((a*G) mod m)).x = ((a*G) mod m).n by A6,A13,A14,
FINSEQ_1:def 7
.= ((a*G).n) mod m by A5,A13,Def1
.= (a*G.n) mod m by RVSUM_1:44;
hence ((a*(F ^ G)) mod m).x = (((a*F) mod m) ^ ((a*G) mod m)).x by A15;
end;
end;
hence thesis;
end;
A16: dom ((a*(F ^ G)) mod m) = dom (a*(F ^ G)) by Def1
.= dom (F ^ G) by VALUED_1:def 5;
dom (((a*F) mod m) ^ ((a*G) mod m)) = Seg(len(((a*F) mod m) ^ ((a*G) mod
m))) by FINSEQ_1:def 3
.= Seg(len((a*F) mod m)+len((a*G) mod m)) by FINSEQ_1:22
.= Seg(len(a*F)+len((a*G) mod m)) by Def2
.= Seg(len(a*F)+len(a*G)) by Def2
.= Seg(len(F)+len(a*G)) by NEWTON:2
.= Seg(len(F)+len(G)) by NEWTON:2
.= Seg(len(F ^ G)) by FINSEQ_1:22
.= dom(F ^ G) by FINSEQ_1:def 3;
hence thesis by A16,A9;
end;
:: Function of (Element of NAT) |^ (Element of NAT)
theorem
a <> 0 & m <> 0 & a,m are_coprime implies
for b holds a |^ b,m are_coprime
proof
defpred P[Nat] means (a |^ $1),m are_coprime;
assume
A1: a <> 0 & m <> 0 & a,m are_coprime;
A2: for b be Nat holds P[b] implies P[b+1]
proof
let b be Nat;
(a |^ (b+1)) = (a |^ b)*(a |^ 1) by NEWTON:8
.= (a |^ b)*a;
hence thesis by A1,EULER_1:14;
end;
(a |^ 0) gcd m = 1 gcd m & m gcd 1 = 1 by NEWTON:4,51;
then
A4: P[0] by INT_2:def 3;
for b be Nat holds P[b] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
begin :: Euler's Theorem and Fermat's Little Theorem
::$N Euler's Generalization of Fermat's Little Theorem
::$L https://en.wikipedia.org/wiki/Euler's_theorem Euler's Theorem
theorem Th18:
a <> 0 & m > 1 & a,m are_coprime implies (a |^ Euler m) mod m = 1
proof
assume that
A1: a <> 0 and
A2: m > 1 and
A3: a,m are_coprime;
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 X};
A5: x in X implies a*x mod m in X
proof
assume x in X;
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;
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;
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 thesis by A6,A11,A12;
end;
A13: X = Y
proof
thus X c= Y
proof
let x be object;
assume x in X;
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;
i mod m <> 0
proof
assume i mod m = 0;
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;
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 X by A19,A21;
hence thesis by A14,A18,A17,A20,A22;
end;
let y be object;
assume y in Y;
then
ex yy being Element of NAT st y = yy & ex u being Element of NAT st yy
= a*u mod m & u in X;
hence thesis by A5;
end;
A23: xi in X & xj in X & xi <> xj implies a*xi mod m <> a*xj mod m
proof
assume that
A24: xi in X and
A25: xj in X and
A26: xi <> xj;
set tm = a*xi mod m,sm = a*xj mod m;
assume
A27: a*xi mod m = a*xj mod m;
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: sm = (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;
tm = (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,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;
end;
reconsider FX = Sgm X as FinSequence of NAT;
reconsider FYY = (a*FX) as natural-valued FinSequence;
reconsider FY = FYY mod m as natural-valued FinSequence;
A35: X c= Seg m
proof
let x be object;
assume x in X;
then
ex xx being Element of NAT st x = xx & m,xx are_coprime & xx >=
1 & xx <= m;
hence thesis by FINSEQ_1:1;
end;
then reconsider X 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 = Y
proof
thus rng FY c= Y
proof
let x be object;
assume x in rng FY;
then consider y being object such that
A40: y in dom FY and
A41: x = FY.y by FUNCT_1:def 3;
reconsider 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 thesis by A41,A42;
end;
let y be object;
assume y in Y;
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 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 thesis by A38,A47,FUNCT_1:def 3;
end;
A49: FY is one-to-one
proof
A50: FX is one-to-one by a35,FINSEQ_3:92;
let x1,x2 be object;
assume that
A51: x1 in dom FY and
A52: x2 in dom FY and
A53: FY.x1 = FY.x2;
A54: x2 in dom FX by A37,A52,FINSEQ_1:def 3;
reconsider x2 as Element of NAT by A52;
A55: x1 in dom FX by A37,A51,FINSEQ_1:def 3;
reconsider 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 & FX.x2 in X & FX.x1 <> FX.x2) by A23,A53,A57;
hence thesis by a35,A55,A54,A56,A50,FINSEQ_1:def 14;
end;
for x be object holds card Coim(FX,x) = card Coim(FY,x)
proof
let x be object;
per cases;
suppose
A58: x in 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 thesis by A60,A61;
end;
suppose
not x in X;
then ( not x in rng FX)& FY"{x} = {} by A13,a35,A39,FINSEQ_1:def 14
,FUNCT_1:72;
hence thesis by FUNCT_1:72;
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 P[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 st P[n] holds P[n+1]
proof
let n;
now
per cases;
suppose
A67: n+1 <= len FY;
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: P[n];
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 P[n+1];
end;
suppose
n+1 > len FY;
hence thesis;
end;
end;
hence thesis;
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: P[0] by NEWTON:4,RVSUM_1:94;
for n holds P[n] from NAT_1:sch 2(A79,A66);
hence thesis by A65,A78;
end;
A80: (Product FX),m are_coprime
proof
defpred P[Nat] means $1 <= len FX implies (Product (FX|$1)),m
are_coprime;
A81: FX|len(FX) = FX by FINSEQ_1:58;
A82: for n st P[n] holds P[n+1]
proof
let n;
now
per cases;
suppose
A83: len FX >= 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
,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 P[n];
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 P[n+1] by A84,RVSUM_1:96;
end;
suppose
len FX < n+1;
hence thesis;
end;
end;
hence thesis;
end;
(Product (FX|0)) gcd m = 1 by NEWTON:51,RVSUM_1:94;
then
A88: P[0] by INT_2:def 3;
for n holds P[n] from NAT_1:sch 2(A88,A82);
hence thesis by A81;
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 thesis by A2,A4,A64,A89,A80,Th12;
end;
NOW:
now
let m,n;
thus m,n are_coprime iff
for k being Nat st k divides m & k divides n holds k = 1
proof
hereby
assume m,n are_coprime;
then
A1: m gcd n = 1;
let k be Nat;
assume k divides m & k divides n;
then k divides 1 by A1,NAT_D:def 5;
hence k = 1 by WSIERP_1:15;
end;
assume for k be Nat st k divides m & k divides n holds k = 1;
then
A2: for k be Nat st k divides m & k divides n holds k divides 1;
1 divides m & 1 divides n by NAT_D:6;
hence m gcd n = 1 by A2,NAT_D:def 5;
end;
end;
Th12P:
for p,k,m being Nat holds
(p |^ k) mod m = ((p mod m) |^ k) mod m
proof
let p,k,m be Nat;
defpred P[Nat] means (p |^ $1) mod m = ((p mod m) |^ $1) mod m;
A1: for n st P[n] holds P[n+1]
proof
let n;
assume
A2: P[n];
(p |^ (n+1)) mod m = ((p |^ n)*(p |^ 1)) mod m by NEWTON:8
.= (((p |^ n) mod m)*(p mod m)) mod m by NAT_D:67
.= (((p mod m) |^ n)*(p mod m)) mod m by A2,Th7
.= ((p mod m) |^ (n + 1)) mod m by NEWTON:6;
hence thesis;
end;
(p |^ 0) mod m = 1 mod m by NEWTON:4;
then
A3: P[0] by NEWTON:4;
for n holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
::$N Fermat's Little Theorem
theorem ThX:
m is prime implies (a |^ m) mod m = a mod m
proof
assume
A2: m is prime;
per cases;
suppose
A3: a,m are_coprime;
per cases;
suppose
A1: a <> 0;
m-1 > 1-1 by A2,XREAL_1:9;
then reconsider mm = m-1 as Element of NAT by INT_1:3;
Euler m = m-1 by A2,EULER_1:20;
then ((a |^ mm) mod m)*a = 1*a by A1,A2,A3,Th18;
then mm+1 = m & ((a |^ mm)*a) mod m = a mod m by Th7;
hence thesis by NEWTON:6;
end;
suppose a = 0;
hence thesis by A2,NEWTON:11;
end;
end;
suppose not a,m are_coprime;
then consider p being Nat such that
A5: p divides a and
A6: p divides m and
A7: p <> 1 by NOW;
m divides a by A2,A5,A6,A7;
then consider k being Nat such that
A7: a = m*k by NAT_D:def 3;
A8: (m*k) mod m = 0;
((m*k) |^ m) mod m = (((m*k) mod m) |^ m) mod m by Th12P
.= 0 mod m by A2,NEWTON:11
.= 0 by INT_1:73;
hence thesis by A7;
end;
end;
::$N Euler's Generalization of Fermat's Little Theorem
theorem
a <> 0 & m > 1 & a,m are_coprime implies
a |^ Euler m, 1 are_congruent_mod m
proof
assume that
A1: a <> 0 and
A2: m > 1 and
A3: a,m are_coprime;
(a |^ Euler m) mod m = 1 by A1,A2,A3,Th18
.= 1 mod m by A2,NAT_D:14;
hence thesis by A2,NAT_D:64;
end;
::$N Fermat's Little Theorem
theorem
m is prime implies a|^m, a are_congruent_mod m
proof
assume
A1: m is prime;
(a |^ m) mod m = a mod m by A1,ThX;
hence thesis by A1,NAT_D:64;
end;
theorem
for p,k,m being Nat holds (p |^ k) mod m = ((p mod m) |^ k) mod m by Th12P;
theorem
m,n are_coprime iff
for k being Nat st k divides m & k divides n holds k = 1 by NOW;