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


begin

registration
cluster Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like natural-valued finite-support for set ;
existence
 ex b1 being FinSequence st b1 is natural-valued
proofend;
end;

registration
let a be non empty Nat;
let b be Nat;
clustera |^ b ->  non empty ;
coherence
 not a |^ b is empty
proofend;
end;

registration
cluster natural prime  ->  non empty for set ;
coherence
 for b1 being Prime holds not b1 is empty by INT_2:def_4;
end;

theorem Th1: :: NAT_3:1
for a, b, c, d being Nat st a divides c & b divides d holds
a * b divides c * d
proofend;

theorem Th2: :: NAT_3:2
for a, b being Nat st 1 < a holds
b <= a |^ b
proofend;

theorem Th3: :: NAT_3:3
for a, n being Nat st a <> 0 holds
n divides n |^ a
proofend;

theorem Th4: :: NAT_3:4
for i, j, m, n being Nat st i < j &amp; m |^ j divides n holds
m |^ (i + 1) divides n
proofend;

theorem Th5: :: NAT_3:5
for a, b being Nat
for p being Prime st p divides a |^ b holds
p divides a
proofend;

theorem Th6: :: NAT_3:6
for b being Nat
for p, a being Prime st a divides p |^ b holds
a = p
proofend;

theorem :: NAT_3:7
for a being Nat
for f being FinSequence of NAT st a in rng f holds
a divides Product f
proofend;

theorem :: NAT_3:8
for p being Prime
for f being FinSequence of SetPrimes st p divides Product f holds
p in rng f
proofend;

:: Power
definition
let f be real-valued FinSequence;
let a be Nat;
funcf |^ a ->  FinSequence means :Def1: :: NAT_3:def 1
( len it = len f &amp; ( for i being set st i in dom it holds
it . i = (f . i) |^ a ) );
existence
 ex b1 being FinSequence st
( len b1 = len f &amp; ( for i being set st i in dom b1 holds
b1 . i = (f . i) |^ a ) )
proofend;
uniqueness
 for b1, b2 being FinSequence st len b1 = len f &amp; ( for i being set st i in dom b1 holds
b1 . i = (f . i) |^ a ) &amp; len b2 = len f &amp; ( for i being set st i in dom b2 holds
b2 . i = (f . i) |^ a ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines |^ NAT_3:def_1_:_
 for f being real-valued FinSequence
for a being Nat
for b3 being FinSequence holds
( b3 = f |^ a iff ( len b3 = len f &amp; ( for i being set st i in dom b3 holds
b3 . i = (f . i) |^ a ) ) );

registration
let f be real-valued FinSequence;
let a be Nat;
clusterf |^ a ->  real-valued ;
coherence
 f |^ a is real-valued
proofend;
end;

registration
let f be natural-valued FinSequence;
let a be Nat;
clusterf |^ a ->  natural-valued ;
coherence
 f |^ a is natural-valued
proofend;
end;

definition
let f be FinSequence of REAL ;
let a be Nat;
:: original:|^
redefine funcf |^ a ->  FinSequence of REAL ;
coherence
 f |^ a is FinSequence of REAL
proofend;
end;

definition
let f be FinSequence of NAT ;
let a be Nat;
:: original:|^
redefine funcf |^ a ->  FinSequence of NAT ;
coherence
 f |^ a is FinSequence of NAT
proofend;
end;

theorem Th9: :: NAT_3:9
for f being FinSequence of REAL holds f |^ 0 = (len f) |-> 1
proofend;

theorem :: NAT_3:10
for f being FinSequence of REAL holds f |^ 1 = f
proofend;

theorem Th11: :: NAT_3:11
for a being Nat holds (<*> REAL) |^ a = <*> REAL
proofend;

theorem Th12: :: NAT_3:12
for a being Nat
for r being Real holds <*r*> |^ a = <*(r |^ a)*>
proofend;

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)
proofend;

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)
proofend;

theorem :: NAT_3:15
for a being Nat
for f being FinSequence of REAL holds Product (f |^ a) = (Product f) |^ a
proofend;

begin

registration
let X be set ;
cluster Relation-like X -defined Function-like V14(X) natural-valued finite-support for set ;
existence
 ex b1 being ManySortedSet of X st
( b1 is natural-valued &amp; b1 is finite-support )
proofend;
end;

definition
let X be set ;
let b be real-valued ManySortedSet of X;
let a be Nat;
funca * b ->  ManySortedSet of X means :Def2: :: NAT_3:def 2
 for i being set holds it . i = a * (b . i);
existence
 ex b1 being ManySortedSet of X st
for i being set holds b1 . i = a * (b . i)
proofend;
uniqueness
 for b1, b2 being ManySortedSet of X st ( for i being set holds b1 . i = a * (b . i) ) &amp; ( for i being set holds b2 . i = a * (b . i) ) holds
b1 = b2
proofend;
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 b4 being ManySortedSet of X holds
( b4 = a * b iff for i being set holds b4 . i = a * (b . i) );

registration
let X be set ;
let b be real-valued ManySortedSet of X;
let a be Nat;
clustera * b ->  real-valued ;
coherence
 a * b is real-valued
proofend;
end;

registration
let X be set ;
let b be natural-valued ManySortedSet of X;
let a be Nat;
clustera * b ->  natural-valued ;
coherence
 a * b is natural-valued
proofend;
end;

registration
let X be set ;
let b be real-valued ManySortedSet of X;
cluster support (0 * b) ->  empty ;
coherence
 support (0 * b) is empty
proofend;
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)
proofend;

registration
let X be set ;
let b be real-valued finite-support ManySortedSet of X;
let a be Nat;
clustera * b ->  finite-support ;
coherence
 a * b is finite-support
proofend;
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 ) &amp; ( b1 . i > b2 . i implies it . i = b2 . i ) );
existence
 ex b1 being ManySortedSet of X st
for i being set holds
( ( b1 . i <= b2 . i implies b1 . i = b1 . i ) &amp; ( b1 . i > b2 . i implies b1 . i = b2 . i ) )
proofend;
uniqueness
 for b1, b2 being ManySortedSet of X st ( for i being set holds
( ( b1 . i <= b2 . i implies b1 . i = b1 . i ) &amp; ( b1 . i > b2 . i implies b1 . i = b2 . i ) ) ) &amp; ( for i being set holds
( ( b1 . i <= b2 . i implies b2 . i = b1 . i ) &amp; ( b1 . i > b2 . i implies b2 . i = b2 . i ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines min NAT_3:def_3_:_
 for X being set
for b1, b2 being real-valued ManySortedSet of X
for b4 being ManySortedSet of X holds
( b4 = min (b1,b2) iff for i being set holds
( ( b1 . i <= b2 . i implies b4 . i = b1 . i ) &amp; ( b1 . i > b2 . i implies b4 . i = b2 . i ) ) );

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

registration
let X be set ;
let b1, b2 be natural-valued ManySortedSet of X;
cluster min (b1,b2) ->  natural-valued ;
coherence
 min (b1,b2) is natural-valued
proofend;
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)
proofend;

registration
let X be set ;
let b1, b2 be real-valued finite-support ManySortedSet of X;
cluster min (b1,b2) ->  finite-support ;
coherence
 min (b1,b2) is finite-support
proofend;
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 ) &amp; ( b1 . i > b2 . i implies it . i = b1 . i ) );
existence
 ex b1 being ManySortedSet of X st
for i being set holds
( ( b1 . i <= b2 . i implies b1 . i = b2 . i ) &amp; ( b1 . i > b2 . i implies b1 . i = b1 . i ) )
proofend;
uniqueness
 for b1, b2 being ManySortedSet of X st ( for i being set holds
( ( b1 . i <= b2 . i implies b1 . i = b2 . i ) &amp; ( b1 . i > b2 . i implies b1 . i = b1 . i ) ) ) &amp; ( for i being set holds
( ( b1 . i <= b2 . i implies b2 . i = b2 . i ) &amp; ( b1 . i > b2 . i implies b2 . i = b1 . i ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines max NAT_3:def_4_:_
 for X being set
for b1, b2 being real-valued ManySortedSet of X
for b4 being ManySortedSet of X holds
( b4 = max (b1,b2) iff for i being set holds
( ( b1 . i <= b2 . i implies b4 . i = b2 . i ) &amp; ( b1 . i > b2 . i implies b4 . i = b1 . i ) ) );

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

registration
let X be set ;
let b1, b2 be natural-valued ManySortedSet of X;
cluster max (b1,b2) ->  natural-valued ;
coherence
 max (b1,b2) is natural-valued
proofend;
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)
proofend;

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

registration
let A be set ;
cluster Relation-like A -defined Function-like V14(A) complex-yielding finite-support for set ;
existence
 ex b1 being ManySortedSet of A st
( b1 is finite-support &amp; b1 is complex-yielding )
proofend;
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 &amp; f = b * (canFS (support b)) );
existence
 ex b1 being complex number ex f being FinSequence of COMPLEX st
( b1 = Product f &amp; f = b * (canFS (support b)) )
proofend;
uniqueness
 for b1, b2 being complex number st ex f being FinSequence of COMPLEX st
( b1 = Product f &amp; f = b * (canFS (support b)) ) &amp; ex f being FinSequence of COMPLEX st
( b2 = Product f &amp; f = b * (canFS (support b)) ) holds
b1 = b2 ;
end;

:: deftheorem Def5 defines Product NAT_3:def_5_:_
 for A being set
for b being complex-yielding finite-support ManySortedSet of A
for b3 being complex number holds
( b3 = Product b iff ex f being FinSequence of COMPLEX st
( b3 = Product f &amp; f = b * (canFS (support 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
proofend;
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)
proofend;

definition
let X be set ;
let b be real-valued ManySortedSet of X;
let n be non empty Nat;
funcb |^ n ->  ManySortedSet of X means :Def6: :: NAT_3:def 6
( support it = support b &amp; ( for i being set holds it . i = (b . i) |^ n ) );
existence
 ex b1 being ManySortedSet of X st
( support b1 = support b &amp; ( for i being set holds b1 . i = (b . i) |^ n ) )
proofend;
uniqueness
 for b1, b2 being ManySortedSet of X st support b1 = support b &amp; ( for i being set holds b1 . i = (b . i) |^ n ) &amp; support b2 = support b &amp; ( for i being set holds b2 . i = (b . i) |^ n ) holds
b1 = b2
proofend;
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 b4 being ManySortedSet of X holds
( b4 = b |^ n iff ( support b4 = support b &amp; ( for i being set holds b4 . i = (b . i) |^ n ) ) );

registration
let X be set ;
let b be natural-valued ManySortedSet of X;
let n be non empty Nat;
clusterb |^ n ->  natural-valued ;
coherence
 b |^ n is natural-valued
proofend;
end;

registration
let X be set ;
let b be real-valued finite-support ManySortedSet of X;
let n be non empty Nat;
clusterb |^ n ->  finite-support ;
coherence
 b |^ n is finite-support
proofend;
end;

theorem Th20: :: NAT_3:20
for A being set holds Product (EmptyBag A) = 1
proofend;

begin

definition
let n, d be Nat;
assume that
B1: d <> 1 and
B2: n <> 0 ;
funcd |-count n ->  Nat means :Def7: :: NAT_3:def 7
( d |^ it divides n &amp; not d |^ (it + 1) divides n );
existence
 ex b1 being Nat st
( d |^ b1 divides n &amp; not d |^ (b1 + 1) divides n )
proofend;
uniqueness
 for b1, b2 being Nat st d |^ b1 divides n &amp; not d |^ (b1 + 1) divides n &amp; d |^ b2 divides n &amp; not d |^ (b2 + 1) divides n holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines |-count NAT_3:def_7_:_
 for n, d being Nat st d <> 1 &amp; n <> 0 holds
for b3 being Nat holds
( b3 = d |-count n iff ( d |^ b3 divides n &amp; not d |^ (b3 + 1) divides n ) );

definition
let n, d be Nat;
:: original:|-count
redefine funcd |-count n ->  Element of NAT ;
coherence
 d |-count n is Element of NAT by ORDINAL1:def_12;
end;

theorem Th21: :: NAT_3:21
for n being Nat st n <> 1 holds
n |-count 1 = 0
proofend;

theorem :: NAT_3:22
for n being Nat st 1 < n holds
n |-count n = 1
proofend;

theorem Th23: :: NAT_3:23
for b, a being Nat st b <> 0 &amp; b < a &amp; a <> 1 holds
a |-count b = 0
proofend;

theorem :: NAT_3:24
for a being Nat
for p being Prime st a <> 1 &amp; a <> p holds
a |-count p = 0
proofend;

theorem Th25: :: NAT_3:25
for b, a being Nat st 1 < b holds
b |-count (b |^ a) = a
proofend;

theorem Th26: :: NAT_3:26
for b, a being Nat st b <> 1 &amp; a <> 0 &amp; b divides b |^ (b |-count a) holds
b divides a
proofend;

theorem Th27: :: NAT_3:27
for b, a being Nat st b <> 1 holds
( ( a <> 0 &amp; b |-count a = 0 ) iff not b divides a )
proofend;

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)
proofend;

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))
proofend;

theorem Th30: :: NAT_3:30
for p being Prime
for a, b being non empty Nat st b divides a holds
p |-count b <= p |-count a
proofend;

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)
proofend;

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)
proofend;

begin

definition
let n be Nat;
func prime_exponents n ->  ManySortedSet of SetPrimes  means :Def8: :: NAT_3:def 8
 for p being Prime holds it . p = p |-count n;
existence
 ex b1 being ManySortedSet of SetPrimes st
for p being Prime holds b1 . p = p |-count n
proofend;
uniqueness
 for b1, b2 being ManySortedSet of SetPrimes st ( for p being Prime holds b1 . p = p |-count n ) &amp; ( for p being Prime holds b2 . p = p |-count n ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines prime_exponents NAT_3:def_8_:_
 for n being Nat
for b2 being ManySortedSet of SetPrimes holds
( b2 = prime_exponents n iff for p being Prime holds b2 . p = p |-count n );

notation
let n be Nat;
synonym  pfexp n for  prime_exponents n;
end;

theorem Th33: :: NAT_3:33
for n being Nat
for x being set st x in dom (pfexp n) holds
x is Prime
proofend;

theorem Th34: :: NAT_3:34
for n being Nat
for x being set st x in support (pfexp n) holds
x is Prime
proofend;

theorem Th35: :: NAT_3:35
for a, n being Nat st a > n &amp; n <> 0 holds
(pfexp n) . a = 0
proofend;

registration
let n be Nat;
cluster prime_exponents n ->  natural-valued ;
coherence
 pfexp n is natural-valued
proofend;
end;

theorem :: NAT_3:36
for a, b being Nat st a in support (pfexp b) holds
a divides b
proofend;

theorem Th37: :: NAT_3:37
for b, a being Nat st not b is empty &amp; a is Prime &amp; a divides b holds
a in support (pfexp b)
proofend;

registration
let n be non empty Nat;
cluster prime_exponents n ->  finite-support ;
coherence
 pfexp n is finite-support
proofend;
end;

theorem Th38: :: NAT_3:38
for p being Prime
for a being non empty Nat st p divides a holds
(pfexp a) . p <> 0
proofend;

theorem Th39: :: NAT_3:39
pfexp 1 = EmptyBag SetPrimes
proofend;

registration
cluster support (pfexp 1) ->  empty ;
coherence
 support (pfexp 1) is empty
proofend;
end;

theorem Th40: :: NAT_3:40
for a being Nat
for p being Prime holds (pfexp (p |^ a)) . p = a
proofend;

theorem :: NAT_3:41
for p being Prime holds (pfexp p) . p = 1
proofend;

theorem Th42: :: NAT_3:42
for a being Nat
for p being Prime st a <> 0 holds
support (pfexp (p |^ a)) = {p}
proofend;

theorem Th43: :: NAT_3:43
for p being Prime holds support (pfexp p) = {p}
proofend;

registration
let p be Prime;
let a be non empty Nat;
cluster support (pfexp (p |^ a)) -> 1 -element ;
coherence
 support (pfexp (p |^ a)) is 1 -element
proofend;
end;

registration
let p be Prime;
cluster support (pfexp p) -> 1 -element ;
coherence
 support (pfexp p) is 1 -element
proofend;
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)
proofend;

theorem Th45: :: NAT_3:45
for a, b being non empty Nat holds support (pfexp a) c= support (pfexp (a * b))
proofend;

theorem Th46: :: NAT_3:46
for a, b being non empty Nat holds support (pfexp (a * b)) = (support (pfexp a)) \/ (support (pfexp b))
proofend;

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)))
proofend;

theorem :: NAT_3:48
for a, b being non empty Nat holds support (pfexp a) = support (pfexp (a |^ b))
proofend;

theorem :: NAT_3:49
for n, m being non empty Nat holds pfexp (n * m) = (pfexp n) + (pfexp m)
proofend;

theorem :: NAT_3:50
for m, n being non empty Nat st m divides n holds
pfexp (n div m) = (pfexp n) -' (pfexp m)
proofend;

theorem :: NAT_3:51
for a being Nat
for n being non empty Nat holds pfexp (n |^ a) = a * (pfexp n)
proofend;

theorem Th52: :: NAT_3:52
for n being non empty Nat st support (pfexp n) = {} holds
n = 1
proofend;

theorem :: NAT_3:53
for m, n being non empty Nat holds pfexp (n gcd m) = min ((pfexp n),(pfexp m))
proofend;

theorem :: NAT_3:54
for m, n being non empty Nat holds pfexp (n lcm m) = max ((pfexp n),(pfexp m))
proofend;

begin

definition
let n be non empty Nat;
func prime_factorization n ->  ManySortedSet of SetPrimes  means :Def9: :: NAT_3:def 9
( support it = support (pfexp n) &amp; ( for p being Nat st p in support (pfexp n) holds
it . p = p |^ (p |-count n) ) );
existence
 ex b1 being ManySortedSet of SetPrimes st
( support b1 = support (pfexp n) &amp; ( for p being Nat st p in support (pfexp n) holds
b1 . p = p |^ (p |-count n) ) )
proofend;
uniqueness
 for b1, b2 being ManySortedSet of SetPrimes st support b1 = support (pfexp n) &amp; ( for p being Nat st p in support (pfexp n) holds
b1 . p = p |^ (p |-count n) ) &amp; support b2 = support (pfexp n) &amp; ( for p being Nat st p in support (pfexp n) holds
b2 . p = p |^ (p |-count n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines prime_factorization NAT_3:def_9_:_
 for n being non empty Nat
for b2 being ManySortedSet of SetPrimes holds
( b2 = prime_factorization n iff ( support b2 = support (pfexp n) &amp; ( for p being Nat st p in support (pfexp n) holds
b2 . p = p |^ (p |-count n) ) ) );

notation
let n be non empty Nat;
synonym  ppf n for  prime_factorization n;
end;

:: for prime-power factorization
registration
let n be non empty Nat;
cluster prime_factorization n ->  natural-valued finite-support ;
coherence
 ( ppf n is natural-valued &amp; ppf n is finite-support )
proofend;
end;

theorem Th55: :: NAT_3:55
for p being Prime
for n being non empty Nat st p |-count n = 0 holds
(ppf n) . p = 0
proofend;

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)
proofend;

theorem :: NAT_3:57
for n being non empty Nat st support (ppf n) = {} holds
n = 1
proofend;

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)
proofend;

theorem Th59: :: NAT_3:59
for p being Prime
for n being non empty Nat holds (ppf (p |^ n)) . p = p |^ n
proofend;

theorem :: NAT_3:60
for n, m being non empty Nat holds ppf (n |^ m) = (ppf n) |^ m
proofend;

:: [WP: ] Fundamental_Theorem_of_Arithmetic
theorem :: NAT_3:61
for n being non empty Nat holds Product (ppf n) = n
proofend;