:: 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
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, FINSEQ_1, VALUED_0, XBOOLE_0, NEWTON, ARYTM_3,
RELAT_1, NAT_1, XXREAL_0, ARYTM_1, SUBSET_1, CARD_1, CARD_3, ORDINAL4,
TARSKI, INT_2, FUNCT_1, FINSEQ_2, PRE_POLY, PBOOLE, FINSET_1, XCMPLX_0,
UPROOTS, FUNCT_2, BINOP_2, SETWISEO, INT_1, FUNCOP_1, NAT_3, XREAL_0;
notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_D, INT_2, RELAT_1, FUNCT_1,
FUNCT_2, FINSEQ_1, FINSEQ_2, VALUED_0, PBOOLE, RVSUM_1, NEWTON, WSIERP_1,
TREES_4, BINOP_2, FUNCOP_1, XXREAL_2, SETWOP_2, PRE_POLY;
constructors BINOP_1, SETWISEO, NAT_D, FINSEQOP, FINSOP_1, NEWTON, WSIERP_1,
BINOP_2, XXREAL_2, RELSET_1, PRE_POLY, REAL_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, NUMBERS, XCMPLX_0,
XXREAL_0, NAT_1, INT_1, BINOP_2, MEMBERED, NEWTON, VALUED_0, FINSEQ_1,
XXREAL_2, CARD_1, FUNCT_2, RELSET_1, ZFMISC_1, FINSEQ_2, PRE_POLY,
XREAL_0, RVSUM_1;
requirements NUMERALS, SUBSET, ARITHM, REAL, BOOLE;
begin :: Preliminaries
reserve a, b, n for Nat,
r for Real,
f for FinSequence of REAL;
registration
cluster natural-valued for FinSequence;
end;
registration
let a be non zero Nat;
let b be Nat;
cluster a |^ b -> non zero;
end;
registration
cluster -> non zero for Prime;
end;
reserve p for Prime;
theorem :: NAT_3:1
for a, b, c, d being Nat st a divides c & b divides d holds a*b divides c*d;
theorem :: NAT_3:2
1 < a implies b < a |^ b;
theorem :: NAT_3:3
a <> 0 implies n divides n |^ a;
theorem :: NAT_3:4
for i, j, m, n being Nat st i < j & m |^ j divides n
holds m |^ (i+1) divides n;
theorem :: NAT_3:5
p divides a |^ b implies p divides a;
theorem :: NAT_3:6
for a being Prime st a divides p |^ b holds a = p;
theorem :: NAT_3:7
for f being FinSequence of NAT st a in rng f holds a divides Product f;
theorem :: NAT_3:8
for f being FinSequence of SetPrimes st p divides Product f holds p in rng f;
:: Power
definition
let f be real-valued FinSequence;
let a be Nat;
func f |^ a -> FinSequence means
:: NAT_3:def 1
len it = len f & for i being set st i in dom it holds it.i = f.i |^ a;
end;
registration
let f be real-valued FinSequence;
let a be Nat;
cluster f |^ a -> real-valued;
end;
registration
let f be natural-valued FinSequence;
let a be Nat;
cluster f |^ a -> natural-valued;
end;
definition
let f be FinSequence of REAL;
let a be Nat;
redefine func f |^ a -> FinSequence of REAL;
end;
definition
let f be FinSequence of NAT;
let a be Nat;
redefine func f |^ a -> FinSequence of NAT;
end;
theorem :: NAT_3:9
f |^ 0 = (len f) |-> 1;
theorem :: NAT_3:10
f |^ 1 = f;
theorem :: NAT_3:11
<*>REAL |^ a = <*>REAL;
theorem :: NAT_3:12
<*r*>|^a = <*r|^a*>;
theorem :: NAT_3:13
(f^<*r*>) |^ a = (f|^a)^(<*r*>|^a);
theorem :: NAT_3:14
Product (f|^(b+1)) = Product (f|^b) * Product f;
theorem :: NAT_3:15
Product (f|^a) = (Product f) |^ a;
begin :: More about bags
registration
let X be set;
cluster natural-valued finite-support for ManySortedSet of X;
end;
definition
let X be set, b be real-valued ManySortedSet of X, a be Nat;
func a * b -> ManySortedSet of X means
:: NAT_3:def 2
for i being object holds it.i = a * b.i;
end;
registration
let X be set, b be real-valued ManySortedSet of X, a be Nat;
cluster a * b -> real-valued;
end;
registration
let X be set, b be natural-valued ManySortedSet of X, a be Nat;
cluster a * b -> natural-valued;
end;
registration
let X be set, b be real-valued ManySortedSet of X;
cluster support (0*b) -> empty;
end;
theorem :: NAT_3:16
for X being set, b being real-valued ManySortedSet of X st a <>
0 holds support b = support (a*b);
registration
let X be set, b be real-valued finite-support ManySortedSet of X, a be
Nat;
cluster a * b -> finite-support;
end;
definition
let X be set;
let b1, b2 be real-valued ManySortedSet of X;
func min(b1,b2) -> ManySortedSet of X means
:: 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);
end;
registration
let X be set;
let b1, b2 be real-valued ManySortedSet of X;
cluster min(b1,b2) -> real-valued;
end;
registration
let X be set;
let b1, b2 be natural-valued ManySortedSet of X;
cluster min(b1,b2) -> natural-valued;
end;
theorem :: NAT_3:17
for X being set, b1, b2 being real-valued finite-support
ManySortedSet of X holds support min(b1,b2) c= support b1 \/ support b2;
registration
let X be set;
let b1, b2 be real-valued finite-support ManySortedSet of X;
cluster min(b1,b2) -> finite-support;
end;
definition
let X be set;
let b1, b2 be real-valued ManySortedSet of X;
func max(b1,b2) -> ManySortedSet of X means
:: 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);
end;
registration
let X be set;
let b1, b2 be real-valued ManySortedSet of X;
cluster max(b1,b2) -> real-valued;
end;
registration
let X be set;
let b1, b2 be natural-valued ManySortedSet of X;
cluster max(b1,b2) -> natural-valued;
end;
theorem :: NAT_3:18
for X being set, b1, b2 being real-valued finite-support
ManySortedSet of X holds support max(b1,b2) c= support b1 \/ support b2;
registration
let X be set;
let b1, b2 be real-valued finite-support ManySortedSet of X;
cluster max(b1,b2) -> finite-support;
end;
registration
let A be set;
cluster finite-support complex-valued for ManySortedSet of A;
end;
definition
let A be set, b be finite-support complex-valued ManySortedSet of A;
func Product b -> Complex means
:: NAT_3:def 5
ex f being FinSequence of COMPLEX st it = Product f & f = b*canFS(support b);
end;
definition
let A be set, b be bag of A;
redefine func Product b -> Element of NAT;
end;
theorem :: NAT_3:19
for X being set, a, b being bag of X st support a misses support
b holds Product (a+b) = (Product a) * Product b;
definition
let X be set, b be real-valued ManySortedSet of X, n be non zero Nat;
func b |^ n -> ManySortedSet of X means
:: NAT_3:def 6
support it = support b & for i being object holds it.i = b.i |^ n;
end;
registration
let X be set, b be natural-valued ManySortedSet of X, n be non zero Nat;
cluster b |^ n -> natural-valued;
end;
registration
let X be set, b be real-valued finite-support ManySortedSet of X,
n be non zero Nat;
cluster b |^ n -> finite-support;
end;
theorem :: NAT_3:20
for A being set holds Product EmptyBag A = 1;
begin :: Multiplicity of a divisor
definition
let n, d be Nat such that
d <> 1 and
n <> 0;
func d |-count n -> Nat means
:: NAT_3:def 7
d |^ it divides n & not d |^ (it+1) divides n;
end;
definition
let n, d be Nat;
redefine func d |-count n -> Element of NAT;
end;
theorem :: NAT_3:21
n <> 1 implies n |-count 1 = 0;
theorem :: NAT_3:22
1 < n implies n |-count n = 1;
theorem :: NAT_3:23
b <> 0 & b < a & a <> 1 implies a |-count b = 0;
theorem :: NAT_3:24
a <> 1 & a <> p implies a |-count p = 0;
theorem :: NAT_3:25
1 < b implies b |-count (b|^a) = a;
theorem :: NAT_3:26
b <> 1 & a <> 0 & b divides b |^ (b |-count a) implies b divides a;
theorem :: NAT_3:27
b <> 1 implies (a <> 0 & b |-count a = 0 iff not b divides a);
theorem :: NAT_3:28
for a, b being non zero Nat holds p |-count (a*b) =
(p |-count a) + (p |-count b);
theorem :: NAT_3:29
for a, b being non zero Nat holds p |^ (p |-count (a
*b)) = (p |^ (p |-count a)) * (p |^ (p |-count b));
theorem :: NAT_3:30
for a, b being non zero Nat st b divides a holds p
|-count b <= p |-count a;
theorem :: NAT_3:31
for a, b being non zero Nat st b divides a holds p
|-count (a div b) = (p |-count a) -' (p |-count b);
theorem :: NAT_3:32
for a being non zero Nat holds p |-count (a|^b) = b
* (p |-count a);
begin :: Exponents in prime-power factorization
definition
let n be Nat;
func prime_exponents n -> ManySortedSet of SetPrimes means
:: NAT_3:def 8
for p being Prime holds it.p = p |-count n;
end;
notation
let n be Nat;
synonym pfexp n for prime_exponents n;
end;
theorem :: NAT_3:33
for x being set st x in dom pfexp n holds x is Prime;
theorem :: NAT_3:34
for x being set st x in support pfexp n holds x is Prime;
theorem :: NAT_3:35
a > n & n <> 0 implies (pfexp n).a = 0;
registration
let n be Nat;
cluster pfexp n -> natural-valued;
end;
theorem :: NAT_3:36
a in support pfexp b implies a divides b;
theorem :: NAT_3:37
b is non empty & a is Prime & a divides b implies a in support pfexp b;
registration
let n be non zero Nat;
cluster pfexp n -> finite-support;
end;
theorem :: NAT_3:38
for a being non zero Nat st p divides a holds (pfexp a).p <> 0;
theorem :: NAT_3:39
pfexp 1 = EmptyBag SetPrimes;
registration
cluster support pfexp 1 -> empty;
end;
theorem :: NAT_3:40
(pfexp (p|^a)).p = a;
theorem :: NAT_3:41
(pfexp p).p = 1;
theorem :: NAT_3:42
a <> 0 implies support pfexp (p|^a) = {p};
theorem :: NAT_3:43
support pfexp p = {p};
registration
let p be Prime;
let a be non zero Nat;
cluster support pfexp (p|^a) -> 1-element;
end;
registration
let p be Prime;
cluster support pfexp p -> 1-element;
end;
theorem :: NAT_3:44
for a, b being non zero Nat st a,b are_coprime holds
support pfexp a misses support pfexp b;
theorem :: NAT_3:45
for a,b being non zero Nat holds support pfexp a c=
support pfexp (a*b);
theorem :: NAT_3:46
for a, b being non zero Nat holds support pfexp (a*b) = support
pfexp a \/ support pfexp b;
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;
theorem :: NAT_3:48
for a, b being non zero Nat holds support pfexp a =
support pfexp (a|^b);
reserve n, m for non zero Nat;
theorem :: NAT_3:49
pfexp (n*m) = pfexp n + pfexp m;
theorem :: NAT_3:50
m divides n implies pfexp (n div m) = pfexp n -' pfexp m;
theorem :: NAT_3:51
pfexp (n|^a) = a * pfexp n;
theorem :: NAT_3:52
support pfexp n = {} implies n = 1;
theorem :: NAT_3:53
for m, n being non zero Nat holds pfexp (n gcd m) = min(pfexp n, pfexp m);
theorem :: NAT_3:54
for m, n being non zero Nat holds pfexp (n lcm m) = max(pfexp n, pfexp m);
begin :: Prime-power factorization
definition
let n be non zero Nat;
func prime_factorization n -> ManySortedSet of SetPrimes means
:: 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);
end;
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 ppf n -> natural-valued finite-support;
end;
theorem :: NAT_3:55
p |-count n = 0 implies (ppf n).p = 0;
theorem :: NAT_3:56
p |-count n <> 0 implies (ppf n).p = p |^ (p |-count n);
theorem :: NAT_3:57
support ppf n = {} implies n = 1;
theorem :: NAT_3:58
for a, b being non zero Nat st a, b are_coprime holds
ppf (a*b) = ppf a + ppf b;
theorem :: NAT_3:59
(ppf (p |^ n)).p = p |^ n;
theorem :: NAT_3:60
ppf (n|^m) = (ppf n) |^ m;
::$N Fundamental Theorem of Arithmetic
theorem :: NAT_3:61
Product ppf n = n;