:: EULER_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for a, b being Nat holds a gcd b = a hcf b
proof end;

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

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

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

theorem Th1: :: EULER_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Nat holds
( a,b are_relative_prime iff a,b are_relative_prime )
proof end;

theorem Th2: :: EULER_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Nat
for t being Integer st m > 1 & m * t >= 1 holds
t >= 1
proof end;

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

Lm6: for m being Nat
for t being Integer st m > 1 & m * t >= 0 holds
t >= 0
by REAL_2:145;

theorem :: EULER_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: EULER_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th5: :: EULER_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, m being Nat st a <> 0 & b <> 0 & m <> 0 & a,m are_relative_prime & b,m are_relative_prime holds
m,(a * b) mod m are_relative_prime
proof end;

theorem Th6: :: EULER_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, b, n, a being Nat st m > 1 & b <> 0 & m,n are_relative_prime & a,m are_relative_prime & n = (a * b) mod m holds
m,b are_relative_prime
proof end;

theorem Th7: :: EULER_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n being Nat holds (m mod n) mod n = m mod n
proof end;

theorem :: EULER_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for l, m, n being Nat holds (l + m) mod n = ((l mod n) + (m mod n)) mod n
proof end;

theorem Th9: :: EULER_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for l, m, n being Nat holds (l * m) mod n = (l * (m mod n)) mod n
proof end;

theorem :: EULER_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for l, m, n being Nat holds (l * m) mod n = ((l mod n) * m) mod n by Th9;

theorem Th11: :: EULER_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for l, m, n being Nat holds (l * m) mod n = ((l mod n) * (m mod n)) mod n
proof end;

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

Lm7: for f being FinSequence of NAT
for r being Nat holds Product (f ^ <*r*>) = (Product f) * r
by RVSUM_1:126;

Lm8: for f1, f2 being FinSequence of NAT holds Product (f1 ^ f2) = (Product f1) * (Product f2)
by RVSUM_1:127;

theorem :: EULER_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: EULER_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: EULER_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: EULER_2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: EULER_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: EULER_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: EULER_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: EULER_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: EULER_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: EULER_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: EULER_2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: EULER_2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: EULER_2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th25: :: EULER_2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R1, R2 being FinSequence of NAT st R1,R2 are_fiberwise_equipotent holds
Product R1 = Product R2
proof end;

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:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th27: :: EULER_2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, m, n being Nat st a <> 0 & m > 1 & n <> 0 & (a * n) mod m = n mod m & m,n are_relative_prime holds
a mod m = 1
proof end;

theorem :: EULER_2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Nat
for F being FinSequence of NAT holds (F mod m) mod m = F mod m
proof end;

theorem :: EULER_2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

definition
let n, k be Nat;
:: original: |^
redefine func n |^ k -> Nat;
coherence
n |^ k is Nat by NEWTON:99;
end;

theorem :: EULER_2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, m being Nat st a <> 0 & m <> 0 & a,m are_relative_prime holds
for b being Nat holds a |^ b,m are_relative_prime
proof end;

theorem Th33: :: EULER_2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, m being Nat st a <> 0 & m > 1 & a,m are_relative_prime holds
(a |^ (Euler m)) mod m = 1
proof end;

theorem :: EULER_2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, m being Nat st a <> 0 & m is prime & a,m are_relative_prime holds
(a |^ m) mod m = a mod m
proof end;