:: 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
proof end;
end;

registration
let a be non empty Nat;
let b be Nat;
cluster a |^ b -> non empty ;
coherence
not a |^ b is empty
proof end;
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
proof end;

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

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

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

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

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

theorem :: NAT_3:7
for a being Nat
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;

:: Power
definition
let f be real-valued FinSequence;
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
ex b1 being FinSequence st
( len b1 = len f & ( for i being set st i in dom b1 holds
b1 . i = (f . i) |^ a ) )
proof end;
uniqueness
for b1, b2 being FinSequence st len b1 = len f & ( for i being set st i in dom b1 holds
b1 . i = (f . i) |^ a ) & len b2 = len f & ( for i being set st i in dom b2 holds
b2 . i = (f . i) |^ a ) holds
b1 = b2
proof end;
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 & ( 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;
cluster f |^ a -> real-valued ;
coherence
f |^ a is real-valued
proof end;
end;

registration
let f be natural-valued FinSequence;
let a be Nat;
cluster f |^ a -> natural-valued ;
coherence
f |^ a is natural-valued
proof end;
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
proof end;
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
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 Nat holds (<*> REAL) |^ a = <*> REAL
proof end;

theorem Th12: :: NAT_3:12
for a being Nat
for r being Real holds <*r*> |^ a = <*(r |^ a)*>
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)
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)
proof end;

theorem :: NAT_3:15
for a being Nat
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 for set ;
existence
ex b1 being ManySortedSet of X st
( b1 is natural-valued & b1 is finite-support )
proof end;
end;

definition
let X be set ;
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
ex b1 being ManySortedSet of X st
for i being set holds b1 . i = a * (b . i)
proof end;
uniqueness
for b1, b2 being ManySortedSet of X st ( for i being set holds b1 . i = a * (b . i) ) & ( for i being set holds b2 . i = a * (b . i) ) holds
b1 = b2
proof end;
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;
cluster a * b -> real-valued ;
coherence
a * b is real-valued
proof end;
end;

registration
let X be set ;
let b be natural-valued ManySortedSet of X;
let a be Nat;
cluster a * b -> natural-valued ;
coherence
a * b is natural-valued
proof end;
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
proof end;
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)
proof end;

registration
let X be set ;
let b be real-valued finite-support ManySortedSet of X;
let a be Nat;
cluster a * b -> finite-support ;
coherence
a * b is finite-support
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
ex b1 being ManySortedSet of X st
for i being set holds
( ( b1 . i <= b2 . i implies b1 . i = b1 . i ) & ( b1 . i > b2 . i implies b1 . i = b2 . i ) )
proof end;
uniqueness
for b1, b2 being ManySortedSet of X st ( for i being set holds
( ( b1 . i <= b2 . i implies b1 . i = b1 . i ) & ( b1 . i > b2 . i implies b1 . i = b2 . i ) ) ) & ( for i being set holds
( ( b1 . i <= b2 . i implies b2 . i = b1 . i ) & ( b1 . i > b2 . i implies b2 . i = b2 . i ) ) ) holds
b1 = b2
proof end;
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 ) & ( 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
proof end;
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
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
min (b1,b2) is finite-support
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
ex b1 being ManySortedSet of X st
for i being set holds
( ( b1 . i <= b2 . i implies b1 . i = b2 . i ) & ( b1 . i > b2 . i implies b1 . i = b1 . i ) )
proof end;
uniqueness
for b1, b2 being ManySortedSet of X st ( for i being set holds
( ( b1 . i <= b2 . i implies b1 . i = b2 . i ) & ( b1 . i > b2 . i implies b1 . i = b1 . i ) ) ) & ( for i being set holds
( ( b1 . i <= b2 . i implies b2 . i = b2 . i ) & ( b1 . i > b2 . i implies b2 . i = b1 . i ) ) ) holds
b1 = b2
proof end;
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 ) & ( 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
proof end;
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
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
max (b1,b2) is finite-support
proof end;
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 & b1 is complex-yielding )
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
ex b1 being complex number ex f being FinSequence of COMPLEX st
( b1 = Product f & f = b * (canFS (support b)) )
proof end;
uniqueness
for b1, b2 being complex number st ex f being FinSequence of COMPLEX st
( b1 = Product f & f = b * (canFS (support b)) ) & ex f being FinSequence of COMPLEX st
( b2 = Product f & 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 & 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
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 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
ex b1 being ManySortedSet of X st
( support b1 = support b & ( for i being set holds b1 . i = (b . i) |^ n ) )
proof end;
uniqueness
for b1, b2 being ManySortedSet of X st support b1 = support b & ( for i being set holds b1 . i = (b . i) |^ n ) & support b2 = support b & ( for i being set holds b2 . i = (b . i) |^ n ) holds
b1 = b2
proof end;
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 & ( 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;
cluster b |^ n -> natural-valued ;
coherence
b |^ n is natural-valued
proof end;
end;

registration
let X be set ;
let b be real-valued finite-support ManySortedSet of X;
let n be non empty Nat;
cluster b |^ n -> finite-support ;
coherence
b |^ n is finite-support
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 Nat;
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
ex b1 being Nat st
( d |^ b1 divides n & not d |^ (b1 + 1) divides n )
proof end;
uniqueness
for b1, b2 being Nat st d |^ b1 divides n & not d |^ (b1 + 1) divides n & d |^ b2 divides n & not d |^ (b2 + 1) divides n holds
b1 = b2
proof end;
end;

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

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;

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

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

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

theorem :: NAT_3:24
for a being Nat
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 Nat st 1 < b holds
b |-count (b |^ a) = a
proof end;

theorem Th26: :: NAT_3:26
for b, a being Nat 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 Nat 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 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))
proof end;

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
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)
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)
proof end;

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
proof end;
uniqueness
for b1, b2 being ManySortedSet of SetPrimes st ( for p being Prime holds b1 . p = p |-count n ) & ( for p being Prime holds b2 . p = p |-count n ) holds
b1 = b2
proof end;
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
proof end;

theorem Th34: :: NAT_3:34
for n being Nat
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 Nat st a > n & n <> 0 holds
(pfexp n) . a = 0
proof end;

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

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

theorem Th37: :: NAT_3:37
for b, a being Nat 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 Nat;
cluster prime_exponents n -> finite-support ;
coherence
pfexp n is finite-support
proof end;
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
proof end;

theorem Th39: :: NAT_3:39
pfexp 1 = EmptyBag SetPrimes
proof end;

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

theorem Th40: :: NAT_3:40
for a being Nat
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 Nat
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 Nat;
cluster support (pfexp (p |^ a)) -> 1 -element ;
coherence
support (pfexp (p |^ a)) is 1 -element
proof end;
end;

registration
let p be Prime;
cluster support (pfexp p) -> 1 -element ;
coherence
support (pfexp p) is 1 -element
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 Nat 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 Nat holds support (pfexp a) = support (pfexp (a |^ b))
proof end;

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

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

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

theorem Th52: :: NAT_3:52
for n being non empty Nat 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 Nat;
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
ex b1 being ManySortedSet of SetPrimes st
( support b1 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b1 . p = p |^ (p |-count n) ) )
proof end;
uniqueness
for b1, b2 being ManySortedSet of SetPrimes st support b1 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b1 . p = p |^ (p |-count n) ) & support b2 = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b2 . p = p |^ (p |-count n) ) holds
b1 = b2
proof end;
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) & ( 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 & ppf n is finite-support )
proof end;
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
proof 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)
proof end;

theorem :: NAT_3:57
for n being non empty Nat 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 Nat holds (ppf (p |^ n)) . p = p |^ n
proof end;

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

:: WP: Fundamental Theorem of Arithmetic
theorem :: NAT_3:61
for n being non empty Nat holds Product (ppf n) = n
proof end;