:: NAT_3 semantic presentation

Lemma1: for b₁ being natural number
for b₂ being set st b₂ in Seg b₁ holds
b₂ is Nat
;

registration

let c₁ be empty set ;
cluster Card a₁ -> empty ;
coherence by CARD_1:47;

end;

registration

cluster natural-yielding -> real-yielding set ;
coherence

proof end;

end;

registration

cluster real-yielding natural-yielding set ;
existence

proof end;

end;

registration

let c₁ be non empty natural number ;
let c₂ be natural number ;
cluster a₁ |^ a₂ -> non empty ;
coherence

proof end;

end;

registration

cluster -> non empty Element of NAT ;
coherence

proof end;

end;

theorem Th1: :: NAT_3:1

for b₁, b₂, b₃, b₄ being natural number st b₁ divides b₃ & b₂ divides b₄ holds
b₁ * b₂ divides b₃ * b₄

proof end;

theorem Th2: :: NAT_3:2

for b₁, b₂ being natural number st 1 < b₁ holds
b₂ <= b₁ |^ b₂

proof end;

theorem Th3: :: NAT_3:3

for b₁, b₂ being natural number st b₁ <> 0 holds
b₂ divides b₂ |^ b₁

proof end;

theorem Th4: :: NAT_3:4

for b₁, b₂, b₃, b₄ being natural number st b₁ < b₂ & b₃ |^ b₂ divides b₄ holds
b₃ |^ (b₁ + 1) divides b₄

proof end;

theorem Th5: :: NAT_3:5

for b₁, b₂ being natural number
for b₃ being Prime st b₃ divides b₁ |^ b₂ holds
b₃ divides b₁

proof end;

theorem Th6: :: NAT_3:6

for b₁ being natural number
for b₂, b₃ being Prime st b₃ divides b₂ |^ b₁ holds
b₃ = b₂

proof end;

theorem Th7: :: NAT_3:7

for b₁ being natural number
for b₂ being FinSequence of NAT st b₁ in rng b₂ holds
b₁ divides Product b₂

proof end;

theorem Th8: :: NAT_3:8

for b₁ being Prime
for b₂ being FinSequence of SetPrimes st b₁ divides Product b₂ holds
b₁ in rng b₂

proof end;

definition

let c₁ be real-yielding FinSequence;
let c₂ be natural number ;
func c₁ |^ c₂ -> FinSequence means :Def1: :: NAT_3:def 1
( len a₃ = len a₁ & ( for b₁ being set st b₁ in dom a₃ holds
a₃ . b₁ = (a₁ . b₁) |^ a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines |^ NAT_3:def 1 :

registration

let c₁ be real-yielding FinSequence;
let c₂ be natural number ;
cluster a₁ |^ a₂ -> real-yielding ;
coherence

proof end;

end;

registration

let c₁ be natural-yielding FinSequence;
let c₂ be natural number ;
cluster a₁ |^ a₂ -> real-yielding natural-yielding ;
coherence

proof end;

end;

definition

let c₁ be FinSequence of REAL ;
let c₂ be natural number ;
redefine func |^ as c₁ |^ c₂ -> FinSequence of REAL ;
coherence

proof end;

end;

definition

let c₁ be FinSequence of NAT ;
let c₂ be natural number ;
redefine func |^ as c₁ |^ c₂ -> FinSequence of NAT ;
coherence

proof end;

end;

theorem Th9: :: NAT_3:9

for b₁ being FinSequence of REAL holds b₁ |^ 0 = (len b₁) |-> 1

proof end;

theorem Th10: :: NAT_3:10

for b₁ being FinSequence of REAL holds b₁ |^ 1 = b₁

proof end;

theorem Th11: :: NAT_3:11

for b₁ being natural number holds (<*> REAL ) |^ b₁ = <*> REAL

proof end;

theorem Th12: :: NAT_3:12

for b₁ being natural number
for b₂ being Real holds <*b₂*> |^ b₁ = <*(b₂ |^ b₁)*>

proof end;

theorem Th13: :: NAT_3:13

for b₁ being natural number
for b₂ being Real
for b₃ being FinSequence of REAL holds (b₃ ^ <*b₂*>) |^ b₁ = (b₃ |^ b₁) ^ (<*b₂*> |^ b₁)

proof end;

theorem Th14: :: NAT_3:14

for b₁ being natural number
for b₂ being FinSequence of REAL holds Product (b₂ |^ (b₁ + 1)) = (Product (b₂ |^ b₁)) * (Product b₂)

proof end;

theorem Th15: :: NAT_3:15

for b₁ being natural number
for b₂ being FinSequence of REAL holds Product (b₂ |^ b₁) = (Product b₂) |^ b₁

proof end;

registration

let c₁ be set ;
cluster real-yielding natural-yielding finite-support ManySortedSet of a₁;
existence

proof end;

end;

definition

let c₁ be set ;
let c₂ be real-yielding ManySortedSet of c₁;
let c₃ be natural number ;
func c₃ * c₂ -> ManySortedSet of a₁ means :Def2: :: NAT_3:def 2
for b₁ being set holds a₄ . b₁ = a₃ * (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines * NAT_3:def 2 :

registration

let c₁ be set ;
let c₂ be real-yielding ManySortedSet of c₁;
let c₃ be natural number ;
cluster a₃ * a₂ -> real-yielding ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be natural-yielding ManySortedSet of c₁;
let c₃ be natural number ;
cluster a₃ * a₂ -> real-yielding natural-yielding ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be real-yielding ManySortedSet of c₁;
cluster support (0 * a₂) -> empty ;
coherence

proof end;

end;

theorem Th16: :: NAT_3:16

for b₁ being natural number
for b₂ being set
for b₃ being real-yielding ManySortedSet of b₂ st b₁ <> 0 holds
support b₃ = support (b₁ * b₃)

proof end;

registration

let c₁ be set ;
let c₂ be real-yielding finite-support ManySortedSet of c₁;
let c₃ be natural number ;
cluster a₃ * a₂ -> real-yielding finite-support ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂, c₃ be real-yielding ManySortedSet of c₁;
func min c₂,c₃ -> ManySortedSet of a₁ means :Def3: :: NAT_3:def 3
for b₁ being set holds
( ( a₂ . b₁ <= a₃ . b₁ implies a₄ . b₁ = a₂ . b₁ ) & ( a₂ . b₁ > a₃ . b₁ implies a₄ . b₁ = a₃ . b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines min NAT_3:def 3 :

registration

let c₁ be set ;
let c₂, c₃ be real-yielding ManySortedSet of c₁;
cluster min a₂,a₃ -> real-yielding ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂, c₃ be natural-yielding ManySortedSet of c₁;
cluster min a₂,a₃ -> real-yielding natural-yielding ;
coherence

proof end;

end;

theorem Th17: :: NAT_3:17

for b₁ being set
for b₂, b₃ being real-yielding finite-support ManySortedSet of b₁ holds support (min b₂,b₃) c= (support b₂) \/ (support b₃)

proof end;

registration

let c₁ be set ;
let c₂, c₃ be real-yielding finite-support ManySortedSet of c₁;
cluster min a₂,a₃ -> real-yielding finite-support ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂, c₃ be real-yielding ManySortedSet of c₁;
func max c₂,c₃ -> ManySortedSet of a₁ means :Def4: :: NAT_3:def 4
for b₁ being set holds
( ( a₂ . b₁ <= a₃ . b₁ implies a₄ . b₁ = a₃ . b₁ ) & ( a₂ . b₁ > a₃ . b₁ implies a₄ . b₁ = a₂ . b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines max NAT_3:def 4 :

registration

let c₁ be set ;
let c₂, c₃ be real-yielding ManySortedSet of c₁;
cluster max a₂,a₃ -> real-yielding ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂, c₃ be natural-yielding ManySortedSet of c₁;
cluster max a₂,a₃ -> real-yielding natural-yielding ;
coherence

proof end;

end;

theorem Th18: :: NAT_3:18

for b₁ being set
for b₂, b₃ being real-yielding finite-support ManySortedSet of b₁ holds support (max b₂,b₃) c= (support b₂) \/ (support b₃)

proof end;

registration

let c₁ be set ;
let c₂, c₃ be real-yielding finite-support ManySortedSet of c₁;
cluster max a₂,a₃ -> real-yielding finite-support ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be bag of c₁;
func Product c₂ -> natural number means :Def5: :: NAT_3:def 5
ex b₁ being FinSequence of NAT st
( a₃ = Product b₁ & b₁ = a₂ * (canFS (support a₂)) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def5 defines Product NAT_3:def 5 :

definition

let c₁ be set ;
let c₂ be bag of c₁;
redefine func Product as Product c₂ -> Nat;
coherence by ORDINAL2:def 21;

end;

theorem Th19: :: NAT_3:19

for b₁ being set
for b₂, b₃ being bag of b₁ st support b₂ misses support b₃ holds
Product (b₂ + b₃) = (Product b₂) * (Product b₃)

proof end;

definition

let c₁ be set ;
let c₂ be real-yielding ManySortedSet of c₁;
let c₃ be non empty natural number ;
func c₂ |^ c₃ -> ManySortedSet of a₁ means :Def6: :: NAT_3:def 6
( support a₄ = support a₂ & ( for b₁ being set holds a₄ . b₁ = (a₂ . b₁) |^ a₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines |^ NAT_3:def 6 :

registration

let c₁ be set ;
let c₂ be natural-yielding ManySortedSet of c₁;
let c₃ be non empty natural number ;
cluster a₂ |^ a₃ -> real-yielding natural-yielding ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be real-yielding finite-support ManySortedSet of c₁;
let c₃ be non empty natural number ;
cluster a₂ |^ a₃ -> finite-support ;
coherence

proof end;

end;

theorem Th20: :: NAT_3:20

for b₁ being set holds Product (EmptyBag b₁) = 1

proof end;

definition

let c₁, c₂ be natural number ;
assume that
E24: c₂ <> 1 and
E25: c₁ <> 0 ;
func c₂ |-count c₁ -> Nat means :Def7: :: NAT_3:def 7
( a₂ |^ a₃ divides a₁ & not a₂ |^ (a₃ + 1) divides a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines |-count NAT_3:def 7 :

theorem Th21: :: NAT_3:21

for b₁ being natural number st b₁ <> 1 holds
b₁ |-count 1 = 0

proof end;

theorem Th22: :: NAT_3:22

for b₁ being natural number st 1 < b₁ holds
b₁ |-count b₁ = 1

proof end;

theorem Th23: :: NAT_3:23

for b₁, b₂ being natural number st b₁ <> 0 & b₁ < b₂ & b₂ <> 1 holds
b₂ |-count b₁ = 0

proof end;

theorem Th24: :: NAT_3:24

for b₁ being natural number
for b₂ being Prime st b₁ <> 1 & b₁ <> b₂ holds
b₁ |-count b₂ = 0

proof end;

theorem Th25: :: NAT_3:25

for b₁, b₂ being natural number st 1 < b₁ holds
b₁ |-count (b₁ |^ b₂) = b₂

proof end;

theorem Th26: :: NAT_3:26

for b₁, b₂ being natural number st b₁ <> 1 & b₂ <> 0 & b₁ divides b₁ |^ (b₁ |-count b₂) holds
b₁ divides b₂

proof end;

theorem Th27: :: NAT_3:27

for b₁, b₂ being natural number st b₁ <> 1 holds
( ( b₂ <> 0 & b₁ |-count b₂ = 0 ) iff not b₁ divides b₂ )

proof end;

theorem Th28: :: NAT_3:28

for b₁ being Prime
for b₂, b₃ being non empty natural number holds b₁ |-count (b₂ * b₃) = (b₁ |-count b₂) + (b₁ |-count b₃)

proof end;

theorem Th29: :: NAT_3:29

for b₁ being Prime
for b₂, b₃ being non empty natural number holds b₁ |^ (b₁ |-count (b₂ * b₃)) = (b₁ |^ (b₁ |-count b₂)) * (b₁ |^ (b₁ |-count b₃))

proof end;

theorem Th30: :: NAT_3:30

for b₁ being Prime
for b₂, b₃ being non empty natural number st b₃ divides b₂ holds
b₁ |-count b₃ <= b₁ |-count b₂

proof end;

theorem Th31: :: NAT_3:31

for b₁ being Prime
for b₂, b₃ being non empty natural number st b₃ divides b₂ holds
b₁ |-count (b₂ div b₃) = (b₁ |-count b₂) -' (b₁ |-count b₃)

proof end;

theorem Th32: :: NAT_3:32

for b₁ being natural number
for b₂ being Prime
for b₃ being non empty natural number holds b₂ |-count (b₃ |^ b₁) = b₁ * (b₂ |-count b₃)

proof end;

definition

let c₁ be natural number ;
func prime_exponents c₁ -> ManySortedSet of SetPrimes means :Def8: :: NAT_3:def 8
for b₁ being Prime holds a₂ . b₁ = b₁ |-count a₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines prime_exponents NAT_3:def 8 :

notation

let c₁ be natural number ;
synonym pfexp c₁ for prime_exponents c₁;

end;

theorem Th33: :: NAT_3:33

for b₁ being natural number
for b₂ being set st b₂ in dom (pfexp b₁) holds
b₂ is Prime

proof end;

theorem Th34: :: NAT_3:34

for b₁ being natural number
for b₂ being set st b₂ in support (pfexp b₁) holds
b₂ is Prime

proof end;

theorem Th35: :: NAT_3:35

for b₁, b₂ being natural number st b₁ > b₂ & b₂ <> 0 holds
(pfexp b₂) . b₁ = 0

proof end;

registration

let c₁ be natural number ;
cluster prime_exponents a₁ -> real-yielding natural-yielding ;
coherence

proof end;

end;

theorem Th36: :: NAT_3:36

for b₁, b₂ being natural number st b₁ in support (pfexp b₂) holds
b₁ divides b₂

proof end;

theorem Th37: :: NAT_3:37

for b₁, b₂ being natural number st not b₁ is empty & b₂ is Prime & b₂ divides b₁ holds
b₂ in support (pfexp b₁)

proof end;

registration

let c₁ be non empty natural number ;
cluster prime_exponents a₁ -> real-yielding natural-yielding finite-support ;
coherence

proof end;

end;

theorem Th38: :: NAT_3:38

for b₁ being Prime
for b₂ being non empty natural number st b₁ divides b₂ holds
(pfexp b₂) . b₁ <> 0

proof end;

theorem Th39: :: NAT_3:39

pfexp 1 = EmptyBag SetPrimes

proof end;

registration

cluster support (pfexp 1) -> empty ;
coherence

proof end;

end;

theorem Th40: :: NAT_3:40

for b₁ being natural number
for b₂ being Prime holds (pfexp (b₂ |^ b₁)) . b₂ = b₁

proof end;

theorem Th41: :: NAT_3:41

for b₁ being Prime holds (pfexp b₁) . b₁ = 1

proof end;

theorem Th42: :: NAT_3:42

for b₁ being natural number
for b₂ being Prime st b₁ <> 0 holds
support (pfexp (b₂ |^ b₁)) = {b₂}

proof end;

theorem Th43: :: NAT_3:43

for b₁ being Prime holds support (pfexp b₁) = {b₁}

proof end;

registration

let c₁ be Prime;
let c₂ be non empty natural number ;
cluster support (pfexp (a₁ |^ a₂)) -> non empty trivial ;
coherence

proof end;

end;

registration

let c₁ be Prime;
cluster support (pfexp a₁) -> non empty trivial ;
coherence

proof end;

end;

theorem Th44: :: NAT_3:44

for b₁, b₂ being non empty Nat st b₁,b₂ are_relative_prime holds
support (pfexp b₁) misses support (pfexp b₂)

proof end;

theorem Th45: :: NAT_3:45

for b₁, b₂ being non empty natural number holds support (pfexp b₁) c= support (pfexp (b₁ * b₂))

proof end;

theorem Th46: :: NAT_3:46

for b₁, b₂ being non empty Nat holds support (pfexp (b₁ * b₂)) = (support (pfexp b₁)) \/ (support (pfexp b₂))

proof end;

theorem Th47: :: NAT_3:47

for b₁, b₂ being non empty Nat st b₁,b₂ are_relative_prime holds
card (support (pfexp (b₁ * b₂))) = (card (support (pfexp b₁))) + (card (support (pfexp b₂)))

proof end;

theorem Th48: :: NAT_3:48

for b₁, b₂ being non empty natural number holds support (pfexp b₁) = support (pfexp (b₁ |^ b₂))

proof end;

theorem Th49: :: NAT_3:49

for b₁, b₂ being non empty natural number holds pfexp (b₁ * b₂) = (pfexp b₁) + (pfexp b₂)

proof end;

theorem Th50: :: NAT_3:50

for b₁, b₂ being non empty natural number st b₁ divides b₂ holds
pfexp (b₂ div b₁) = (pfexp b₂) -' (pfexp b₁)

proof end;

theorem Th51: :: NAT_3:51

for b₁ being natural number
for b₂ being non empty natural number holds pfexp (b₂ |^ b₁) = b₁ * (pfexp b₂)

proof end;

theorem Th52: :: NAT_3:52

for b₁ being non empty natural number st support (pfexp b₁) = {} holds
b₁ = 1

proof end;

theorem Th53: :: NAT_3:53

for b₁, b₂ being non empty Nat holds pfexp (b₂ hcf b₁) = min (pfexp b₂),(pfexp b₁)

proof end;

theorem Th54: :: NAT_3:54

for b₁, b₂ being non empty Nat holds pfexp (b₂ lcm b₁) = max (pfexp b₂),(pfexp b₁)

proof end;

definition

let c₁ be non empty natural number ;
func prime_factorization c₁ -> ManySortedSet of SetPrimes means :Def9: :: NAT_3:def 9
( support a₂ = support (pfexp a₁) & ( for b₁ being natural number st b₁ in support (pfexp a₁) holds
a₂ . b₁ = b₁ |^ (b₁ |-count a₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines prime_factorization NAT_3:def 9 :

notation

let c₁ be non empty natural number ;
synonym ppf c₁ for prime_factorization c₁;

end;

registration

let c₁ be non empty natural number ;
cluster prime_factorization a₁ -> real-yielding natural-yielding finite-support ;
coherence

proof end;

end;

theorem Th55: :: NAT_3:55

for b₁ being Prime
for b₂ being non empty natural number st b₁ |-count b₂ = 0 holds
(ppf b₂) . b₁ = 0

proof end;

theorem Th56: :: NAT_3:56

for b₁ being Prime
for b₂ being non empty natural number st b₁ |-count b₂ <> 0 holds
(ppf b₂) . b₁ = b₁ |^ (b₁ |-count b₂)

proof end;

theorem Th57: :: NAT_3:57

for b₁ being non empty natural number st support (ppf b₁) = {} holds
b₁ = 1

proof end;

theorem Th58: :: NAT_3:58

for b₁, b₂ being non empty Nat st b₁,b₂ are_relative_prime holds
ppf (b₁ * b₂) = (ppf b₁) + (ppf b₂)

proof end;

theorem Th59: :: NAT_3:59

for b₁ being Prime
for b₂ being non empty natural number holds (ppf (b₁ |^ b₂)) . b₁ = b₁ |^ b₂

proof end;

theorem Th60: :: NAT_3:60

for b₁, b₂ being non empty natural number holds ppf (b₁ |^ b₂) = (ppf b₁) |^ b₂

proof end;

theorem Th61: :: NAT_3:61

for b₁ being non empty natural number holds Product (ppf b₁) = b₁

proof end;