:: 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-2016 Association of Mizar Users

environ

vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, FUNCT_1, XBOOLE_0;
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, NUMBERS, XCMPLX_1, XREAL_1, FINSEQ_5, XXREAL_0, ORDINAL1, NAT_D, CLASSES1;
schemes NAT_1, FINSEQ_1;
registrations FUNCT_1, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, NEWTON, VALUED_0, FINSET_1, CARD_1;
constructors HIDDEN, REAL_1, SQUARE_1, NAT_1, NAT_D, NEWTON, RFINSEQ, WSIERP_1, EULER_1, RECDEF_1, CLASSES1, BINOP_2, RELSET_1, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities RELAT_1;
expansions FUNCT_1;


Lm1: for t being Integer holds
( t < 1 iff t <= 0 )
proof end;

Lm2: for a being Nat st a <> 0 holds
a - 1 >= 0
proof end;

Lm3: for z being Integer holds 1 gcd z = 1
proof end;

:: Very useful theorem
theorem :: EULER_2:1
for a, b being Nat holds
( a,b are_coprime iff a,b are_coprime ) ;

theorem Th2: :: EULER_2:2
for m being Nat
for t being Integer st m * t >= 1 holds
t >= 1
proof end;

Lm4: for m being Nat
for z being Integer st 1 - m <= z & z <= m - 1 & m divides z holds
z = 0
proof end;

theorem Th3: :: EULER_2:3
for a, b, m being Nat st a <> 0 & b <> 0 & m <> 0 & a,m are_coprime & b,m are_coprime holds
m,(a * b) mod m are_coprime
proof end;

theorem Th4: :: EULER_2:4
for a, b, m, n being Nat st m > 1 & m,n are_coprime & n = (a * b) mod m holds
m,b are_coprime
proof end;

theorem Th5: :: EULER_2:5
for m, n being Nat holds (m mod n) mod n = m mod n
proof end;

theorem :: EULER_2:6
for m, n, l being Nat holds (l + m) mod n = ((l mod n) + (m mod n)) mod n
proof end;

theorem Th7: :: EULER_2:7
for m, n, l being Nat holds (l * m) mod n = (l * (m mod n)) mod n
proof end;

theorem :: EULER_2:8
for m, n, l being Nat holds (l * m) mod n = ((l mod n) * m) mod n by Th7;

theorem Th9: :: EULER_2:9
for m, n, l being Nat holds (l * m) mod n = ((l mod n) * (m mod n)) mod n
proof end;

definition
let f be FinSequence of NAT ;
let a be Nat;
:: original: *
redefine func a * f -> FinSequence of NAT ;
coherence
a * f is FinSequence of NAT
proof end;
end;

theorem Th10: :: EULER_2:10
for R1, R2 being FinSequence of NAT st R1,R2 are_fiberwise_equipotent holds
Product R1 = Product R2
proof end;

:: Function of (FinSequence of NAT) mod Element of NAT
definition
let f be FinSequence of NAT ;
let m be Nat;
func f mod m -> FinSequence of NAT means :Def1: :: EULER_2:def 1
( len it = len f & ( for i being Nat st i in dom f holds
it . i = (f . i) mod m ) );
existence
ex b1 being FinSequence of NAT st
( len b1 = len f & ( for i being Nat st i in dom f holds
b1 . i = (f . i) mod m ) )
proof end;
uniqueness
for b1, b2 being FinSequence of NAT st len b1 = len f & ( for i being Nat st i in dom f holds
b1 . i = (f . i) mod m ) & len b2 = len f & ( for i being Nat st i in dom f holds
b2 . i = (f . i) mod m ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines mod EULER_2:def 1 :
for f being FinSequence of NAT
for m being Nat
for b3 being FinSequence of NAT holds
( b3 = f mod m iff ( len b3 = len f & ( for i being Nat st i in dom f holds
b3 . i = (f . i) mod m ) ) );

theorem :: EULER_2:11
for m being Nat
for f being FinSequence of NAT st m <> 0 holds
(Product (f mod m)) mod m = (Product f) mod m
proof end;

theorem Th12: :: EULER_2:12
for a, m, n being Nat st a <> 0 & m > 1 & (a * n) mod m = n mod m & m,n are_coprime holds
a mod m = 1
proof end;

theorem :: EULER_2:13
for m being Nat
for F being FinSequence of NAT holds (F mod m) mod m = F mod m
proof end;

theorem :: EULER_2:14
for a, m being Nat
for F being FinSequence of NAT holds (a * (F mod m)) mod m = (a * F) mod m
proof end;

theorem :: EULER_2:15
for m being Nat
for F, G being FinSequence of NAT holds (F ^ G) mod m = (F mod m) ^ (G mod m)
proof end;

theorem :: EULER_2:16
for a, m being Nat
for F, G being FinSequence of NAT holds (a * (F ^ G)) mod m = ((a * F) mod m) ^ ((a * G) mod m)
proof end;

:: Function of (Element of NAT) |^ (Element of NAT)
theorem :: EULER_2:17
for a, m being Nat st a <> 0 & m <> 0 & a,m are_coprime holds
for b being Nat holds a |^ b,m are_coprime
proof end;

:: WP: Euler's Generalization of Fermat's Little Theorem
theorem Th18: :: EULER_2:18
for a, m being Nat st a <> 0 & m > 1 & a,m are_coprime holds
(a |^ (Euler m)) mod m = 1
proof end;

::End of Euler's Theorem
:: WP: Small Fermat's Theorem
theorem :: EULER_2:19
for a, m being Nat st a <> 0 & m is prime & a,m are_coprime holds
(a |^ m) mod m = a mod m
proof end;