:: 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-2021 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, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, CARD_1, RELAT_1, FUNCT_1, RECDEF_1, INT_1, INT_2, FINSET_1, 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, RECDEF_1, CLASSES1, BINOP_2, RELSET_1, NUMBERS; registrations FUNCT_1, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, NEWTON, VALUED_0, FINSET_1, CARD_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminary reserve a,b,m,x,n,l,xi,xj for Nat, t,z for Integer, f,F for FinSequence of NAT; :: Very useful theorem theorem :: EULER_2:1 a,(b qua Integer) are_coprime iff a,b are_coprime; theorem :: EULER_2:2 m*t >= 1 implies t >= 1; theorem :: EULER_2:3 a <> 0 & b <> 0 & m <> 0 & a,m are_coprime & b,m are_coprime implies m,a*b mod m are_coprime; theorem :: EULER_2:4 m > 1 & m,n are_coprime & n = a*b mod m implies m,b are_coprime; theorem :: EULER_2:5 (m mod n) mod n = m mod n; theorem :: EULER_2:6 (l+m) mod n = ((l mod n)+(m mod n)) mod n; theorem :: EULER_2:7 (l*m) mod n = (l*(m mod n)) mod n; theorem :: EULER_2:8 (l*m) mod n = ((l mod n)*m) mod n; theorem :: EULER_2:9 (l*m) mod n = ((l mod n)*(m mod n)) mod n; begin :: Function of Element of NAT*(FinSequence of NAT) definition let f,a; redefine func a*f -> FinSequence of NAT; end; theorem :: EULER_2:10 for R1,R2 be FinSequence of NAT st R1,R2 are_fiberwise_equipotent holds Product R1 = Product R2; 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 :: EULER_2:def 1 len(it) = len(f) & for i being Nat st i in dom f holds it.i = (f.i) mod m; end; theorem :: EULER_2:11 for f be FinSequence of NAT st m <> 0 holds (Product(f mod m)) mod m = (Product f) mod m; theorem :: EULER_2:12 a <> 0 & m > 1 & a*n mod m = n mod m & m,n are_coprime implies a mod m = 1; theorem :: EULER_2:13 (F mod m) mod m = F mod m; theorem :: EULER_2:14 (a*(F mod m)) mod m = (a*F) mod m; theorem :: EULER_2:15 for F,G being FinSequence of NAT holds (F ^ G) mod m = (F mod m) ^ (G mod m); theorem :: EULER_2:16 for F,G being FinSequence of NAT holds (a*(F ^ G)) mod m = ((a*F) mod m) ^ ((a*G) mod m); :: Function of (Element of NAT) |^ (Element of NAT) theorem :: EULER_2:17 a <> 0 & m <> 0 & a,m are_coprime implies for b holds a |^ b,m are_coprime; begin :: Euler's Theorem and Small Fermat's Theorem ::$N Euler's Generalization of Fermat's Little Theorem theorem :: EULER_2:18 a <> 0 & m > 1 & a,m are_coprime implies (a |^ Euler m) mod m = 1; ::End of Euler's Theorem ::$N Small Fermat's Theorem theorem :: EULER_2:19 ::Small Fermat's theorem a <> 0 & m is prime & a,m are_coprime implies (a |^ m) mod m = a mod m;