NAT_3: Fundamental {T}heorem of {A}rithmetic

:: Fundamental {T}heorem of {A}rithmetic
:: by Artur Korni{\l}owicz and Piotr Rudnicki
::
:: Received February 13, 2004
:: Copyright (c) 2004-2011 Association of Mizar Users

begin

registration

cluster Relation-like Function-like finite FinSequence-like FinSubsequence-like natural-valued finite-support set ;
existence

proof end;

end;

registration

let a be non empty natural number ;
let b be natural number ;
cluster a |^ b -> non empty ;
coherence

proof end;

end;

registration

cluster natural prime -> non empty set ;
coherence by INT_2:def 5;

end;

theorem Th1: :: NAT_3:1

for a, b, c, d being natural number st a divides c & b divides d holds
a * b divides c * d

proof end;

theorem Th2: :: NAT_3:2

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

proof end;

theorem Th3: :: NAT_3:3

for a, n being natural number st a <> 0 holds
n divides n |^ a

proof end;

theorem Th4: :: NAT_3:4

for i, j, m, n being natural number st i < j & m |^ j divides n holds
m |^ (i + 1) divides n

proof end;

theorem Th5: :: NAT_3:5

for a, b being natural number
for p being Prime st p divides a |^ b holds
p divides a

proof end;

theorem Th6: :: NAT_3:6

for b being natural number
for p, a being Prime st a divides p |^ b holds
a = p

proof end;

theorem :: NAT_3:7

for a being natural number
for f being FinSequence of NAT st a in rng f holds
a divides Product f

proof end;

theorem :: NAT_3:8

for p being Prime
for f being FinSequence of SetPrimes st p divides Product f holds
p in rng f

proof end;

definition

let f be real-valued FinSequence;
let a be natural number ;
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

proof end;

proof end;

end;

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

registration

let f be real-valued FinSequence;
let a be natural number ;
cluster f |^ a -> real-valued ;
coherence

proof end;

end;

registration

let f be natural-valued FinSequence;
let a be natural number ;
cluster f |^ a -> natural-valued ;
coherence

proof end;

end;

definition

let f be FinSequence of REAL ;
let a be natural number ;
:: original: |^
redefine func f |^ a -> FinSequence of REAL ;
coherence

proof end;

end;

definition

let f be FinSequence of NAT ;
let a be natural number ;
:: original: |^
redefine func f |^ a -> FinSequence of NAT ;
coherence

proof end;

end;

theorem Th9: :: NAT_3:9

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

proof end;

theorem :: NAT_3:10

for f being FinSequence of REAL holds f |^ 1 = f

proof end;

theorem Th11: :: NAT_3:11

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

proof end;

theorem Th12: :: NAT_3:12

for a being natural number
for r being Real holds <*r*> |^ a = <*(r |^ a)*>

proof end;

theorem Th13: :: NAT_3:13

for a being natural number
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 natural number
for f being FinSequence of REAL holds Product (f |^ (b + 1)) = (Product (f |^ b)) * (Product f)

proof end;

theorem :: NAT_3:15

for a being natural number
for f being FinSequence of REAL holds Product (f |^ a) = (Product f) |^ a

proof end;

begin

registration

let X be set ;
cluster Relation-like X -defined Function-like V14(X) natural-valued finite-support set ;
existence

proof end;

end;

definition

let X be set ;
let b be real-valued ManySortedSet of X;
let a be natural number ;
func a * b -> ManySortedSet of X means :Def2: :: NAT_3:def 2
for i being set holds it . i = a * (b . i);
existence

proof end;

proof end;

end;

:: deftheorem Def2 defines * NAT_3:def 2 :

registration

let X be set ;
let b be real-valued ManySortedSet of X;
let a be natural number ;
cluster a * b -> real-valued ;
coherence

proof end;

end;

registration

let X be set ;
let b be natural-valued ManySortedSet of X;
let a be natural number ;
cluster a * b -> natural-valued ;
coherence

proof end;

end;

registration

let X be set ;
let b be real-valued ManySortedSet of X;
cluster support (0 * b) -> empty ;
coherence

proof end;

end;

theorem Th16: :: NAT_3:16

for a being natural number
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 natural number ;
cluster a * b -> finite-support ;
coherence

proof end;

end;

definition

let X be set ;
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

proof end;

proof end;

end;

:: deftheorem Def3 defines min NAT_3:def 3 :

registration

let X be set ;
let b1, b2 be real-valued ManySortedSet of X;
cluster min (b1,b2) -> real-valued ;
coherence

proof end;

end;

registration

let X be set ;
let b1, b2 be natural-valued ManySortedSet of X;
cluster min (b1,b2) -> natural-valued ;
coherence

proof end;

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)

proof end;

registration

let X be set ;
let b1, b2 be real-valued finite-support ManySortedSet of X;
cluster min (b1,b2) -> finite-support ;
coherence

proof end;

end;

definition

let X be set ;
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

proof end;

proof end;

end;

:: deftheorem Def4 defines max NAT_3:def 4 :

registration

let X be set ;
let b1, b2 be real-valued ManySortedSet of X;
cluster max (b1,b2) -> real-valued ;
coherence

proof end;

end;

registration

let X be set ;
let b1, b2 be natural-valued ManySortedSet of X;
cluster max (b1,b2) -> natural-valued ;
coherence

proof end;

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)

proof end;

registration

let X be set ;
let b1, b2 be real-valued finite-support ManySortedSet of X;
cluster max (b1,b2) -> finite-support ;
coherence

proof end;

end;

registration

let A be set ;
cluster Relation-like A -defined Function-like V14(A) complex-yielding finite-support set ;
existence

proof end;

end;

definition

let A be set ;
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

proof end;

end;

:: deftheorem Def5 defines Product NAT_3:def 5 :

definition

let A be set ;
let b be bag of A;
:: original: Product
redefine func Product b -> Element of NAT ;
coherence

proof end;

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)

proof end;

definition

let X be set ;
let b be real-valued ManySortedSet of X;
let n be non empty natural number ;
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

proof end;

proof end;

end;

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

registration

let X be set ;
let b be natural-valued ManySortedSet of X;
let n be non empty natural number ;
cluster b |^ n -> natural-valued ;
coherence

proof end;

end;

registration

let X be set ;
let b be real-valued finite-support ManySortedSet of X;
let n be non empty natural number ;
cluster b |^ n -> finite-support ;
coherence

proof end;

end;

theorem Th20: :: NAT_3:20

for A being set holds Product (EmptyBag A) = 1

proof end;

begin

definition

let n, d be natural number ;
assume that
A1: d <> 1 and
A2: n <> 0 ;
func d |-count n -> Nat means :Def7: :: NAT_3:def 7
( d |^ it divides n & not d |^ (it + 1) divides n );
existence

proof end;

proof end;

end;

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

definition

let n, d be natural number ;
:: original: |-count
redefine func d |-count n -> Element of NAT ;
coherence by ORDINAL1:def 13;

end;

theorem Th21: :: NAT_3:21

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

proof end;

theorem :: NAT_3:22

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

proof end;

theorem Th23: :: NAT_3:23

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

proof end;

theorem :: NAT_3:24

for a being natural number
for p being Prime st a <> 1 & a <> p holds
a |-count p = 0

proof end;

theorem Th25: :: NAT_3:25

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

proof end;

theorem Th26: :: NAT_3:26

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

proof end;

theorem Th27: :: NAT_3:27

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

proof end;

theorem Th28: :: NAT_3:28

for p being Prime
for a, b being non empty natural number 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 natural number holds p |^ (p |-count (a * b)) = (p |^ (p |-count a)) * (p |^ (p |-count b))

proof end;

theorem Th30: :: NAT_3:30

for p being Prime
for a, b being non empty natural number st b divides a holds
p |-count b <= p |-count a

proof end;

theorem Th31: :: NAT_3:31

for p being Prime
for a, b being non empty natural number 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 natural number
for p being Prime
for a being non empty natural number holds p |-count (a |^ b) = b * (p |-count a)

proof end;

begin

definition

let n be natural number ;
func prime_exponents n -> ManySortedSet of SetPrimes means :Def8: :: NAT_3:def 8
for p being Prime holds it . p = p |-count n;
existence

proof end;

proof end;

end;

:: deftheorem Def8 defines prime_exponents NAT_3:def 8 :

notation

let n be natural number ;
synonym pfexp n for prime_exponents n;

end;

theorem Th33: :: NAT_3:33

for n being natural number
for x being set st x in dom (pfexp n) holds
x is Prime

proof end;

theorem Th34: :: NAT_3:34

for n being natural number
for x being set st x in support (pfexp n) holds
x is Prime

proof end;

theorem Th35: :: NAT_3:35

for a, n being natural number st a > n & n <> 0 holds
(pfexp n) . a = 0

proof end;

registration

let n be natural number ;
cluster prime_exponents n -> natural-valued ;
coherence

proof end;

end;

theorem :: NAT_3:36

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

proof end;

theorem Th37: :: NAT_3:37

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

proof end;

registration

let n be non empty natural number ;
cluster prime_exponents n -> finite-support ;
coherence

proof end;

end;

theorem Th38: :: NAT_3:38

for p being Prime
for a being non empty natural number st p divides a holds
(pfexp a) . p <> 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 a being natural number
for p being Prime holds (pfexp (p |^ a)) . p = a

proof end;

theorem :: NAT_3:41

for p being Prime holds (pfexp p) . p = 1

proof end;

theorem Th42: :: NAT_3:42

for a being natural number
for p being Prime st a <> 0 holds
support (pfexp (p |^ a)) = {p}

proof end;

theorem Th43: :: NAT_3:43

for p being Prime holds support (pfexp p) = {p}

proof end;

registration

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

proof end;

end;

registration

let p be Prime;
cluster support (pfexp p) -> non empty trivial ;
coherence

proof end;

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)

proof end;

theorem Th45: :: NAT_3:45

for a, b being non empty natural number holds support (pfexp a) c= support (pfexp (a * 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)))

proof end;

theorem :: NAT_3:48

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

proof end;

theorem :: NAT_3:49

for n, m being non empty natural number holds pfexp (n * m) = (pfexp n) + (pfexp m)

proof end;

theorem :: NAT_3:50

for m, n being non empty natural number st m divides n holds
pfexp (n div m) = (pfexp n) -' (pfexp m)

proof end;

theorem :: NAT_3:51

for a being natural number
for n being non empty natural number holds pfexp (n |^ a) = a * (pfexp n)

proof end;

theorem Th52: :: NAT_3:52

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

proof end;

theorem :: NAT_3:53

for m, n being non empty Nat holds pfexp (n gcd m) = min ((pfexp n),(pfexp m))

proof end;

theorem :: NAT_3:54

for m, n being non empty Nat holds pfexp (n lcm m) = max ((pfexp n),(pfexp m))

proof end;

begin

definition

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

proof end;

proof end;

end;

:: deftheorem Def9 defines prime_factorization NAT_3:def 9 :

notation

let n be non empty natural number ;
synonym ppf n for prime_factorization n;

end;

registration

let n be non empty natural number ;
cluster prime_factorization n -> natural-valued finite-support ;
coherence

proof end;

end;

theorem Th55: :: NAT_3:55

for p being Prime
for n being non empty natural number st p |-count n = 0 holds
(ppf n) . p = 0

proof end;

theorem Th56: :: NAT_3:56

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

proof end;

theorem :: NAT_3:57

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

proof end;

theorem Th58: :: NAT_3:58

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

proof end;

theorem Th59: :: NAT_3:59

for p being Prime
for n being non empty natural number holds (ppf (p |^ n)) . p = p |^ n

proof end;

theorem :: NAT_3:60

for n, m being non empty natural number holds ppf (n |^ m) = (ppf n) |^ m

proof end;

theorem :: NAT_3:61

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

proof end;