:: by Artur Korni{\l}owicz and Piotr Rudnicki

::

:: Received February 13, 2004

:: Copyright (c) 2004-2012 Association of Mizar Users

begin

registration

ex b_{1} being FinSequence st b_{1} is natural-valued
end;

cluster Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like natural-valued finite-support for set ;

existence ex b

proof end;

:: Power

definition

let f be real-valued FinSequence;

let a be Nat;

ex b_{1} being FinSequence st

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

b_{1} . i = (f . i) |^ a ) )

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

b_{1} . i = (f . i) |^ a ) & len b_{2} = len f & ( for i being set st i in dom b_{2} holds

b_{2} . i = (f . i) |^ a ) holds

b_{1} = b_{2}

end;
let a be Nat;

func f |^ a -> FinSequence means :Def1: :: NAT_3:def 1

( len it = len f & ( for i being set st i in dom it holds

it . i = (f . i) |^ a ) );

existence ( len it = len f & ( for i being set st i in dom it holds

it . i = (f . i) |^ a ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

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

for f being real-valued FinSequence

for a being Nat

for b_{3} being FinSequence holds

( b_{3} = f |^ a iff ( len b_{3} = len f & ( for i being set st i in dom b_{3} holds

b_{3} . i = (f . i) |^ a ) ) );

for f being real-valued FinSequence

for a being Nat

for b

( b

b

registration
end;

registration
end;

definition

let f be FinSequence of REAL ;

let a be Nat;

:: original: |^

redefine func f |^ a -> FinSequence of REAL ;

coherence

f |^ a is FinSequence of REAL

end;
let a be Nat;

:: original: |^

redefine func f |^ a -> FinSequence of REAL ;

coherence

f |^ a is FinSequence of REAL

proof end;

definition

let f be FinSequence of NAT ;

let a be Nat;

:: original: |^

redefine func f |^ a -> FinSequence of NAT ;

coherence

f |^ a is FinSequence of NAT

end;
let a be Nat;

:: original: |^

redefine func f |^ a -> FinSequence of NAT ;

coherence

f |^ a is FinSequence of NAT

proof end;

theorem Th13: :: NAT_3:13

for a being Nat

for r being Real

for f being FinSequence of REAL holds (f ^ <*r*>) |^ a = (f |^ a) ^ (<*r*> |^ a)

for r being Real

for f being FinSequence of REAL holds (f ^ <*r*>) |^ a = (f |^ a) ^ (<*r*> |^ a)

proof end;

theorem Th14: :: NAT_3:14

for b being Nat

for f being FinSequence of REAL holds Product (f |^ (b + 1)) = (Product (f |^ b)) * (Product f)

for f being FinSequence of REAL holds Product (f |^ (b + 1)) = (Product (f |^ b)) * (Product f)

proof end;

begin

registration

let X be set ;

existence

ex b_{1} being ManySortedSet of X st

( b_{1} is natural-valued & b_{1} is finite-support )

end;
existence

ex b

( b

proof end;

definition

let X be set ;

let b be real-valued ManySortedSet of X;

let a be Nat;

ex b_{1} being ManySortedSet of X st

for i being set holds b_{1} . i = a * (b . i)

for b_{1}, b_{2} being ManySortedSet of X st ( for i being set holds b_{1} . i = a * (b . i) ) & ( for i being set holds b_{2} . i = a * (b . i) ) holds

b_{1} = b_{2}

end;
let b be real-valued ManySortedSet of X;

let a be Nat;

func a * b -> ManySortedSet of X means :Def2: :: NAT_3:def 2

for i being set holds it . i = a * (b . i);

existence for i being set holds it . i = a * (b . i);

ex b

for i being set holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines * NAT_3:def 2 :

for X being set

for b being real-valued ManySortedSet of X

for a being Nat

for b_{4} being ManySortedSet of X holds

( b_{4} = a * b iff for i being set holds b_{4} . i = a * (b . i) );

for X being set

for b being real-valued ManySortedSet of X

for a being Nat

for b

( b

registration

let X be set ;

let b be real-valued ManySortedSet of X;

let a be Nat;

coherence

a * b is real-valued

end;
let b be real-valued ManySortedSet of X;

let a be Nat;

coherence

a * b is real-valued

proof end;

registration

let X be set ;

let b be natural-valued ManySortedSet of X;

let a be Nat;

coherence

a * b is natural-valued

end;
let b be natural-valued ManySortedSet of X;

let a be Nat;

coherence

a * b is natural-valued

proof end;

registration

let X be set ;

let b be real-valued ManySortedSet of X;

coherence

support (0 * b) is empty

end;
let b be real-valued ManySortedSet of X;

coherence

support (0 * b) is empty

proof end;

theorem Th16: :: NAT_3:16

for a being Nat

for X being set

for b being real-valued ManySortedSet of X st a <> 0 holds

support b = support (a * b)

for X being set

for b being real-valued ManySortedSet of X st a <> 0 holds

support b = support (a * b)

proof end;

registration

let X be set ;

let b be real-valued finite-support ManySortedSet of X;

let a be Nat;

coherence

a * b is finite-support

end;
let b be real-valued finite-support ManySortedSet of X;

let a be Nat;

coherence

a * b is finite-support

proof end;

definition

let X be set ;

let b1, b2 be real-valued ManySortedSet of X;

ex b_{1} being ManySortedSet of X st

for i being set holds

( ( b1 . i <= b2 . i implies b_{1} . i = b1 . i ) & ( b1 . i > b2 . i implies b_{1} . i = b2 . i ) )

for b_{1}, b_{2} being ManySortedSet of X st ( for i being set holds

( ( b1 . i <= b2 . i implies b_{1} . i = b1 . i ) & ( b1 . i > b2 . i implies b_{1} . i = b2 . i ) ) ) & ( for i being set holds

( ( b1 . i <= b2 . i implies b_{2} . i = b1 . i ) & ( b1 . i > b2 . i implies b_{2} . i = b2 . i ) ) ) holds

b_{1} = b_{2}

end;
let b1, b2 be real-valued ManySortedSet of X;

func min (b1,b2) -> ManySortedSet of X means :Def3: :: NAT_3:def 3

for i being set holds

( ( b1 . i <= b2 . i implies it . i = b1 . i ) & ( b1 . i > b2 . i implies it . i = b2 . i ) );

existence for i being set holds

( ( b1 . i <= b2 . i implies it . i = b1 . i ) & ( b1 . i > b2 . i implies it . i = b2 . i ) );

ex b

for i being set holds

( ( b1 . i <= b2 . i implies b

proof end;

uniqueness for b

( ( b1 . i <= b2 . i implies b

( ( b1 . i <= b2 . i implies b

b

proof end;

:: deftheorem Def3 defines min NAT_3:def 3 :

for X being set

for b1, b2 being real-valued ManySortedSet of X

for b_{4} being ManySortedSet of X holds

( b_{4} = min (b1,b2) iff for i being set holds

( ( b1 . i <= b2 . i implies b_{4} . i = b1 . i ) & ( b1 . i > b2 . i implies b_{4} . i = b2 . i ) ) );

for X being set

for b1, b2 being real-valued ManySortedSet of X

for b

( b

( ( b1 . i <= b2 . i implies b

registration

let X be set ;

let b1, b2 be real-valued ManySortedSet of X;

coherence

min (b1,b2) is real-valued

end;
let b1, b2 be real-valued ManySortedSet of X;

coherence

min (b1,b2) is real-valued

proof end;

registration

let X be set ;

let b1, b2 be natural-valued ManySortedSet of X;

coherence

min (b1,b2) is natural-valued

end;
let b1, b2 be natural-valued ManySortedSet of X;

coherence

min (b1,b2) is natural-valued

proof end;

theorem Th17: :: NAT_3:17

for X being set

for b1, b2 being real-valued finite-support ManySortedSet of X holds support (min (b1,b2)) c= (support b1) \/ (support b2)

for b1, b2 being real-valued finite-support ManySortedSet of X holds support (min (b1,b2)) c= (support b1) \/ (support b2)

proof end;

registration

let X be set ;

let b1, b2 be real-valued finite-support ManySortedSet of X;

coherence

min (b1,b2) is finite-support

end;
let b1, b2 be real-valued finite-support ManySortedSet of X;

coherence

min (b1,b2) is finite-support

proof end;

definition

let X be set ;

let b1, b2 be real-valued ManySortedSet of X;

ex b_{1} being ManySortedSet of X st

for i being set holds

( ( b1 . i <= b2 . i implies b_{1} . i = b2 . i ) & ( b1 . i > b2 . i implies b_{1} . i = b1 . i ) )

for b_{1}, b_{2} being ManySortedSet of X st ( for i being set holds

( ( b1 . i <= b2 . i implies b_{1} . i = b2 . i ) & ( b1 . i > b2 . i implies b_{1} . i = b1 . i ) ) ) & ( for i being set holds

( ( b1 . i <= b2 . i implies b_{2} . i = b2 . i ) & ( b1 . i > b2 . i implies b_{2} . i = b1 . i ) ) ) holds

b_{1} = b_{2}

end;
let b1, b2 be real-valued ManySortedSet of X;

func max (b1,b2) -> ManySortedSet of X means :Def4: :: NAT_3:def 4

for i being set holds

( ( b1 . i <= b2 . i implies it . i = b2 . i ) & ( b1 . i > b2 . i implies it . i = b1 . i ) );

existence for i being set holds

( ( b1 . i <= b2 . i implies it . i = b2 . i ) & ( b1 . i > b2 . i implies it . i = b1 . i ) );

ex b

for i being set holds

( ( b1 . i <= b2 . i implies b

proof end;

uniqueness for b

( ( b1 . i <= b2 . i implies b

( ( b1 . i <= b2 . i implies b

b

proof end;

:: deftheorem Def4 defines max NAT_3:def 4 :

for X being set

for b1, b2 being real-valued ManySortedSet of X

for b_{4} being ManySortedSet of X holds

( b_{4} = max (b1,b2) iff for i being set holds

( ( b1 . i <= b2 . i implies b_{4} . i = b2 . i ) & ( b1 . i > b2 . i implies b_{4} . i = b1 . i ) ) );

for X being set

for b1, b2 being real-valued ManySortedSet of X

for b

( b

( ( b1 . i <= b2 . i implies b

registration

let X be set ;

let b1, b2 be real-valued ManySortedSet of X;

coherence

max (b1,b2) is real-valued

end;
let b1, b2 be real-valued ManySortedSet of X;

coherence

max (b1,b2) is real-valued

proof end;

registration

let X be set ;

let b1, b2 be natural-valued ManySortedSet of X;

coherence

max (b1,b2) is natural-valued

end;
let b1, b2 be natural-valued ManySortedSet of X;

coherence

max (b1,b2) is natural-valued

proof end;

theorem Th18: :: NAT_3:18

for X being set

for b1, b2 being real-valued finite-support ManySortedSet of X holds support (max (b1,b2)) c= (support b1) \/ (support b2)

for b1, b2 being real-valued finite-support ManySortedSet of X holds support (max (b1,b2)) c= (support b1) \/ (support b2)

proof end;

registration

let X be set ;

let b1, b2 be real-valued finite-support ManySortedSet of X;

coherence

max (b1,b2) is finite-support

end;
let b1, b2 be real-valued finite-support ManySortedSet of X;

coherence

max (b1,b2) is finite-support

proof end;

registration

let A be set ;

existence

ex b_{1} being ManySortedSet of A st

( b_{1} is finite-support & b_{1} is complex-yielding )

end;
existence

ex b

( b

proof end;

definition

let A be set ;

let b be complex-yielding finite-support ManySortedSet of A;

ex b_{1} being complex number ex f being FinSequence of COMPLEX st

( b_{1} = Product f & f = b * (canFS (support b)) )

for b_{1}, b_{2} being complex number st ex f being FinSequence of COMPLEX st

( b_{1} = Product f & f = b * (canFS (support b)) ) & ex f being FinSequence of COMPLEX st

( b_{2} = Product f & f = b * (canFS (support b)) ) holds

b_{1} = b_{2}
;

end;
let b be complex-yielding finite-support ManySortedSet of A;

func Product b -> complex number means :Def5: :: NAT_3:def 5

ex f being FinSequence of COMPLEX st

( it = Product f & f = b * (canFS (support b)) );

existence ex f being FinSequence of COMPLEX st

( it = Product f & f = b * (canFS (support b)) );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

:: deftheorem Def5 defines Product NAT_3:def 5 :

for A being set

for b being complex-yielding finite-support ManySortedSet of A

for b_{3} being complex number holds

( b_{3} = Product b iff ex f being FinSequence of COMPLEX st

( b_{3} = Product f & f = b * (canFS (support b)) ) );

for A being set

for b being complex-yielding finite-support ManySortedSet of A

for b

( b

( b

definition

let A be set ;

let b be bag of A;

:: original: Product

redefine func Product b -> Element of NAT ;

coherence

Product b is Element of NAT

end;
let b be bag of A;

:: original: Product

redefine func Product b -> Element of NAT ;

coherence

Product b is Element of NAT

proof end;

theorem Th19: :: NAT_3:19

for X being set

for a, b being bag of X st support a misses support b holds

Product (a + b) = (Product a) * (Product b)

for a, b being bag of X st support a misses support b holds

Product (a + b) = (Product a) * (Product b)

proof end;

definition

let X be set ;

let b be real-valued ManySortedSet of X;

let n be non empty Nat;

ex b_{1} being ManySortedSet of X st

( support b_{1} = support b & ( for i being set holds b_{1} . i = (b . i) |^ n ) )

for b_{1}, b_{2} being ManySortedSet of X st support b_{1} = support b & ( for i being set holds b_{1} . i = (b . i) |^ n ) & support b_{2} = support b & ( for i being set holds b_{2} . i = (b . i) |^ n ) holds

b_{1} = b_{2}

end;
let b be real-valued ManySortedSet of X;

let n be non empty Nat;

func b |^ n -> ManySortedSet of X means :Def6: :: NAT_3:def 6

( support it = support b & ( for i being set holds it . i = (b . i) |^ n ) );

existence ( support it = support b & ( for i being set holds it . i = (b . i) |^ n ) );

ex b

( support b

proof end;

uniqueness for b

b

proof end;

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

for X being set

for b being real-valued ManySortedSet of X

for n being non empty Nat

for b_{4} being ManySortedSet of X holds

( b_{4} = b |^ n iff ( support b_{4} = support b & ( for i being set holds b_{4} . i = (b . i) |^ n ) ) );

for X being set

for b being real-valued ManySortedSet of X

for n being non empty Nat

for b

( b

registration

let X be set ;

let b be natural-valued ManySortedSet of X;

let n be non empty Nat;

coherence

b |^ n is natural-valued

end;
let b be natural-valued ManySortedSet of X;

let n be non empty Nat;

coherence

b |^ n is natural-valued

proof end;

registration

let X be set ;

let b be real-valued finite-support ManySortedSet of X;

let n be non empty Nat;

coherence

b |^ n is finite-support

end;
let b be real-valued finite-support ManySortedSet of X;

let n be non empty Nat;

coherence

b |^ n is finite-support

proof end;

begin

definition

let n, d be Nat;

assume that

B1: d <> 1 and

B2: n <> 0 ;

ex b_{1} being Nat st

( d |^ b_{1} divides n & not d |^ (b_{1} + 1) divides n )

for b_{1}, b_{2} being Nat st d |^ b_{1} divides n & not d |^ (b_{1} + 1) divides n & d |^ b_{2} divides n & not d |^ (b_{2} + 1) divides n holds

b_{1} = b_{2}

end;
assume that

B1: d <> 1 and

B2: n <> 0 ;

func d |-count n -> Nat means :Def7: :: NAT_3:def 7

( d |^ it divides n & not d |^ (it + 1) divides n );

existence ( d |^ it divides n & not d |^ (it + 1) divides n );

ex b

( d |^ b

proof end;

uniqueness for b

b

proof end;

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

for n, d being Nat st d <> 1 & n <> 0 holds

for b_{3} being Nat holds

( b_{3} = d |-count n iff ( d |^ b_{3} divides n & not d |^ (b_{3} + 1) divides n ) );

for n, d being Nat st d <> 1 & n <> 0 holds

for b

( b

definition

let n, d be Nat;

:: original: |-count

redefine func d |-count n -> Element of NAT ;

coherence

d |-count n is Element of NAT by ORDINAL1:def 12;

end;
:: original: |-count

redefine func d |-count n -> Element of NAT ;

coherence

d |-count n is Element of NAT by ORDINAL1:def 12;

theorem Th28: :: NAT_3:28

for p being Prime

for a, b being non empty Nat holds p |-count (a * b) = (p |-count a) + (p |-count b)

for a, b being non empty Nat holds p |-count (a * b) = (p |-count a) + (p |-count b)

proof end;

theorem Th29: :: NAT_3:29

for p being Prime

for a, b being non empty Nat holds p |^ (p |-count (a * b)) = (p |^ (p |-count a)) * (p |^ (p |-count b))

for a, b being non empty Nat holds p |^ (p |-count (a * b)) = (p |^ (p |-count a)) * (p |^ (p |-count b))

proof end;

theorem Th31: :: NAT_3:31

for p being Prime

for a, b being non empty Nat st b divides a holds

p |-count (a div b) = (p |-count a) -' (p |-count b)

for a, b being non empty Nat st b divides a holds

p |-count (a div b) = (p |-count a) -' (p |-count b)

proof end;

theorem Th32: :: NAT_3:32

for b being Nat

for p being Prime

for a being non empty Nat holds p |-count (a |^ b) = b * (p |-count a)

for p being Prime

for a being non empty Nat holds p |-count (a |^ b) = b * (p |-count a)

proof end;

begin

definition

let n be Nat;

ex b_{1} being ManySortedSet of SetPrimes st

for p being Prime holds b_{1} . p = p |-count n

for b_{1}, b_{2} being ManySortedSet of SetPrimes st ( for p being Prime holds b_{1} . p = p |-count n ) & ( for p being Prime holds b_{2} . p = p |-count n ) holds

b_{1} = b_{2}

end;
func prime_exponents n -> ManySortedSet of SetPrimes means :Def8: :: NAT_3:def 8

for p being Prime holds it . p = p |-count n;

existence for p being Prime holds it . p = p |-count n;

ex b

for p being Prime holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines prime_exponents NAT_3:def 8 :

for n being Nat

for b_{2} being ManySortedSet of SetPrimes holds

( b_{2} = prime_exponents n iff for p being Prime holds b_{2} . p = p |-count n );

for n being Nat

for b

( b

registration
end;

registration
end;

theorem Th44: :: NAT_3:44

for a, b being non empty Nat st a,b are_relative_prime holds

support (pfexp a) misses support (pfexp b)

support (pfexp a) misses support (pfexp b)

proof end;

theorem Th46: :: NAT_3:46

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

proof end;

theorem :: NAT_3:47

for a, b being non empty Nat st a,b are_relative_prime holds

card (support (pfexp (a * b))) = (card (support (pfexp a))) + (card (support (pfexp b)))

card (support (pfexp (a * b))) = (card (support (pfexp a))) + (card (support (pfexp b)))

proof end;

begin

definition

let n be non empty Nat;

ex b_{1} being ManySortedSet of SetPrimes st

( support b_{1} = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

b_{1} . p = p |^ (p |-count n) ) )

for b_{1}, b_{2} being ManySortedSet of SetPrimes st support b_{1} = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

b_{1} . p = p |^ (p |-count n) ) & support b_{2} = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

b_{2} . p = p |^ (p |-count n) ) holds

b_{1} = b_{2}

end;
func prime_factorization n -> ManySortedSet of SetPrimes means :Def9: :: NAT_3:def 9

( support it = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

it . p = p |^ (p |-count n) ) );

existence ( support it = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

it . p = p |^ (p |-count n) ) );

ex b

( support b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def9 defines prime_factorization NAT_3:def 9 :

for n being non empty Nat

for b_{2} being ManySortedSet of SetPrimes holds

( b_{2} = prime_factorization n iff ( support b_{2} = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds

b_{2} . p = p |^ (p |-count n) ) ) );

for n being non empty Nat

for b

( b

b

:: for prime-power factorization

registration
end;

theorem Th56: :: NAT_3:56

for p being Prime

for n being non empty Nat st p |-count n <> 0 holds

(ppf n) . p = p |^ (p |-count n)

for n being non empty Nat st p |-count n <> 0 holds

(ppf n) . p = p |^ (p |-count n)

proof end;