:: Fundamental {T}heorem of {A}rithmetic
:: by Artur Korni{\l}owicz and Piotr Rudnicki
::
:: Received February 13, 2004
:: Copyright (c) 2004-2026 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, INT_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;
definitions TARSKI, XBOOLE_0, INT_1, INT_2, NAT_D, FINSEQ_1, VALUED_0,
PRE_POLY;
equalities FINSEQ_1, FINSEQ_2, PBOOLE, ORDINAL1;
expansions TARSKI, XBOOLE_0, INT_2, NAT_D, FINSEQ_1, VALUED_0, PBOOLE;
theorems ORDINAL1, NEWTON, NAT_1, XCMPLX_1, INT_1, CARD_4, XREAL_0, RVSUM_1,
INT_2, PEPIN, FUNCT_1, CARD_2, PREPOWER, FINSEQ_1, TARSKI, XBOOLE_1,
FUNCOP_1, WSIERP_1, XBOOLE_0, FINSEQ_2, FINSEQ_3, FINSEQ_4, RELAT_1,
FINSOP_1, FUNCT_2, XREAL_1, XXREAL_0, NAT_D, VALUED_0, XXREAL_2,
PARTFUN1, PRE_POLY, CARD_1;
schemes NAT_1, PRE_CIRC, FINSEQ_1, FINSEQ_2, PBOOLE, CLASSES1;
begin :: Preliminaries
reserve a, b, n for Nat,
r for Real,
f for FinSequence of REAL;
registration
cluster natural-valued for FinSequence;
existence
proof
take the FinSequence of NAT;
thus thesis;
end;
end;
registration
let a be non zero Nat;
let b be Nat;
cluster a |^ b -> non zero;
coherence by CARD_4:3;
end;
registration
cluster -> non zero for Prime;
coherence by INT_2:def 4;
end;
reserve p for Prime;
theorem Th1:
for a,b,c,d being Integer st a divides c & b divides d holds a*b divides c*d
proof
let a, b, c, d be Integer;
given x being Integer such that
A1: c = a*x;
given y being Integer such that
A2: d = b*y;
take x*y;
thus thesis by A1,A2;
end;
theorem Th2:
1 < a implies b < a |^ b
proof
defpred P[Nat] means $1 < a |^ $1;
assume
A1: 1 < a;
then reconsider a1 = a-1 as Element of NAT by INT_1:5;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
then
A3: k+1 < a |^ k + 1 by XREAL_1:6;
A4: now
set x = a |^ k;
assume x + 1 > x * a;
then x*a - (x+1) < (x+1) - (x+1) by XREAL_1:14;
then x*a1 - 1 + 1 < 0+1 by XREAL_1:6;
then x = 0 or a1 = 0 by NAT_1:13;
hence contradiction by A1;
end;
a |^ (k+1) = a |^ k * a by NEWTON:6;
hence thesis by A3,A4,XXREAL_0:2;
end;
A5: P[ 0 ] by A1;
for k being Nat holds P[k] from NAT_1:sch 2(A5,A2);
hence thesis;
end;
theorem Th3:
a <> 0 implies n divides n |^ a
proof
assume a <> 0;
then consider b being Nat such that
A1: a = b+1 by NAT_1:6;
reconsider b as Element of NAT by ORDINAL1:def 12;
n |^ 1 divides n |^ (b+1) by NAT_1:12,NEWTON:89;
hence thesis by A1;
end;
theorem Th4:
for i, j, m, n being Nat st i < j & m |^ j divides n
holds m |^ (i+1) divides n
proof
let i, j, m, n be Nat such that
A1: i < j and
A2: m |^ j divides n;
reconsider i,j,m as Element of NAT by ORDINAL1:def 12;
i+1 <= j by A1,NAT_1:13;
then m |^ (i+1) divides m |^ j by NEWTON:89;
hence thesis by A2,NAT_D:4;
end;
theorem Th5:
p divides a |^ b implies p divides a
proof
assume that
A1: p divides a |^ b and
A2: not p divides a;
reconsider p,a as Element of NAT by ORDINAL1:def 12;
defpred P[Nat] means p divides a|^($1+1);
A3: for k being Nat st k <> 0 & P[k] ex n being Nat st n < k & P[n]
proof
let k be Nat such that
A4: k <> 0 and
A5: P[k];
A6: p divides a |^ k * a by A5,NEWTON:6;
take k-'1;
A7: k >= 0+1 by A4,NAT_1:13;
then k-1 >= 0+1-1 by XREAL_1:13;
then k-'1 = k-1 by XREAL_0:def 2;
then k-'1 < k-0 by XREAL_1:15;
hence k-'1 < k;
k-'1+1 = k by A7,XREAL_1:235;
hence thesis by A2,A6,NEWTON:80;
end;
now
assume 0+1 > b;
then b = 0 by NAT_1:13;
then p divides 1 by A1,NEWTON:4;
then p = 1 by WSIERP_1:15;
hence contradiction by INT_2:def 4;
end;
then b = b-'1+1 by XREAL_1:235;
then
A8: ex k being Nat st P[k] by A1;
P[ 0 ] from NAT_1:sch 7(A8,A3);
hence thesis by A2;
end;
theorem Th6:
for a being Prime st a divides p |^ b holds a = p
proof
let a be Prime;
assume a divides p |^ b;
then a <> 1 & a divides p by Th5,INT_2:def 4;
hence thesis by INT_2:def 4;
end;
theorem
for f being FinSequence of NAT st a in rng f holds a divides Product f
proof
defpred P[FinSequence of NAT] means for a being Nat st a in rng
$1 holds a divides Product $1;
A1: for p being FinSequence of NAT, n being Element of NAT st P[p] holds P[p
^<*n*>]
proof
let p be FinSequence of NAT, n be Element of NAT such that
A2: P[p];
set p1 = p^<*n*>;
A3: rng p1 = rng p \/ rng <*n*> by FINSEQ_1:31;
A4: Product p1 = Product p * n by RVSUM_1:96;
let a be Nat such that
A5: a in rng p1;
per cases by A5,A3,XBOOLE_0:def 3;
suppose
a in rng p;
hence thesis by A2,A4,NAT_D:9;
end;
suppose
a in rng <*n*>;
then a in {n} by FINSEQ_1:39;
then a = n by TARSKI:def 1;
hence thesis by A4;
end;
end;
A6: P[<*>NAT qua FinSequence of NAT];
for p being FinSequence of NAT holds P[p] from FINSEQ_2:sch 2(A6,A1);
hence thesis;
end;
theorem
for f being FinSequence of SetPrimes st p divides Product f holds p in rng f
proof
let f be FinSequence of SetPrimes;
defpred P[FinSequence] means
ex f being FinSequence of SetPrimes st f = $1 &
for p being Prime st p divides Product f holds p in rng f;
A1: now
let f be FinSequence of SetPrimes, n be Element of SetPrimes;
set f1 = f^<*n*>;
assume
A2: P[f];
thus P[f1]
proof
reconsider nn = n as Nat;
reconsider ff = f as FinSequence of NAT;
reconsider f2 = f1 as FinSequence of SetPrimes;
take f2;
thus f2 = f1;
let p be Prime;
assume p divides Product f2;
then
A3: p divides Product ff * n by RVSUM_1:96;
per cases by A3,NEWTON:80;
suppose
A4: p divides Product f;
A5: rng f c= rng f1 by FINSEQ_1:29;
p in rng f by A2,A4;
hence thesis by A5;
end;
suppose
A6: p divides nn;
nn is prime by NEWTON:def 6;
then p = 1 or p = n by A6;
then p in {n} by INT_2:def 4,TARSKI:def 1;
then
A7: p in rng <*n*> by FINSEQ_1:38;
rng <*n*> c= rng f1 by FINSEQ_1:30;
hence thesis by A7;
end;
end;
end;
A8: P[<*>SetPrimes]
proof
take <*>SetPrimes;
thus thesis by INT_2:def 4,NAT_D:7,RVSUM_1:94;
end;
for p being FinSequence of SetPrimes holds P[p] from FINSEQ_2:sch 2(A8,A1);
then P[f];
hence thesis;
end;
:: Power
definition
let f be real-valued FinSequence;
let a be Nat;
func f |^ a -> FinSequence means
:Def1:
len it = len f & for i being set st i in dom it holds it.i = f.i |^ a;
existence
proof
deffunc F(Nat) = f.$1 |^ a;
consider p being FinSequence such that
A1: len p = len f & for k being Nat st k in dom p holds p.k = F(k)
from FINSEQ_1:sch 2;
take p;
thus thesis by A1;
end;
uniqueness
proof
let g,h be FinSequence such that
A2: len g = len f and
A3: for i being set st i in dom g holds g.i = f.i |^ a and
A4: len h = len f and
A5: for i being set st i in dom h holds h.i = f.i |^ a;
A6: dom g = Seg len g & dom h = Seg len h by FINSEQ_1:def 3;
for k being Nat st k in dom g holds g.k = h.k
proof
let k be Nat such that
A7: k in dom g;
thus g.k = f.k |^ a by A3,A7
.= h.k by A2,A4,A5,A6,A7;
end;
hence thesis by A2,A4,A6,FINSEQ_1:13;
end;
end;
registration
let f be real-valued FinSequence;
let a be Nat;
cluster f |^ a -> real-valued;
coherence
proof
let x be object;
set g = f|^a;
assume x in dom g;
then (f |^ a).x = f.x |^ a by Def1;
hence thesis;
end;
end;
registration
let f be natural-valued FinSequence;
let a be Nat;
cluster f |^ a -> natural-valued;
coherence
proof
let x be object;
set g = f|^a;
assume x in dom g;
then (f |^ a).x = f.x |^ a by Def1;
hence thesis;
end;
end;
definition
let f be FinSequence of REAL;
let a be Nat;
redefine func f |^ a -> FinSequence of REAL; :: redefines |^ (NAT_3, definition)
coherence
proof
thus rng (f|^a) c= REAL;
end;
end;
definition
let f be FinSequence of NAT;
let a be Nat;
redefine func f |^ a -> FinSequence of NAT; :: redefines |^ (NAT_3, definition)
coherence
proof
thus rng (f|^a) c= NAT by VALUED_0:def 6;
end;
end;
theorem Th9:
f |^ 0 = (len f) |-> 1
proof
A1: len (f|^0) = len f by Def1;
A2: for k being Nat st 1 <= k & k <= len (f|^0) holds (f|^0).k = (len f |->
1).k
proof
let k be Nat;
assume
A3: 1 <= k & k <= len (f|^0);
then
A4: k in dom (f|^0) by FINSEQ_3:25;
A5: k in Seg len f by A1,A3;
thus (f|^0).k = f.k |^ 0 by A4,Def1
.= 1 by NEWTON:4
.= (len f |-> 1).k by A5,FUNCOP_1:7;
end;
len (len f |-> 1) = len f by CARD_1:def 7;
hence thesis by A1,A2;
end;
theorem
f |^ 1 = f
proof
A1: for k being Nat st 1 <= k & k <= len (f|^1) holds (f|^1).k = f.k
proof
let k be Nat;
assume 1 <= k & k <= len (f|^1);
then k in dom (f|^1) by FINSEQ_3:25;
hence (f|^1).k = f.k |^ 1 by Def1
.= f.k;
end;
len (f|^1) = len f by Def1;
hence thesis by A1;
end;
theorem Th11:
<*>REAL |^ a = <*>REAL
proof
len (<*>REAL |^ a) = len <*>REAL by Def1
.= 0;
hence thesis;
end;
theorem Th12:
<*r*>|^a = <*r|^a*>
proof
A1: len (<*r*>|^a) = len <*r*> by Def1
.= 1 by FINSEQ_1:40;
0+1 in Seg (0+1);
then 1 in dom (<*r*>|^a) by A1,FINSEQ_1:def 3;
then (<*r*>|^a).1 = (<*r*>.1) |^ a by Def1
.= r |^ a;
hence thesis by A1,FINSEQ_1:40;
end;
theorem Th13:
(f^<*r*>) |^ a = (f|^a)^(<*r*>|^a)
proof
A1: len (f|^a) = len f by Def1;
A2: len ((f^<*r*>) |^ a) = len (f^<*r*>) by Def1
.= len f + len <*r*> by FINSEQ_1:22
.= len f + 1 by FINSEQ_1:40;
then
A3: dom ((f^<*r*>) |^ a) = Seg(len f +1) by FINSEQ_1:def 3;
A4: now
let i be Nat such that
A5: i in dom ((f^<*r*>) |^ a);
A6: 1 <= i by A3,A5,FINSEQ_1:1;
A7: i <= len f + 1 by A3,A5,FINSEQ_1:1;
per cases by A7,XXREAL_0:1;
suppose
i < len f +1;
then
A8: i <= len f by NAT_1:13;
then
A9: i in dom f by A6,FINSEQ_3:25;
A10: i in dom (f|^a) by A1,A6,A8,FINSEQ_3:25;
thus ((f^<*r*>) |^ a).i = (f^<*r*>).i |^ a by A5,Def1
.= f.i |^a by A9,FINSEQ_1:def 7
.= (f|^a).i by A10,Def1
.= ((f|^a)^(<*r*>|^a)).i by A10,FINSEQ_1:def 7;
end;
suppose
A11: i = len f +1;
thus ((f^<*r*>) |^ a).i = (f^<*r*>).i |^ a by A5,Def1
.= r |^ a by A11,FINSEQ_1:42
.= ((f|^a)^(<*r|^a*>)).i by A1,A11,FINSEQ_1:42
.= ((f|^a)^(<*r*>|^a)).i by Th12;
end;
end;
len ((f|^a)^(<*r*>|^a)) = len (f|^a) + len (<*r*>|^a) by FINSEQ_1:22
.= len f + len (<*r*>|^a) by Def1
.= len f + len (<*r|^a*>) by Th12
.= len f + 1 by FINSEQ_1:40;
hence thesis by A2,A4,FINSEQ_2:9;
end;
theorem Th14:
Product (f|^(b+1)) = Product (f|^b) * Product f
proof
defpred P[FinSequence of REAL] means for b being Nat holds
Product ($1|^(b+1)) = Product ($1|^b) * Product $1;
A1: now
let p be FinSequence of REAL, x being Element of REAL such that
A2: P[p];
thus P[p^<*x*>]
proof
set p1 = p^<*x*>;
let b be Nat;
reconsider xb1 = x|^(b+1), xb = x|^b as Real;
p1 |^ (b+1) = (p|^(b+1))^(<*x*>|^(b+1)) by Th13;
hence Product (p1|^(b+1)) = Product (p|^(b+1)) * Product (<*x*>|^(b+1))
by RVSUM_1:97
.= (Product (p|^b) * Product p) * Product (<*x*>|^(b+1)) by A2
.= (Product (p|^b) * Product p) * Product (<*xb1*>) by Th12
.= (Product (p|^b) * Product p) * x|^(b+1)
.= (Product (p|^b) * Product p) * (x|^b * x) by NEWTON:6
.= Product (p|^b) * x|^b * x * Product p
.= Product (p|^b ^ <*xb*>) * x * Product p by RVSUM_1:96
.= Product (p|^b ^ (<*x*>|^b)) * x * Product p by Th12
.= Product (p1|^b) * x * Product p by Th13
.= Product (p1|^b) * (Product p * x)
.= Product (p1|^b) * Product p1 by RVSUM_1:96;
end;
end;
A3: P[<*>REAL]
proof
set f = <*>REAL;
let b be Nat;
thus Product (f|^(b+1)) = 1 by Th11,RVSUM_1:94
.= Product (f|^b) * Product f by Th11,RVSUM_1:94;
end;
for p being FinSequence of REAL holds P[p] from FINSEQ_2:sch 2(A3, A1);
hence thesis;
end;
theorem
Product (f|^a) = (Product f) |^ a
proof
defpred P[Nat] means Product (f|^$1) = (Product f) |^ $1;
A1: P[b] implies P[b+1]
proof
assume
A2: P[b];
thus Product (f|^(b+1)) = Product (f|^b) * Product f by Th14
.= (Product f) |^ (b+1) by A2,NEWTON:6;
end;
Product (f|^0) = Product ((len f) |-> 1) by Th9
.= 1 by RVSUM_1:102
.= (Product f) |^ 0 by NEWTON:4;
then
A3: P[ 0 ];
P[b] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
begin :: More about bags
registration
let X be set;
cluster natural-valued finite-support for ManySortedSet of X;
existence
proof
set r = the natural-valued finite-support ManySortedSet of X;
r = r;
hence thesis;
end;
end;
definition
let X be set, b be real-valued ManySortedSet of X, a be Nat;
func a * b -> ManySortedSet of X means
:Def2:
for i being object holds it.i = a * b.i;
existence
proof
deffunc F(object) = a * b.$1;
consider f being ManySortedSet of X such that
A1: for i being object st i in X holds f.i = F(i) from PBOOLE:sch 4;
take f;
let i be object;
per cases;
suppose
i in X;
hence thesis by A1;
end;
suppose
A2: not i in X;
A3: dom b = X by PARTFUN1:def 2;
dom f = X by PARTFUN1:def 2;
hence f.i = a * (0 qua Nat) by A2,FUNCT_1:def 2
.= a * b.i by A2,A3,FUNCT_1:def 2;
end;
end;
uniqueness
proof
let f, g be ManySortedSet of X such that
A4: for i being object holds f.i = a * b.i and
A5: for i being object holds g.i = a * b.i;
for i being object st i in X holds f.i = g.i
proof
let i be object;
assume i in X;
thus f.i = a * b.i by A4
.= g.i by A5;
end;
hence thesis;
end;
end;
registration
let X be set, b be real-valued ManySortedSet of X, a be Nat;
cluster a * b -> real-valued;
coherence
proof
let x be object;
assume x in dom (a*b);
(a*b).x = a * b.x by Def2;
then (a*b).x is real;
hence thesis;
end;
end;
registration
let X be set, b be natural-valued ManySortedSet of X, a be Nat;
cluster a * b -> natural-valued;
coherence
proof
let x be object;
assume x in dom (a*b);
(a*b).x = a * b.x by Def2;
hence thesis;
end;
end;
registration
let X be set, b be real-valued ManySortedSet of X;
cluster support (0*b) -> empty;
coherence
proof
assume support (0*b) is non empty;
then consider x being object such that
A1: x in support (0*b);
(0*b).x <> 0 by A1,PRE_POLY:def 7;
then 0 * b.x <> 0 by Def2;
hence thesis;
end;
end;
theorem Th16:
for X being set, b being real-valued ManySortedSet of X st a <>
0 holds support b = support (a*b)
proof
let X be set, b be real-valued ManySortedSet of X such that
A1: a <> 0;
hereby
let x be object;
assume x in support b;
then b.x <> 0 by PRE_POLY:def 7;
then a*b.x <> 0 by A1;
then (a*b).x <> 0 by Def2;
hence x in support (a*b) by PRE_POLY:def 7;
end;
let x be object;
assume x in support (a*b);
then (a*b).x <> 0 by PRE_POLY:def 7;
then a*b.x <> 0 by Def2;
then b.x <> 0;
hence thesis by PRE_POLY:def 7;
end;
registration
let X be set, b be real-valued finite-support ManySortedSet of X, a be
Nat;
cluster a * b -> finite-support;
coherence
proof
per cases;
suppose
a = 0;
hence support (a*b) is finite;
end;
suppose
a <> 0;
then support (a*b) = support b by Th16;
hence support (a*b) is finite;
end;
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:
for i being object holds
(b1.i <= b2.i implies it.i = b1.i) & (b1.i > b2.i implies it.i = b2.i);
existence
proof
deffunc G(set) = b2.$1;
deffunc F(set) = b1.$1;
defpred P[set] means b1.$1 <= b2.$1;
consider f being ManySortedSet of X such that
A1: for i being Element of X st i in X holds (P[i] implies f.i = F(i))
& (not P[i] implies f.i = G(i)) from PRE_CIRC:sch 2;
take f;
let i be object;
per cases;
suppose
i in X;
hence thesis by A1;
end;
suppose
A2: not i in X;
then not i in dom f by PARTFUN1:def 2;
then
A3: f.i = 0 by FUNCT_1:def 2;
(not i in dom b1) & not i in dom b2 by A2,PARTFUN1:def 2;
hence thesis by A3,FUNCT_1:def 2;
end;
end;
uniqueness
proof
let f, g be ManySortedSet of X such that
A4: for i being object holds (b1.i <= b2.i implies f.i = b1.i) & (b1.i >
b2.i implies f.i = b2.i) and
A5: for i being object holds (b1.i <= b2.i implies g.i = b1.i) & (b1.i >
b2.i implies g.i = b2.i);
now
let i be object;
assume i in X;
per cases;
suppose
A6: b1.i <= b2.i;
hence f.i = b1.i by A4
.= g.i by A5,A6;
end;
suppose
A7: b1.i > b2.i;
hence f.i = b2.i by A4
.= g.i by A5,A7;
end;
end;
hence thesis;
end;
end;
registration
let X be set;
let b1, b2 be real-valued ManySortedSet of X;
cluster min(b1,b2) -> real-valued;
coherence
proof
let x be object;
set f = min(b1,b2);
assume x in dom f;
b1.x <= b2.x or b1.x > b2.x;
hence thesis by Def3;
end;
end;
registration
let X be set;
let b1, b2 be natural-valued ManySortedSet of X;
cluster min(b1,b2) -> natural-valued;
coherence
proof
let x be object;
set f = min(b1,b2);
assume x in dom f;
b1.x <= b2.x or b1.x > b2.x;
hence thesis by Def3;
end;
end;
theorem Th17:
for X being set, b1, b2 being real-valued finite-support ManySortedSet of X
holds support min(b1,b2) c= support b1 \/ support b2
proof
let X be set;
let b1, b2 be real-valued finite-support ManySortedSet of X;
set f = min(b1,b2);
let x be object;
assume x in support f;
then
A1: f.x <> 0 by PRE_POLY:def 7;
f.x = b1.x or f.x = b2.x by Def3;
then x in support b1 or x in support b2 by A1,PRE_POLY:def 7;
hence thesis by XBOOLE_0:def 3;
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
support min(b1,b2) c= support b1 \/ support b2 by Th17;
hence support min(b1,b2) is finite;
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:
for i being object holds
(b1.i <= b2.i implies it.i = b2.i) & (b1.i > b2.i implies it.i = b1.i);
existence
proof
deffunc G(set) = b1.$1;
deffunc F(set) = b2.$1;
defpred P[set] means b1.$1 <= b2.$1;
consider f being ManySortedSet of X such that
A1: for i being Element of X st i in X holds (P[i] implies f.i = F(i))
& (not P[i] implies f.i = G(i)) from PRE_CIRC:sch 2;
take f;
let i be object;
per cases;
suppose
i in X;
hence thesis by A1;
end;
suppose
A2: not i in X;
then not i in dom f by PARTFUN1:def 2;
then
A3: f.i = 0 by FUNCT_1:def 2;
( not i in dom b1)& not i in dom b2 by A2,PARTFUN1:def 2;
hence thesis by A3,FUNCT_1:def 2;
end;
end;
uniqueness
proof
let f, g be ManySortedSet of X such that
A4: for i being object holds (b1.i <= b2.i implies f.i = b2.i) & (b1.i >
b2.i implies f.i = b1.i) and
A5: for i being object holds (b1.i <= b2.i implies g.i = b2.i) & (b1.i >
b2.i implies g.i = b1.i);
now
let i be object;
assume i in X;
per cases;
suppose
A6: b1.i <= b2.i;
hence f.i = b2.i by A4
.= g.i by A5,A6;
end;
suppose
A7: b1.i > b2.i;
hence f.i = b1.i by A4
.= g.i by A5,A7;
end;
end;
hence thesis;
end;
end;
registration
let X be set;
let b1, b2 be real-valued ManySortedSet of X;
cluster max(b1,b2) -> real-valued;
coherence
proof
let x be object;
set f = max(b1,b2);
assume x in dom f;
b1.x <= b2.x or b1.x > b2.x;
hence thesis by Def4;
end;
end;
registration
let X be set;
let b1, b2 be natural-valued ManySortedSet of X;
cluster max(b1,b2) -> natural-valued;
coherence
proof
let x be object;
set f = max(b1,b2);
assume x in dom f;
b1.x <= b2.x or b1.x > b2.x;
hence thesis by Def4;
end;
end;
theorem Th18:
for X being set, b1, b2 being real-valued finite-support ManySortedSet of X
holds support max(b1,b2) c= support b1 \/ support b2
proof
let X be set;
let b1, b2 be real-valued finite-support ManySortedSet of X;
set f = max(b1,b2);
let x be object;
assume x in support f;
then
A1: f.x <> 0 by PRE_POLY:def 7;
f.x = b1.x or f.x = b2.x by Def4;
then x in support b1 or x in support b2 by A1,PRE_POLY:def 7;
hence thesis by XBOOLE_0:def 3;
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
support max(b1,b2) c= support b1 \/ support b2 by Th18;
hence support max(b1,b2) is finite;
end;
end;
registration
let A be set;
cluster finite-support complex-valued for ManySortedSet of A;
existence
proof
set f = the finite-support natural-valued ManySortedSet of A;
f is complex-valued;
hence thesis;
end;
end;
definition
let A be set, b be finite-support complex-valued ManySortedSet of A;
func Product b -> Complex means
:Def5:
ex f being FinSequence of COMPLEX st it = Product f & f = b*canFS(support b);
existence
proof
set cS = canFS(support b);
set f = b*cS;
A1: rng f c= COMPLEX by VALUED_0:def 1;
support b c= dom b & rng cS = support b by FUNCT_2:def 3,PRE_POLY:37;
then dom f = dom cS by RELAT_1:27;
then dom f = Seg len cS by FINSEQ_1:def 3;
then f is FinSequence by FINSEQ_1:def 2;
then reconsider f as FinSequence of COMPLEX by A1,FINSEQ_1:def 4;
take Product f;
thus thesis;
end;
uniqueness;
end;
definition
let A be set, b be bag of A;
redefine func Product b -> Element of NAT; :: redefines Product (NAT_3, definition)
coherence
proof
consider f being FinSequence of COMPLEX such that
A1: Product b = Product f and
A2: f = b*canFS support b by Def5;
rng b c= NAT & rng f c= rng b by A2,RELAT_1:26,VALUED_0:def 6;
then rng f c= NAT;
then reconsider g = f as FinSequence of NAT by FINSEQ_1:def 4;
Product g in NAT;
hence thesis by A1;
end;
end;
theorem Th19:
for X being set, a, b being bag of X st support a misses support b
holds Product (a+b) = (Product a) * Product b
proof
let X be set, a, b be bag of X;
set ab= a+b;
set Pa = Product a, Pb = Product b, Pab = Product ab;
set sab = support (a+b);
set sa = support a;
set sb = support b;
set ca = canFS(support a), cb = canFS(support b);
set cg = ca^cb, cf = canFS(support ab);
set p = cg" * cf;
A1: rng cf = sab by FUNCT_2:def 3;
assume support a misses support b;
then
A2: support a /\ support b = {};
A3: rng ca = sa by FUNCT_2:def 3;
A4: sab = sa \/ sb by PRE_POLY:38;
A5: rng cb = sb by FUNCT_2:def 3;
then
A6: rng cg = sab by A4,A3,FINSEQ_1:31;
A7: len cb = card sb & len ca = card sa by FINSEQ_1:93;
then
A8: len cg = card sa + card sb - card {} by FINSEQ_1:22
.= card sab by A2,A4,CARD_2:45;
then
A9: cg is one-to-one by A6,FINSEQ_4:62;
then
A10: dom (cg") = sab by A6,FUNCT_1:33;
then
A11: rng p = rng (cg") by A1,RELAT_1:28;
dom cg = Seg card sab by A8,FINSEQ_1:def 3;
then
A12: rng (cg") = Seg card sab by A9,FUNCT_1:33;
consider fa being FinSequence of COMPLEX such that
A13: Pa = Product fa and
A14: fa = a*canFS(support a) by Def5;
consider fb being FinSequence of COMPLEX such that
A15: Pb = Product fb and
A16: fb = b*canFS(support b) by Def5;
set g = fa^fb;
consider f being FinSequence of COMPLEX such that
A17: Pab = Product f and
A18: f = ab*canFS(support ab) by Def5;
dom a = X by PARTFUN1:def 2;
then
A19: dom ca = dom fa by A14,A3,RELAT_1:27;
then
A20: len ca = len fa by FINSEQ_3:29;
len cf = card sab by FINSEQ_1:93;
then
A21: dom cf = Seg card sab by FINSEQ_1:def 3;
then
A22: dom p = Seg card sab by A1,A10,RELAT_1:27;
A23: dom ab = X by PARTFUN1:def 2;
then
A24: dom f = Seg card sab by A18,A21,A1,RELAT_1:27;
dom b = X by PARTFUN1:def 2;
then dom cb = dom fb by A16,A5,RELAT_1:27;
then
A25: len cb = len fb by FINSEQ_3:29;
then len g = card sa + card sb - card {} by A7,A20,FINSEQ_1:22
.= card sab by A2,A4,CARD_2:45;
then
A26: dom g = Seg card sab by FINSEQ_1:def 3;
then reconsider p as Function of dom g, dom g by A12,A22,A11,FUNCT_2:1;
p is onto by A12,A26,A11,FUNCT_2:def 3;
then reconsider p as Permutation of dom g by A9;
A27: dom (g*p) = Seg card sab by A12,A22,A26,A11,RELAT_1:27;
A28: len cg = len ca + len cb by FINSEQ_1:22;
now
let x be object;
set cgx = cg".(cf.x);
assume
A29: x in dom f;
then
A30: (g*p).x = g.(p.x) by A24,A27,FUNCT_1:12
.= g.cgx by A21,A24,A29,FUNCT_1:13;
A31: cf.x in sab by A21,A1,A24,A29,FUNCT_1:3;
then consider d being object such that
A32: d in dom cg and
A33: cg.d = cf.x by A6,FUNCT_1:def 3;
cgx in Seg card sab by A10,A12,A31,FUNCT_1:3;
then reconsider cgx as Nat;
reconsider cgxN = cgx as Nat;
A34: cgx = d by A9,A32,A33,FUNCT_1:34;
then
A35: 1 <= cgxN by A32,FINSEQ_3:25;
A36: cgxN <= len fa + len fb by A20,A25,A28,A32,A34,FINSEQ_3:25;
per cases by A4,A31,XBOOLE_0:def 3;
suppose
cf.x in sa;
then
A37: not cf.x in sb by A2,XBOOLE_0:def 4;
now
A38: cgx -len ca <= len ca + len cb - len ca by A20,A25,A36,XREAL_1:9;
assume len fa < cgx;
then
A39: len fa +1 <= cgx by NAT_1:13;
then
A40: len ca +1 - len ca <= cgx - len ca by A20,XREAL_1:9;
then cgx - len ca is Element of NAT by INT_1:3;
then
A41: cgx-len ca in dom cb by A40,A38,FINSEQ_3:25;
cg.cgxN = cb.(cgx-len ca) by A20,A25,A36,A39,FINSEQ_1:23;
hence contradiction by A5,A33,A34,A37,A41,FUNCT_1:3;
end;
then
A42: cgxN in dom fa by A35,FINSEQ_3:25;
then
A43: cg.cgx = ca.cgx by A19,FINSEQ_1:def 7;
A44: g.cgx = fa.cgxN by A42,FINSEQ_1:def 7
.= a.(cf.x) by A14,A19,A33,A34,A42,A43,FUNCT_1:13;
thus f.x = ab.(cf.x) by A18,A29,FUNCT_1:12
.= a.(cf.x) + b.(cf.x) by PRE_POLY:def 5
.= a.(cf.x) + 0 by A37,PRE_POLY:def 7
.= (g*p).x by A30,A44;
end;
suppose
A45: cf.x in sb;
A46: now
assume len fa +1 > cgx;
then cgx <= len fa by NAT_1:13;
then
A47: cgx in dom ca by A19,A35,FINSEQ_3:25;
then ca.cgx in sa by A3,FUNCT_1:3;
then cg.cgxN in sa by A47,FINSEQ_1:def 7;
hence contradiction by A2,A33,A34,A45,XBOOLE_0:def 4;
end;
then
A48: cg.cgx = cb.(cgx-len ca) by A20,A25,A36,FINSEQ_1:23;
A49: cgx-len ca <= len ca + len cb - len ca by A20,A25,A36,XREAL_1:9;
A50: len ca + 1 - len ca <= cgx-len ca by A20,A46,XREAL_1:9;
then cgxN-len ca in NAT by INT_1:3;
then
A51: cgxN-len ca in dom cb by A49,A50,FINSEQ_3:25;
A52: g.cgx = fb.(cgxN-len fa) by A36,A46,FINSEQ_1:23
.= b.(cf.x) by A16,A20,A33,A34,A48,A51,FUNCT_1:13;
A53: not cf.x in sa by A2,A45,XBOOLE_0:def 4;
thus f.x = ab.(cf.x) by A18,A29,FUNCT_1:12
.= a.(cf.x) + b.(cf.x) by PRE_POLY:def 5
.= 0 + b.(cf.x) by A53,PRE_POLY:def 7
.= (g*p).x by A30,A52;
end;
end;
then
A54: f = g*p by A18,A21,A1,A23,A27,FUNCT_1:2,RELAT_1:27;
thus Product (a+b) = multcomplex $$ f by A17,RVSUM_1:def 13
.= multcomplex $$ g by A54,FINSOP_1:7
.= Product g by RVSUM_1:def 13
.= (Product a) * Product b by A13,A15,RVSUM_1:97;
end;
definition
let X be set, b be real-valued ManySortedSet of X, n be non zero Nat;
func b |^ n -> ManySortedSet of X means
:Def6:
support it = support b & for i being object holds it.i = b.i |^ n;
existence
proof
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
deffunc F(Element of X) = b.$1 |^ n;
defpred P[object,object] means
ex a being Element of X st a = $1 & $2 = F(a);
A1: n1 >= 1 by NAT_1:53;
A2: for e being object st e in X ex u being object st P[e,u]
proof
let e be object;
assume e in X;
then reconsider f = e as Element of X;
take F(f), f;
thus thesis;
end;
consider f being Function such that
A3: dom f = X and
A4: for x being object st x in X holds P[x,f.x] from CLASSES1:sch 1(A2);
reconsider f as ManySortedSet of X by A3,PARTFUN1:def 2,RELAT_1:def 18;
take f;
A5: dom b = X by PARTFUN1:def 2;
now
let x be object;
reconsider xx=x as set by TARSKI:1;
hereby
assume
A6: x in support f;
assume not x in support b;
then b.x = 0 by PRE_POLY:def 7;
then
A7: b.xx |^ n = 0 by A1,NEWTON:11;
support f c= X by A3,PRE_POLY:37;
then P[x,f.x] by A4,A6;
hence contradiction by A6,A7,PRE_POLY:def 7;
end;
A8: now
per cases;
suppose
x in X;
then P[x,f.x] by A4;
hence f.x = b.xx |^ n1;
end;
suppose
A9: not x in X;
hence f.x = 0 by A3,FUNCT_1:def 2
.= (0 qua Nat) |^ n1 by A1,NEWTON:11
.= b.xx |^ n1 by A5,A9,FUNCT_1:def 2;
end;
end;
assume x in support b;
then b.x <> 0 by PRE_POLY:def 7;
then f.x <> 0 by A8,CARD_4:3;
hence x in support f by PRE_POLY:def 7;
end;
hence support f = support b by TARSKI:2;
let i be object;
per cases;
suppose
i in X;
then P[i,f.i] by A4;
hence thesis;
end;
suppose
A10: not i in X;
hence f.i = 0 by A3,FUNCT_1:def 2
.= (0 qua Nat) |^ n by A1,NEWTON:11
.= b.i |^ n by A5,A10,FUNCT_1:def 2;
end;
end;
uniqueness
proof
let it1, it2 be ManySortedSet of X such that
support it1 = support b and
A11: for i being object holds it1.i = b.i |^ n and
support it2 = support b and
A12: for i being object holds it2.i = b.i |^ n;
now
let x be object such that
x in X;
thus it1.x = b.x |^ n by A11
.= it2.x by A12;
end;
hence it1 = it2;
end;
end;
registration
let X be set, b be natural-valued ManySortedSet of X, n be non zero Nat;
cluster b |^ n -> natural-valued;
coherence
proof
let x be object;
set f = b |^ n;
assume x in dom f;
f.x = b.x |^ n by Def6;
hence thesis;
end;
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;
coherence
proof
support b|^n = support b by Def6;
hence support b|^n is finite;
end;
end;
theorem Th20:
for A being set holds Product EmptyBag A = 1
proof
let A be set;
set b = EmptyBag A;
set cS = canFS(support b);
b*cS = <*>COMPLEX;
hence thesis by Def5,RVSUM_1:94;
end;
begin :: Multiplicity of a divisor
definition
let n, d be Nat such that
A1: d <> 1 and
A2: n <> 0;
func d |-count n -> Nat means
:Def7:
d |^ it divides n & not d |^ (it+1) divides n;
existence
proof
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
per cases;
suppose
A3: d = 0;
take 0;
(0 qua Nat) |^ 0 = 1 by NEWTON:4;
hence d |^ 0 divides n by A3,NAT_D:6;
not 0 divides n1 by A2;
hence not d |^ (0+1) divides n by A3;
end;
suppose
A4: d <> 0;
defpred P[Nat] means d |^ $1 divides n;
A5: for k being Nat st P[k] holds k <= n1
proof
let k be Nat;
assume P[k];
then
A6: d |^ k <= n by A2,NAT_D:7;
k <= d |^ k by A1,A4,Th2,NAT_1:25;
hence thesis by A6,XXREAL_0:2;
end;
A7: ex k being Nat st P[k]
proof
take 0;
d |^ 0 = 1 by NEWTON:4;
hence thesis by NAT_D:6;
end;
consider k being Nat such that
A8: P[k] & for n being Nat st P[n] holds n <= k from NAT_1:sch 6(A5
,A7 );
take k;
k+(0 qua Nat)< k+1 by XREAL_1:6;
hence thesis by A8;
end;
end;
uniqueness
proof
reconsider d1 = d as Element of NAT by ORDINAL1:def 12;
let a, b be Nat such that
A9: d |^ a divides n and
A10: ( not d |^ (a+1) divides n)& d |^ b divides n and
A11: not d |^ (b+1) divides n and
A12: a <> b;
reconsider a,b as Element of NAT by ORDINAL1:def 12;
per cases by A12,XXREAL_0:1;
suppose
A13: a < b;
then consider x being Nat such that
A14: a + x = b by NAT_1:10;
reconsider x as Element of NAT by ORDINAL1:def 12;
now
assume 0+1 > x;
then x = 0 by NAT_1:13;
hence contradiction by A13,A14;
end;
then a+1 <= a+x by XREAL_1:6;
then d1 |^ (a+1) divides d1 |^ (a+x) by NEWTON:89;
hence contradiction by A10,A14,NAT_D:4;
end;
suppose
A15: b < a;
then consider x being Nat such that
A16: b + x = a by NAT_1:10;
reconsider x as Element of NAT by ORDINAL1:def 12;
now
assume 0+1 > x;
then x = 0 by NAT_1:13;
hence contradiction by A15,A16;
end;
then b+1 <= b+x by XREAL_1:6;
then d1 |^ (b+1) divides d1 |^ (b+x) by NEWTON:89;
hence contradiction by A9,A11,A16,NAT_D:4;
end;
end;
end;
definition
let n, d be Nat;
redefine func d |-count n -> Element of NAT; :: redefines |-count (NAT_3, definition)
coherence by ORDINAL1:def 12;
end;
theorem Th21:
n <> 1 implies n |-count 1 = 0
proof
assume
A1: 1 <> n;
A2: now
assume
A3: n |^ (0+1) divides 1;
then n |^ 1 <= 1 by NAT_D:7;
then n <= 1;
then n = 0 by A1,NAT_1:25;
then 0 divides 1 by A3;
hence contradiction;
end;
n |^ 0 divides 1 by NEWTON:4;
hence thesis by A2,Def7;
end;
theorem
1 < n implies n |-count n = 1
proof
assume
A1: 1 < n;
A2: now
assume n |^ (1+1) divides n;
then n |^ 2 <= n by A1,NAT_D:7;
hence contradiction by A1,PREPOWER:13;
end;
n |^ 1 divides n;
hence thesis by A1,A2,Def7;
end;
theorem Th23:
b <> 0 & b < a & a <> 1 implies a |-count b = 0
proof
assume that
A1: b <> 0 and
A2: b < a and
A3: a <> 1;
a |^ 0 = 1 by NEWTON:4;
then
A4: a |^ 0 divides b by NAT_D:6;
not a |^ (0+1) divides b by A1,A2,NAT_D:7;
hence thesis by A1,A3,A4,Def7;
end;
theorem
a <> 1 & a <> p implies a |-count p = 0
proof
assume that
A1: a <> 1 and
A2: a <> p;
a |^ 0 = 1 by NEWTON:4;
then
A3: a |^ 0 divides p by NAT_D:6;
not a |^ (0+1) divides p by A1,A2,INT_2:def 4;
hence thesis by A1,A3,Def7;
end;
theorem Th25:
1 < b implies b |-count (b|^a) = a
proof
reconsider a as Element of NAT by ORDINAL1:def 12;
assume
A1: b > 1;
then reconsider b as non zero Element of NAT by ORDINAL1:def 12;
now
b|^a divides b|^(a+1) by NAT_1:11,NEWTON:89;
then
A2: b|^a <= b|^(a+1) by NAT_D:7;
assume b|^(a+1) divides b|^a;
then b|^(a+1) <= b|^a by NAT_D:7;
then b|^a = b|^(a+1) by A2,XXREAL_0:1;
then a+0 = a+1 by A1,PEPIN:30;
hence contradiction;
end;
hence thesis by A1,Def7;
end;
theorem Th26:
b <> 1 & a <> 0 & b divides b |^ (b |-count a) implies b divides a
proof
assume that
A1: b <> 1 & a <> 0 and
A2: b divides b |^ (b |-count a);
b |^ (b |-count a) divides a by A1,Def7;
hence thesis by A2,NAT_D:4;
end;
theorem Th27:
b <> 1 implies (a <> 0 & b |-count a = 0 iff not b divides a)
proof
1 divides a by NAT_D:6;
then
A1: b |^ 0 divides a by NEWTON:4;
assume
A2: b <> 1;
thus a <> 0 & b |-count a = 0 implies not b divides a
proof
assume that
A3: a <> 0 & b |-count a = 0 and
A4: b divides a;
not b |^ (0+1) divides a by A2,A3,Def7;
hence contradiction by A4;
end;
assume not b divides a;
then ( not b |^ (0+1) divides a)& a <> 0 by NAT_D:6;
hence thesis by A2,A1,Def7;
end;
theorem Th28:
for a, b being non zero Nat holds
p |-count (a*b) = (p |-count a) + (p |-count b)
proof
let a,b be non zero Nat;
set x = p |-count a;
set y = p |-count b;
A1: p <> 1 by INT_2:def 4;
then
A2: p |^ y divides b by Def7;
A3: p |^ x divides a by A1,Def7;
A4: now
assume p |^ (x+y+1) divides a*b;
then consider v being Nat such that
A5: a*b = p |^ (x+y+1) * v;
p |^ (x+y+1) = p |^ (x+y) * p by NEWTON:6;
then
A6: a*b = p |^ (x+y) * (p * v) by A5;
consider t being Nat such that
A7: a = (p |^ x) * t by A3;
A8: not p |^ (x+1) divides a by A1,Def7;
A9: not p |^ (y+1) divides b by A1,Def7;
consider u being Nat such that
A10: b = (p |^ y) * u by A2;
a*b = (p |^ x) * (p |^ y) * t * u by A7,A10
.= p |^ (x+y) * t * u by NEWTON:8
.= p |^ (x+y) * (t * u);
then p*v = t*u by A6,XCMPLX_1:5;
then
A11: p divides t*u;
per cases by A11,NEWTON:80;
suppose
p divides t;
then consider t1 being Nat such that
A12: t = p * t1;
a = (p |^ x) * p * t1 by A7,A12
.= p |^ (x+1) * t1 by NEWTON:6;
hence contradiction by A8;
end;
suppose
p divides u;
then consider t1 being Nat such that
A13: u = p * t1;
b = (p |^ y) * p * t1 by A10,A13
.= p |^ (y+1) * t1 by NEWTON:6;
hence contradiction by A9;
end;
end;
p |^ (x+y) = p |^ x * p |^ y by NEWTON:8;
then p |^ (x+y) divides a*b by A3,A2,Th1;
hence thesis by A1,A4,Def7;
end;
theorem Th29:
for a, b being non zero Nat holds
p |^ (p |-count (a*b)) = (p |^ (p |-count a)) * (p |^ (p |-count b))
proof
let a,b be non zero Nat;
set x = p |-count a;
set y = p |-count b;
thus p |^ (p |-count (a*b)) = p |^ (x + y) by Th28
.= (p |^ x) * (p |^ y) by NEWTON:8;
end;
theorem Th30:
for a, b being non zero Nat st b divides a holds p |-count b <= p |-count a
proof
let a,b be non zero Nat;
set x = p |-count a;
set y = p |-count b;
set z = p |-count (a div b);
0+1 <= p |^ z by NAT_1:13;
then
A1: 1 * p |^ y <= p |^ z * p |^ y by XREAL_1:66;
assume b divides a;
then
A2: a = b * (a div b);
then a div b <> 0;
then p > 1 & p |^ y <= p |^ x by A2,A1,Th29,INT_2:def 4;
hence thesis by PEPIN:66;
end;
theorem Th31:
for a, b being non zero Nat st b divides a holds
p |-count (a div b) = (p |-count a) -' (p |-count b)
proof
let a,b be non zero Nat;
set x = p |-count a;
set y = p |-count b;
set z = p |-count (a div b);
assume
A1: b divides a;
then a = b * (a div b);
then a div b <> 0;
then p |-count (b*(a div b)) = y + z by Th28;
then
A2: z + y = x + 0 by A1;
y <= x by A1,Th30;
then y-y <= x-y by XREAL_1:13;
hence thesis by A2,XREAL_0:def 2;
end;
theorem Th32:
for a being non zero Nat holds p |-count (a|^b) = b * (p |-count a)
proof
let a be non zero Nat;
A1: p <> 1 by INT_2:def 4;
defpred P[Nat] means p |-count (a|^$1) = $1 * (p |-count a);
A2: for x being Nat st P[x] holds P[x+1]
proof
let x be Nat such that
A3: P[x];
thus p |-count (a|^(x+1)) = p |-count (a|^x*a) by NEWTON:6
.= x * (p |-count a) + 1 * (p |-count a) by A3,Th28
.= (x+1) * (p |-count a);
end;
p |-count (a|^0) = p |-count 1 by NEWTON:4
.= 0 * (p |-count a) by A1,Th21;
then
A4: P[ 0 ];
for x being Nat holds P[x] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
begin :: Exponents in prime-power factorization
definition
let n be Nat;
func prime_exponents n -> ManySortedSet of SetPrimes means
:Def8:
for p being Prime holds it.p = p |-count n;
existence
proof
deffunc F(Nat) = $1 |-count n;
defpred P[object,object] means ex w being Nat st w = $1 & $2 = F(w);
A1: for i being object st i in SetPrimes ex j being object st P[i,j]
proof
let i be object;
assume i in SetPrimes;
then reconsider i as prime Element of NAT by NEWTON:def 6;
take F(i), i;
thus thesis;
end;
consider f being ManySortedSet of SetPrimes such that
A2: for i being object st i in SetPrimes holds P[i,f.i] from PBOOLE:sch 3
(A1);
take f;
let i be Prime;
i in SetPrimes by NEWTON:def 6;
then P[i,f.i] by A2;
hence thesis;
end;
uniqueness
proof
let f, g be ManySortedSet of SetPrimes such that
A3: for i being Prime holds f.i = i |-count n and
A4: for i being Prime holds g.i = i |-count n;
now
let i be object;
assume i in SetPrimes;
then reconsider a = i as prime Element of NAT by NEWTON:def 6;
thus f.i = a |-count n by A3
.= g.i by A4;
end;
hence thesis;
end;
end;
notation
let n be Nat;
synonym pfexp n for prime_exponents n;
end;
theorem Th33:
for x being set st x in dom pfexp n holds x is Prime
proof
let x be set;
assume x in dom pfexp n;
then x in SetPrimes by PARTFUN1:def 2;
hence thesis by NEWTON:def 6;
end;
theorem Th34:
for x being set st x in support pfexp n holds x is Prime
proof
let x be set;
set f = pfexp n;
A1: support f c= dom f by PRE_POLY:37;
assume x in support f;
hence thesis by A1,Th33;
end;
theorem Th35:
a > n & n <> 0 implies (pfexp n).a = 0
proof
assume
A1: a > n & n <> 0;
reconsider a as Element of NAT by ORDINAL1:def 12;
per cases;
suppose
a is not prime;
then not a in dom pfexp n by Th33;
hence thesis by FUNCT_1:def 2;
end;
suppose
A2: a is prime;
then a <> 1;
then a |-count n = 0 by A1,Th23;
hence thesis by A2,Def8;
end;
end;
registration
let n be Nat;
cluster pfexp n -> natural-valued;
coherence
proof
let x be object;
set f = pfexp n;
assume x in dom f;
then reconsider x as Prime by Th33;
f.x = x |-count n by Def8;
hence thesis;
end;
end;
theorem
a in support pfexp b implies a divides b
proof
set f = pfexp b;
assume
A1: a in support f;
then reconsider a as Prime by Th34;
A2: a <> 1 & f.a = a |-count b by Def8,INT_2:def 4;
f.a <> 0 by A1,PRE_POLY:def 7;
hence thesis by A2,Th27;
end;
theorem Th37:
b is non empty & a is Prime & a divides b implies a in support pfexp b
proof
assume that
A1: b is non empty and
A2: a is Prime and
A3: a divides b;
1 < a by A2,INT_2:def 4;
then
A4: a |-count b <> 0 by A1,A3,Th27;
(pfexp b).a = a |-count b by A2,Def8;
hence thesis by A4,PRE_POLY:def 7;
end;
registration
let n be non zero Nat;
cluster pfexp n -> finite-support;
coherence
proof
defpred P[Nat] means $1 is prime;
deffunc F(set) = $1;
set f = pfexp n;
reconsider n as Element of NAT by ORDINAL1:def 12;
set A = {F(i) where i is Nat: i <= n & P[i]};
A1: support f c= A
proof
let x be object;
assume
A2: x in support f;
then reconsider x as Prime by Th34;
f.x <> 0 by A2,PRE_POLY:def 7;
then x is prime Element of NAT & x <= n by Th35,ORDINAL1:def 12;
hence thesis;
end;
A is finite from FINSEQ_1:sch 6;
hence support f is finite by A1;
end;
end;
theorem Th38:
for a being non zero Nat st p divides a holds (pfexp a).p <> 0
proof
let a be non zero Nat;
assume p divides a;
then
A1: p |^ (0+1) divides a;
(pfexp a).p = p |-count a & p <> 1 by Def8,INT_2:def 4;
hence thesis by A1,Def7;
end;
theorem Th39:
pfexp 1 = EmptyBag SetPrimes
proof
set f = pfexp 1;
for z being object st z in dom f holds f.z = 0
proof
let z be object;
assume z in dom f;
then reconsider z as Prime by Th33;
A1: z <> 1 by INT_2:def 4;
f.z = z |-count 1 by Def8
.= 0 by A1,Th21;
hence thesis;
end;
then
A2: f = (dom f) --> 0 by FUNCOP_1:11;
dom f = SetPrimes by PARTFUN1:def 2;
hence thesis by A2;
end;
registration
cluster support pfexp 1 -> empty;
coherence by Th39;
end;
theorem Th40:
(pfexp (p|^a)).p = a
proof
set f = pfexp (p|^a);
p > 1 & f.p = p |-count (p|^a) by Def8,INT_2:def 4;
hence thesis by Th25;
end;
theorem
(pfexp p).p = 1
proof
p = p |^ 1;
hence thesis by Th40;
end;
theorem Th42:
a <> 0 implies support pfexp (p|^a) = {p}
proof
set f = pfexp (p|^a);
assume a <> 0;
then p divides p|^a by Th3;
then
A1: f.p <> 0 by Th38;
thus support f c= {p}
proof
let x be object;
assume
A2: x in support f;
then reconsider x as Prime by Th34;
A3: x <> 1 & f.x = x |-count (p|^a) by Def8,INT_2:def 4;
f.x <> 0 by A2,PRE_POLY:def 7;
then x divides p|^a by A3,Th27;
then x = p by Th6;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {p};
then x = p by TARSKI:def 1;
hence thesis by A1,PRE_POLY:def 7;
end;
theorem Th43:
support pfexp p = {p}
proof
p = p |^ 1;
hence thesis by Th42;
end;
registration
let p be Prime;
let a be non zero Nat;
cluster support pfexp (p|^a) -> 1-element;
coherence
proof
support pfexp (p|^a) = {p} by Th42;
hence thesis;
end;
end;
registration
let p be Prime;
cluster support pfexp p -> 1-element;
coherence
proof
support pfexp p = {p} by Th43;
hence thesis;
end;
end;
theorem Th44:
for a, b being non zero Nat st a,b are_coprime holds
support pfexp a misses support pfexp b
proof
let a, b be non zero Nat;
set f = pfexp a;
set g = pfexp b;
assume a,b are_coprime;
then
A1: a gcd b = 1;
assume support f meets support g;
then consider x being object such that
A2: x in support f and
A3: x in support g by XBOOLE_0:3;
reconsider x as Prime by A2,Th34;
A4: f.x = x |-count a by Def8;
A5: g.x = x |-count b by Def8;
g.x <> 0 by A3,PRE_POLY:def 7;
then
A6: x divides x |^ (x |-count b) by A5,Th3;
A7: x <> 1 by INT_2:def 4;
then x |^ (x |-count b) divides b by Def7;
then
A8: x divides b by A6,NAT_D:4;
f.x <> 0 by A2,PRE_POLY:def 7;
then
A9: x divides x |^ (x |-count a) by A4,Th3;
x |^ (x |-count a) divides a by A7,Def7;
then x divides a by A9,NAT_D:4;
then x divides 1 by A1,A8,NAT_D:def 5;
hence contradiction by A7,WSIERP_1:15;
end;
theorem Th45:
for a,b being non zero Nat holds support pfexp a c= support pfexp (a*b)
proof
let a, b be non zero Nat;
set f = pfexp a;
set h = pfexp (a*b);
let x be object;
assume
A1: x in support f;
then reconsider x as Prime by Th34;
A2: f.x = x |-count a by Def8;
f.x <> 0 by A1,PRE_POLY:def 7;
then
A3: x divides x |^ (x |-count a) by A2,Th3;
A4: x <> 1 by INT_2:def 4;
then x |^ (x |-count a) divides a by Def7;
then x divides a by A3,NAT_D:4;
then x |^ 1 divides a;
then
A5: x |^ (0+1) divides a*b by NAT_D:9;
h.x = x |-count (a*b) by Def8;
then h.x <> 0 by A4,A5,Def7;
hence thesis by PRE_POLY:def 7;
end;
theorem Th46:
for a, b being non zero Nat holds
support pfexp (a*b) = support pfexp a \/ support pfexp b
proof
let a, b be non zero Nat;
set f = pfexp a;
set g = pfexp b;
set h = pfexp (a*b);
thus support h c= support f \/ support g
proof
let x be object;
assume
A1: x in support h;
then reconsider x as Prime by Th34;
A2: h.x <> 0 by A1,PRE_POLY:def 7;
A3: x <> 1 by INT_2:def 4;
A4: h.x = x |-count (a*b) & x |^ (x |-count(a*b)) = (x |^ (x |-count a)) *
(x |^ (x |-count b)) by Def8,Th29;
per cases by A2,A4,Th3,NEWTON:80;
suppose
x divides x |^ (x |-count a);
then x divides a by A3,Th26;
then f.x <> 0 by Th38;
then x in support f by PRE_POLY:def 7;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x divides x |^ (x |-count b);
then x divides b by A3,Th26;
then g.x <> 0 by Th38;
then x in support g by PRE_POLY:def 7;
hence thesis by XBOOLE_0:def 3;
end;
end;
support f c= support h & support g c= support h by Th45;
hence thesis by XBOOLE_1:8;
end;
theorem
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
let a, b be non zero Nat;
assume
A1: a,b are_coprime;
support pfexp (a*b) = support pfexp a \/ support pfexp b by Th46;
hence thesis by A1,Th44,CARD_2:40;
end;
theorem
for a, b being non zero Nat holds support pfexp a = support pfexp (a|^b)
proof
let a, b be non zero Nat;
set f = pfexp a;
set g = pfexp (a|^b);
a|^b = a|^(b-'1) * a by PEPIN:26;
hence support f c= support g by Th45;
let x be object;
assume
A1: x in support g;
then reconsider x as Prime by Th34;
A2: g.x = x |-count (a|^b) & x <> 1 by Def8,INT_2:def 4;
g.x <> 0 by A1,PRE_POLY:def 7;
then x divides a|^b by A2,Th27;
then f.x <> 0 by Th5,Th38;
hence thesis by PRE_POLY:def 7;
end;
reserve n, m for non zero Nat;
theorem
pfexp (n*m) = pfexp n + pfexp m
proof
for i being object st i in SetPrimes holds (pfexp (n*m)).i = (pfexp n +
pfexp m).i
proof
let i be object;
assume i in SetPrimes;
then reconsider a = i as prime Element of NAT by NEWTON:def 6;
thus (pfexp (n*m)).i = a |-count (n*m) by Def8
.= (a |-count n) + (a |-count m) by Th28
.= (pfexp n).i + (a |-count m) by Def8
.= (pfexp n).i + (pfexp m).i by Def8
.= (pfexp n + pfexp m).i by PRE_POLY:def 5;
end;
hence thesis;
end;
theorem
m divides n implies pfexp (n div m) = pfexp n -' pfexp m
proof
assume
A1: m divides n;
for i being object st i in SetPrimes holds (pfexp (n div m)).i = (pfexp n
-' pfexp m).i
proof
let i be object;
assume i in SetPrimes;
then reconsider a = i as prime Element of NAT by NEWTON:def 6;
thus (pfexp (n div m)).i = a |-count (n div m) by Def8
.= (a |-count n) -' (a |-count m) by A1,Th31
.= (pfexp n).i -' (a |-count m) by Def8
.= (pfexp n).i -' (pfexp m).i by Def8
.= (pfexp n -' pfexp m).i by PRE_POLY:def 6;
end;
hence thesis;
end;
theorem
pfexp (n|^a) = a * pfexp n
proof
for i being object st i in SetPrimes
holds (pfexp (n|^a)).i = (a * pfexp n) .i
proof
let i be object;
assume i in SetPrimes;
then reconsider x = i as prime Element of NAT by NEWTON:def 6;
thus (pfexp (n|^a)).i = x |-count (n|^a) by Def8
.= a * (x |-count n) by Th32
.= a * (pfexp n).i by Def8
.= (a * pfexp n).i by Def2;
end;
hence thesis;
end;
theorem Th52:
support pfexp n = {} implies n = 1
proof
assume that
A1: support pfexp n = {} and
A2: n <> 1;
n >= 0+1 by NAT_1:13;
then n > 1 by A2,XXREAL_0:1;
then n >= 1+1 by NAT_1:13;
then consider p being Element of NAT such that
A3: p is prime and
A4: p divides n by INT_2:31;
p > 1 by A3;
then p |-count n <> 0 by A4,Th27;
then (pfexp n).p <> 0 by A3,Def8;
hence contradiction by A1,PRE_POLY:def 7;
end;
theorem
for m, n being non zero Nat holds pfexp (n gcd m) = min(pfexp n, pfexp m)
proof
let m, n be non zero Nat;
now
set rhs = min(pfexp n, pfexp m);
set lhs = pfexp (n gcd m);
let i be object;
assume i in SetPrimes;
then reconsider j = i as prime Element of NAT by NEWTON:def 6;
set x = j |-count n, y = j |-count m, z = j |-count (n gcd m);
A1: lhs.j = z by Def8;
A2: j <> 1 by INT_2:def 4;
then
A3: j |^ x divides n by Def7;
A4: n gcd m <> 0 by INT_2:5;
then
A5: j |^ z divides (n gcd m) by A2,Def7;
A6: not j |^ (z+1) divides (n gcd m) by A2,A4,Def7;
A7: not j |^ (y+1) divides m by A2,Def7;
A8: j |^ y divides m by A2,Def7;
n gcd m divides m by NAT_D:def 5;
then
A9: j |^ z divides m by A5,NAT_D:4;
A10: (pfexp n).j = x by Def8;
n gcd m divides n by NAT_D:def 5;
then
A11: j |^ z divides n by A5,NAT_D:4;
A12: (pfexp m).j = y by Def8;
A13: not j |^ (x+1) divides n by A2,Def7;
thus lhs.i = rhs.i
proof
per cases;
suppose
A14: (pfexp n).j <= (pfexp m).j;
A15: now
assume
A16: z < x;
then z < y by A10,A12,A14,XXREAL_0:2;
then
A17: j |^ (z+1) divides m by A8,Th4;
j |^ (z+1) divides n by A3,A16,Th4;
hence contradiction by A6,A17,NAT_D:def 5;
end;
A18: z <= x by A13,A11,Th4;
rhs.j = x by A10,A14,Def3;
hence thesis by A1,A18,A15,XXREAL_0:1;
end;
suppose
A19: (pfexp n).j > (pfexp m).j;
A20: now
assume
A21: z < y;
then z < x by A10,A12,A19,XXREAL_0:2;
then
A22: j |^ (z+1) divides n by A3,Th4;
j |^ (z+1) divides m by A8,A21,Th4;
hence contradiction by A6,A22,NAT_D:def 5;
end;
A23: z <= y by A7,A9,Th4;
rhs.j = y by A12,A19,Def3;
hence thesis by A1,A23,A20,XXREAL_0:1;
end;
end;
end;
hence thesis;
end;
theorem
for m, n being non zero Nat holds pfexp (n lcm m) = max(pfexp n, pfexp m)
proof
let m, n be non zero Nat;
now
set rhs = max(pfexp n, pfexp m);
set lhs = pfexp (n lcm m);
let i be object;
A1: m divides n lcm m by NAT_D:def 4;
assume i in SetPrimes;
then reconsider j = i as prime Element of NAT by NEWTON:def 6;
set x = j |-count n, y = j |-count m, z = j |-count (n lcm m);
A2: lhs.j = z by Def8;
A3: (pfexp n).j = x by Def8;
A4: j > 1 by INT_2:def 4;
then
A5: not j |^ (x+1) divides n by Def7;
A6: n lcm m <> 0 by INT_2:4;
then
A7: j |^ z divides (n lcm m) by A4,Def7;
A8: not j |^ (z+1) divides (n lcm m) by A4,A6,Def7;
A9: (pfexp m).j = y by Def8;
A10: n divides n lcm m by NAT_D:def 4;
A11: j |^ x divides n by A4,Def7;
then
A12: j |^ x divides n lcm m by A10,NAT_D:4;
A13: not j |^ (y+1) divides m by A4,Def7;
A14: j |^ y divides m by A4,Def7;
then
A15: j |^ y divides n lcm m by A1,NAT_D:4;
thus lhs.i = rhs.i
proof
per cases;
suppose
A16: (pfexp n).j <= (pfexp m).j;
A17: now
consider p being Nat such that
A18: y = x+p by A3,A9,A16,NAT_1:10;
consider t being Nat such that
A19: n = (j |^ x) * t by A11;
A20: now
assume j divides t;
then consider w being Nat such that
A21: t = j*w;
n = (j |^ x) * j * w by A19,A21
.= (j |^ (x+1)) * w by NEWTON:6;
hence contradiction by A5;
end;
consider u being Nat such that
A22: n lcm m = n*u by A10;
assume y < z;
then j |^ (y+1) divides n lcm m by A7,Th4;
then consider k being Nat such that
A23: n lcm m = (j |^ (y+1))*k;
A24: n lcm m = (j |^ y)*j*k by A23,NEWTON:6
.= (j |^ y)*(k*j);
(j |^ x)*((j |^ p) *(k*j)) = ((j |^ x)*(j |^ p)) *(k*j)
.= (j |^ x)*(t*u) by A24,A19,A22,A18,NEWTON:8;
then (j |^p)*k*j = t*u by XCMPLX_1:5;
then j divides t*u;
then j divides u by A20,NEWTON:80;
then consider w being Nat such that
A25: u = j*w;
(j |^ y)*k*j = n*w*j by A24,A22,A25;
then (j |^ y)*k = n*w by XCMPLX_1:5;
then
A26: n divides (j |^ y)*k;
consider t being Nat such that
A27: m = (j |^ y) * t by A14;
A28: now
assume j divides t;
then consider w being Nat such that
A29: t = j*w;
m = (j |^ y) * j * w by A27,A29
.= (j |^ (y+1)) * w by NEWTON:6;
hence contradiction by A13;
end;
consider u being Nat such that
A30: n lcm m = m*u by A1;
(j |^ y)*(k*j) = (j |^ y)*(t*u) by A24,A27,A30;
then k*j = t*u by XCMPLX_1:5;
then j divides t*u;
then j divides u by A28,NEWTON:80;
then consider w being Nat such that
A31: u = j*w;
(j |^ y)*k*j = m*w*j by A24,A30,A31;
then (j |^ y)*k = m*w by XCMPLX_1:5;
then m divides (j |^ y)*k;
then
A32: n lcm m divides (j |^ y)*k by A26,NAT_D:def 4;
0 <> k by A23,INT_2:4;
then j |^ (y+1) <= j |^ y by A23,A32,NAT_D:7,XREAL_1:68;
then (j |^ y) * j <= (j |^ y)*1 by NEWTON:6;
then j <= 1 by XREAL_1:68;
hence contradiction by INT_2:def 4;
end;
A33: y <= z by A8,A15,Th4;
rhs.j = y by A9,A16,Def4;
hence thesis by A2,A33,A17,XXREAL_0:1;
end;
suppose
A34: (pfexp n).j > (pfexp m).j;
A35: now
consider p being Nat such that
A36: x = y+p by A3,A9,A34,NAT_1:10;
consider t being Nat such that
A37: m = (j |^ y) * t by A14;
A38: now
assume j divides t;
then consider w being Nat such that
A39: t = j*w;
m = (j |^ y) * j * w by A37,A39
.= (j |^ (y+1)) * w by NEWTON:6;
hence contradiction by A13;
end;
consider u being Nat such that
A40: n lcm m = m*u by A1;
assume x < z;
then j |^ (x+1) divides n lcm m by A7,Th4;
then consider k being Nat such that
A41: n lcm m = (j |^ (x+1))*k;
A42: n lcm m = (j |^ x)*j*k by A41,NEWTON:6
.= (j |^ x)*(k*j);
(j |^ y)*((j |^ p) *(k*j)) = (j |^ y)*(j |^ p) *(k*j)
.= (j|^y)*(t*u) by A42,A37,A40,A36,NEWTON:8;
then t*u = (j|^p)*k*j by XCMPLX_1:5;
then j divides t*u;
then j divides u by A38,NEWTON:80;
then consider w being Nat such that
A43: u = j*w;
(j |^ x)*k*j = m*w*j by A42,A40,A43;
then (j |^ x)*k = m*w by XCMPLX_1:5;
then
A44: m divides (j |^ x)*k;
consider t being Nat such that
A45: n = (j |^ x) * t by A11;
A46: now
assume j divides t;
then consider w being Nat such that
A47: t = j*w;
n = (j |^ x) * j * w by A45,A47
.= (j |^ (x+1)) * w by NEWTON:6;
hence contradiction by A5;
end;
consider u being Nat such that
A48: n lcm m = n*u by A10;
(j |^ x)*(k*j) = (j |^ x)*(t*u) by A42,A45,A48;
then k*j = t*u by XCMPLX_1:5;
then j divides t*u;
then j divides u by A46,NEWTON:80;
then consider w being Nat such that
A49: u = j*w;
(j |^ x)*k*j = n*w*j by A42,A48,A49;
then (j |^ x)*k = n*w by XCMPLX_1:5;
then n divides (j |^ x)*k;
then
A50: n lcm m divides (j |^ x)*k by A44,NAT_D:def 4;
0 <> k by A41,INT_2:4;
then j |^ (x+1) <= j |^ x by A41,A50,NAT_D:7,XREAL_1:68;
then (j |^ x) * j <= (j |^ x)*1 by NEWTON:6;
then j <= 1 by XREAL_1:68;
hence contradiction by INT_2:def 4;
end;
A51: x <= z by A8,A12,Th4;
rhs.j = x by A3,A34,Def4;
hence thesis by A2,A51,A35,XXREAL_0:1;
end;
end;
end;
hence thesis;
end;
begin :: Prime-power factorization
definition
let n be non zero Nat;
func prime_factorization n -> ManySortedSet of SetPrimes means :Def9:
support it = support pfexp n &
for p being Nat st p in support pfexp n holds it.p = p |^ (p |-count n);
existence
proof
defpred P[object,object] means
for p being Prime st $1 = p holds
(p in support pfexp n implies $2 = p |^ (p |-count n)) &
(not p in support pfexp n implies $2 = 0);
A1: for x being object st x in SetPrimes ex y being object st P[x,y]
proof
let x be object;
assume x in SetPrimes;
then reconsider i = x as prime Element of NAT by NEWTON:def 6;
per cases;
suppose
A2: i in support pfexp n;
take i |^ (i |-count n);
let p be Prime;
assume p = x;
hence thesis by A2;
end;
suppose
A3: not i in support pfexp n;
take 0;
let p be Prime;
assume p = x;
hence thesis by A3;
end;
end;
consider f being Function such that
A4: dom f = SetPrimes and
A5: for x being object st x in SetPrimes holds P[x,f.x] from CLASSES1:sch
1(A1 );
A6: support f c= SetPrimes by A4,PRE_POLY:37;
A7: now
let x be object;
hereby
assume
A8: x in support f;
then x in SetPrimes by A6;
then reconsider i = x as prime Element of NAT by NEWTON:def 6;
assume not x in support pfexp n;
then f.i = 0 by A5,A6,A8;
hence contradiction by A8,PRE_POLY:def 7;
end;
assume
A9: x in support pfexp n;
then x in SetPrimes;
then reconsider i = x as prime Element of NAT by NEWTON:def 6;
f.i = i |^ (i |-count n) by A5,A9;
hence x in support f by PRE_POLY:def 7;
end;
reconsider f as ManySortedSet of SetPrimes by A4,PARTFUN1:def 2
,RELAT_1:def 18;
take f;
thus support f = support pfexp n by A7,TARSKI:2;
let p be Nat;
assume
A10: p in support pfexp n;
then p is Prime by Th34;
hence thesis by A5,A10;
end;
uniqueness
proof
let it1, it2 be ManySortedSet of SetPrimes such that
A11: support it1 = support pfexp n and
A12: for p being Nat st p in support pfexp n holds it1.p =
p|^(p|-count n) and
A13: support it2 = support pfexp n and
A14: for p being Nat st p in support pfexp n holds it2.p =
p|^(p|-count n);
now
let i be object;
assume i in SetPrimes;
then reconsider p = i as prime Element of NAT by NEWTON:def 6;
per cases;
suppose
A15: p in support pfexp n;
hence it1.i = p|^(p|-count n) by A12
.= it2.i by A14,A15;
end;
suppose
A16: not p in support pfexp n;
hence it1.i = 0 by A11,PRE_POLY:def 7
.= it2.i by A13,A16,PRE_POLY:def 7;
end;
end;
hence it1 = it2;
end;
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;
coherence
proof
rng ppf n c= NAT
proof
let y be object;
assume y in rng ppf n;
then consider x being object such that
A1: x in dom ppf n and
A2: (ppf n).x = y by FUNCT_1:def 3;
dom ppf n = SetPrimes by PARTFUN1:def 2;
then reconsider x as prime Element of NAT by A1,NEWTON:def 6;
per cases;
suppose
x in support pfexp n;
then (ppf n).x = x |^ (x |-count n) by Def9;
hence thesis by A2;
end;
suppose
not x in support pfexp n;
then not x in support ppf n by Def9;
then (ppf n).x = 0 by PRE_POLY:def 7;
hence thesis by A2;
end;
end;
hence ppf n is natural-valued;
support ppf n = support pfexp n by Def9;
hence support ppf n is finite;
end;
end;
theorem Th55:
p |-count n = 0 implies (ppf n).p = 0
proof
assume p |-count n = 0;
then (pfexp n).p = 0 by Def8;
then not p in support pfexp n by PRE_POLY:def 7;
then not p in support ppf n by Def9;
hence thesis by PRE_POLY:def 7;
end;
theorem Th56:
p |-count n <> 0 implies (ppf n).p = p |^ (p |-count n)
proof
assume p |-count n <> 0;
then (pfexp n).p <> 0 by Def8;
then p in support pfexp n by PRE_POLY:def 7;
hence thesis by Def9;
end;
theorem
support ppf n = {} implies n = 1
proof
assume support ppf n = {};
then support pfexp n = {} by Def9;
hence thesis by Th52;
end;
theorem Th58:
for a,b being non zero Nat st a, b are_coprime holds ppf(a*b) = ppf a + ppf b
proof
let a, b be non zero Nat such that
A1: a, b are_coprime;
reconsider an = a, bn = b as non zero Nat;
now
A2: a gcd b = 1 by A1;
let i be object;
assume i in SetPrimes;
then reconsider p = i as prime Element of NAT by NEWTON:def 6;
A3: p > 1 by INT_2:def 4;
A4: p |-count (an*bn) = (p |-count a) + (p |-count b) by Th28;
per cases;
suppose
A5: p |-count (a*b) = 0;
then
A6: (p |-count b) = 0 by A4;
A7: (p |-count a) = 0 by A4,A5;
thus (ppf (a*b)).i = 0 by A5,Th55
.= 0 + (ppf b).i by A6,Th55
.= (ppf a).i + (ppf b).i by A7,Th55
.= (ppf a + ppf b).i by PRE_POLY:def 5;
end;
suppose
A8: p |-count (a*b) <> 0;
thus (ppf (a*b)).i = (ppf a + ppf b).i
proof
per cases by A4,A8;
suppose
A9: (p |-count a) <> 0;
A10: now
consider ka being Nat such that
A11: (p |-count a) = ka+1 by A9,NAT_1:6;
p |^ (p |-count a) divides a by A3,Def7;
then p*(p|^ka) divides a by A11,NEWTON:6;
then consider la being Nat such that
A12: a = p*(p|^ka)*la;
a = p*((p|^ka)*la) by A12;
then
A13: p divides a;
assume (p |-count b) <> 0;
then consider kb being Nat such that
A14: (p |-count b) = kb+1 by NAT_1:6;
p |^ (p |-count b) divides b by A3,Def7;
then p*(p|^kb) divides b by A14,NEWTON:6;
then consider lb being Nat such that
A15: b = p*(p|^kb)*lb;
b = p*((p|^kb)*lb) by A15;
then p divides b;
then p divides 1 by A2,A13,NAT_D:def 5;
hence contradiction by A3,NAT_D:7;
end;
hence (ppf (a*b)).i = p |^ (p |-count a) by A4,A8,Th56
.= (ppf a).p + 0 by A9,Th56
.= (ppf a).p + (ppf b).p by A10,Th55
.= (ppf a + ppf b).i by PRE_POLY:def 5;
end;
suppose
A16: (p |-count b) <> 0;
A17: now
assume (p |-count a) <> 0;
then consider ka being Nat such that
A18: (p |-count a) = ka+1 by NAT_1:6;
p |^ (p |-count a) divides a by A3,Def7;
then p*(p|^ka) divides a by A18,NEWTON:6;
then consider la being Nat such that
A19: a = p*(p|^ka)*la;
a = p*((p|^ka)*la) by A19;
then
A20: p divides a;
consider kb being Nat such that
A21: (p |-count b) = kb+1 by A16,NAT_1:6;
p |^ (p |-count b) divides b by A3,Def7;
then p*(p|^kb) divides b by A21,NEWTON:6;
then consider lb being Nat such that
A22: b = p*(p|^kb)*lb;
b = p*((p|^kb)*lb) by A22;
then p divides b;
then p divides 1 by A2,A20,NAT_D:def 5;
hence contradiction by A3,NAT_D:7;
end;
hence (ppf (a*b)).i = p |^ (p |-count b) by A4,A8,Th56
.= 0+(ppf b).p by A16,Th56
.= (ppf a).p + (ppf b).p by A17,Th55
.= (ppf a + ppf b).i by PRE_POLY:def 5;
end;
end;
end;
end;
hence thesis;
end;
theorem Th59:
(ppf (p |^ n)).p = p |^ n
proof
p > 1 by INT_2:def 4;
then p |-count (p |^ n) = n by Th25;
hence thesis by Th56;
end;
theorem
ppf (n|^m) = (ppf n) |^ m
proof
now
let i be object;
A1: m >= 0+1 by NAT_1:13;
A2: ((ppf n) |^ m).i = (ppf n).i |^ m by Def6;
assume i in SetPrimes;
then reconsider p = i as prime Element of NAT by NEWTON:def 6;
A3: p |-count (n |^ m) = m * (p |-count n) by Th32;
per cases;
suppose
A4: p |-count n = 0;
hence (ppf (n|^m)).i = 0 by A3,Th55
.= (0 qua Nat) |^ m by A1,NEWTON:11
.= ((ppf n) |^ m).i by A2,A4,Th55;
end;
suppose
A5: p |-count n <> 0;
hence (ppf (n|^m)).i = p |^ (p |-count (n |^ m)) by A3,Th56
.= (p |^ (p |-count n)) |^ m by A3,NEWTON:9
.= ((ppf n) |^ m).i by A2,A5,Th56;
end;
end;
hence thesis;
end;
::$N Fundamental Theorem of Arithmetic
::$L https://en.wikipedia.org/wiki/Fundamental_theorem_of_arithmetic Fundamental Theorem of Arithmetic
theorem
Product ppf n = n
proof
defpred P[Nat] means for n being non zero Nat st
support ppf n c= Seg $1 holds Product ppf n = n;
A1: support ppf n = support pfexp n by Def9;
A2: P[ 0 ]
proof
let n be non zero Nat;
A3: {} c= support ppf n;
assume support ppf n c= Seg 0;
then
A4: support ppf n = {} by A3;
A5: now
reconsider k = n as Nat;
assume n <> 1;
then k > 1 by NAT_1:53;
then k >=1+1 by NAT_1:13;
then ex p being Element of NAT st p is prime & p divides k by INT_2:31;
then support pfexp n is non empty by Th37;
hence contradiction by A4,Def9;
end;
ppf n = EmptyBag SetPrimes by A4,PRE_POLY:81;
hence thesis by A5,Th20;
end;
A6: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A7: P[k];
let n be non zero Nat such that
A8: support ppf n c= Seg (k+1);
A9: support ppf n = support pfexp n by Def9;
per cases;
suppose
A10: not support ppf n c= Seg k;
set p = k+1;
set e = p |-count n;
set s = p |^ e;
A11: now
assume
A12: not k+1 in support ppf n;
support ppf n c= Seg k
proof
let x be object;
assume
A13: x in support ppf n;
then reconsider m = x as Nat;
m <= k+1 by A8,A13,FINSEQ_1:1;
then m < k+1 by A12,A13,XXREAL_0:1;
then
A14: m <= k by NAT_1:13;
x is Prime by A9,A13,Th34;
then 1 <= m by INT_2:def 4;
hence thesis by A14;
end;
hence contradiction by A10;
end;
then
A15: p is Prime by A9,Th34;
then
A16: p > 1 by INT_2:def 4;
then s divides n by Def7;
then consider t being Nat such that
A17: n = s * t;
reconsider s, t as non zero Nat by A17;
A18: dom ppf s = SetPrimes by PARTFUN1:def 2;
(pfexp n).p = e by A15,Def8;
then
A19: e <> 0 by A9,A11,PRE_POLY:def 7;
reconsider s1 = s, t1 = t as non zero Nat;
A20: support ppf t = support pfexp t by Def9;
A21: support ppf t c= Seg k
proof
set f = p |-count t;
let x be object;
assume
A22: x in support ppf t;
then reconsider m = x as Nat;
A23: x in support pfexp t by A22,Def9;
A24: now
assume
A25: m = p;
(pfexp t).p = f by A15,Def8;
then f <> 0 by A23,A25,PRE_POLY:def 7;
then f >= 0+1 by NAT_1:13;
then consider g being Nat such that
A26: f = 1+g by NAT_1:10;
p |^ f divides t by A16,Def7;
then consider u being Nat such that
A27: t = (p |^ f)*u;
n = s * (((p |^ g)*p)*u) by A17,A26,A27,NEWTON:6
.= s*p *((p |^ g)*u)
.= (p |^ (e+1))*((p |^ g)*u) by NEWTON:6;
then p |^ (e+1) divides n;
hence contradiction by A16,Def7;
end;
support ppf t c= support ppf n by A9,A17,A20,Th45;
then m in support ppf n by A22;
then m <= k+1 by A8,FINSEQ_1:1;
then m < p by A24,XXREAL_0:1;
then
A28: m <= k by NAT_1:13;
x is Prime by A23,Th34;
then 1 <= m by INT_2:def 4;
hence thesis by A28;
end;
s1,t1 are_coprime
proof
set u = s1 gcd t1;
A29: u divides t1 by NAT_D:def 5;
u <> 0 by INT_2:5;
then
A30: 0+1 <= u by NAT_1:13;
assume s1 gcd t1 <> 1;
then u > 1 by A30,XXREAL_0:1;
then u >= 1+1 by NAT_1:13;
then consider r being Element of NAT such that
A31: r is prime and
A32: r divides u by INT_2:31;
u divides s1 by NAT_D:def 5;
then r divides s1 by A32,NAT_D:4;
then r divides p by A31,Th5;
then r = 1 or r = p by A15,INT_2:def 4;
then p divides t1 by A31,A32,A29,NAT_D:4;
then p in support pfexp t by A15,Th37;
then k+1 <= k by A20,A21,FINSEQ_1:1;
hence contradiction by NAT_1:13;
end;
then
A33: ppf n = ppf s + ppf t by A17,Th58;
consider f being FinSequence of COMPLEX such that
A34: Product ppf s = Product f and
A35: f = (ppf s)*canFS(support ppf s) by Def5;
support ppf s = support pfexp s by Def9;
then
A36: support ppf s = {p} by A15,A19,Th42;
then f = (ppf s)*<*p*> by A35,FINSEQ_1:94
.= <* (ppf s).p *> by A11,A18,FINSEQ_2:34;
then
A37: Product ppf s = (ppf s).p by A34
.= s by A15,A19,Th59;
now
assume (support ppf s) /\ (support ppf t) <> {};
then consider x being object such that
A38: x in (support ppf s) /\ support ppf t by XBOOLE_0:def 1;
x in support ppf s by A38,XBOOLE_0:def 4;
then
A39: x = p by A36,TARSKI:def 1;
x in support ppf t by A38,XBOOLE_0:def 4;
then p <= k by A21,A39,FINSEQ_1:1;
hence contradiction by NAT_1:13;
end;
then
A40: support ppf s misses support ppf t;
Product ppf t = t by A7,A21;
hence thesis by A17,A40,A33,A37,Th19;
end;
suppose
support ppf n c= Seg k;
hence thesis by A7;
end;
end;
A41: for k being Nat holds P[k] from NAT_1:sch 2(A2,A6);
per cases;
suppose
support ppf n is empty;
hence thesis by A2;
end;
suppose
support ppf n is non empty;
then reconsider S = support ppf n as finite non empty Subset of NAT
by XBOOLE_1:1;
A42: max S is Nat by TARSKI:1;
support ppf n c= Seg max S
proof
let x be object;
assume
A43: x in support ppf n;
then reconsider m = x as Nat;
x is Prime by A1,A43,Th34;
then
A44: 1 <= m by INT_2:def 4;
m <= max S by A43,XXREAL_2:def 8;
hence thesis by A44;
end;
hence thesis by A42,A41;
end;
end;