:: 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-2012 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; notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XXREAL_0, CARD_1, RELAT_1, FUNCT_1, RECDEF_1, INT_1, INT_2, FINSET_1, ORDINAL1, NAT_1, NAT_D, NEWTON, EULER_1, CLASSES1, RFINSEQ, RVSUM_1, FINSEQ_1, FINSEQ_3, TREES_4, WSIERP_1; constructors REAL_1, SQUARE_1, NAT_1, NAT_D, NEWTON, RFINSEQ, WSIERP_1, EULER_1, SEQ_1, RECDEF_1, CLASSES1, BINOP_2, RELSET_1; registrations FUNCT_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, SEQM_3, NEWTON, XBOOLE_0, VALUED_0, FINSET_1, CARD_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, FUNCT_1, XBOOLE_0, RELAT_1; 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, XCMPLX_1, XREAL_1, FINSEQ_5, XXREAL_0, ORDINAL1, NAT_D, CLASSES1; schemes NAT_1, FINSEQ_1; begin :: Preliminary reserve a,b,m,x,n,l,xi,xj for Nat, t,z for Integer, f,F for FinSequence of NAT; Lm1: t < 1 iff t <= 0 proof 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; hence thesis; end; Lm2: a <> 0 implies a-1 >= 0 proof assume a <> 0; then a >= 1 by NAT_1:14; then a-1 >= 1-1 by XREAL_1:9; hence thesis; end; Lm3: 1 gcd z = 1 proof thus 1 gcd z = abs 1 gcd abs(z) by INT_2:34 .= 1 gcd abs z by ABSVALUE:def 1 .= 1 by NEWTON:51; end; :: Very useful theorem theorem a,(b qua Integer) are_relative_prime iff a,b are_relative_prime; 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 r >= 1 by Th2; then 1-1 <= t by XREAL_1:20; hence contradiction by A7; end; end; hence contradiction; end; theorem Th3: a <> 0 & b <> 0 & m <> 0 & a,m are_relative_prime & b,m are_relative_prime implies m,a*b mod m are_relative_prime proof assume that A1: a <> 0 and A2: b <> 0 and A3: m <> 0 and A4: a,m are_relative_prime & b,m are_relative_prime; a*b,m are_relative_prime by A1,A3,A4,EULER_1:14; then A5: a*b gcd m = 1 by INT_2:def 3; 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,XCMPLX_1:5; then a*b+(-t)*m gcd m = a*b gcd m by EULER_1:16; hence thesis by A6,A5,INT_2:def 3; end; theorem Th4: m > 1 & m,n are_relative_prime & n = a*b mod m implies m,b are_relative_prime proof assume that A1: m > 1 and A2: m,n are_relative_prime 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_relative_prime; then A9: m gcd b <> 1 by INT_2:def 3; A10: k <> -1 by NAT_1:2; 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,A10,INT_1:9; end; tm = 0 implies m gcd n <> 1 by A1,A3,A4,A6,A8,NEWTON:52; hence contradiction by A2,A11,INT_2:def 3; end; theorem Th5: (m mod n) mod n = m mod n proof per cases; suppose n <> 0; then ex t being Nat st m = n*t+(m mod n) & m mod n < n by NAT_D:def 2; hence thesis by NAT_D:24; end; suppose A1: n = 0; hence (m mod n) mod n = 0 by NAT_D:def 2 .= m mod n by A1,NAT_D:def 2; end; end; theorem (l+m) mod n = ((l mod n)+(m mod n)) mod n proof thus (l+m) mod n = ((l mod n)+m) mod n by NAT_D:22 .= ((l mod n)+(m mod n)) mod n by NAT_D:23; end; theorem Th7: (l*m) mod n = (l*(m mod n)) mod n proof per cases; suppose n <> 0; then consider t being Nat such that A1: m = n*t+(m mod n) and (m mod n) FinSequence of NAT; coherence proof rng(a*f) c= NAT proof let x be set; assume x in rng (a*f); then consider xx being set such that A1: xx in dom (a*f) and A2: x = (a*f).xx by FUNCT_1:def 3; reconsider xx as Element of NAT by A1; (a*f).xx = a*(f.xx) by RVSUM_1:44; hence thesis by A2; end; hence thesis by FINSEQ_1:def 4; end; end; theorem Th10: for R1,R2 be FinSequence of NAT st R1,R2 are_fiberwise_equipotent holds Product R1 = Product R2 proof let R1,R2 be FinSequence of NAT; defpred P[Nat] means for f,g be FinSequence of NAT st f,g are_fiberwise_equipotent & len f = $1 holds Product f = Product g; A1: for n st P[n] holds P[n+1] proof let n; assume A2: P[n]; let f,g be FinSequence of NAT; assume that A3: f,g are_fiberwise_equipotent and A4: len f = n+1; reconsider a = f.(n+1) as Element of NAT; 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 15 .= (g|(Seg m))|(Seg m1) by FINSEQ_1:def 15 .= g|((Seg m)/\(Seg m1)) by RELAT_1:71 .= g|(Seg m1) by A12,XBOOLE_1:28 .= g|m1 by FINSEQ_1:def 15; now let x be set; card Coim(f,x) = card Coim(g,x) by A3,CLASSES1:def 9; 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 9; 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 NAT; 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 A17,A18; end; begin :: Modulus for Finite Sequence of Natural :: Function of (FinSequence of NAT) mod Element of NAT definition let f be FinSequence of NAT,m be Nat; func f mod m -> FinSequence of NAT means :Def1: len(it) = len(f) & for i being Nat st i in dom f holds it.i = (f.i) mod m; existence proof deffunc F(Nat) = (f.$1) mod m; consider g be FinSequence such that A1: len g = len f and A2: for k being Nat st k in dom g holds g.k = F(k) from FINSEQ_1:sch 2; rng g c= NAT proof let x be set; assume x in rng g; then consider y being set such that A3: y in dom g and A4: x = g.y by FUNCT_1:def 3; reconsider y as Element of NAT by A3; g.y = (f.y) mod m by A2,A3; hence thesis by A4; end; then reconsider g as FinSequence of NAT by FINSEQ_1:def 4; take g; thus len g = len f by A1; let k be Nat; assume k in dom f; then k in dom g by A1,FINSEQ_3:29; hence thesis by A2; end; uniqueness proof let fa,fb be FinSequence of NAT such that A5: len(f) = len(fa) and A6: for i being Nat st i in dom f holds fa.i = (f.i) mod m and A7: len(f) = len(fb) and A8: for i being Nat st i in dom f holds fb.i = (f.i) mod m; now let X be set such that A9: dom f = X; A10: for i being Nat st i in X holds fa.i = fb.i proof given j being Nat 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; A13: dom f = Seg len f by FINSEQ_1:def 3 .= dom fb by A7,FINSEQ_1:def 3; dom f = Seg len f by FINSEQ_1:def 3 .= dom fa by A5,FINSEQ_1:def 3; hence thesis by A9,A13,A10,FINSEQ_1:13; end; hence thesis; end; end; theorem for f be FinSequence of NAT st m <> 0 holds (Product(f mod m)) mod m = (Product f) mod m proof defpred P[Nat] means for f be FinSequence of NAT st m <> 0 & len f = $1 holds (Product(f mod m)) mod m = (Product f) mod m; let f be FinSequence of NAT; 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 FinSequence of NAT; assume that A5: m <> 0 and A6: len f = n+1; reconsider fn = f|n as FinSequence of NAT; A7: len fn = n by A6,FINSEQ_1:59,NAT_1:11; A8: len (f mod m) = n+1 by A6,Def1; 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 15; 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 15; 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; len((f mod m)|n) = len(fn mod m) by A7,A9,Def1; 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 Th9 .= (((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 Th5; (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,Th9; end; A20: P[0] proof let f be FinSequence of NAT; assume that m <> 0 and A21: len f=0; A22: f = <*> NAT & len (f mod m) = 0 by A21,Def1; 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: a <> 0 & m > 1 & a*n mod m = n mod m & m,n are_relative_prime implies a mod m = 1 proof assume that A1: a <> 0 and A2: m > 1 and A3: a*n mod m = n mod m and A4: m,n are_relative_prime; 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,XREAL_1:158; 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 by NAT_D:13 .= 1 by A2,NAT_D:24; hence thesis; end; theorem (F mod m) mod m = F mod m proof A1: dom (F mod m) = Seg(len(F mod m)) by FINSEQ_1:def 3 .= Seg(len F) by Def1 .= dom F by FINSEQ_1:def 3; A2: for x being set st x in dom F holds ((F mod m) mod m).x = (F mod m).x proof let x be set; assume A3: x in dom F; then reconsider x as Element of NAT; ((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 Th5 .= (F mod m).x by A3,Def1; hence thesis; end; dom ((F mod m) mod m) = Seg(len((F mod m) mod m)) by FINSEQ_1:def 3 .= Seg(len(F mod m)) by Def1 .= Seg(len F) by Def1 .= dom F by FINSEQ_1:def 3; hence thesis by A1,A2,FUNCT_1:2; end; theorem (a*(F mod m)) mod m = (a*F) mod m proof A1: dom (a*F) = Seg(len(a*F)) by FINSEQ_1:def 3 .= Seg(len F) by NEWTON:2 .= dom F by FINSEQ_1:def 3; A2: dom (a*(F mod m)) = Seg(len(a*(F mod m))) by FINSEQ_1:def 3 .= Seg(len(F mod m)) by NEWTON:2 .= Seg(len F) by Def1 .= dom F by FINSEQ_1:def 3; A3: for x being set st x in dom F holds ((a*(F mod m)) mod m).x = ((a*F) mod m).x proof let x be set; assume A4: x in dom F; then reconsider x as Element of NAT; ((a*(F mod m)) mod m).x = (a*(F mod m)).x mod m by A2,A4,Def1 .= (a*(F mod m).x ) mod m by RVSUM_1:44 .= (a*(F.x mod m)) mod m by A4,Def1 .= (a*F.x) mod m by Th7 .= (a*F).x mod m by RVSUM_1:44 .= ((a*F) mod m).x by A1,A4,Def1; hence thesis; end; A5: dom ((a*F) mod m) = Seg(len((a*F) mod m)) by FINSEQ_1:def 3 .= Seg(len(a*F)) by Def1 .= Seg(len F) by NEWTON:2 .= dom F by FINSEQ_1:def 3; dom ((a*(F mod m)) mod m) = Seg(len((a*(F mod m)) mod m)) by FINSEQ_1:def 3 .= Seg(len(a*(F mod m))) by Def1 .= Seg(len(F mod m)) by NEWTON:2 .= Seg(len F) by Def1 .= dom F by FINSEQ_1:def 3; hence thesis by A5,A3,FUNCT_1:2; end; theorem for F,G being FinSequence of NAT holds (F ^ G) mod m = (F mod m) ^ (G mod m) proof let F,G be FinSequence of NAT; A1: dom ((F ^ G) mod m) = Seg(len((F ^ G) mod m)) by FINSEQ_1:def 3 .= Seg(len(F ^ G)) by Def1 .= dom (F ^ G) by FINSEQ_1:def 3; A2: dom (G mod m) = Seg(len(G mod m)) by FINSEQ_1:def 3 .= Seg(len G) by Def1 .= dom G by FINSEQ_1:def 3; A3: dom (F mod m) = Seg(len(F mod m)) by FINSEQ_1:def 3 .= Seg(len F) by Def1 .= dom F by FINSEQ_1:def 3; A4: for x being set st x in dom (F ^ G) holds ((F ^ G) mod m).x = ((F mod m) ^ (G mod m)).x proof let x be set; 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 Def1; 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 Def1 .= Seg(len(F)+len(G)) by Def1 .= Seg(len(F ^ G)) by FINSEQ_1:22 .= dom (F ^ G) by FINSEQ_1:def 3; hence thesis by A1,A4,FUNCT_1:2; end; theorem for F,G being FinSequence of NAT holds (a*(F ^ G)) mod m = ((a*F) mod m) ^ ((a*G) mod m) proof let F,G be FinSequence of NAT; reconsider FG = F ^ G as FinSequence of NAT; A1: dom (a*(F ^ G)) = Seg(len(a*FG)) by FINSEQ_1:def 3 .= Seg(len(FG)) by NEWTON:2 .= dom (F ^ G) by FINSEQ_1:def 3; A2: dom (a*G) = Seg(len(a*G)) by FINSEQ_1:def 3 .= Seg(len G) by NEWTON:2 .= dom G by FINSEQ_1:def 3; A3: dom ((a*G) mod m) = Seg(len((a*G) mod m)) by FINSEQ_1:def 3 .= Seg(len (a*G)) by Def1 .= Seg(len(G)) by NEWTON:2 .= dom G by FINSEQ_1:def 3; A4: dom (a*F) = Seg(len(a*F)) by FINSEQ_1:def 3 .= Seg(len F) by NEWTON:2 .= dom F by FINSEQ_1:def 3; A5: dom ((a*F) mod m) = Seg(len((a*F) mod m)) by FINSEQ_1:def 3 .= Seg(len (a*F)) by Def1 .= Seg(len(F)) by NEWTON:2 .= dom F by FINSEQ_1:def 3; A6: for x being set st x in dom (F ^ G) holds ((a*(F ^ G)) mod m).x = (((a*F ) mod m) ^ ((a*G) mod m)).x proof reconsider H = F ^ G as FinSequence of NAT; let x be set; assume A7: x in dom (F ^ G); then reconsider x as Element of NAT; now per cases by A7,FINSEQ_1:25; suppose A8: x in dom F; A9: ((a*(F ^ G)) mod m).x = ((a*(F ^ G)).x) mod m by A1,A7,Def1 .= (a*H.x) mod m by RVSUM_1:44 .= (a*(F.x)) mod m by A8,FINSEQ_1:def 7; (((a*F) mod m) ^ ((a*G) mod m)).x = ((a*F) mod m).x by A5,A8, FINSEQ_1:def 7 .= ((a*F).x) mod m by A4,A8,Def1 .= (a*(F.x)) mod m by RVSUM_1:44; hence ((a*(F ^ G)) mod m).x = (((a*F) mod m) ^ ((a*G) mod m)).x by A9; end; suppose ex n being Nat st n in dom G & x=len F+n; then consider n being Element of NAT such that A10: n in dom G and A11: x=len F+n; A12: ((a*(F ^ G)) mod m).x = ((a*(F ^ G)).x) mod m by A1,A7,Def1 .= (a*H.x) mod m by RVSUM_1:44 .= (a*G.n) mod m by A10,A11,FINSEQ_1:def 7; len ((a*F) mod m) = len(a*F) by Def1 .= len F by NEWTON:2; then (((a*F) mod m) ^ ((a*G) mod m)).x = ((a*G) mod m).n by A3,A10,A11, FINSEQ_1:def 7 .= ((a*G).n) mod m by A2,A10,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 A12; end; end; hence thesis; end; A13: dom ((a*(F ^ G)) mod m) = Seg(len((a*FG) mod m)) by FINSEQ_1:def 3 .= Seg(len(a*FG)) by Def1 .= Seg(len(FG)) by NEWTON:2 .= dom (F ^ G) by FINSEQ_1:def 3; 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 Def1 .= Seg(len(a*F)+len(a*G)) by Def1 .= 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 A13,A6,FUNCT_1:2; end; :: Function of (Element of NAT) |^ (Element of NAT) theorem a <> 0 & m <> 0 & a,m are_relative_prime implies for b holds a |^ b,m are_relative_prime proof defpred P[Nat] means (a |^ $1),m are_relative_prime; assume A1: a <> 0 & m <> 0 & a,m are_relative_prime; A2: for b holds P[b] implies P[b+1] proof let b; A3: (a |^ (b+1)) = (a |^ b)*(a |^ 1) by NEWTON:8 .= (a |^ b)*a by NEWTON:5; assume (a |^ b),m are_relative_prime; hence thesis by A1,A3,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 holds P[b] from NAT_1:sch 2(A4,A2); hence thesis; end; begin :: Euler's Theorem and Small Fermat's Theorem ::$N Euler's Generalization of Fermat's Little Theorem theorem Th18: a <> 0 & m > 1 & a,m are_relative_prime implies (a |^ Euler m) mod m = 1 proof assume that A1: a <> 0 and A2: m > 1 and A3: a,m are_relative_prime; 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: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_relative_prime and A8: t >= 1 and t <= m; A9: a*t,m are_relative_prime 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,INT_2:def 3; 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,Th3; hence thesis by A6,A11,A12; end; A13: X = Y proof thus X c= Y proof let x be set; assume x in X; 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: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; 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 A2,EULER_1:15 .= m*1 by Lm3 .= m; hence contradiction by A2,A15,INT_2:def 3; 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 EULER_1:12; then m,im are_relative_prime 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 set; 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_relative_prime 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_relative_prime 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 FinSequence of NAT; reconsider FY = FYY mod m as FinSequence of NAT; A34: X c= Seg m proof let x be set; assume x in X; then ex xx being Element of NAT st x = xx & m,xx are_relative_prime & xx >= 1 & xx <= m; hence thesis by FINSEQ_1:1; end; then reconsider X as finite set; dom FYY = Seg(len FYY) by FINSEQ_1:def 3 .= Seg(len FX) by NEWTON:2; 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:2; then A37: dom FX = dom FY by FINSEQ_1:def 3; A38: rng FY = Y proof thus rng FY c= Y proof let x be set; assume x in rng FY; then consider y being set such that A39: y in dom FY and A40: x = FY.y by FUNCT_1:def 3; reconsider y as Element of NAT by A39; FX.y in rng FX by A37,A39,FUNCT_1:def 3; 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:44; hence thesis by A40,A41; end; let y be set; assume y in Y; 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 3; reconsider xx as Element of NAT by A46; FY.xx = (FYY.xx) mod m by A35,A46,Def1 .= y by A42,A44,A47,RVSUM_1:44; hence thesis by A37,A46,FUNCT_1:def 3; end; A48: FY is one-to-one proof A49: FX is one-to-one by A34,FINSEQ_3:92; let x1,x2 be set; assume that A50: x1 in dom FY and A51: x2 in dom FY and A52: FY.x1 = FY.x2; A53: x2 in dom FX by A36,A51,FINSEQ_1:def 3; reconsider x2 as Element of NAT by A51; A54: x1 in dom FX by A36,A50,FINSEQ_1:def 3; reconsider 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 3; A56: FY.x2 = (FYY.x2) mod m by A35,A53,Def1 .= (a*FX.x2) mod m by RVSUM_1:44; FY.x1 = (FYY.x1) mod m by A35,A54,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,A52,A56; hence thesis by A34,A54,A53,A55,A49,FINSEQ_1:def 13,FUNCT_1:def 4; end; for x be set holds card Coim(FX,x) = card Coim(FY,x) proof let x be set; now per cases; suppose A57: x in X; A58: FX is one-to-one by A34,FINSEQ_3:92; x in rng FX by A34,A57,FINSEQ_1:def 13; then A59: len(FX-{x}) = len(FX)-1 by A58,FINSEQ_3:90; 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:59; len(FY-{x}) = len(FY)-1 by A13,A38,A48,A57,FINSEQ_3:90; hence thesis by A59,A60; end; suppose not x in X; then ( not x in rng FX)& FY"{x} = {} by A13,A34,A38,FINSEQ_1:def 13 ,FUNCT_1:72; hence thesis by FUNCT_1:72; end; end; hence thesis; end; then A61: FX,FY are_fiberwise_equipotent by CLASSES1:def 9; then A62: len(FX) = len(FY) by RFINSEQ:3; A63: (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 15; then A64: FY = FY|len FY by FINSEQ_2:20; A65: for n st P[n] holds P[n+1] proof let n; now per cases; suppose A66: n+1 <= len FY; then len (FX|(n+1)) = n+1 by A62,FINSEQ_1:59; then A67: FX|(n+1) = (FX|(n+1))|n ^ <* (FX|(n+1)).(n+1) *> by RFINSEQ:7; assume A68: P[n]; 0+1 <= n+1 by NAT_1:13; then A69: n+1 in dom FY by A66,FINSEQ_3:25; A70: (FY|(n+1)).(n+1) = FY.(n+1) by FINSEQ_3:112; A71: (FX|(n+1)).(n+1) = FX.(n+1) by FINSEQ_3:112; A72: n <= n+1 by NAT_1:11; then A73: len(FY|n) = n by A66,FINSEQ_1:59,XXREAL_0:2; A74: (FX|(n+1))|n = FX|n by A72,FINSEQ_5:77; A75: (FY|(n+1))|n = FY|n by A72,FINSEQ_5:77; A76: len (FY|(n+1)) = n+1 by A66,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 A75,A70,RVSUM_1:96 .= (((a |^ len(FY|n)*Product(FX|n)) mod m) *(FY.(n+1) mod m)) mod m by A66,A68,A72,Th9,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 Th5 .= ((a |^ len(FY|n)*Product(FX|n))*(a*FX).(n+1)) mod m by Th9 .= (a |^ n*Product (FX|n))*(a*(FX.(n+1))) mod m by A73,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 A76, NEWTON:6 .= (a |^ len(FY|(n+1)))*(Product(FX|(n+1))) mod m by A67,A74,A71, 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 15; then A77: FX = FX|len FY by A62,FINSEQ_2:20; A78: P[0] by NEWTON:4,RVSUM_1:94; for n holds P[n] from NAT_1:sch 2(A78,A65); hence thesis by A64,A77; end; A79: (Product FX),m are_relative_prime proof defpred P[Nat] means $1 <= len FX implies (Product (FX|$1)),m are_relative_prime; A80: FX|len(FX) = FX by FINSEQ_1:58; A81: for n st P[n] holds P[n+1] proof let n; now per cases; suppose A82: 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 A82,FINSEQ_1:59; then A83: FF = (FF|n) ^ <*ff*> by RFINSEQ:7; 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:6; then (FX|(n+1)).(n+1) = FX.(n+1) & n+1 in dom FX by A82,FINSEQ_3:25 ,112; then A85: (FX|(n+1)).(n+1) in rng FX by FUNCT_1:def 3; 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 P[n]; then a,m9 are_relative_prime by A82,A84,FINSEQ_5:77,XXREAL_0:2; then a*b,m9 are_relative_prime by A86,INT_2:26; hence P[n+1] by A83,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 A87: P[0] by INT_2:def 3; for n holds P[n] from NAT_1:sch 2(A87,A81); hence thesis by A80; end; len(FX) = card X by A34,FINSEQ_3:39 .= Euler m by EULER_1:def 1; then A88: len FY = Euler m by A61,RFINSEQ:3; (Product FX) mod m = (Product FY) mod m by A61,Th10; hence thesis by A2,A63,A88,A4,A79,Th12; end; ::End of Euler's Theorem ::$N Small Fermat's Theorem theorem ::Small Fermat's theorem a <> 0 & m is prime & a,m are_relative_prime implies (a |^ m) mod m = a mod m proof assume that A1: a<>0 and A2: m is prime and A3: a,m are_relative_prime; A4: m > 1 by A2,INT_2:def 4; then m-1 > 1-1 by 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,A3,A4,Th18; then mm+1 = m & ((a |^ mm)*a) mod m = a mod m by Th7; hence thesis by NEWTON:6; end;