:: EULER_2 semantic presentation

Lemma1: for b₁, b₂ being Nat holds b₁ gcd b₂ = b₁ hcf b₂

proof end;

Lemma2: for b₁ being Integer holds
( b₁ < 1 iff b₁ <= 0 )

proof end;

Lemma3: for b₁ being Nat st b₁ <> 0 holds
b₁ - 1 >= 0

proof end;

Lemma4: for b₁ being Integer holds 1 gcd b₁ = 1

proof end;

theorem Th1: :: EULER_2:1

for b₁, b₂ being Nat holds
( b₁,b₂ are_relative_prime iff b₁,b₂ are_relative_prime )

proof end;

theorem Th2: :: EULER_2:2

for b₁ being Nat
for b₂ being Integer st b₁ > 1 & b₁ * b₂ >= 1 holds
b₂ >= 1

proof end;

Lemma7: for b₁ being Nat
for b₂ being Integer st b₁ > 1 & 1 - b₁ <= b₂ & b₂ <= b₁ - 1 & b₁ divides b₂ holds
b₂ = 0

proof end;

Lemma8: for b₁ being Nat
for b₂ being Integer st b₁ > 1 & b₁ * b₂ >= 0 holds
b₂ >= 0
by REAL_2:145;

theorem Th3: :: EULER_2:3

canceled;

theorem Th4: :: EULER_2:4

canceled;

theorem Th5: :: EULER_2:5

for b₁, b₂, b₃ being Nat st b₁ <> 0 & b₂ <> 0 & b₃ <> 0 & b₁,b₃ are_relative_prime & b₂,b₃ are_relative_prime holds
b₃,(b₁ * b₂) mod b₃ are_relative_prime

proof end;

theorem Th6: :: EULER_2:6

for b₁, b₂, b₃, b₄ being Nat st b₁ > 1 & b₂ <> 0 & b₁,b₃ are_relative_prime & b₄,b₁ are_relative_prime & b₃ = (b₄ * b₂) mod b₁ holds
b₁,b₂ are_relative_prime

proof end;

theorem Th7: :: EULER_2:7

for b₁, b₂ being Nat holds (b₁ mod b₂) mod b₂ = b₁ mod b₂

proof end;

theorem Th8: :: EULER_2:8

for b₁, b₂, b₃ being Nat holds (b₁ + b₂) mod b₃ = ((b₁ mod b₃) + (b₂ mod b₃)) mod b₃

proof end;

theorem Th9: :: EULER_2:9

for b₁, b₂, b₃ being Nat holds (b₁ * b₂) mod b₃ = (b₁ * (b₂ mod b₃)) mod b₃

proof end;

theorem Th10: :: EULER_2:10

for b₁, b₂, b₃ being Nat holds (b₁ * b₂) mod b₃ = ((b₁ mod b₃) * b₂) mod b₃ by Th9;

theorem Th11: :: EULER_2:11

for b₁, b₂, b₃ being Nat holds (b₁ * b₂) mod b₃ = ((b₁ mod b₃) * (b₂ mod b₃)) mod b₃

proof end;

definition

let c₁ be Nat;
let c₂ be FinSequence of NAT ;
redefine func * as c₁ * c₂ -> FinSequence of NAT ;
coherence

proof end;

end;

Lemma14: for b₁ being FinSequence of NAT
for b₂ being Nat holds Product (b₁ ^ <*b₂*>) = (Product b₁) * b₂
by RVSUM_1:126;

Lemma15: for b₁, b₂ being FinSequence of NAT holds Product (b₁ ^ b₂) = (Product b₁) * (Product b₂)
by RVSUM_1:127;

theorem Th12: :: EULER_2:12

canceled;

theorem Th13: :: EULER_2:13

canceled;

theorem Th14: :: EULER_2:14

canceled;

theorem Th15: :: EULER_2:15

canceled;

theorem Th16: :: EULER_2:16

canceled;

theorem Th17: :: EULER_2:17

canceled;

theorem Th18: :: EULER_2:18

canceled;

theorem Th19: :: EULER_2:19

canceled;

theorem Th20: :: EULER_2:20

canceled;

theorem Th21: :: EULER_2:21

canceled;

theorem Th22: :: EULER_2:22

canceled;

theorem Th23: :: EULER_2:23

canceled;

theorem Th24: :: EULER_2:24

canceled;

theorem Th25: :: EULER_2:25

for b₁, b₂ being FinSequence of NAT st b₁,b₂ are_fiberwise_equipotent holds
Product b₁ = Product b₂

proof end;

definition

let c₁ be FinSequence of NAT ;
let c₂ be Nat;
func c₁ mod c₂ -> FinSequence of NAT means :Def1: :: EULER_2:def 1
( len a₃ = len a₁ & ( for b₁ being Nat st b₁ in dom a₁ holds
a₃ . b₁ = (a₁ . b₁) mod a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines mod EULER_2:def 1 :

theorem Th26: :: EULER_2:26

for b₁ being Nat
for b₂ being FinSequence of NAT st b₁ <> 0 holds
(Product (b₂ mod b₁)) mod b₁ = (Product b₂) mod b₁

proof end;

theorem Th27: :: EULER_2:27

for b₁, b₂, b₃ being Nat st b₁ <> 0 & b₂ > 1 & b₃ <> 0 & (b₁ * b₃) mod b₂ = b₃ mod b₂ & b₂,b₃ are_relative_prime holds
b₁ mod b₂ = 1

proof end;

theorem Th28: :: EULER_2:28

for b₁ being Nat
for b₂ being FinSequence of NAT holds (b₂ mod b₁) mod b₁ = b₂ mod b₁

proof end;

theorem Th29: :: EULER_2:29

for b₁, b₂ being Nat
for b₃ being FinSequence of NAT holds (b₁ * (b₃ mod b₂)) mod b₂ = (b₁ * b₃) mod b₂

proof end;

theorem Th30: :: EULER_2:30

for b₁ being Nat
for b₂, b₃ being FinSequence of NAT holds (b₂ ^ b₃) mod b₁ = (b₂ mod b₁) ^ (b₃ mod b₁)

proof end;

theorem Th31: :: EULER_2:31

for b₁, b₂ being Nat
for b₃, b₄ being FinSequence of NAT holds (b₁ * (b₃ ^ b₄)) mod b₂ = ((b₁ * b₃) mod b₂) ^ ((b₁ * b₄) mod b₂)

proof end;

definition

let c₁, c₂ be Nat;
redefine func |^ as c₁ |^ c₂ -> Nat;
coherence by NEWTON:99;

end;

theorem Th32: :: EULER_2:32

for b₁, b₂ being Nat st b₁ <> 0 & b₂ <> 0 & b₁,b₂ are_relative_prime holds
for b₃ being Nat holds b₁ |^ b₃,b₂ are_relative_prime

proof end;

theorem Th33: :: EULER_2:33

for b₁, b₂ being Nat st b₁ <> 0 & b₂ > 1 & b₁,b₂ are_relative_prime holds
(b₁ |^ (Euler b₂)) mod b₂ = 1

proof end;

theorem Th34: :: EULER_2:34

for b₁, b₂ being Nat st b₁ <> 0 & b₂ is prime & b₁,b₂ are_relative_prime holds
(b₁ |^ b₂) mod b₂ = b₁ mod b₂

proof end;