:: by Yoshinori Fujisawa , Yasushi Fuwa and Hidetaka Shimizu

::

:: Received June 10, 1998

:: Copyright (c) 1998-2016 Association of Mizar Users

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

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

m,(a * b) mod m are_coprime

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

end;
let a be Nat;

:: original: *

redefine func a * f -> FinSequence of NAT ;

coherence

a * f is FinSequence of NAT

proof end;

:: Function of (FinSequence of NAT) mod Element of NAT

definition

let f be FinSequence of NAT ;

let m be Nat;

ex b_{1} being FinSequence of NAT st

( len b_{1} = len f & ( for i being Nat st i in dom f holds

b_{1} . i = (f . i) mod m ) )

for b_{1}, b_{2} being FinSequence of NAT st len b_{1} = len f & ( for i being Nat st i in dom f holds

b_{1} . i = (f . i) mod m ) & len b_{2} = len f & ( for i being Nat st i in dom f holds

b_{2} . i = (f . i) mod m ) holds

b_{1} = b_{2}

end;
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 ( len it = len f & ( for i being Nat st i in dom f holds

it . i = (f . i) mod m ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines mod EULER_2:def 1 :

for f being FinSequence of NAT

for m being Nat

for b_{3} being FinSequence of NAT holds

( b_{3} = f mod m iff ( len b_{3} = len f & ( for i being Nat st i in dom f holds

b_{3} . i = (f . i) mod m ) ) );

for f being FinSequence of NAT

for m being Nat

for b

( b

b

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

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

a mod m = 1

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)

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

for b being Nat holds a |^ b,m are_coprime

proof end;