Copyright (c) 1998 Association of Mizar Users
environ vocabulary INT_1, FINSEQ_1, INT_2, ARYTM_3, ABSVALUE, ARYTM_1, NAT_1, RELAT_1, FUNCT_1, RFINSEQ, SQUARE_1, BOOLE, CARD_1, EULER_1, FINSET_1, FILTER_0, CARD_3, GROUP_1; notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, CARD_1, INT_1, INT_2, SQUARE_1, FINSET_1, NAT_1, FUNCT_1, NEWTON, EULER_1, RFINSEQ, RVSUM_1, RELAT_1, FINSEQ_1, FINSEQ_3, SETWOP_2, TOPREAL1, TREES_4, WSIERP_1, GROUP_1; constructors SQUARE_1, FINSEQ_3, REAL_1, EULER_1, RFINSEQ, MONOID_0, SETWOP_2, TOPREAL1, WSIERP_1, NAT_1, INT_2, SEQ_1, MEMBERED, CARD_4; clusters FINSET_1, INT_1, RELSET_1, FINSUB_1, FUNCT_1, FINSEQ_3, NAT_1, XREAL_0, MEMBERED, NUMBERS, ORDINAL2; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, FUNCT_1, XBOOLE_0; theorems INT_2, AXIOMS, FINSEQ_1, NAT_LAT, NAT_1, ABSVALUE, REAL_1, RLVECT_1, INT_1, GR_CY_2, FUNCT_1, REAL_2, EULER_1, PREPOWER, GR_CY_1, JORDAN4, RFINSEQ, FINSUB_1, FINSEQ_2, RVSUM_1, TOPREAL1, FINSEQ_3, FINSET_1, NEWTON, RELAT_1, JORDAN3, GROUP_4, SCMFSA9A, XBOOLE_1, XCMPLX_0, XCMPLX_1, URYSOHN1; schemes NAT_1, FINSEQ_1; begin :: Preliminary reserve a,b,m,x,n,k,l,xi,xj for Nat, t,z for Integer, f,F for FinSequence of NAT; Lm1:0 <> a & 0 <> b implies a gcd b = a hcf b proof assume 0 <> a & 0 <> b; then 0 < a & 0 < b by NAT_1:19; then abs(a) = a & abs(b) = b by ABSVALUE:def 1; hence thesis by INT_2:def 3; end; Lm2:t < 1 iff t <= 0 proof t < 1 implies t <= 0 proof assume A1:t < 1; assume A2:t > 0; then reconsider t as Nat by INT_1:16; t >= 1 by A2,RLVECT_1:99; hence contradiction by A1; end; hence thesis by AXIOMS:22; end; Lm3:a <> 0 implies a-1 >= 0 proof assume a <> 0; then a >= 1 by RLVECT_1:99; then a-1 >= 1-1 by REAL_1:49; hence thesis; end; Lm4:1 gcd z = 1 proof thus 1 gcd z = abs(1 ) hcf abs(z) by INT_2:def 3 .= 1 hcf abs(z) by ABSVALUE:def 1 .= 1 by NAT_LAT:35; end; Lm5:a,b are_relative_prime implies b,a are_relative_prime proof assume a,b are_relative_prime; then a hcf b = 1 by INT_2:def 6; hence thesis by INT_2:def 6; end; :::::::::::::::::::::::::::: :: :: :: Very useful theorem :: :: :: :::::::::::::::::::::::::::: theorem Th1:a,(b qua Integer) are_relative_prime iff a,b are_relative_prime proof thus a,(b qua Integer) are_relative_prime implies a,b are_relative_prime proof assume a,(b qua Integer) are_relative_prime; then A1:a gcd b = 1 by INT_2:def 4; a >= 0 & b >= 0 by NAT_1:18; then abs(a) = a & abs(b) = b by ABSVALUE:def 1; then a hcf b = 1 by A1,INT_2:def 3; hence thesis by INT_2:def 6; end; assume a,b are_relative_prime; then A2:a hcf b = 1 by INT_2:def 6; a >= 0 & b >= 0 by NAT_1:18; then abs(a) = a & abs(b) = b by ABSVALUE:def 1; then a gcd b = 1 by A2,INT_2:def 3; hence thesis by INT_2:def 4; end; theorem Th2:m > 1 & m*t >= 1 implies t >= 1 proof assume A1:m > 1 & m*t >= 1; assume A2:t < 1; A3:m > 0 by A1,AXIOMS:22; t <= 0 by A2,Lm2; then m*t <= 0 by A3,REAL_2:123; hence contradiction by A1,Lm2; end; Lm6:m > 1 & 1-m <= z & z <= m-1 & m divides z implies z = 0 proof assume A1:m > 1 & 1-m <= z & z <= m-1 & m divides z; assume A2:z <> 0; consider t being Integer such that A3:z = m*t by A1,INT_1:def 9; A4:t <> 0 by A2,A3; now per cases by A4; suppose A5:t > 0; then reconsider t as Nat by INT_1:16; t >= 1 by A5,RLVECT_1:99; then m*t >= m by NAT_LAT:2; then m*t+1 > m by NAT_1:38; hence contradiction by A1,A3,REAL_1:84; suppose A6:t < 0; 1 <= m*t+m*1 by A1,A3,REAL_1:86; then A7:1 <= m*(t+1) by XCMPLX_1:8; reconsider r = (t+1) as Integer; r >= 1 by A1,A7,Th2; then 1-1 <= t by REAL_1:86; hence contradiction by A6; end; hence contradiction; end; theorem Th3:m > 1 & m*t >= 0 implies t >= 0 proof assume A1:m > 1 & m*t >= 0; assume A2:t < 0; then t*m < t by A1,REAL_2:145; hence contradiction by A1,A2,AXIOMS:22; end; canceled; theorem Th5: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 A1:a <> 0 & b <> 0 & m <> 0 & a,m are_relative_prime & b,m are_relative_prime; then a*b,m are_relative_prime by EULER_1:15; then A2:a*b hcf m = 1 by INT_2:def 6; consider t being Nat such that A3:a*b = m*t+(a*b mod m) and (a*b mod m) < m by A1,NAT_1:def 2; A4:a*b mod m = a*b-m*t by A3,XCMPLX_1:26 .= a*b+(-m*t) by XCMPLX_0:def 8 .= a*b+(-t)*m by XCMPLX_1:175; A5:a*b <> a*0 by A1,XCMPLX_1:5; then A6:a*b+(-t)*m gcd m = a*b gcd m by A1,EULER_1:17; A7: a*b gcd m = 1 by A1,A2,A5,Lm1; a*b mod m >= 0 & m >= 0 by NAT_1:18; then abs(a*b mod m) = a*b mod m & abs(m) = m by ABSVALUE:def 1; then (a*b mod m) hcf m = 1 by A4,A6,A7,INT_2:def 3; hence thesis by INT_2:def 6; end; theorem Th6:m > 1 & b <> 0 & m,n are_relative_prime & a,m are_relative_prime & n = a*b mod m implies m,b are_relative_prime proof assume A1:m > 1 & b <> 0 & m,n are_relative_prime & a,m are_relative_prime & n = a*b mod m; assume not m,b are_relative_prime; then A2:m hcf b <> 1 by INT_2:def 6; set k = m hcf b; A3: m <> 0 by A1; then m > 0 & b > 0 by A1,NAT_1:19; then A4:k > 0 by NAT_LAT:43; A5:k divides m & k divides b by NAT_1:def 5; then consider km being Nat such that A6:m = k*km by NAT_1:def 3; A7:k <> 0 & km <> 0 by A1,A6; consider kb being Nat such that A8:b = k*kb by A5,NAT_1:def 3; consider p being Nat such that A9:a*(k*kb) = (k*km)*p+(a*(k*kb) mod (k*km)) & (a*(k*kb) mod (k*km)) < k*km by A3,A6,NAT_1:def 2; A10:(a*(k*kb) mod (k*km)) = a*(k*kb)-(k*km)*p by A9,XCMPLX_1:26 .= (a*k)*kb-(k*km)*p by XCMPLX_1:4 .= (k*a)*kb-k*(km*p) by XCMPLX_1:4 .= k*(a*kb)-k*(km*p) by XCMPLX_1:4 .= k*((a*kb)-(km*p)) by XCMPLX_1:40; set tm = (a*kb)-(km*p); A11:tm = 0 implies m gcd n <> 1 proof assume A12: tm = 0; A13:0 = abs(0) by ABSVALUE:7; k*km >= 0 by NAT_1:18; then k*km = abs(k*km) by ABSVALUE:def 1; then k*km gcd 0 = k*km hcf 0 by A13,INT_2:def 3 .= k*km by NAT_LAT:36; hence thesis by A1,A6,A8,A10,A12; end; A14:tm <> 0 implies m gcd n <> 1 proof assume A15:tm <> 0; assume A16:m gcd n = 1; A17:k <> -1 by NAT_1:18; m gcd n = k*(km gcd tm) by A1,A4,A6,A7,A8,A10,A15,EULER_1:16; hence contradiction by A2,A16,A17,INT_1:22; end; A18:m gcd n = abs(m) hcf abs(n) by INT_2:def 3; m >= 0 & n >= 0 by NAT_1:18; then m = abs(m) & n = abs(n) by ABSVALUE:def 1; hence contradiction by A1,A11,A14,A18,INT_2:def 6; end; theorem Th7:for n holds (m mod n) mod n = m mod n proof let n; per cases; suppose n <> 0; then ex t being Nat st m = n*t+(m mod n) & m mod n < n by NAT_1:def 2; hence thesis by GR_CY_1:4; suppose A1: n = 0; hence (m mod n) mod n = 0 by NAT_1:def 2 .= m mod n by A1,NAT_1:def 2; end; theorem for n holds (l+m) mod n = ((l mod n)+(m mod n)) mod n proof let n; thus (l+m) mod n = ((l mod n)+m) mod n by GR_CY_1:2 .= ((l mod n)+(m mod n)) mod n by GR_CY_1:3; end; theorem Th9:for n holds (l*m) mod n = (l*(m mod n)) mod n proof let n; per cases; suppose n <> 0; then consider t being Nat such that A1: m = n*t+(m mod n) & (m mod n)<n by NAT_1:def 2; (l*m) mod n =(l*(n*t)+l*(m mod n)) mod n by A1,XCMPLX_1:8 .=((l*t)*n+l*(m mod n)) mod n by XCMPLX_1:4; hence (l*m) mod n = (l*(m mod n)) mod n by GR_CY_1:1; suppose A2: n = 0; hence (l*m) mod n = 0 by NAT_1:def 2 .= (l*(m mod n)) mod n by A2,NAT_1:def 2; end; theorem Th10:for n holds (l*m) mod n = ((l mod n)*m) mod n proof let n; per cases; suppose n <> 0; then consider t being Nat such that A1: l = n*t+(l mod n) & (l mod n)<n by NAT_1:def 2; (l*m) mod n = (m*(n*t)+m*(l mod n)) mod n by A1,XCMPLX_1:8 .=((m*t)*n+m*(l mod n)) mod n by XCMPLX_1:4; hence (l*m) mod n = ((l mod n)*m) mod n by GR_CY_1:1; suppose A2: n = 0; hence (l*m) mod n = 0 by NAT_1:def 2 .= ((l mod n)*m) mod n by A2,NAT_1:def 2; end; theorem Th11:for n holds (l*m) mod n = ((l mod n)*(m mod n)) mod n proof let n; (l*m) mod n = (l*(m mod n)) mod n by Th9; hence thesis by Th10; end; begin :::::::::::::::::::::::::::::::::::::::::::: :: :: :: Function of Nat*(FinSequence of NAT) :: :: :: :::::::::::::::::::::::::::::::::::::::::::: definition let a,f; redefine func a*f -> 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) & x = (a*f).xx by FUNCT_1:def 5; A2:xx in Seg len (a*f) by A1,FINSEQ_1:def 3; Seg len (a*f) is Subset of NAT by FINSUB_1:def 5; then reconsider xx as Nat by A2; (a*f).xx = a*(f.xx) by RVSUM_1:66; hence thesis by A1; end; hence thesis by FINSEQ_1:def 4; end; end; ::::::::::::::::::::::::::::::::::::::::: :: :: :: Function of Product(FinSequence of NAT) :: :: :: ::::::::::::::::::::::::::::::::::::::::: Lm7:for f be FinSequence of NAT, r be Nat holds Product(f^<*r*>) = Product f*r by RVSUM_1:126; Lm8:for f1,f2 be FinSequence of NAT holds Product(f1^f2) = Product f1*Product f2 by RVSUM_1:127; canceled 13; theorem Th25:for R1,R2 be FinSequence of NAT st R1,R2 are_fiberwise_equipotent holds Product R1 = Product R2 proof 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:P[0] proof let f,g be FinSequence of NAT; assume f,g are_fiberwise_equipotent & len f = 0; then len g = 0 & f = <*>NAT by FINSEQ_1:32,RFINSEQ:16; hence thesis by FINSEQ_1:32; end; A2:for n st P[n] holds P[n+1] proof let n; assume A3:P[n]; let f,g be FinSequence of NAT; assume A4:f,g are_fiberwise_equipotent & len f = n+1; then A5:rng f = rng g & len f = len g by RFINSEQ:1,16; 0<n+1 by NAT_1:19; then 0+1<=n+1 by NAT_1:38; then A6:n+1 in dom f by A4,FINSEQ_3:27; reconsider a = f.(n+1) as Nat; a in rng g by A5,A6,FUNCT_1:def 5; then consider m such that A7:m in dom g & g.m = a by FINSEQ_2:11; A8:g = (g|m)^(g/^m) by RFINSEQ:21; A9:1<=m & m<=len g by A7,FINSEQ_3:27; then max(0,m-1) = m-1 by FINSEQ_2:4; then reconsider m1 = m-1 as Nat by FINSEQ_2:5; set gg = g/^m, gm = g|m; A10:len gm = m by A9,TOPREAL1:3; A11:m = m1+1 by XCMPLX_1:27; m in Seg m by A9,FINSEQ_1:3; then gm.m = a & m in dom g by A7,RFINSEQ:19; then A12:gm = (gm|m1)^<*a*> by A10,A11,RFINSEQ:20; m1<=m by A11,NAT_1:29; then A13:Seg m1 c= Seg m by FINSEQ_1:7; A14:gm|m1 = gm|(Seg m1) by TOPREAL1:def 1 .= (g|(Seg m))|(Seg m1) by TOPREAL1:def 1 .= g|((Seg m)/\(Seg m1)) by RELAT_1:100 .= g|(Seg m1) by A13,XBOOLE_1:28 .= g|m1 by TOPREAL1:def 1; set fn = f|n; n<=n+1 by NAT_1:29; then A15:len fn = n by A4,TOPREAL1:3; A16:f = fn ^ <*a*> by A4,RFINSEQ:20; now let x be set; card(f"{x}) = card(g"{x}) by A4,RFINSEQ:def 1; then card(fn"{x})+card(<*a*>"{x}) = card(((g|m1)^<*a*>^(g/^m))"{x}) by A8,A12,A14,A16,FINSEQ_3:63 .= card(((g|m1)^<*a*>)"{x})+card((g/^m)"{x}) by FINSEQ_3:63 .= card((g|m1)"{x})+card(<*a*>"{x})+card((g/^m)"{x}) by FINSEQ_3:63 .= card((g|m1)"{x})+card((g/^m)"{x})+card(<*a*>"{x}) by XCMPLX_1:1 .= card(((g|m1)^(g/^m))"{x})+card(<*a*>"{x}) by FINSEQ_3:63; hence card(fn"{x}) = card(((g|m1)^(g/^m))"{x}) by XCMPLX_1:2; end; then fn, (g|m1)^(g/^m) are_fiberwise_equipotent by RFINSEQ:def 1; then Product fn = Product((g|m1)^gg) by A3,A15; hence Product f = Product((g|m1)^gg)*Product <*a*> by A16,Lm8 .= Product(g|m1)*Product gg*Product <*a*> by Lm8 .= Product(g|m1)*Product <*a*>*Product gg by XCMPLX_1:4 .= Product gm*Product gg by A12,A14,Lm8 .= Product g by A8,Lm8; end; A17:for n holds P[n] from Ind(A1,A2); let R1,R2 be FinSequence of NAT; assume A18:R1,R2 are_fiberwise_equipotent; len R1 = len R1; hence thesis by A17,A18; end; begin::Modulus for Finite Sequence of Natural :::::::::::::::::::::::::::::::::::::::::::::::: :: :: :: Function of (FinSequence of NAT) mod 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 Seg len f holds g.k = F(k) from SeqLambda; 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 & x = g.y by FUNCT_1:def 5; A4:y in Seg len g by A3,FINSEQ_1:def 3; Seg len g is Subset of NAT by FINSUB_1:def 5; then reconsider y as Nat by A4; g.y = (f.y) mod m by A1,A2,A4; hence x in NAT by A3; 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 Seg len f by FINSEQ_1:def 3; hence g.k = (f.k) mod m by A2; end; uniqueness proof let fa,fb be FinSequence of NAT such that A5:len(f) = len(fa) & for i being Nat st i in dom f holds fa.i = (f.i) mod m and A6:len(f) = len(fb) & for i being Nat st i in dom f holds fb.i = (f.i) mod m; now let X be set such that A7:dom f = X; A8: dom f = Seg len f by FINSEQ_1:def 3 .= dom fa by A5,FINSEQ_1:def 3; A9: dom f = Seg len f by FINSEQ_1:def 3 .= dom fb by A6,FINSEQ_1:def 3; for i being Nat st i in X holds fa.i = fb.i proof given j being Nat such that A10: j in X & fa.j <> fb.j; j in X & fa.j <> (f.j) mod m by A6,A7,A10; hence contradiction by A5,A7; end; hence fa = fb by A7,A8,A9,FINSEQ_1:17; 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; A1:P[0] proof let f be FinSequence of NAT; assume A2:m <> 0 & len f=0; then A3:f = <*> NAT by FINSEQ_1:32; len (f mod m) = 0 by A2,Def1; hence thesis by A3,FINSEQ_1:32; end; A4:for n st P[n] holds P[n+1] proof let n; assume A5:P[n]; let f be FinSequence of NAT; assume A6:m <> 0 & len f = n+1; reconsider fn = f|n as FinSequence of NAT; A7:n <= n+1 by NAT_1:29; A8:n <= len f by A6,NAT_1:29; A9:len fn = n by A6,A7,TOPREAL1:3; A10: (Product f) mod m = (Product (fn ^ <* f.(n+1) *>)) mod m by A6,RFINSEQ :20 .= ((Product fn)*f.(n+1)) mod m by RVSUM_1:126; A11:len (f mod m) = n+1 by A6,Def1; A12:(f mod m)|n = fn mod m proof A13:len((f mod m)|n) = n by A7,A11,TOPREAL1:3; then A14:len((f mod m)|n) = len(fn mod m) by A9,Def1; 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 A15:1 <= i & i <= len ((f mod m)|n); then A16:i in Seg n by A13,FINSEQ_1:3; then A17: ((f mod m)|Seg n).i = (f mod m).i by FUNCT_1:72; i <= len f by A8,A13,A15,AXIOMS:22; then A18:i in dom f by A15,FINSEQ_3:27; A19: (f|n).i = ((f|Seg n).i) by TOPREAL1:def 1; i in dom fn by A9,A13,A15,FINSEQ_3:27; then (fn mod m).i = fn.i mod m by Def1 .= f.i mod m by A16,A19,FUNCT_1:72 .= (f mod m).i by A18,Def1; hence thesis by A17,TOPREAL1:def 1; end; hence thesis by A14,FINSEQ_1:18; end; 0<n+1 by NAT_1:19; then 0+1<=n+1 by NAT_1:38; then n+1 in dom f by A6,FINSEQ_3:27; then (f mod m).(n+1) = f.(n+1) mod m by Def1; then f mod m = (fn mod m) ^ <* f.(n+1) mod m *> by A11,A12,RFINSEQ:20; then Product (f mod m) mod m = ((Product (fn mod m))*(f.(n+1) mod m)) mod m by RVSUM_1:126 .= (((Product (fn mod m)) mod m)*((f.(n+1) mod m) mod m)) mod m by Th11 .= (((Product fn) mod m)*((f.(n+1) mod m) mod m)) mod m by A5,A6,A9 .= (((Product fn) mod m)*(f.(n+1) mod m)) mod m by Th7; hence thesis by A10,Th11; end; A20:for n holds P[n] from Ind(A1,A4); let f be FinSequence of NAT; assume A21:m <> 0; len(f) is Nat; hence thesis by A20,A21; end; theorem Th27:a <> 0 & m > 1 & n <> 0 & a*n mod m = n mod m & m,n are_relative_prime implies a mod m = 1 proof assume A1:a <> 0 & m > 1 & n <> 0 & a*n mod m = n mod m & m,n are_relative_prime; then A2:m <> 0; then consider k1 be Nat such that A3:a*n = m*k1+(a*n mod m) and (a*n mod m) < m by NAT_1:def 2; A4:(a*n mod m) = a*n-m*k1 by A3,XCMPLX_1:26; consider k2 be Nat such that A5:n = m*k2+(n mod m) and (n mod m) < m by A2,NAT_1:def 2; (n mod m) = n-m*k2 by A5,XCMPLX_1:26; then a*n-1*n = m*k1-m*k2 by A1,A4,XCMPLX_1:24; then (a-1)*n = m*k1-m*k2 by XCMPLX_1:40; then (a-1)*n = m*(k1-k2) by XCMPLX_1:40; then A6:m divides (a-1)*n by INT_1:def 9; reconsider t = (a-1),m,n as Integer; m,n are_relative_prime by A1,Th1; then m divides t by A6,INT_2:40; then consider tt be Integer such that A7:(a-1) = m*tt by INT_1:def 9; A8:a = m*tt+1 by A7,XCMPLX_1:27; a-1 >= 0 by A1,Lm3; then tt >= 0 by A1,A7,Th3; then reconsider tt,m as Nat by INT_1:16; a mod m = (((m*tt) mod m)+1) mod m by A8,GR_CY_1:2 .= (0+1) mod m by GROUP_4:101 .= 1 by A1,GR_CY_1:4; hence thesis; end; theorem for F holds (F mod m) mod m = F mod m proof let F; A1: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; A2: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; 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 A4:x in Seg len F by FINSEQ_1:def 3; Seg len F is Subset of NAT by FINSUB_1:def 5; then reconsider x as Nat by A4; ((F mod m) mod m).x = ((F mod m).x) mod m by A2,A3,Def1 .= (F.x mod m) mod m by A3,Def1 .= F.x mod m by Th7 .= (F mod m).x by A3,Def1; hence thesis; end; hence thesis by A1,A2,FUNCT_1:9; end; theorem for F holds (a*(F mod m)) mod m = (a*F) mod m proof let F; A1: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:6 .= Seg(len F) by Def1 .= 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:6 .= Seg(len F) by Def1 .= dom F by FINSEQ_1:def 3; A3: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:6 .= dom F by FINSEQ_1:def 3; A4:dom (a*F) = Seg(len(a*F)) by FINSEQ_1:def 3 .= Seg(len F) by NEWTON:6 .= dom F by FINSEQ_1:def 3; 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 A5:x in dom F; then A6:x in Seg len F by FINSEQ_1:def 3; Seg len F is Subset of NAT by FINSUB_1:def 5; then reconsider x as Nat by A6; ((a*(F mod m)) mod m).x = (a*(F mod m)).x mod m by A2,A5,Def1 .= (a*(F mod m).x ) mod m by RVSUM_1:66 .= (a*(F.x mod m)) mod m by A5,Def1 .= (a*F.x) mod m by Th9 .= (a*F).x mod m by RVSUM_1:66 .= ((a*F) mod m).x by A4,A5,Def1; hence thesis; end; hence thesis by A1,A3,FUNCT_1:9; 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 ((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:35 .= Seg(len(F)+len(G mod m)) by Def1 .= Seg(len(F)+len(G)) by Def1 .= Seg(len(F ^ G)) by FINSEQ_1:35 .= dom (F ^ 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: 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; 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 A6: x in Seg len (F ^ G) by FINSEQ_1:def 3; Seg len (F ^ G) is Subset of NAT by FINSUB_1:def 5; then reconsider x as Nat by A6; now per cases by A5,FINSEQ_1:38; suppose A7: x in dom F; A8:((F ^ G) mod m).x = (F ^ G).x mod m by A5,Def1 .= F.x mod m by A7,FINSEQ_1:def 7; ((F mod m) ^ (G mod m)).x = (F mod m).x by A3,A7,FINSEQ_1:def 7 .= F.x mod m by A7,Def1; hence ((F ^ G) mod m).x = ((F mod m) ^ (G mod m)).x by A8; suppose ex n being Nat st n in dom G & x=len F+n; then consider n being Nat such that A9:n in dom G & x=len F+n; A10: len (F mod m) = len F by Def1; A11:((F ^ G) mod m).x = (F ^ G).x mod m by A5,Def1 .= G.n mod m by A9,FINSEQ_1:def 7; ((F mod m) ^ (G mod m)).x = (G mod m).n by A4,A9,A10,FINSEQ_1:def 7 .= G.n mod m by A9,Def1; hence ((F ^ G) mod m).x = ((F mod m) ^ (G mod m)).x by A11; end; hence thesis; end; hence thesis by A1,A2,FUNCT_1:9; 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)) mod m) = Seg(len((a*FG) mod m)) by FINSEQ_1:def 3 .= Seg(len(a*FG)) by Def1 .= Seg(len(FG)) by NEWTON:6 .= dom (F ^ G) by FINSEQ_1:def 3; A2: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:35 .= 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:6 .= Seg(len(F)+len(G)) by NEWTON:6 .= Seg(len(F ^ G)) by FINSEQ_1:35 .= dom(F ^ G) by FINSEQ_1:def 3; A3:dom (a*(F ^ G)) = Seg(len(a*FG)) by FINSEQ_1:def 3 .= Seg(len(FG)) by NEWTON:6 .= dom (F ^ G) by FINSEQ_1:def 3; A4:dom (a*F) = Seg(len(a*F)) by FINSEQ_1:def 3 .= Seg(len F) by NEWTON:6 .= 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:6 .= dom F by FINSEQ_1:def 3; A6:dom (a*G) = Seg(len(a*G)) by FINSEQ_1:def 3 .= Seg(len G) by NEWTON:6 .= dom G by FINSEQ_1:def 3; A7: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:6 .= dom G by FINSEQ_1:def 3; 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 let x be set; assume A8:x in dom (F ^ G); reconsider H = F ^ G as FinSequence of NAT; A9: x in Seg len (F ^ G) by A8,FINSEQ_1:def 3; Seg len (F ^ G) is Subset of NAT by FINSUB_1:def 5; then reconsider x as Nat by A9; now per cases by A8,FINSEQ_1:38; suppose A10: x in dom F; A11:((a*(F ^ G)) mod m).x = ((a*(F ^ G)).x) mod m by A3,A8,Def1 .= (a*H.x) mod m by RVSUM_1:66 .= (a*(F.x)) mod m by A10,FINSEQ_1:def 7; (((a*F) mod m) ^ ((a*G) mod m)).x = ((a*F) mod m).x by A5,A10,FINSEQ_1:def 7 .= ((a*F).x) mod m by A4,A10,Def1 .= (a*(F.x)) mod m by RVSUM_1:66; hence ((a*(F ^ G)) mod m).x = (((a*F) mod m) ^ ((a*G) mod m)).x by A11; suppose ex n being Nat st n in dom G & x=len F+n; then consider n being Nat such that A12:n in dom G & x=len F+n; A13: len ((a*F) mod m) = len(a*F) by Def1 .= len F by NEWTON:6; A14:((a*(F ^ G)) mod m).x = ((a*(F ^ G)).x) mod m by A3,A8,Def1 .= (a*H.x) mod m by RVSUM_1:66 .= (a*G.n) mod m by A12,FINSEQ_1:def 7; (((a*F) mod m) ^ ((a*G) mod m)).x = ((a*G) mod m).n by A7,A12,A13,FINSEQ_1:def 7 .= ((a*G).n) mod m by A6,A12,Def1 .= (a*G.n) mod m by RVSUM_1:66; hence ((a*(F ^ G)) mod m).x = (((a*F) mod m) ^ ((a*G) mod m)).x by A14; end; hence thesis; end; hence thesis by A1,A2,FUNCT_1:9; end; ::::::::::::::::::::::::::::::::::: :: :: :: Function of (Nat) |^ (Nat) :: :: :: ::::::::::::::::::::::::::::::::::: definition let n,k; redefine func n |^ k -> Nat; coherence by URYSOHN1:8; end; theorem a <> 0 & m <> 0 & a,m are_relative_prime implies for b holds (a |^ b),m are_relative_prime proof assume A1:a <> 0 & m <> 0 & a,m are_relative_prime; A2:(a |^ 0) hcf m = 1 hcf m by NEWTON:9; defpred P[Nat] means (a |^ $1),m are_relative_prime; m hcf 1 = 1 by NAT_LAT:35; then A3:P[0] by A2,INT_2:def 6; A4:for b holds P[b] implies P[b+1] proof let b; assume A5:(a |^ b),m are_relative_prime; A6:(a |^ (b+1)) = (a |^ b)*(a |^ 1) by NEWTON:13 .= (a |^ b)*a by NEWTON:10; a |^ b <> 0 by A1,PREPOWER:12; hence thesis by A1,A5,A6,EULER_1:15; end; for b holds P[b] from Ind(A3,A4); hence thesis; end; begin:: Euler's Theorem and Small Fermat's Theorem :::::::::::::::::::::::::::::::::::::::::::::::: :: :: :: Euler's Theorem & Small Fermat's Theorem :: :: :: :::::::::::::::::::::::::::::::::::::::::::::::: theorem ::Euler's theorem Th33:a <> 0 & m > 1 & a,m are_relative_prime implies (a |^ Euler m) mod m = 1 proof assume A1:a <> 0 & m > 1 & a,m are_relative_prime; then A2:m <> 0; set X = {k where k is Nat : m,k are_relative_prime & k >= 1 & k <= m}; set Y = {l where l is Nat : ex u being Nat st l = a*u mod m & u in X}; ::Begin Euler's Lemma1 A3:x in X implies a*x mod m in X proof assume x in X; then consider t being Nat such that A4:t = x and A5:m,t are_relative_prime and A6:t >= 1 & t <= m; m hcf t = 1 by A5,INT_2:def 6; then A7:t,m are_relative_prime by INT_2:def 6; A8:t <> 0 by A6; then A9:a*t,m are_relative_prime by A1,A2,A7,EULER_1:15; m hcf t = 1 by A5,INT_2:def 6; then t,m are_relative_prime by INT_2:def 6; then A10:m,a*t mod m are_relative_prime by A1,A2,A8,Th5; a*t mod m <> 0 proof assume a*t mod m = 0; then consider s being Nat such that A11:a*t = m*s+0 and 0 < m by A2,NAT_1:def 2; s hcf 1 = 1 by NAT_LAT:35; then m*s hcf m*1 = m by EULER_1:6; hence contradiction by A1,A9,A11,INT_2:def 6; end; then A12:a*t mod m >= 1 by RLVECT_1:99; m > 0 by A2,NAT_1:19; then a*t mod m <= m by NAT_1:46; hence thesis by A4,A10,A12; end; ::End of Euler's Lemma1 ::Begin Euler's Lemma2 A13:xi in X & xj in X & xi <> xj implies a*xi mod m <> a*xj mod m proof assume A14:xi in X & xj in X & xi <> xj; assume A15:a*xi mod m = a*xj mod m; set tm = a*xi mod m,sm = a*xj mod m; A16:m > 0 by A2,NAT_1:19; consider t being Nat such that A17:t = xi and m,t are_relative_prime and A18:t >= 1 & t <= m by A14; A19:tm = (a*t)-m*((a*t) div m) by A16,A17,GR_CY_2:1; consider s being Nat such that A20:s = xj and m,s are_relative_prime and A21:s >= 1 & s <= m by A14; A22:sm = (a*s)-m*((a*s) div m) by A16,A20,GR_CY_2:1; tm-sm = 0 by A15,XCMPLX_1:14; then 0 = ((a*t)-m*((a*t) div m))-(a*s)+m*((a*s) div m) by A19,A22,XCMPLX_1:37 .= ((a*t)-(a*s)-m*((a*t) div m))+m*((a*s) div m) by XCMPLX_1:21 .= a*(t-s)-m*((a*t) div m)+m*((a*s) div m) by XCMPLX_1:40 .= a*(t-s)-(m*((a*t) div m)-m*((a*s) div m)) by XCMPLX_1:37 .= a*(t-s)-m*(((a*t) div m)-((a*s) div m)) by XCMPLX_1:40; then a*(t-s) = m*(((a*t) div m)-((a*s) div m)) by XCMPLX_1:15; then A23:m divides a*(t-s) by INT_1:def 9; reconsider m,a,c = (t-s) as Integer; a,m are_relative_prime by A1,Th1; then A24:m divides c by A23,INT_2:40; 1-m <= c & c <= m-1 by A18,A21,REAL_1:92; then t-s = 0 by A1,A24,Lm6; hence contradiction by A14,A17,A20,XCMPLX_1:15; end; ::End of Euler's Lemma2 ::Begin Euler's Lemma3 A25:X = Y proof thus X c= Y proof let x be set; assume x in X; then consider xx being Nat such that A26:x = xx and A27:m,xx are_relative_prime and A28:xx >= 1 & xx <= m; xx <> m by A1,A27,EULER_1:2; then xx < m by A28,AXIOMS:21; then A29:xx mod m = xx by GR_CY_1:4; A30:xx <> 0 by A28; consider i,j being Integer such that A31:i*a+j*m = xx by A1,EULER_1:11; i = (i div m)*m+(i mod m) by A2,GR_CY_2:4; then A32: xx = (i div m)*m*a+(i mod m)*a+j*m by A31,XCMPLX_1:8 .= (i mod m)*a+((i div m)*a)*m+j*m by XCMPLX_1:4 .= (i mod m)*a+(m*((i div m)*a)+m*j) by XCMPLX_1:1 .= (i mod m)*a+(((i div m)*a)+j)*m by XCMPLX_1:8; A33:m > 0 by A2,NAT_1:19; A34:i mod m <> 0 proof assume i mod m = 0; then 0 = i-(i div m)*m by A2,INT_1:def 8; then i = (i div m)*m by XCMPLX_1:15; then A35:xx = ((i div m)*a)*m+j*m by A31,XCMPLX_1:4 .= m*((i div m)*a+j) by XCMPLX_1:8; then A36:((i div m)*a+j) <> 0 & 1 <> 0 by A28; m gcd xx = m*1 gcd m*((i div m)*a+j) by A35 .= m*(1 gcd ((i div m)*a+j)) by A33,A36,EULER_1:16 .= m*1 by Lm4 .= m; then m hcf xx = m by A2,A30,Lm1; hence contradiction by A1,A27,INT_2:def 6; end; i mod m >= 0 by A33,GR_CY_2:2; then reconsider im = i mod m as Nat by INT_1:16; A37:im >= 1 by A34,RLVECT_1:99; A38:im <= m by A33,GR_CY_2:3; reconsider ij = (i mod m)*a+(((i div m)*a)+j)*m as Nat by A32; A39: ij mod m = ((i mod m)*a+(((i div m)*a)+j)*m) mod m by SCMFSA9A:5 .= (i mod m)*a mod m by EULER_1:13 .= im*a mod m by SCMFSA9A:5; then m,im are_relative_prime by A1,A27,A29,A32,A34,Th6; then im in X by A37,A38; hence x in Y by A26,A29,A32,A39; end; let y be set; assume y in Y; then consider yy being Nat such that A40:y = yy and A41:ex u being Nat st yy = a*u mod m & u in X; consider uu being Nat such that A42:yy = a*uu mod m and A43:uu in X by A41; thus y in X by A3,A40,A42,A43; end; ::End of Euler'S Lemma3 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; ::Begin Euler's Lemma4 A44:X c= Seg m proof let x be set; assume x in X; then consider xx being Nat such that A45:x = xx and m,xx are_relative_prime and A46:xx >= 1 & xx <= m; thus thesis by A45,A46,FINSEQ_1:3; end; ::End of Euler's Lemma4 then reconsider X as finite set by FINSET_1:13; A47:len(FX) = card X by A44,FINSEQ_3:44 .= Euler m by EULER_1:def 1; A48: dom FY = Seg(len FY) by FINSEQ_1:def 3 .= Seg(len FYY) by Def1 .= Seg(len FX) by NEWTON:6; then A49: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 A50:dom FX = dom FYY by FINSEQ_1:def 3; ::Begin Euler's Lemma5 A51: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 A52:y in dom FY & x = FY.y by FUNCT_1:def 5; A53:y in Seg len FY by A52,FINSEQ_1:def 3; Seg len FY is Subset of NAT by FINSUB_1:def 5; then reconsider y as Nat by A53; y in dom FX by A48,A52,FINSEQ_1:def 3; then A54: FY.y = (FYY.y) mod m by A50,Def1 .= (a*FX.y) mod m by RVSUM_1:66; FX.y in rng FX by A49,A52,FUNCT_1:def 5; then FX.y in X by A44,FINSEQ_1:def 13; hence thesis by A52,A54; end; let y be set; assume y in Y; then consider yy being Nat such that A55:y = yy and A56:ex u being Nat st yy = a*u mod m & u in X; consider uu being Nat such that A57:yy = a*uu mod m and A58:uu in X by A56; A59: Seg len FX is Subset of NAT by FINSUB_1:def 5; uu in rng FX by A44,A58,FINSEQ_1:def 13; then consider xx being set such that A60:xx in dom FX & uu = FX.xx by FUNCT_1:def 5; xx in Seg len FX by A60,FINSEQ_1:def 3; then reconsider xx as Nat by A59; FY.xx = (FYY.xx) mod m by A50,A60,Def1 .= y by A55,A57,A60,RVSUM_1:66; hence y in rng FY by A49,A60,FUNCT_1:def 5; end; ::End of Euler's Lemma5 ::Begin Euler's Lemma6 A61: FY is one-to-one proof let x1,x2 be set; assume A62: x1 in dom FY & x2 in dom FY & FY.x1 = FY.x2; then A63:x1 in dom FX & x2 in dom FX & FY.x1 = FY.x2 by A48,FINSEQ_1:def 3; A64:Seg len FX is Subset of NAT by FINSUB_1:def 5; then reconsider x1 as Nat by A48,A62; reconsider x2 as Nat by A48,A62,A64; A65: FY.x1 = (FYY.x1) mod m by A50,A63,Def1 .= (a*FX.x1) mod m by RVSUM_1:66; A66: FY.x2 = (FYY.x2) mod m by A50,A63,Def1 .= (a*FX.x2) mod m by RVSUM_1:66; A67: FX.x1 in rng FX by A49,A62,FUNCT_1:def 5; A68: FX.x2 in rng FX by A49,A62,FUNCT_1:def 5; A69:FX is one-to-one by A44,FINSEQ_3:99; not(FX.x1 in X & FX.x2 in X & FX.x1 <> FX.x2) by A13,A62,A65,A66; hence thesis by A44,A63,A67,A68,A69,FINSEQ_1:def 13,FUNCT_1:def 8; end; ::End of Euler's Lemma6 ::Begin Euler's Lemma7 for x be set holds card (FX"{x}) = card (FY"{x}) proof let x be set; now per cases; suppose A70: x in X; then A71: x in rng FX by A44,FINSEQ_1:def 13; FX is one-to-one by A44,FINSEQ_3:99; then len(FX-{x}) = len(FX)-1 by A71,FINSEQ_3:97; then 0 = len(FX)-1-len(FX-{x}) by XCMPLX_1:14 .= len(FX)-(1+len(FX-{x})) by XCMPLX_1:36 .= len(FX)-len(FX-{x})-1 by XCMPLX_1:36; then 0+1 = len(FX)-len(FX-{x})-1+1; then A72: 1 = len(FX)-len(FX-{x})-(1-1) by XCMPLX_1:37 .= len(FX)-len(FX-{x})-0; len(FX-{x})-len(FX-{x}) = len(FX)-card(FX"{x})-len(FX-{x}) by FINSEQ_3:66; then 0 = len(FX)-card(FX"{x})-len(FX-{x}) by XCMPLX_1:14 .= len(FX)-(card(FX"{x})+len(FX-{x})) by XCMPLX_1:36 .= len(FX)-len(FX-{x})-card(FX"{x}) by XCMPLX_1:36; then 0+card(FX"{x}) = len(FX)-len(FX-{x})-card(FX"{x})+card(FX"{x}); then A73: card(FX"{x}) = len(FX)-len(FX-{x})-(card(FX"{x})-card(FX"{x})) by XCMPLX_1:37 .= len(FX)-len(FX-{x})-0 by XCMPLX_1:14; len(FY-{x}) = len(FY)-1 by A25,A51,A61,A70,FINSEQ_3:97; then 0 = len(FY)-1-len(FY-{x}) by XCMPLX_1:14 .= len(FY)-(1+len(FY-{x})) by XCMPLX_1:36 .= len(FY)-len(FY-{x})-1 by XCMPLX_1:36; then 0+1 = len(FY)-len(FY-{x})-1 +1; then A74: 1 = len(FY)-len(FY-{x})-(1-1) by XCMPLX_1:37 .= len(FY)-len(FY-{x})-0; len(FY-{x}) = len(FY)-card(FY"{x}) by FINSEQ_3:66; then 0 = len(FY)-card(FY"{x})-len(FY-{x}) by XCMPLX_1:14 .= len(FY)-(card(FY"{x})+len(FY-{x})) by XCMPLX_1:36 .= len(FY)-len(FY-{x})-card(FY"{x}) by XCMPLX_1:36; then 0+card(FY"{x}) = len(FY)-len(FY-{x})-card(FY"{x})+card(FY"{x}); then card(FY"{x}) = len(FY)-len(FY-{x})-(card(FY"{x})-card(FY"{x})) by XCMPLX_1:37 .= len(FY)-len(FY-{x})-0 by XCMPLX_1:14; hence thesis by A72,A73,A74; suppose A75: not(x in X); then A76: not(x in rng FX) by A44,FINSEQ_1:def 13; FY"{x} = {} by A25,A51,A75,FUNCT_1:142; hence thesis by A76,FUNCT_1:142; end; hence thesis; end; ::End of Euler's Lemma7 then A77:FX,FY are_fiberwise_equipotent by RFINSEQ:def 1; then A78:(Product FX) mod m = (Product FY) mod m by Th25; A79:len(FX) = len(FY) by A77,RFINSEQ:16; ::Begin Euler's Lemma8 A80:(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; A81: P[0] proof 0 <= len FY by NAT_1:18; then A82: len (FY|0) = 0 by TOPREAL1:3; 0 <= len FX by NAT_1:18; then len (FX|0) = 0 by TOPREAL1:3; then Product (FX|0) = 1 by FINSEQ_1:25,RVSUM_1:124; then a |^ len(FY|0)*Product (FX|0) = 1 by A82,NEWTON:9; hence thesis by A82,FINSEQ_1:25,RVSUM_1:124; end; A83: for n st P[n] holds P[n+1] proof let n; now per cases; suppose A84: n+1 <= len FY; assume A85:P[n]; A86:n <= n+1 by NAT_1:29; then n <= len FY by A84,AXIOMS:22; then A87:len(FY|n) = n by TOPREAL1:3; A88:len (FY|(n+1)) = n+1 by A84,TOPREAL1:3; then A89:FY|(n+1) = (FY|(n+1))|n ^ <* (FY|(n+1)).(n+1) *> by RFINSEQ:20; 0 < n+1 by NAT_1:19; then 0+1 <= n+1 by NAT_1:38; then A90: n+1 in dom FY by A84,FINSEQ_3:27; A91:(FY|(n+1))|n = FY|n by A86,JORDAN4:15; A92: (FY|(n+1)).(n+1) = FY.(n+1) by JORDAN3:20; len (FX|(n+1)) = n+1 by A79,A84,TOPREAL1:3; then A93:FX|(n+1) = (FX|(n+1))|n ^ <* (FX|(n+1)).(n+1) *> by RFINSEQ:20; A94:(FX|(n+1))|n = FX|n by A86,JORDAN4:15; A95: (FX|(n+1)).(n+1) = FX.(n+1) by JORDAN3:20; (Product(FY|(n+1))) mod m = (Product(FY|n)*FY.(n+1)) mod m by A89,A91,A92,Lm7 .= (((a |^ len(FY|n)*Product(FX|n)) mod m) *(FY.(n+1) mod m)) mod m by A84,A85,A86,Th11,AXIOMS:22 .= (((a |^ len(FY|n)*Product(FX|n)) mod m) *((FYY.(n+1) mod m) mod m)) mod m by A49,A50,A90,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 |^ len(FY|n)*Product (FX|n))*(a*(FX.(n+1))) mod m by RVSUM_1:66 .= a |^ len(FY|n)*Product(FX|n)*a*(FX.(n+1)) mod m by XCMPLX_1:4 .= (a |^ len(FY|n)*a)*Product(FX|n)*(FX.(n+1)) mod m by XCMPLX_1:4 .= (a |^ n*a)*(Product(FX|n)*(FX.(n+1))) mod m by A87,XCMPLX_1:4 .= (a |^ len(FY|(n+1)))*(Product(FX|n)*(FX.(n+1))) mod m by A88,NEWTON:11 .= (a |^ len(FY|(n+1)))*(Product(FX|(n+1))) mod m by A93,A94,A95, Lm7; hence P[n+1]; suppose n+1 > len FY; hence thesis; end; hence thesis; end; A96: for n holds P[n] from Ind(A81,A83); FY|len FY = FY|(Seg len FY) by TOPREAL1:def 1; then A97:FY = FY|len FY by FINSEQ_2:23; FX|len FX = FX|(Seg len FX) by TOPREAL1:def 1; then FX = FX|len FY by A79,FINSEQ_2:23; hence thesis by A96,A97; end; ::End of Euler's Lemma8 A98: len FY = Euler m by A47,A77,RFINSEQ:16; A99:a |^ Euler m <> 0 by A1,PREPOWER:12; ::Begin Euler's Lemma9 A100:Product FX <> 0 proof assume Product FX = 0; then consider k such that A101:k in dom FX and A102:FX.k = 0 by RVSUM_1:133; A103:rng FX = X by A44,FINSEQ_1:def 13; FX.k in rng FX by A101,FUNCT_1:def 5; then consider p being Nat such that A104:FX.k = p and m,p are_relative_prime and A105:p >= 1 & p <= m by A103; thus contradiction by A102,A104,A105; end; ::End of Euler's Lemma9 ::Begin Euler's Lemma10 (Product FX),m are_relative_prime proof defpred P[Nat] means $1 <= len FX implies (Product (FX|$1)),m are_relative_prime; A106: P[0] proof 0 <= len FX by NAT_1:18; then len (FX|0) = 0 by TOPREAL1:3; then (Product (FX|0)) = 1 by FINSEQ_1:25,RVSUM_1:124; then (Product (FX|0)) hcf m = 1 by NAT_LAT:35; hence thesis by INT_2:def 6; end; A107: for n st P[n] holds P[n+1] proof let n; now per cases; suppose A108:len FX >= n+1; assume A109:P[n]; A110: n <= n+1 by NAT_1:29; reconsider FF = (FX|(n+1)) as FinSequence of NAT; reconsider ff = FF.(n+1) as Nat; len FF = n+1 by A108,TOPREAL1:3; then A111:FF = (FF|n) ^ <*ff*> by RFINSEQ:20; n <= n+1 by NAT_1:29; then A112:FX|n = FF|n by JORDAN4:15; A113:rng FX = X by A44,FINSEQ_1:def 13; A114:(FX|(n+1)).(n+1) = FX.(n+1) by JORDAN3:20; n >= 0 by NAT_1:18; then 0+1 <= (n+1) by AXIOMS:24; then n+1 in dom FX by A108,FINSEQ_3:27; then (FX|(n+1)).(n+1) in rng FX by A114,FUNCT_1:def 5; then consider p being Nat such that A115:ff = p and A116:m,p are_relative_prime and p >= 1 & p <= m by A113; reconsider a = (Product (FF|n)),b = ff,m' = m as Integer; A117:a,m' are_relative_prime by A108,A109,A110,A112,Th1,AXIOMS:22; b,m' are_relative_prime by A115,A116,Th1; then a*b,m' are_relative_prime by A117,INT_2:41; then (Product ((FF|n) ^ <*ff*>)),m' are_relative_prime by Lm7; hence P[n+1] by A111,Th1; suppose len FX < n+1; hence thesis; end; hence thesis; end; A118:for n holds P[n] from Ind(A106,A107); FX|len(FX) = FX by TOPREAL1:2; hence thesis by A118; end; ::End of Euler's Lemma10 then m,(Product FX) are_relative_prime by Lm5; hence thesis by A1,A78,A80,A98,A99,A100,Th27; end; ::End of Euler'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 A1: a<>0 & m is prime & a,m are_relative_prime; then A2: m > 1 by INT_2:def 5; then m-1 > 1-1 by REAL_1:54; then reconsider mm = m-1 as Nat by INT_1:16; A3:mm+1 = m-(1-1) by XCMPLX_1:37 .= m; Euler m = m-1 by A1,EULER_1:21; then ((a |^ mm) mod m)*a = 1*a by A1,A2,Th33; then ((a |^ mm)*a) mod m = a mod m by Th10; hence thesis by A3,NEWTON:11; end;