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

registration

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

existence
ex b₁ being FinSequence st b₁ is natural-valued

proof end;

end;

registration

let a be non zero Nat;
let b be Nat;

cluster a |^ b -> non zero ;

coherence
not a |^ b is zero by CARD_4:3;

end;

registration

cluster V35() prime -> non zero for set ;

coherence
for b₁ being Prime holds not b₁ is zero 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 b₁ being FinSequence st
( len b₁ = len f & ( for i being set st i in dom b₁ holds
b₁ . i = (f . i) |^ a ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence st len b₁ = len f & ( for i being set st i in dom b₁ holds
b₁ . i = (f . i) |^ a ) & len b₂ = len f & ( for i being set st i in dom b₂ holds
b₂ . i = (f . i) |^ a ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines |^ NAT_3:def 1 :
for f being real-valued FinSequence
for a being Nat
for b₃ being FinSequence holds
( b₃ = f |^ a iff ( len b₃ = len f & ( for i being set st i in dom b₃ holds
b₃ . 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;

registration

let X be set ;

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

existence
ex b₁ being ManySortedSet of X st
( b₁ is natural-valued & b₁ 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 object holds it . i = a * (b . i);

existence
ex b₁ being ManySortedSet of X st
for i being object holds b₁ . i = a * (b . i)

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of X st ( for i being object holds b₁ . i = a * (b . i) ) & ( for i being object holds b₂ . i = a * (b . i) ) holds
b₁ = b₂

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 b₄ being ManySortedSet of X holds
( b₄ = a * b iff for i being object holds b₄ . 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 object holds
( ( b1 . i <= b2 . i implies it . i = b1 . i ) & ( b1 . i > b2 . i implies it . i = b2 . i ) );

existence
ex b₁ being ManySortedSet of X st
for i being object holds
( ( b1 . i <= b2 . i implies b₁ . i = b1 . i ) & ( b1 . i > b2 . i implies b₁ . i = b2 . i ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of X st ( for i being object holds
( ( b1 . i <= b2 . i implies b₁ . i = b1 . i ) & ( b1 . i > b2 . i implies b₁ . i = b2 . i ) ) ) & ( for i being object holds
( ( b1 . i <= b2 . i implies b₂ . i = b1 . i ) & ( b1 . i > b2 . i implies b₂ . i = b2 . i ) ) ) holds
b₁ = b₂

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 b₄ being ManySortedSet of X holds
( b₄ = min (b1,b2) iff for i being object holds
( ( b1 . i <= b2 . i implies b₄ . i = b1 . i ) & ( b1 . i > b2 . i implies b₄ . 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 object holds
( ( b1 . i <= b2 . i implies it . i = b2 . i ) & ( b1 . i > b2 . i implies it . i = b1 . i ) );

existence
ex b₁ being ManySortedSet of X st
for i being object holds
( ( b1 . i <= b2 . i implies b₁ . i = b2 . i ) & ( b1 . i > b2 . i implies b₁ . i = b1 . i ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of X st ( for i being object holds
( ( b1 . i <= b2 . i implies b₁ . i = b2 . i ) & ( b1 . i > b2 . i implies b₁ . i = b1 . i ) ) ) & ( for i being object holds
( ( b1 . i <= b2 . i implies b₂ . i = b2 . i ) & ( b1 . i > b2 . i implies b₂ . i = b1 . i ) ) ) holds
b₁ = b₂

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 b₄ being ManySortedSet of X holds
( b₄ = max (b1,b2) iff for i being object holds
( ( b1 . i <= b2 . i implies b₄ . i = b2 . i ) & ( b1 . i > b2 . i implies b₄ . 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-valued finite-support for set ;

existence
ex b₁ being ManySortedSet of A st
( b₁ is finite-support & b₁ is complex-valued )

proof end;

end;

definition

let A be set ;
let b be complex-valued finite-support ManySortedSet of A;

func Product b -> Complex means :Def5: :: NAT_3:def 5
ex f being FinSequence of COMPLEX st
( it = Product f & f = b * (canFS (support b)) );

existence
ex b₁ being Complex ex f being FinSequence of COMPLEX st
( b₁ = Product f & f = b * (canFS (support b)) )

proof end;

uniqueness
for b₁, b₂ being Complex st ex f being FinSequence of COMPLEX st
( b₁ = Product f & f = b * (canFS (support b)) ) & ex f being FinSequence of COMPLEX st
( b₂ = Product f & f = b * (canFS (support b)) ) holds
b₁ = b₂ ;

end;

:: deftheorem Def5 defines Product NAT_3:def 5 :
for A being set
for b being complex-valued finite-support ManySortedSet of A
for b₃ being Complex holds
( b₃ = Product b iff ex f being FinSequence of COMPLEX st
( b₃ = 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 zero Nat;

func b |^ n -> ManySortedSet of X means :Def6: :: NAT_3:def 6
( support it = support b & ( for i being object holds it . i = (b . i) |^ n ) );

existence
ex b₁ being ManySortedSet of X st
( support b₁ = support b & ( for i being object holds b₁ . i = (b . i) |^ n ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of X st support b₁ = support b & ( for i being object holds b₁ . i = (b . i) |^ n ) & support b₂ = support b & ( for i being object holds b₂ . i = (b . i) |^ n ) holds
b₁ = b₂

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 zero Nat
for b₄ being ManySortedSet of X holds
( b₄ = b |^ n iff ( support b₄ = support b & ( for i being object holds b₄ . i = (b . i) |^ n ) ) );

registration

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

definition

let n, d be Nat;
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
ex b₁ being Nat st
( d |^ b₁ divides n & not d |^ (b₁ + 1) divides n )

proof end;

uniqueness
for b₁, b₂ being Nat st d |^ b₁ divides n & not d |^ (b₁ + 1) divides n & d |^ b₂ divides n & not d |^ (b₂ + 1) divides n holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines |-count NAT_3:def 7 :
for n, d being Nat st d <> 1 & n <> 0 holds
for b₃ being Nat holds
( b₃ = d |-count n iff ( d |^ b₃ divides n & not d |^ (b₃ + 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 a, b 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 a, b being Nat st 1 < b holds
b |-count (b |^ a) = a

proof end;

theorem Th26: :: NAT_3:26

for a, b 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 a, b 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 zero 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 zero 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 zero 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 zero 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 zero Nat holds p |-count (a |^ b) = b * (p |-count a)

proof end;

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 b₁ being ManySortedSet of SetPrimes st
for p being Prime holds b₁ . p = p |-count n

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of SetPrimes st ( for p being Prime holds b₁ . p = p |-count n ) & ( for p being Prime holds b₂ . p = p |-count n ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines prime_exponents NAT_3:def 8 :
for n being Nat
for b₂ being ManySortedSet of SetPrimes holds
( b₂ = prime_exponents n iff for p being Prime holds b₂ . 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 a, b 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 zero 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 zero 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 by Th39;

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 zero 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 zero Nat st a,b are_coprime holds
support (pfexp a) misses support (pfexp b)

proof end;

theorem Th45: :: NAT_3:45

for a, b being non zero Nat holds support (pfexp a) c= support (pfexp (a * b))

proof end;

theorem Th46: :: NAT_3:46

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

proof end;

theorem :: NAT_3:47

for a, b being non zero Nat st a,b are_coprime 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 zero Nat holds support (pfexp a) = support (pfexp (a |^ b))

proof end;

theorem :: NAT_3:49

for n, m being non zero Nat holds pfexp (n * m) = (pfexp n) + (pfexp m)

proof end;

theorem :: NAT_3:50

for n, m being non zero 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 zero Nat holds pfexp (n |^ a) = a * (pfexp n)

proof end;

theorem Th52: :: NAT_3:52

for n being non zero Nat st support (pfexp n) = {} holds
n = 1

proof end;

theorem :: NAT_3:53

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

proof end;

theorem :: NAT_3:54

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

proof end;

definition

let n be non zero 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 b₁ being ManySortedSet of SetPrimes st
( support b₁ = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b₁ . p = p |^ (p |-count n) ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of SetPrimes st support b₁ = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b₁ . p = p |^ (p |-count n) ) & support b₂ = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b₂ . p = p |^ (p |-count n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines prime_factorization NAT_3:def 9 :
for n being non zero Nat
for b₂ being ManySortedSet of SetPrimes holds
( b₂ = prime_factorization n iff ( support b₂ = support (pfexp n) & ( for p being Nat st p in support (pfexp n) holds
b₂ . p = p |^ (p |-count n) ) ) );

notation

let n be non zero Nat;
synonym ppf n for prime_factorization n;

end;

:: for prime-power factorization

registration

let n be non zero 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 zero 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 zero Nat st p |-count n <> 0 holds
(ppf n) . p = p |^ (p |-count n)

proof end;

theorem :: NAT_3:57

for n being non zero Nat st support (ppf n) = {} holds
n = 1

proof end;

theorem Th58: :: NAT_3:58

for a, b being non zero Nat st a,b are_coprime holds
ppf (a * b) = (ppf a) + (ppf b)

proof end;

theorem Th59: :: NAT_3:59

for p being Prime
for n being non zero Nat holds (ppf (p |^ n)) . p = p |^ n

proof end;

theorem :: NAT_3:60

for n, m being non zero Nat holds ppf (n |^ m) = (ppf n) |^ m

proof end;

:: Fundamental Theorem of Arithmetic

theorem :: NAT_3:61

for n being non zero Nat holds Product (ppf n) = n

proof end;