:: EULER_1 semantic presentation

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

proof end;

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

proof end;

Lemma3: for b₁, b₂ being Nat
for b₃ being Integer st b₃ > 0 & b₁ = b₃ & b₂ > 0 holds
b₃ mod b₂ = b₁ mod b₂

proof end;

Lemma4: for b₁, b₂ being Nat
for b₃ being Integer holds
( b₁ = b₃ & b₂ > 0 & b₂ divides b₃ iff ( b₁ = b₃ & b₂ > 0 & b₂ divides b₁ ) )

proof end;

Lemma5: for b₁ being Nat
for b₂ being Integer st b₁ <> 0 & [\(b₂ / b₁)/] + 1 >= b₂ / b₁ holds
b₁ >= b₂ - ([\(b₂ / b₁)/] * b₁)

proof end;

theorem Th1: :: EULER_1:1

for b₁, b₂ being natural number holds
( b₁ in b₂ iff b₁ < b₂ )

proof end;

Lemma7: not 1 is prime
by INT_2:def 5;

theorem Th2: :: EULER_1:2

for b₁ being Nat holds
( b₁,b₁ are_relative_prime iff b₁ = 1 )

proof end;

theorem Th3: :: EULER_1:3

for b₁, b₂ being Nat st b₁ <> 0 & b₁ < b₂ & b₂ is prime holds
b₁,b₂ are_relative_prime

proof end;

theorem Th4: :: EULER_1:4

for b₁, b₂ being Nat holds
( b₁ is prime & b₂ in { b₃ where B is Nat : ( b₁,b₃ are_relative_prime & b₃ >= 1 & b₃ <= b₁ ) } iff ( b₁ is prime & b₂ in b₁ & not b₂ in {0} ) )

proof end;

theorem Th5: :: EULER_1:5

for b₁ being finite set
for b₂ being set st b₂ in b₁ holds
card (b₁ \ {b₂}) = (card b₁) - (card {b₂})

proof end;

theorem Th6: :: EULER_1:6

for b₁, b₂ being Nat st b₁ hcf b₂ = 1 holds
for b₃ being Nat holds (b₁ * b₃) hcf (b₂ * b₃) = b₃

proof end;

theorem Th7: :: EULER_1:7

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

proof end;

theorem Th8: :: EULER_1:8

for b₁, b₂ being Nat st b₁ hcf b₂ = 1 holds
(b₁ + b₂) hcf b₂ = 1

proof end;

theorem Th9: :: EULER_1:9

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

proof end;

theorem Th10: :: EULER_1:10

for b₁, b₂ being Nat st b₁,b₂ are_relative_prime holds
ex b₃ being Nat st
( ex b₄, b₅ being Integer st
( b₃ = (b₄ * b₁) + (b₅ * b₂) & b₃ > 0 ) & ( for b₄ being Nat st ex b₅, b₆ being Integer st
( b₄ = (b₅ * b₁) + (b₆ * b₂) & b₄ > 0 ) holds
b₃ <= b₄ ) )

proof end;

theorem Th11: :: EULER_1:11

for b₁, b₂ being Nat st b₁,b₂ are_relative_prime holds
for b₃ being Nat ex b₄, b₅ being Integer st (b₄ * b₁) + (b₅ * b₂) = b₃

proof end;

theorem Th12: :: EULER_1:12

for b₁, b₂ being non empty finite set st ex b₃ being Function of b₁,b₂ st
( b₃ is one-to-one & b₃ is onto ) holds
Card b₁ = Card b₂

proof end;

theorem Th13: :: EULER_1:13

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

proof end;

theorem Th14: :: EULER_1:14

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

proof end;

theorem Th15: :: EULER_1:15

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₃ are_relative_prime

proof end;

theorem Th16: :: EULER_1:16

for b₁, b₂, b₃ being Integer st b₁ <> 0 & b₂ <> 0 & b₃ > 0 holds
(b₃ * b₁) gcd (b₃ * b₂) = b₃ * (b₁ gcd b₂)

proof end;

theorem Th17: :: EULER_1:17

for b₁, b₂ being Nat
for b₃ being Integer st b₁ <> 0 & b₂ <> 0 holds
(b₁ + (b₃ * b₂)) gcd b₂ = b₁ gcd b₂

proof end;

definition

let c₁ be Nat;
func Euler c₁ -> Nat equals :: EULER_1:def 1
Card { b₁ where B is Nat : ( a₁,b₁ are_relative_prime & b₁ >= 1 & b₁ <= a₁ ) } ;
coherence

proof end;

end;

:: deftheorem Def1 defines Euler EULER_1:def 1 :

set c₁ = { b₁ where B is Nat : ( 1,b₁ are_relative_prime & b₁ >= 1 & b₁ <= 1 ) } ;

for b₁ being set holds
( b₁ in { b₂ where B is Nat : ( 1,b₂ are_relative_prime & b₂ >= 1 & b₂ <= 1 ) } iff b₁ = 1 )

proof end;

then E24: Card {1} = Card { b₁ where B is Nat : ( 1,b₁ are_relative_prime & b₁ >= 1 & b₁ <= 1 ) } by TARSKI:def 1
.= Euler 1 ;

theorem Th18: :: EULER_1:18

Euler 1 = 1 by Lemma24, CARD_1:79;

set c₂ = { b₁ where B is Nat : ( 2,b₁ are_relative_prime & b₁ >= 1 & b₁ <= 2 ) } ;

for b₁ being set holds
( b₁ in { b₂ where B is Nat : ( 2,b₂ are_relative_prime & b₂ >= 1 & b₂ <= 2 ) } iff b₁ = 1 )

proof end;

then E25: Card {1} = Card { b₁ where B is Nat : ( 2,b₁ are_relative_prime & b₁ >= 1 & b₁ <= 2 ) } by TARSKI:def 1
.= Euler 2 ;

theorem Th19: :: EULER_1:19

Euler 2 = 1 by Lemma25, CARD_1:79;

theorem Th20: :: EULER_1:20

for b₁ being Nat st b₁ > 1 holds
Euler b₁ <= b₁ - 1

proof end;

theorem Th21: :: EULER_1:21

for b₁ being Nat st b₁ is prime holds
Euler b₁ = b₁ - 1

proof end;

theorem Th22: :: EULER_1:22

for b₁, b₂ being Nat st b₁ > 1 & b₂ > 1 & b₁,b₂ are_relative_prime holds
Euler (b₁ * b₂) = (Euler b₁) * (Euler b₂)

proof end;