:: On the Properties of the {M}\"obius Function
:: by Magdalena Jastrz\c{e}bska and Adam Grabowski
::
:: Received March 21, 2006
:: Copyright (c) 2006-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, XBOOLE_0, SUBSET_1, FUNCT_1, CARD_1, XCMPLX_0, INT_2,
XXREAL_0, ARYTM_3, FINSEQ_1, RELAT_1, ABIAN, NEWTON, NAT_3, PRE_POLY,
NAT_1, UPROOTS, CARD_3, TARSKI, INT_1, FINSET_1, ARYTM_1, PYTHTRIP,
ZFMISC_1, SQUARE_1, REAL_1, SETFAM_1, PBOOLE, VALUED_0, FUNCOP_1,
MOEBIUS1, FUNCT_7, NUMBER09;
notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, ZFMISC_1, ORDINAL1, CARD_1,
NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, NEWTON, SETFAM_1, RELAT_1, FUNCT_1,
FUNCT_2, FINSEQ_1, VALUED_0, PBOOLE, SQUARE_1, RVSUM_1, FUNCOP_1,
XXREAL_2, NAT_3, DOMAIN_1, ABIAN, UPROOTS, PYTHTRIP, RECDEF_1, PRE_POLY,
REAL_1, NAT_1, NAT_D, INT_2;
constructors NAT_D, FINSOP_1, WSIERP_1, ABIAN, PEPIN, PYTHTRIP, UPROOTS,
NAT_3, RECDEF_1, BINOP_2, XXREAL_2, REAL_1, DOMAIN_1, RELSET_1;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, FINSET_1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, NEWTON, NAT_3,
VALUED_0, XXREAL_2, CARD_1, RELSET_1, PRE_POLY, NAT_2;
requirements NUMERALS, SUBSET, ARITHM, REAL, BOOLE;
definitions TARSKI, XBOOLE_0;
equalities RVSUM_1, SQUARE_1;
expansions TARSKI, XBOOLE_0;
theorems XBOOLE_0, NAT_3, NEWTON, INT_2, NAT_2, WSIERP_1, CARD_1, PEPIN,
NAT_1, XCMPLX_1, XREAL_1, PYTHTRIP, ABIAN, ORDINAL1, EULER_1, XREAL_0,
FINSEQ_1, XBOOLE_1, TARSKI, ZFMISC_1, RVSUM_1, FINSEQ_2, NUMBERS, INT_1,
FUNCT_1, PBOOLE, UPROOTS, CARD_4, FUNCOP_1, RELAT_1, FINSOP_1, XXREAL_0,
NAT_D, VALUED_0, XXREAL_2, FUNCT_2, PARTFUN1, PRE_POLY, MEASURE6;
schemes FUNCT_2, CLASSES1, PRE_CIRC, SUBSET_1, NAT_1;
begin :: Preliminaries
Lm1: for X, Y, Z, x being set st X misses Y holds x in X /\ Z implies
not x in Y /\ Z by XBOOLE_1:76,XBOOLE_0:3;
scheme
LambdaNATC{A() -> Nat, B() -> set, F(object)->set}:
ex f being sequence of B() st f.0 = A() &
for x being non zero Element of NAT holds f.x = F(x)
provided
A1: A() in B() and
A2: for x being non zero Element of NAT holds F(x) in B()
proof
deffunc G(object) = A();
defpred C[object] means $1 = 0;
A3: for x being object st x in NAT
holds (C[x] implies G(x) in B()) & (not C[x]
implies F(x) in B()) by A1,A2;
ex f being sequence of B() st for x being object st x in NAT holds (C[x
] implies f.x = G(x)) & (not C[x] implies f.x = F(x)) from FUNCT_2:sch 5(A3);
then consider f being sequence of B() such that
A4: for x being object st x in NAT holds (C[x] implies f.x = G(x)) & (not C
[x] implies f.x = F(x));
take f;
thus thesis by A4;
end;
registration
cluster non prime non zero for Element of NAT;
existence by INT_2:29;
cluster non prime non zero for Nat;
existence by INT_2:29;
end;
theorem Th1:
for n being non zero Nat holds n <> 1 implies n >= 2
proof
let n be non zero Nat;
assume
A1: n <> 1;
assume n < 2;
then n < 1 + 1;
then n <= 0 + 1 by NAT_1:13;
hence contradiction by A1,NAT_1:8;
end;
theorem
for k, n, i being Nat st 1 <= k holds i in Seg n iff k * i in Seg (k * n)
proof
let k, n, i be Nat;
assume
A1: 1 <= k;
hereby
assume
A2: i in Seg n;
then i <= n by FINSEQ_1:1;
then
A3: k * i <= k * n by NAT_1:4;
1 <= i by A2,FINSEQ_1:1;
then 1 * 1 <= k * i by A1,XREAL_1:66;
hence k * i in Seg (k * n) by A3,FINSEQ_1:1;
end;
assume
A4: k * i in Seg (k * n);
then 0 < i by FINSEQ_1:1;
then
A5: 0 + 1 <= i by NAT_1:13;
k * i <= k * n by A4,FINSEQ_1:1;
then i <= n by A1,XREAL_1:68;
hence thesis by A5,FINSEQ_1:1;
end;
theorem
for m, n being Nat st m, n are_coprime holds m > 0 or n > 0
proof
let a, b be Nat;
assume a,b are_coprime;
then a is odd or b is odd by PYTHTRIP:10;
hence thesis by ABIAN:12;
end;
Lm2: for n being Nat st n <> 1 ex p being Prime st p divides n
proof
let n be Nat;
assume
A1: n <> 1;
per cases;
suppose
n is zero;
hence thesis by INT_2:28,NAT_D:6;
end;
suppose
n is non zero;
then ex p being Element of NAT st p is prime & p divides n
by A1,Th1,INT_2:31;
hence thesis;
end;
end;
theorem Th4:
for n being non prime Nat st n <> 1 ex p being Prime st p divides n & p <> n
proof
let n be non prime Nat;
assume n <> 1;
then ex p being Prime st p divides n by Lm2;
hence thesis;
end;
theorem Th5:
for n being Nat st n <> 1 ex p being Prime st p divides n
proof
let n be Nat;
assume
A2: n <> 1;
per cases;
suppose
n is Prime;
hence thesis;
end;
suppose
not n is Prime;
then ex p being Prime st p divides n & p <> n by A2,Th4;
hence thesis;
end;
end;
theorem Th6:
for p being Prime, n being non zero Nat holds p
divides n iff p |-count n > 0
proof
let p be Prime, n be non zero Nat;
A1: p <> 1 by INT_2:def 4;
thus p divides n implies p |-count n > 0
proof
assume
A2: p divides n;
p |-count n >= 1
proof
assume p |-count n < 1;
then p |-count n = 0 by NAT_1:25;
then not p |^(0+1) divides n by A1,NAT_3:def 7;
hence contradiction by A2;
end;
hence thesis;
end;
assume p |-count n > 0;
then reconsider d = p |-count n as non zero Nat;
p <> 1 by INT_2:def 4;
then p |^ d divides n by NAT_3:def 7;
then p |^ (0+1) divides n by NAT_3:4;
hence thesis;
end;
theorem Th7:
support ppf 1 = {}
proof
support pfexp 1 = {};
hence thesis by NAT_3:def 9;
end;
theorem Th8:
for p being Prime holds support ppf p = {p}
proof
let p be Prime;
support pfexp p = {p} by NAT_3:43;
hence thesis by NAT_3:def 9;
end;
reserve m, n for Nat;
theorem Th9:
for p being Prime st n <> 0 & m <= p |-count n holds p |^ m divides n
proof
let p be Prime;
assume that
A1: n <> 0 and
A2: m <= p |-count n;
A3: p |^ m divides p |^ (p |-count n) by A2,NEWTON:89;
p > 1 by INT_2:def 4;
then p |^ (p |-count n) divides n by A1,NAT_3:def 7;
hence thesis by A3,NAT_D:4;
end;
theorem Th10:
for a being Nat, p being Prime holds p |^ 2 divides a implies p divides a
proof
let a be Nat;
let p be Prime;
assume p |^ 2 divides a;
then consider t being Nat such that
A1: a = (p |^ 2) * t by NAT_D:def 3;
a = (p * p) * t by A1,WSIERP_1:1
.= p * (p * t);
hence thesis by NAT_D:def 3;
end;
theorem Th11:
for p being Prime, m, n being non zero Nat st
m, n are_coprime & p |^ 2 divides (m * n)
holds p |^ 2 divides m or p |^ 2 divides n
proof
let p be Prime, a, b be non zero Nat;
assume that
A1: a, b are_coprime and
A2: p |^ 2 divides (a * b);
p divides p |^ 2 by NAT_3:3;
then
A3: p divides a * b by A2,NAT_D:4;
per cases by A3,NEWTON:80;
suppose
p divides a;
then
A4: not p divides b by A1,PYTHTRIP:def 2;
p,b are_coprime
proof
reconsider k = p gcd b as Element of NAT by ORDINAL1:def 12;
assume not p, b are_coprime;
then
A5: k <> 1 by INT_2:def 3;
k divides p & k divides b by NAT_D:def 5;
hence contradiction by A4,A5,INT_2:def 4;
end;
then p * p,b are_coprime by EULER_1:14;
then p |^ 2,b are_coprime by WSIERP_1:1;
hence thesis by A2,EULER_1:13;
end;
suppose
p divides b;
then
A6: not p divides a by A1,PYTHTRIP:def 2;
p, a are_coprime
proof
reconsider k = p gcd a as Element of NAT by ORDINAL1:def 12;
assume not p, a are_coprime;
then
A7: k <> 1 by INT_2:def 3;
k divides p & k divides a by NAT_D:def 5;
hence contradiction by A6,A7,INT_2:def 4;
end;
then p * p, a are_coprime by EULER_1:14;
then p |^2, a are_coprime by WSIERP_1:1;
hence thesis by A2,EULER_1:13;
end;
end;
theorem Th12:
for N being Rbag of NAT st support N = {n} holds Sum N = N.n
proof
let N be Rbag of NAT;
reconsider Nn = N.n as Element of REAL by XREAL_0:def 1;
reconsider F = <*Nn*> as FinSequence of REAL;
assume
A1: support N = {n};
{n} c= dom N by PRE_POLY:37,A1;
then n in dom N by ZFMISC_1:31;
then
A2: F = N * <*n*> by FINSEQ_2:34
.= N * canFS(support N) by A1,FINSEQ_1:94;
Sum F = N.n by FINSOP_1:11;
hence thesis by A2,UPROOTS:def 3;
end;
registration
cluster canFS {} -> empty;
coherence;
end;
theorem
for p being Prime st p divides n holds
{ d where d is Element of NAT : d > 0 & d divides n & p divides d } =
{ p * d where d is Element of NAT : d > 0 & d divides (n div p) }
proof
let p be Prime;
assume
A1: p divides n;
set B = { p * d where d is Element of NAT : d > 0 & d divides (n div p) };
set A = { d where d is Element of NAT : d > 0 & d divides n & p divides d };
thus A c= B
proof
let x be object;
assume x in A;
then consider d being Element of NAT such that
A2: d = x and
A3: d > 0 and
A4: d divides n and
A5: p divides d;
consider d1 being Nat such that
A6: d = p * d1 by A5,NAT_D:def 3;
consider d2 being Nat such that
A7: n = d * d2 by A4,NAT_D:def 3;
n = p * (d1 * d2) by A6,A7;
then p divides n by NAT_D:def 3;
p * (n div p) = p * (d1 * d2) by A6,A7;
then n div p = d1 * d2 by XCMPLX_1:5;
then
A8: d1 divides n div p by NAT_D:def 3;
d1 in NAT & d1 > 0 by A3,A6,ORDINAL1:def 12;
hence thesis by A2,A6,A8;
end;
let x be object;
assume x in B;
then consider d being Element of NAT such that
A9: p * d = x and
A10: d > 0 and
A11: d divides (n div p);
reconsider d1 = x as Element of NAT by A9,ORDINAL1:def 12;
consider d2 being Nat such that
A12: n div p = d * d2 by A11,NAT_D:def 3;
(n div p) * p = d * d2 * p by A12;
then n = d2 * (d * p) by A1,NAT_D:3;
then
A13: d1 divides n by A9,NAT_D:def 3;
p divides d1 by A9,NAT_D:def 3;
hence thesis by A9,A10,A13;
end;
theorem Th14:
for n being non zero Nat holds ex k being Element of
NAT st support ppf n c= Seg k
proof
let n be non zero Nat;
A1: support ppf n = support pfexp n by NAT_3:def 9;
per cases;
suppose
A2: support ppf n is empty;
take 0;
thus 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;
take max S;
A3: max S is Element of NAT by ORDINAL1:def 12;
support ppf n c= Seg max S
proof
let x be object;
assume
A4: x in support ppf n;
then reconsider m = x as Nat;
x is Prime by A1,A4,NAT_3:34;
then
A5: 1 <= m by INT_2:def 4;
m <= max S by A4,XXREAL_2:def 8;
hence thesis by A5,FINSEQ_1:1;
end;
hence thesis by A3;
end;
end;
theorem Th15:
for n being non zero Nat, p being Prime
st not p in support ppf n holds p |-count n = 0
proof
let n be non zero Nat, p be Prime;
assume
A1: not p in support ppf n;
assume p |-count n <> 0;
then (ppf n).p = p |^ (p |-count n) by NAT_3:56;
hence thesis by A1,PRE_POLY:def 7;
end;
theorem Th16:
for k being Nat, n being non zero Nat st
support ppf n c= Seg (k+1) & not support ppf n c= Seg k holds k+1 is Prime
proof
let k be Nat, n be non zero Nat;
assume that
A1: support ppf n c= Seg (k+1) and
A2: not support ppf n c= Seg k;
k+1 in support ppf n
proof
assume not k+1 in support ppf n;
then
A3: {k+1} misses support ppf n by ZFMISC_1:50;
support ppf n \ {k+1} c= Seg (k+1) \ {k+1} by A1,XBOOLE_1:33;
then support ppf n c= Seg (k+1) \ {k+1} by A3,XBOOLE_1:83;
hence thesis by A2,FINSEQ_1:10;
end;
then k+1 in support pfexp n by NAT_3:def 9;
hence thesis by NAT_3:34;
end;
theorem Th17:
for m, n being non zero Nat st (for p being Prime
holds p |-count m <= p |-count n) holds support ppf m c= support ppf n
proof
let m, n be non zero Nat;
assume
A1: for p being Prime holds p |-count m <= p |-count n;
let x be object;
assume
A2: x in support ppf m;
then x in support pfexp m by NAT_3:def 9;
then reconsider p = x as Prime by NAT_3:34;
(ppf m).p <> 0 by A2,PRE_POLY:def 7;
then p |-count m <> 0 by NAT_3:55;
then p |-count n > 0 by A1;
then (ppf n).p = p |^ (p |-count n) by NAT_3:56;
hence thesis by PRE_POLY:def 7;
end;
theorem Th18:
for k being Nat, n being non zero Nat st
support ppf n c= Seg (k+1) holds
ex m being non zero Element of NAT, e being Element of NAT st
support ppf m c= Seg k & n = m * ((k+1) |^ e) &
for p being Prime holds
(p in support ppf m implies p |-count m = p |-count n)
& (not p in support ppf m implies p |-count m <= p |-count n)
proof
let k be Nat, n be non zero Nat;
assume
A1: support ppf n c= Seg (k+1);
per cases;
suppose
A2: support ppf n c= Seg k;
reconsider n as non zero Element of NAT by ORDINAL1:def 12;
take n;
take e = 0;
(k+1) |^ e = 1 by NEWTON:4;
hence thesis by A2;
end;
suppose
A3: not support ppf n c= Seg k;
reconsider r = k+1 as non zero Element of NAT;
set e = r |-count n;
set s = r |^ e;
now
assume
A4: not k+1 in support ppf n;
support ppf n c= Seg k
proof
let x be object;
assume
A5: x in support ppf n;
then reconsider m = x as Nat;
x in support pfexp n by A5,NAT_3:def 9;
then x is Prime by NAT_3:34;
then
A6: 1 <= m by INT_2:def 4;
m <= k+1 by A1,A5,FINSEQ_1:1;
then m < k+1 by A4,A5,XXREAL_0:1;
then m <= k by NAT_1:13;
hence thesis by A6,FINSEQ_1:1;
end;
hence contradiction by A3;
end;
then k+1 in support pfexp n by NAT_3:def 9;
then
A7: r is Prime by NAT_3:34;
then
A8: r > 1 by INT_2:def 4;
then s divides n by NAT_3:def 7;
then consider t being Nat such that
A9: n = s * t by NAT_D:def 3;
reconsider s, t as non zero Element of NAT by A9,ORDINAL1:def 12;
A10: support ppf t = support pfexp t by NAT_3:def 9;
A11: support ppf t c= Seg k
proof
set f = r |-count t;
let x be object;
assume
A12: x in support ppf t;
then reconsider m = x as Nat;
A13: x in support pfexp t by A12,NAT_3:def 9;
A14: now
assume
A15: m = r;
(pfexp t).r = f by A7,NAT_3:def 8;
then f <> 0 by A13,A15,PRE_POLY:def 7;
then f >= 0+1 by NAT_1:13;
then consider g being Nat such that
A16: f = 1 + g by NAT_1:10;
r |^ f divides t by A8,NAT_3:def 7;
then consider u being Nat such that
A17: t = (r |^ f)*u by NAT_D:def 3;
reconsider g as Element of NAT by ORDINAL1:def 12;
n = s * (((r |^ g)*r)*u) by A9,A16,A17,NEWTON:6
.= s*r * ((r |^ g)*u)
.= (r |^ (e+1)) * ((r |^ g) * u) by NEWTON:6;
then r |^ (e+1) divides n by NAT_D:def 3;
hence contradiction by A8,NAT_3:def 7;
end;
support pfexp t c= support pfexp n by A9,NAT_3:45;
then support ppf t c= support ppf n by A10,NAT_3:def 9;
then m in support ppf n by A12;
then m <= k+1 by A1,FINSEQ_1:1;
then m < r by A14,XXREAL_0:1;
then
A18: m <= k by NAT_1:13;
x is Prime by A13,NAT_3:34;
then 1 <= m by INT_2:def 4;
hence thesis by A18,FINSEQ_1:1;
end;
A19: e <> 0
proof
assume e = 0;
then n = 1 * t by A9,NEWTON:4;
hence thesis by A3,A11;
end;
take m = t;
take e = (k + 1) |-count n;
support ppf s = support pfexp s by NAT_3:def 9;
then
A20: support ppf s = {r} by A7,A19,NAT_3:42;
A21: now
assume support ppf s meets support ppf t;
then consider x being object such that
A22: x in support ppf s and
A23: x in support ppf t by XBOOLE_0:3;
x = r by A20,A22,TARSKI:def 1;
then r <= k by A11,A23,FINSEQ_1:1;
hence contradiction by NAT_1:13;
end;
for p being Prime holds (p in support ppf m implies p |-count m = p
|-count n) & (not p in support ppf m implies p |-count m <= p |-count n)
proof
let p be Prime;
hereby
assume p in support ppf m;
then not p in support ppf s by A21,XBOOLE_0:3;
then
A24: p |-count s = 0 by Th15;
p |-count n = p |-count (r |^ e) + p |-count t by A9,NAT_3:28;
hence p |-count m = p |-count n by A24;
end;
assume not p in support ppf m;
hence thesis by Th15;
end;
hence thesis by A9,A11;
end;
end;
theorem Th19:
for m, n being non zero Nat st
(for p being Prime holds p |-count m <= p |-count n) holds m divides n
proof
defpred P[Nat] means
for k, l being non zero Element of NAT st
support ppf k c= Seg $1 & support ppf l c= Seg $1 & (for p being Prime holds p
|-count k <= p |-count l) holds k divides l;
let m, n be non zero Nat;
A1: m is Element of NAT & n is Element of NAT by ORDINAL1:def 12;
consider k being Element of NAT such that
A2: support ppf n c= Seg k by Th14;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A4: P[k];
let m, n be non zero Element of NAT;
assume that
A5: support ppf m c= Seg (k + 1) and
A6: support ppf n c= Seg (k + 1) and
A7: for p being Prime holds p |-count m <= p |-count n;
per cases;
suppose
A8: not support ppf n c= Seg k & support ppf m c= Seg k;
reconsider r = k+1 as non zero Element of NAT;
set e = r |-count n;
set s = r |^ e;
now
assume
A9: not k+1 in support ppf n;
support ppf n c= Seg k
proof
let x be object;
assume
A10: x in support ppf n;
then reconsider m = x as Nat;
x in support pfexp n by A10,NAT_3:def 9;
then x is Prime by NAT_3:34;
then
A11: 1 <= m by INT_2:def 4;
m <= k+1 by A6,A10,FINSEQ_1:1;
then m < k+1 by A9,A10,XXREAL_0:1;
then m <= k by NAT_1:13;
hence thesis by A11,FINSEQ_1:1;
end;
hence contradiction by A8;
end;
then
A12: k+1 in support pfexp n by NAT_3:def 9;
then
A13: r is Prime by NAT_3:34;
then
A14: r > 1 by INT_2:def 4;
then s divides n by NAT_3:def 7;
then consider t being Nat such that
A15: n = s * t by NAT_D:def 3;
A16: t divides n by A15,NAT_D:def 3;
reconsider s, t as non zero Element of NAT by A15,ORDINAL1:def 12;
A17: support ppf t = support pfexp t by NAT_3:def 9;
A18: support ppf t c= Seg k
proof
set f = r |-count t;
let x be object;
assume
A19: x in support ppf t;
then reconsider m = x as Nat;
A20: x in support pfexp t by A19,NAT_3:def 9;
A21: now
assume
A22: m = r;
(pfexp t).r = f by A13,NAT_3:def 8;
then f <> 0 by A20,A22,PRE_POLY:def 7;
then f >= 0+1 by NAT_1:13;
then consider g being Nat such that
A23: f = 1 + g by NAT_1:10;
r |^ f divides t by A14,NAT_3:def 7;
then consider u being Nat such that
A24: t = (r |^ f)*u by NAT_D:def 3;
reconsider g as Element of NAT by ORDINAL1:def 12;
n = s * (((r |^ g)*r)*u) by A15,A23,A24,NEWTON:6
.= s*r * ((r |^ g)*u)
.= (r |^ (e+1)) * ((r |^ g) * u) by NEWTON:6;
then r |^ (e+1) divides n by NAT_D:def 3;
hence contradiction by A14,NAT_3:def 7;
end;
support pfexp t c= support pfexp n by A15,NAT_3:45;
then support ppf t c= support ppf n by A17,NAT_3:def 9;
then m in support ppf n by A19;
then m <= k+1 by A6,FINSEQ_1:1;
then m < r by A21,XXREAL_0:1;
then
A25: m <= k by NAT_1:13;
x is Prime by A20,NAT_3:34;
then 1 <= m by INT_2:def 4;
hence thesis by A25,FINSEQ_1:1;
end;
A26: support ppf s = support pfexp s by NAT_3:def 9;
e <> 0
proof
assume e = 0;
then not r divides n by A14,NAT_3:27;
hence thesis by A12,NAT_3:36;
end;
then
A27: support ppf s = {r} by A13,A26,NAT_3:42;
A28: now
assume (support ppf s) meets (support ppf t);
then consider x being object such that
A29: x in support ppf s and
A30: x in support ppf t by XBOOLE_0:3;
x = r by A27,A29,TARSKI:def 1;
then r <= k by A18,A30,FINSEQ_1:1;
hence contradiction by NAT_1:13;
end;
A31: support ppf m c= Seg k & support ppf t c= Seg k & (for p being
Prime holds p |-count m <= p |-count t) implies m divides t by A4;
support ppf n = support pfexp n & support ppf t = support pfexp t
by NAT_3:def 9;
then
A32: support ppf n = support ppf s \/ support ppf t by A15,A26,NAT_3:46;
A33: for p being Prime holds p |-count m <= p |-count t
proof
let p be Prime;
A34: p |-count n = p |-count (r |^ e) + p |-count t by A15,NAT_3:28;
per cases;
suppose
A35: p in support ppf n;
per cases by A32,A35,XBOOLE_0:def 3;
suppose
p in support ppf s;
then
A36: p = k+1 by A27,TARSKI:def 1;
per cases;
suppose
p in support ppf m;
then p <= k by A8,FINSEQ_1:1;
hence thesis by A36,NAT_1:13;
end;
suppose
not p in support ppf m;
hence thesis by Th15;
end;
end;
suppose
p in support ppf t;
then not p in support ppf s by A28,XBOOLE_0:3;
then p |-count s = 0 by Th15;
hence thesis by A7,A34;
end;
end;
suppose
not p in support ppf n;
then p |-count n = 0 by Th15;
hence thesis by A7;
end;
end;
then support ppf m c= support ppf t by Th17;
hence thesis by A16,A18,A33,A31,NAT_D:4;
end;
suppose
A37: not support ppf n c= Seg k & not support ppf m c= Seg k;
then reconsider w = k+1 as Prime by A5,Th16;
consider m1 being non zero Element of NAT, e1 being Element of NAT such
that
A38: support ppf m1 c= Seg k and
A39: m = m1 * ((k+1) |^ e1) and
A40: for p being Prime holds (p in support ppf m1 implies p |-count
m1 = p |-count m) & (not p in support ppf m1 implies p |-count m1 <= p |-count
m) by A5,Th18;
consider m2 being non zero Element of NAT, e2 being Element of NAT such
that
A41: support ppf m2 c= Seg k and
A42: n = m2 * ((k+1) |^ e2) and
A43: for p being Prime holds (p in support ppf m2 implies p |-count
m2 = p |-count n) & (not p in support ppf m2 implies p |-count m2 <= p |-count
n) by A6,Th18;
A44: not w divides m2
proof
assume w divides m2;
then w in support pfexp m2 by NAT_3:37;
then w in support ppf m2 by NAT_3:def 9;
then w <= k by A41,FINSEQ_1:1;
hence thesis by NAT_1:13;
end;
A45: k+1 is Prime by A5,A37,Th16;
for p being Prime holds p |-count m1 <= p |-count m2
proof
let p be Prime;
per cases;
suppose
p in support ppf m1 & p in support ppf m2;
then
p |-count m1 = p |-count m & p |-count m2 = p |-count n by A40,A43;
hence thesis by A7;
end;
suppose
not p in support ppf m1 & p in support ppf m2;
hence thesis by Th15;
end;
suppose
A46: p in support ppf m1 & not p in support ppf m2;
m1 divides m by A39,NAT_D:def 3;
then
A47: p |-count m1 <= p |-count m by NAT_3:30;
A48: p > 1 by INT_2:def 4;
p in support pfexp m1 by A46,NAT_3:def 9;
then p divides m1 by NAT_3:36;
then p |-count m1 <> 0 by A48,NAT_3:27;
then p |-count m1 > 0;
then p |-count n > 0 by A7,A47;
then
A49: p divides n by A48,NAT_3:27;
p |-count m2 = 0 by A46,Th15;
then not p divides m2 by A48,NAT_3:27;
then p divides (k+1) |^ e2 by A42,A49,NEWTON:80;
then p divides (k+1) by NAT_3:5;
then
A50: p = k+1 by A45,A48,INT_2:def 4;
k < k + 1 by NAT_1:13;
hence thesis by A38,A46,A50,FINSEQ_1:1;
end;
suppose
not p in support ppf m1 & not p in support ppf m2;
hence thesis by Th15;
end;
end;
then
A51: m1 divides m2 by A4,A38,A41;
A52: not w divides m1
proof
assume w divides m1;
then w in support pfexp m1 by NAT_3:37;
then w in support ppf m1 by NAT_3:def 9;
then w <= k by A38,FINSEQ_1:1;
hence thesis by NAT_1:13;
end;
A53: w > 1 by INT_2:def 4;
then w |-count (w |^ e2) = e2 by NAT_3:25;
then
A54: w |-count n = (w |-count m2) + e2 by A42,NAT_3:28
.= 0 + e2 by A53,A44,NAT_3:27
.= e2;
w |-count (w |^ e1) = e1 by A53,NAT_3:25;
then w |-count m = (w |-count m1) + e1 by A39,NAT_3:28
.= 0 + e1 by A53,A52,NAT_3:27
.= e1;
then ((k+1) |^ e1) divides ((k+1) |^ e2) by A7,A54,NEWTON:89;
hence thesis by A39,A42,A51,NAT_3:1;
end;
suppose
A55: support ppf n c= Seg k;
support ppf m c= support ppf n by A7,Th17;
then support ppf m c= Seg k by A55;
hence thesis by A4,A7,A55;
end;
end;
A56: P[ 0 ]
proof
let k, l be non zero Element of NAT;
assume that
A57: support ppf k c= Seg 0 and
support ppf l c= Seg 0 and
for p being Prime holds p |-count k <= p |-count l;
support ppf k = {} by A57,XBOOLE_1:3;
then
A58: support pfexp k = {} by NAT_3:def 9;
per cases;
suppose
k <> 1;
then ex p being Prime st p divides k by Lm2;
hence thesis by A58,NAT_3:37;
end;
suppose
k = 1;
hence thesis by NAT_D:6;
end;
end;
A59: for k being Nat holds P[k] from NAT_1:sch 2(A56,A3);
assume
A60: for p being Prime holds p |-count m <= p |-count n;
then support ppf m c= support ppf n by Th17;
then support ppf m c= Seg k by A2;
hence thesis by A60,A59,A2,A1;
end;
begin :: Squarefree Numbers
definition
let x be Nat;
attr x is square-containing means
ex p being Prime st p |^ 2 divides x;
end;
theorem Th20:
for n being Nat st ex p being non zero Nat
st p <> 1 & p |^ 2 divides n holds n is square-containing
proof
let n be Nat;
given p being non zero Nat such that
A1: p <> 1 and
A2: p |^ 2 divides n;
consider r being Prime such that
A3: r divides p by A1,Lm2;
r |^ 2 divides p |^ 2 by A3,WSIERP_1:14;
hence thesis by A2,NAT_D:4;
end;
notation
let x be Nat;
antonym x is square-free for x is square-containing;
end;
theorem Th21:
0 is square-containing
proof
set p = the Prime;
p |^ 2 divides 0 by NAT_D:6;
hence thesis;
end;
theorem Th22:
1 is square-free
proof
assume 1 is square-containing;
then consider n being Prime such that
A1: n |^ 2 divides 1;
n * n divides 1 by A1,WSIERP_1:1;
then n = 1 or n = -1 by WSIERP_1:15,XCMPLX_1:182;
hence contradiction by INT_2:def 4;
end;
registration
cluster square-free -> non zero for Nat;
coherence by Th21;
cluster trivial square-containing -> zero for Nat;
coherence
proof
let n be Nat;
assume
A1: n is trivial square-containing; then
n = 0 or n = 1 by NAT_2:def 1;
hence thesis by A1,Th22;
end;
end;
theorem Th23:
for p being Prime holds p is square-free
proof
let p be Prime;
assume p is square-containing;
then consider n being Prime such that
A1: n |^ 2 divides p;
A2: n divides n |^ 2 by NAT_3:3;
then
A3: n divides p by A1,NAT_D:4;
per cases by A3,INT_2:def 4;
suppose
n = 1;
hence contradiction by INT_2:def 4;
end;
suppose
n = p;
then n |^ 1 = n |^ 2 by A1,A2,NAT_D:5;
then n <= 1 by PEPIN:30;
hence contradiction by INT_2:def 4;
end;
end;
registration
cluster prime -> square-free for Nat;
coherence by Th23;
end;
definition
func SCNAT -> Subset of NAT means
:Def2:
for n being Nat holds n in it iff n is square-free;
existence
proof
defpred P[Nat] means $1 is square-free;
consider X being Subset of NAT such that
A1: for n being Element of NAT holds n in X iff P[n] from SUBSET_1:sch
3;
take X;
let n be Nat;
thus n in X implies n is square-free by A1;
assume
A2: n is square-free;
n is Element of NAT by INT_1:3;
hence thesis by A1,A2;
end;
uniqueness
proof
let X1, X2 be Subset of NAT;
defpred P[Nat] means $1 is square-free;
assume that
A3: for n being Nat holds n in X1 iff n is square-free and
A4: for n being Nat holds n in X2 iff n is square-free;
A5: for y being Element of NAT holds y in X2 iff P[y] by A4;
A6: for y being Element of NAT holds y in X1 iff P[y] by A3;
thus X1 = X2 from SUBSET_1:sch 2(A6,A5);
end;
end;
registration
cluster square-free for Nat;
existence by Th22;
cluster square-containing for Nat;
existence
proof
take 4;
2 |^ 2 = 2*2 by NEWTON:81
.= 4;
hence thesis by INT_2:28;
end;
end;
registration
cluster square non trivial -> square-containing for Nat;
coherence
proof
let n be Nat;
assume
A1: n is square non trivial;
then consider m being Nat such that
A2: n = m^2 by PYTHTRIP:def 3;
A3: m |^ 2 divides n by A2,WSIERP_1:1;
m <> 1^2 & m <> 0^2 by A1,A2,NAT_2:28;
hence thesis by A3,Th20;
end;
end;
theorem Th24:
n is square-free implies for p being Prime holds p |-count n <= 1
proof
assume
A1: n is square-free;
given p being Prime such that
A2: p |-count n > 1;
p |-count n >= 1+1 by A2,NAT_1:13;
then p |^ 2 divides n by A1,Th9;
hence thesis by A1;
end;
theorem Th25:
m * n is square-free implies m is square-free by NAT_D:9;
theorem Th26:
m is square-free & n divides m implies n is square-free
proof
assume that
A1: m is square-free and
A2: n divides m;
ex x being Nat st m = n * x by A2,NAT_D:def 3;
hence thesis by A1,Th25;
end;
theorem Th27:
for p being Prime, m, d being Nat st m is square-free
& p divides m & d divides (m div p) holds d divides m & not p divides d
proof
let p be Prime, m, d be Nat;
assume that
A1: m is square-free and
A2: p divides m;
assume d divides (m div p);
then consider z being Nat such that
A3: m div p = d * z by NAT_D:def 3;
A4: (m div p) * p = d * z * p by A3;
then m = d * (z * p) by A2,NAT_D:3;
hence d divides m by NAT_D:def 3;
assume p divides d;
then consider w being Nat such that
A5: d = p * w by NAT_D:def 3;
m = w * (p * p) * z by A2,A4,A5,NAT_D:3
.= w * (p |^ 2) * z by WSIERP_1:1
.= (p |^ 2) * (w * z);
then p |^ 2 divides m by NAT_D:def 3;
hence thesis by A1;
end;
theorem Th28:
for p being Prime, m, d being Nat st p divides m & d
divides m & not p divides d holds d divides (m div p)
proof
let p be Prime, m,d be Nat;
assume that
A1: p divides m and
A2: d divides m and
A3: not p divides d;
consider z being Nat such that
A4: m = d * z by A2,NAT_D:def 3;
p divides z by A1,A3,A4,NEWTON:80;
then consider u being Nat such that
A5: z = p * u by NAT_D:def 3;
m = d * u * p by A4,A5;
then m div p = d * u;
hence thesis by NAT_D:def 3;
end;
theorem
for p being Prime, m being Nat st m is square-free & p divides m holds
{ d where d is Element of NAT : 0 < d & d divides m & not p divides d } =
{ d where d is Element of NAT : 0 < d & d divides (m div p) }
proof
let p be Prime, m be Nat;
assume that
A1: m is square-free and
A2: p divides m;
set B = { d where d is Element of NAT : 0 < d & d divides (m div p) };
set A = { d where d is Element of NAT : 0 < d & d divides m & not p divides
d };
thus A c= B
proof
let x be object;
assume x in A;
then consider d being Element of NAT such that
A3: d = x & 0 < d and
A4: d divides m & not p divides d;
d divides (m div p) by A2,A4,Th28;
hence thesis by A3;
end;
let x be object;
assume x in B;
then consider d being Element of NAT such that
A5: d = x & 0 < d and
A6: d divides (m div p);
d divides m & not p divides d by A1,A2,A6,Th27;
hence thesis by A5;
end;
begin :: Moebius Function
definition
let n be Nat;
::$N Moebius function
func Moebius n -> Real means
:Def3:
it = 0 if n is square-containing
otherwise ex n1 being non zero Nat st n1 = n & it = (-1) |^ card
support ppf n1;
consistency;
existence
proof
thus n is square-containing implies ex r being Real st r=0;
n is square-free implies ex n9 being non zero Nat st n9 = n
& ex r being Real st r = (-1) |^ card support ppf n9
proof
assume
A1: n is square-free;
n is non zero Nat
proof
set p = the Prime;
assume not n is non zero Nat;
then p|^2 divides n by NAT_D:6;
hence contradiction by A1;
end;
then reconsider n9 = n as non zero Nat;
ex r being Real st r = (-1) |^ card support ppf n9;
hence thesis;
end;
hence thesis;
end;
uniqueness;
end;
theorem Th30:
Moebius 1 = 1
proof
Moebius 1 = (-1) |^ card {} by Def3,Th7,Th22
.= 1 by NEWTON:4;
hence thesis;
end;
theorem
Moebius 2 = -1
proof
Moebius 2 = (-1) |^ card support ppf 2 by Def3,INT_2:28
.= (-1) |^ card {2} by Th8,INT_2:28
.= (-1) |^ 1 by CARD_1:30;
hence thesis;
end;
theorem
Moebius 3 = -1
proof
Moebius 3 = (-1) |^ card support ppf 3 by Def3,PEPIN:41
.= (-1) |^ card {3} by Th8,PEPIN:41
.= (-1) |^ 1 by CARD_1:30;
hence thesis;
end;
theorem Th33:
for n being Nat st n is square-free holds Moebius n <> 0
proof
let n be Nat;
assume n is square-free;
then consider n9 being non zero Nat such that
A1: n9 = n & Moebius n = (-1) |^ card support ppf n9 by Def3;
thus thesis by A1,CARD_4:3;
end;
registration
let n be square-free Nat;
cluster Moebius n -> non zero;
coherence by Th33;
end;
theorem Th34:
for p being Prime holds Moebius p = -1
proof
let p be Prime;
reconsider p1 = p as prime Element of NAT by ORDINAL1:def 12;
Moebius p = (-1) |^ card support ppf p1 by Def3
.= (-1) |^ card {p} by Th8
.= (-1) |^ 1 by CARD_1:30;
hence thesis;
end;
theorem Th35:
for m, n being non zero Nat st m, n are_coprime holds
Moebius (m * n) = Moebius m * Moebius n
proof
let a, b be non zero Nat;
assume
A1: a, b are_coprime;
per cases;
suppose
A2: a is square-free & b is square-free;
A3: a * b is square-free
proof
assume a * b is square-containing;
then consider p being Prime such that
A4: p |^ 2 divides (a * b);
p |^ 2 divides a or p |^ 2 divides b by A1,A4,Th11;
hence contradiction by A2;
end;
A5: Moebius a = (-1) |^ card support ppf a by A2,Def3;
card support pfexp (a*b) = card support pfexp a + card support pfexp b
by A1,NAT_3:47;
then card support ppf (a*b) = card support pfexp a + card support pfexp b
by NAT_3:def 9
.= card support pfexp a + card support ppf b by NAT_3:def 9
.= card support ppf a + card support ppf b by NAT_3:def 9;
then Moebius (a * b) = (-1) |^ (card support ppf a + card support ppf b)
by A3,Def3
.= ((-1) |^ card support ppf a) * ((-1) |^card support ppf b) by NEWTON:8
;
hence thesis by A2,A5,Def3;
end;
suppose
A6: a is square-free & b is square-containing;
then consider p being Prime such that
A7: p |^ 2 divides b;
A8: a * b is square-containing by A7,NAT_D:9;
Moebius b = 0 by A6,Def3;
hence thesis by A8,Def3;
end;
suppose
A9: a is square-containing & b is square-free;
then consider p being Prime such that
A10: p |^2 divides a;
A11: a * b is square-containing by A10,NAT_D:9;
Moebius a = 0 by A9,Def3;
hence thesis by A11,Def3;
end;
suppose
A12: a is square-containing & b is square-containing;
then consider p being Prime such that
A13: p |^ 2 divides a;
A14: a * b is square-containing by A13,NAT_D:9;
Moebius a = 0 by A12,Def3;
hence thesis by A14,Def3;
end;
end;
theorem
for p being Prime, n being Nat st 1 <= n & n * p is square-free
holds Moebius (n * p) = - Moebius n
proof
let p be Prime, a be Nat;
assume that
A1: 1 <= a and
A2: a * p is square-free;
a, p are_coprime
proof
assume not a, p are_coprime;
then consider q being Prime such that
A4: q divides a and
A5: q divides p by PYTHTRIP:def 2;
q = 1 or q = p by A5,INT_2:def 4;
then p * p divides a * p by A4,INT_2:def 4,PYTHTRIP:7;
then p |^ 2 divides a * p by WSIERP_1:1;
hence thesis by A2;
end;
then Moebius (a * p) = (Moebius a) * (Moebius p) by A1,Th35
.= (Moebius a) * (-1) by Th34;
hence thesis;
end;
theorem
for m, n being non zero Nat st not m, n are_coprime holds Moebius (m * n) = 0
proof
let m, n be non zero Nat;
assume not m, n are_coprime;
then consider p being Prime such that
A1: p divides m & p divides n by PYTHTRIP:def 2;
reconsider p as prime Element of NAT by ORDINAL1:def 12;
p * p divides m * n by A1,NAT_3:1;
then p |^ 2 divides m * n by WSIERP_1:1;
then m * n is square-containing;
hence thesis by Def3;
end;
theorem Th38:
for n being Nat holds n in SCNAT iff Moebius n <> 0
proof
let n be Nat;
hereby
assume n in SCNAT;
then n is square-free by Def2;
hence Moebius n <> 0;
end;
assume Moebius n <> 0;
then n is square-free by Def3;
hence thesis by Def2;
end;
begin :: Natural Divisors
definition
let n be Nat;
func NatDivisors n -> Subset of NAT equals
{ k where k is Nat : k <> 0 & k divides n };
coherence
proof
{ k where k is Nat : k <> 0 & k divides n } c= NAT
proof
let x be object;
assume x in { k where k is Nat : k <> 0 & k divides n };
then ex k being Nat st k = x & k <> 0 & k divides n;
hence thesis by ORDINAL1:def 12;
end;
hence thesis;
end;
end;
theorem
for n, k being Nat holds k in NatDivisors n iff 0 < k & k divides n
proof
let n, k be Nat;
hereby
assume k in NatDivisors n;
then ex l being Nat st l = k & l <> 0 & l divides n;
hence 0 < k & k divides n;
end;
thus thesis;
end;
theorem Th40:
for n being non zero Nat holds NatDivisors n c= Seg n
proof
let n be non zero Nat;
let x be object;
assume x in NatDivisors n;
then consider k being Nat such that
A1: x = k and
A2: k <> 0 & k divides n;
1 <= k & k <= n by A2,NAT_1:14,NAT_D:7;
hence thesis by A1,FINSEQ_1:1;
end;
registration
let n be non zero Nat;
cluster NatDivisors n -> included_in_Seg;
coherence
proof
NatDivisors n c= Seg n by Th40;
hence thesis by FINSEQ_1:def 13;
end;
end;
registration
let n be non zero Nat;
cluster NatDivisors n -> finite with_non-empty_elements;
coherence
proof
set P = NatDivisors n;
not 0 in P
proof
assume 0 in P;
then ex k being Nat st k = 0 & k <> 0 & k divides n;
hence contradiction;
end;
hence thesis by MEASURE6:def 2;
end;
end;
theorem Th41:
NatDivisors 1 = {1}
proof
thus NatDivisors 1 c= {1}
proof
let x be object;
assume x in NatDivisors 1;
then consider k being Nat such that
A1: x = k and
k <> 0 and
A2: k divides 1;
k = 1 by A2,WSIERP_1:15;
hence thesis by A1,ZFMISC_1:31;
end;
let x be object;
assume
A3: x in {1};
then reconsider m = x as Element of NAT;
m <> 0 & m divides 1 by A3,TARSKI:def 1;
hence thesis;
end;
begin :: The Sum of the Moebius Function
definition
let X be set;
func SMoebius X -> ManySortedSet of NAT means
:Def5:
support it = X /\ SCNAT
& for k being Nat st k in support it holds it.k = Moebius k;
existence
proof
defpred R[object] means $1 in X /\ SCNAT;
deffunc G(Element of NAT) = 0;
deffunc F(Element of NAT) = Moebius $1;
ex f being ManySortedSet of NAT st for i being Element of NAT st i in
NAT holds (R[i] implies f.i = F(i)) & (not R[i] implies f.i = G(i)) from
PRE_CIRC:sch 2;
then consider f being ManySortedSet of NAT such that
A1: for i being Element of NAT st i in NAT holds (R[i] implies f.i = F
(i)) & (not R[i] implies f.i = G(i));
A2: support f c= SCNAT
proof
dom f = NAT by PARTFUN1:def 2;
then
A3: support f c= NAT by PRE_POLY:37;
let x be object;
assume
A4: x in support f;
then
A5: f.x <> 0 by PRE_POLY:def 7;
per cases;
suppose
R[x];
hence thesis by XBOOLE_0:def 4;
end;
suppose
not R[x];
hence thesis by A1,A4,A5,A3;
end;
end;
A6: support f = X /\ SCNAT
proof
thus support f c= X /\ SCNAT
proof
let x be object;
assume
A7: x in support f;
then x in SCNAT by A2;
then reconsider i = x as Element of NAT;
assume not x in X /\ SCNAT;
then f.i = 0 by A1;
hence contradiction by A7,PRE_POLY:def 7;
end;
let x be object;
assume
A8: x in X /\ SCNAT;
then reconsider i = x as Element of NAT;
x in SCNAT by A8,XBOOLE_0:def 4;
then
A9: Moebius i <> 0 by Th38;
f.i = Moebius i by A1,A8;
hence thesis by A9,PRE_POLY:def 7;
end;
reconsider f as ManySortedSet of NAT;
take f;
thus thesis by A1,A6;
end;
uniqueness
proof
let f, g be ManySortedSet of NAT such that
A10: support f = X /\ SCNAT and
A11: for k being Nat st k in support f holds f.k = Moebius k and
A12: support g = X /\ SCNAT and
A13: for k being Nat st k in support g holds g.k = Moebius k;
for i being object st i in NAT holds f.i = g.i
proof
let i be object;
assume i in NAT;
then reconsider j = i as Element of NAT;
per cases;
suppose
A14: j in support f;
hence f.i = Moebius j by A11
.= g.i by A10,A12,A13,A14;
end;
suppose
A15: not j in support f;
hence f.i = 0 by PRE_POLY:def 7
.= g.i by A10,A12,A15,PRE_POLY:def 7;
end;
end;
hence thesis by PBOOLE:3;
end;
end;
registration
let X be set;
cluster SMoebius X -> real-valued;
coherence
proof
rng SMoebius X c= REAL
proof
let y be object;
assume y in rng SMoebius X;
then consider i being object such that
A1: i in dom SMoebius X and
A2: (SMoebius X).i = y by FUNCT_1:def 3;
dom SMoebius X = NAT by PARTFUN1:def 2;
then reconsider i as Nat by A1;
per cases;
suppose
i in support SMoebius X;
then y = Moebius i by A2,Def5;
hence thesis by XREAL_0:def 1;
end;
suppose
not i in support SMoebius X;
then (SMoebius X).i = In(0,REAL) by PRE_POLY:def 7;
hence thesis by A2;
end;
end;
hence thesis by VALUED_0:def 3;
end;
end;
registration
let X be finite set;
cluster SMoebius X -> finite-support;
coherence
proof
support SMoebius X = X /\ SCNAT by Def5;
hence thesis by PRE_POLY:def 8;
end;
end;
theorem
Sum SMoebius NatDivisors 1 = 1
proof
reconsider J = 1 as Element of NAT;
reconsider M = ({1},1)-bag as Rbag of NAT;
A1: 1 in {1} by TARSKI:def 1;
A2: 1 in SCNAT by Def2,Th22;
J in {1} by TARSKI:def 1;
then J in {1} /\ SCNAT by A2,XBOOLE_0:def 4;
then J in support SMoebius {1} by Def5;
then
A3: (SMoebius {1}).1 = 1 by Def5,Th30;
{1} c= SCNAT by A2,ZFMISC_1:31; then
A4: {1} /\ SCNAT = {1} by XBOOLE_1:28;
for x being object st x in NAT holds (SMoebius {1}).x = M.x
proof
let x be object;
per cases;
suppose
A5: x in {1};
then x = 1 by TARSKI:def 1;
hence thesis by A3,A5,UPROOTS:7;
end;
suppose
A6: not x in {1};
then
A7: not x in support SMoebius {1} by A4,Def5;
M.x = 0 by A6,UPROOTS:6
.= (SMoebius {1}).x by A7,PRE_POLY:def 7;
hence thesis;
end;
end;
then support M = {1} & SMoebius {1} = M by PBOOLE:3,UPROOTS:8;
then Sum SMoebius NatDivisors 1 = M.1 by Th12,Th41
.= 1 by A1,UPROOTS:7;
hence thesis;
end;
theorem
for X, Y being finite Subset of NAT st X misses Y holds support
SMoebius X \/ support SMoebius Y = support (SMoebius X + SMoebius Y)
proof
let X,Y be finite Subset of NAT;
assume
A1: X misses Y;
thus support SMoebius X \/ support SMoebius Y c= support (SMoebius X +
SMoebius Y)
proof
let x be object;
support SMoebius X = X /\ SCNAT & support SMoebius Y = Y /\ SCNAT by Def5;
then
A2: support SMoebius X misses support SMoebius Y by A1,XBOOLE_1:76;
assume
A3: x in support SMoebius X \/ support SMoebius Y;
per cases by A3,XBOOLE_0:def 3;
suppose
A4: x in support SMoebius X;
then not x in support SMoebius Y by A2,XBOOLE_0:3;
then (SMoebius Y).x = 0 by PRE_POLY:def 7;
then (SMoebius X).x + (SMoebius Y).x <> 0 by A4,PRE_POLY:def 7;
then (SMoebius X + SMoebius Y).x <> 0 by PRE_POLY:def 5;
hence thesis by PRE_POLY:def 7;
end;
suppose
A5: x in support SMoebius Y;
then not x in support SMoebius X by A2,XBOOLE_0:3;
then (SMoebius X).x = 0 by PRE_POLY:def 7;
then (SMoebius X).x + (SMoebius Y).x <> 0 by A5,PRE_POLY:def 7;
then (SMoebius X + SMoebius Y).x <> 0 by PRE_POLY:def 5;
hence thesis by PRE_POLY:def 7;
end;
end;
thus thesis by PRE_POLY:75;
end;
theorem
for X, Y being finite Subset of NAT st X misses Y holds SMoebius (X \/
Y) = SMoebius X + SMoebius Y
proof
let X,Y be finite Subset of NAT;
A1: support SMoebius (X \/ Y) = (X \/ Y) /\ SCNAT by Def5
.= (X /\ SCNAT) \/ (Y /\ SCNAT) by XBOOLE_1:23;
assume
A2: X misses Y;
for x being object st x in NAT
holds (SMoebius (X \/ Y)).x = (SMoebius X + SMoebius Y).x
proof
let x be object;
per cases;
suppose
A3: x in support SMoebius (X \/ Y);
per cases by A1,A3,XBOOLE_0:def 3;
suppose
A4: x in X /\ SCNAT;
then reconsider k = x as Element of NAT;
A5: k in support SMoebius X by A4,Def5;
not x in Y /\ SCNAT by A2,A4,Lm1;
then
A6: not k in support SMoebius Y by Def5;
(SMoebius (X \/ Y)).x = Moebius k + (0 qua Nat) by A3,Def5
.= Moebius k + SMoebius Y.k by A6,PRE_POLY:def 7
.= SMoebius X.k + SMoebius Y.k by A5,Def5
.= (SMoebius X + SMoebius Y).x by PRE_POLY:def 5;
hence thesis;
end;
suppose
A7: x in Y /\ SCNAT;
then consider k being Element of NAT such that
A8: k = x;
not x in X /\ SCNAT by A2,A7,Lm1;
then
A9: not k in support SMoebius X by A8,Def5;
A10: k in support SMoebius Y by A7,A8,Def5;
(SMoebius (X \/ Y)).x = Moebius k + (0 qua Nat) by A3,A8,Def5
.= Moebius k + SMoebius X.k by A9,PRE_POLY:def 7
.= SMoebius Y.k + SMoebius X.k by A10,Def5
.= (SMoebius X + SMoebius Y).x by A8,PRE_POLY:def 5;
hence thesis;
end;
end;
suppose
A11: not x in support SMoebius (X \/ Y);
then not x in Y /\ SCNAT by A1,XBOOLE_0:def 3;
then
A12: not x in support SMoebius Y by Def5;
not x in X /\ SCNAT by A1,A11,XBOOLE_0:def 3;
then
A13: not x in support SMoebius X by Def5;
(SMoebius (X \/ Y)).x = 0 by A11,PRE_POLY:def 7
.= SMoebius Y.x + 0 by A12,PRE_POLY:def 7
.= SMoebius Y.x + SMoebius X.x by A13,PRE_POLY:def 7
.= (SMoebius X + SMoebius Y).x by PRE_POLY:def 5;
hence thesis;
end;
end;
hence thesis by PBOOLE:3;
end;
begin :: Prime Factors of a Number
definition
let n be non zero Nat;
func PFactors n -> ManySortedSet of SetPrimes means
:Def6:
support it = support pfexp n &
for p being Nat st p in support pfexp n holds it.p = p;
existence
proof
defpred P[object,object] means
for p being Prime st $1 = p holds (p in support
pfexp n implies $2 = p) & (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;
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 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 NAT_3:34;
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 and
A13: support it2 = support pfexp n and
A14: for p being Nat st p in support pfexp n holds it2.p = p;
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 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 by PBOOLE:3;
end;
end;
registration
let n be non zero Nat;
cluster PFactors n -> finite-support natural-valued;
coherence
proof
A1: rng PFactors n c= NAT
proof
let x be object;
assume x in rng PFactors n;
then consider y being object such that
A2: y in dom PFactors n and
A3: (PFactors n).y = x by FUNCT_1:def 3;
A4: y in SetPrimes by A2,PARTFUN1:def 2;
per cases;
suppose
y in support pfexp n;
then x = y by A3,Def6;
hence thesis by A4;
end;
suppose
not y in support pfexp n;
then not y in support PFactors n by Def6;
then x = 0 by A3,PRE_POLY:def 7;
hence thesis;
end;
end;
support PFactors n = support pfexp n by Def6;
hence thesis by A1,PRE_POLY:def 8,VALUED_0:def 6;
end;
end;
theorem Th45:
PFactors 1 = EmptyBag SetPrimes
proof
set f = PFactors 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 z in SetPrimes by PARTFUN1:def 2;
then reconsider z as Element of NAT;
support pfexp 1 = {};
then not z in support f by Def6;
hence thesis by PRE_POLY:def 7;
end;
then
A1: f = (dom f) --> 0 by FUNCOP_1:11;
dom f = SetPrimes by PARTFUN1:def 2;
hence thesis by A1,PBOOLE:def 3;
end;
theorem Th46:
for p being Prime holds (PFactors p) * <*p*> = <*p*>
proof
let p be Prime;
set f = <*p*>, g = PFactors p;
A1: dom (g * f) = {1}
proof
thus dom (g * f) c= {1}
proof
let x be object;
assume x in dom (g * f);
then x in dom f by FUNCT_1:11;
hence thesis by FINSEQ_1:2,38;
end;
let x be object;
assume
A2: x in {1};
then x = 1 by TARSKI:def 1;
then f.x in SetPrimes by NEWTON:def 6;
then
A3: f.x in dom g by PARTFUN1:def 2;
x in dom f by A2,FINSEQ_1:2,38;
hence thesis by A3,FUNCT_1:11;
end;
A4: for x being object st x in dom (g * f) holds (g * f).x = f.x
proof
let x be object;
(pfexp p).p <> 0 by NAT_3:38;
then
A5: p in support pfexp p by PRE_POLY:def 7;
assume
A6: x in dom (g * f);
then
A7: x = 1 by A1,TARSKI:def 1;
then (g * f).1 = g.(f.1) by A6,FUNCT_1:12
.= g.p
.= p by A5,Def6
.= f.1;
hence thesis by A7;
end;
dom f = {1} by FINSEQ_1:2,38;
hence thesis by A1,A4,FUNCT_1:2;
end;
theorem Th47:
for p being Prime, n being non zero Nat holds (
PFactors (p|^n)) * <* p *> = <* p *>
proof
let p be Prime, n be non zero Nat;
set s = p |^ n;
set f = <*p*>, g = PFactors s;
A1: dom f = {1} by FINSEQ_1:2,38;
A2: dom (g * f) = {1}
proof
thus dom (g * f) c= {1} by A1,FUNCT_1:11;
let x be object;
assume
A3: x in {1};
then x = 1 by TARSKI:def 1;
then f.x in SetPrimes by NEWTON:def 6;
then
A4: f.x in dom g by PARTFUN1:def 2;
x in dom f by A3,FINSEQ_1:2,38;
hence thesis by A4,FUNCT_1:11;
end;
A5: for x being object st x in dom (g * f) holds (g * f).x = f.x
proof
let x be object;
(pfexp p).p <> 0 by NAT_3:38;
then p in support pfexp p by PRE_POLY:def 7;
then
A6: p in support pfexp s by NAT_3:48;
assume
A7: x in dom (g * f);
then
A8: x = 1 by A2,TARSKI:def 1;
then (g * f).1 = g.(f.1) by A7,FUNCT_1:12
.= g.p
.= p by A6,Def6
.= f.1;
hence thesis by A8;
end;
dom (g * f) = dom f by A2,FINSEQ_1:2,38;
hence thesis by A5,FUNCT_1:2;
end;
theorem Th48:
for p being Prime, n being non zero Nat holds p
|-count n = 0 implies (PFactors n).p = 0
proof
let p be Prime, n be non zero Nat;
assume p |-count n = 0;
then (pfexp n).p = 0 by NAT_3:def 8;
then not p in support pfexp n by PRE_POLY:def 7;
then not p in support PFactors n by Def6;
hence thesis by PRE_POLY:def 7;
end;
theorem Th49:
for n being non zero Nat, p being Prime st p |-count
n <> 0 holds (PFactors n).p = p
proof
let n be non zero Nat, p be Prime;
assume p |-count n <> 0;
then (pfexp n).p <> 0 by NAT_3:def 8;
then p in support pfexp n by PRE_POLY:def 7;
hence thesis by Def6;
end;
theorem Th50:
for m, n being non zero Nat st m, n are_coprime holds
PFactors (m * n) = PFactors m + PFactors n
proof
let a, b be non zero Nat;
reconsider an = a, bn = b as non zero Nat;
assume
A1: a, b are_coprime;
now
let i be object;
assume i in SetPrimes;
then reconsider p = i as prime Element of NAT by NEWTON:def 6;
A2: p |-count (an*bn) = (p |-count a) + (p |-count b) by NAT_3:28;
A3: a gcd b = 1 by A1,INT_2:def 3;
A4: p > 1 by INT_2:def 4;
per cases;
suppose
A5: p |-count (a*b) = 0;
then
A6: (p |-count b) = 0 by A2;
A7: (p |-count a) = 0 by A2,A5;
thus (PFactors (a*b)).i = 0 by A5,Th48
.= 0 + (PFactors b).i by A6,Th48
.= (PFactors a).i + (PFactors b).i by A7,Th48
.= (PFactors a + PFactors b).i by PRE_POLY:def 5;
end;
suppose
A8: p |-count (a*b) <> 0;
thus (PFactors (a*b)).i = (PFactors a + PFactors b).i
proof
per cases by A2,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;
reconsider ka as Element of NAT by ORDINAL1:def 12;
p |^ (p |-count a) divides a by A4,NAT_3:def 7;
then p*(p|^ka) divides a by A11,NEWTON:6;
then consider la being Nat such that
A12: a = p*(p|^ka)*la by NAT_D:def 3;
a = p*((p|^ka)*la) by A12;
then
A13: p divides a by NAT_D:def 3;
assume (p |-count b) <> 0;
then consider kb being Nat such that
A14: (p |-count b) = kb+1 by NAT_1:6;
reconsider kb as Element of NAT by ORDINAL1:def 12;
p |^ (p |-count b) divides b by A4,NAT_3:def 7;
then p*(p|^kb) divides b by A14,NEWTON:6;
then consider lb being Nat such that
A15: b = p*(p|^kb)*lb by NAT_D:def 3;
b = p*((p|^kb)*lb) by A15;
then p divides b by NAT_D:def 3;
then p divides 1 by A3,A13,NAT_D:def 5;
hence contradiction by A4,NAT_D:7;
end;
thus (PFactors (a*b)).i = p by A8,Th49
.= (PFactors a).p + 0 by A9,Th49
.= (PFactors a).p + (PFactors b).p by A10,Th48
.= (PFactors a + PFactors 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;
reconsider ka as Element of NAT by ORDINAL1:def 12;
p |^ (p |-count a) divides a by A4,NAT_3:def 7;
then p*(p|^ka) divides a by A18,NEWTON:6;
then consider la being Nat such that
A19: a = p*(p|^ka)*la by NAT_D:def 3;
a = p*((p|^ka)*la) by A19;
then
A20: p divides a by NAT_D:def 3;
consider kb being Nat such that
A21: (p |-count b) = kb+1 by A16,NAT_1:6;
reconsider kb as Element of NAT by ORDINAL1:def 12;
p |^ (p |-count b) divides b by A4,NAT_3:def 7;
then p*(p|^kb) divides b by A21,NEWTON:6;
then consider lb being Nat such that
A22: b = p*(p|^kb)*lb by NAT_D:def 3;
b = p*((p|^kb)*lb) by A22;
then p divides b by NAT_D:def 3;
then p divides 1 by A3,A20,NAT_D:def 5;
hence contradiction by A4,NAT_D:7;
end;
thus (PFactors (a*b)).i = p by A8,Th49
.= 0+(PFactors b).p by A16,Th49
.= (PFactors a).p + (PFactors b).p by A17,Th48
.= (PFactors a + PFactors b).i by PRE_POLY:def 5;
end;
end;
end;
end;
hence thesis by PBOOLE:3;
end;
theorem
for n being non zero Nat, A being finite Subset of NAT st
A =
{k where k is Element of NAT: 0 < k & k divides n & k is square-containing}
holds SMoebius A = EmptyBag NAT
proof
let n be non zero Nat, A be finite Subset of NAT;
assume
A1: A = { k where k is Element of NAT : 0 < k & k divides n & k is
square-containing };
A2: A misses SCNAT
proof
assume A meets SCNAT;
then consider x being object such that
A3: x in A and
A4: x in SCNAT by XBOOLE_0:3;
ex k being Element of NAT st k = x & 0 < k & k divides n & k is
square-containing by A1,A3;
hence thesis by A4,Def2;
end;
for x being object st x in NAT holds (SMoebius A).x = (EmptyBag NAT).x
proof
let x be object;
assume x in NAT;
then reconsider k = x as Element of NAT;
support SMoebius A = A /\ SCNAT by Def5
.= {} by A2;
then (SMoebius A).k = 0 by PRE_POLY:def 7;
hence thesis by PBOOLE:5;
end;
hence thesis by PBOOLE:3;
end;
begin :: The Radical of a Number
definition
let n be non zero Nat;
func Radical n -> Element of NAT equals
Product PFactors n;
coherence;
end;
theorem Th52:
for n being non zero Nat holds Radical n > 0
proof
let n be non zero Nat;
assume Radical n <= 0;
then Product PFactors n = 0;
then consider f being FinSequence of COMPLEX such that
A1: Product f = 0 and
A2: f = (PFactors n) * canFS(support PFactors n) by NAT_3:def 5;
not ex k being Nat st k in dom f & f.k = 0
proof
given k being Nat such that
A3: k in dom f and
A4: f.k = 0;
k in dom canFS support PFactors n by A2,A3,FUNCT_1:11;
then
A5: rng canFS support PFactors n c= support PFactors n & (canFS support
PFactors n).k in rng canFS support PFactors n by FINSEQ_1:def 4,FUNCT_1:3;
then (canFS support PFactors n).k in support PFactors n;
then reconsider
p = (canFS support PFactors n).k as prime Element of NAT by NEWTON:def 6;
p in support PFactors n by A5;
then
A6: p in support pfexp n by Def6;
f.k = (PFactors n).p by A2,A3,FUNCT_1:12
.= p by A6,Def6;
hence thesis by A4;
end;
hence contradiction by A1,RVSUM_1:103;
end;
registration
let n be non zero Nat;
cluster Radical n -> non zero;
coherence by Th52;
end;
theorem
for p being Prime holds p = Radical p
proof
let p be Prime;
A1: support PFactors p = support pfexp p by Def6
.= {p} by NAT_3:43;
reconsider p as prime Element of NAT by ORDINAL1:def 12;
reconsider f = <*p*> as FinSequence of NAT;
rng f c= NAT by FINSEQ_1:def 4;
then rng f c= COMPLEX by NUMBERS:20;
then
A2: Product f = p & f is FinSequence of COMPLEX by FINSEQ_1:def 4,RVSUM_1:95;
f = (PFactors p) * <*p*> by Th46
.= (PFactors p) * canFS({p}) by FINSEQ_1:94;
hence thesis by A1,A2,NAT_3:def 5;
end;
theorem Th54:
for p being Prime, n being non zero Nat holds Radical (p |^ n) = p
proof
let p be Prime, n be non zero Nat;
reconsider p as prime Element of NAT by ORDINAL1:def 12;
reconsider f = <*p*> as FinSequence of NAT;
set s = p |^ n;
A1: f = (PFactors s) * <*p*> by Th47
.= (PFactors s) * canFS({p}) by FINSEQ_1:94;
rng f c= NAT by FINSEQ_1:def 4;
then rng f c= COMPLEX by NUMBERS:20;
then
A2: Product f = p & f is FinSequence of COMPLEX by FINSEQ_1:def 4,RVSUM_1:95;
support PFactors s = support pfexp s by Def6
.= support pfexp p by NAT_3:48
.= {p} by NAT_3:43;
hence thesis by A1,A2,NAT_3:def 5;
end;
theorem Th55:
for n being non zero Nat holds Radical n divides n
proof
defpred P[Nat] means for n being non zero Nat st
support PFactors n c= Seg $1 holds Radical n divides n;
let n be non zero Nat;
A1: ex mS being Element of NAT st support ppf n c= Seg mS by Th14;
A2: support ppf n = support pfexp n by NAT_3:def 9
.= support PFactors n by Def6;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A4: P[k];
let n be non zero Nat such that
A5: support PFactors n c= Seg (k+1);
A6: support pfexp n = support PFactors n by Def6;
per cases;
suppose
A7: not support PFactors n c= Seg k;
set p = k+1;
set e = p |-count n;
set s = p |^ e;
A8: now
assume
A9: not k+1 in support PFactors n;
support PFactors n c= Seg k
proof
let x be object;
assume
A10: x in support PFactors n;
then reconsider m = x as Nat;
m <= k+1 by A5,A10,FINSEQ_1:1;
then m < k+1 by A9,A10,XXREAL_0:1;
then
A11: m <= k by NAT_1:13;
x is Prime by A6,A10,NAT_3:34;
then 1 <= m by INT_2:def 4;
hence thesis by A11,FINSEQ_1:1;
end;
hence contradiction by A7;
end;
then
A12: p is Prime by A6,NAT_3:34;
then
A13: p > 1 by INT_2:def 4;
then s divides n by NAT_3:def 7;
then consider t being Nat such that
A14: n = s * t by NAT_D:def 3;
reconsider s, t as non zero Nat by A14;
consider f being FinSequence of COMPLEX such that
A15: Product PFactors s = Product f and
A16: f = (PFactors s)*canFS(support PFactors s) by NAT_3:def 5;
A17: dom PFactors s = SetPrimes by PARTFUN1:def 2;
A18: support ppf s = support pfexp s by NAT_3:def 9;
then
A19: support ppf s = support PFactors s by Def6;
(pfexp n).p = e by A12,NAT_3:def 8;
then
A20: e <> 0 by A6,A8,PRE_POLY:def 7;
then
A21: support ppf s = {p} by A12,A18,NAT_3:42;
then
A22: p in support pfexp s by A18,TARSKI:def 1;
A23: support PFactors t c= Seg k
proof
set f = p |-count t;
let x be object;
assume
A24: x in support PFactors t;
then reconsider m = x as Nat;
A25: x in support pfexp t by A24,Def6;
A26: now
assume
A27: m = p;
(pfexp t).p = f by A12,NAT_3:def 8;
then f <> 0 by A25,A27,PRE_POLY:def 7;
then f >= 0+1 by NAT_1:13;
then consider g being Nat such that
A28: f = 1 + g by NAT_1:10;
p |^ f divides t by A13,NAT_3:def 7;
then consider u being Nat such that
A29: t = (p |^ f)*u by NAT_D:def 3;
reconsider g as Element of NAT by ORDINAL1:def 12;
n = s * (((p |^ g)*p)*u) by A14,A28,A29,NEWTON:6
.= s*p * ((p |^ g)*u)
.= (p |^ (e+1))*((p |^ g)*u) by NEWTON:6;
then p |^ (e+1) divides n by NAT_D:def 3;
hence contradiction by A13,NAT_3:def 7;
end;
support pfexp t c= support pfexp n by A14,NAT_3:45;
then support PFactors t c= support PFactors n by A6,Def6;
then m in support PFactors n by A24;
then m <= k+1 by A5,FINSEQ_1:1;
then m < p by A26,XXREAL_0:1;
then
A30: m <= k by NAT_1:13;
x is Prime by A25,NAT_3:34;
then 1 <= m by INT_2:def 4;
hence thesis by A30,FINSEQ_1:1;
end;
then
A31: Radical t divides t by A4;
support PFactors s = {p} by A18,A21,Def6;
then f = (PFactors s)*<*p*> by A16,FINSEQ_1:94
.= <* (PFactors s).p *> by A8,A17,FINSEQ_2:34;
then Product PFactors s = (PFactors s).p by A15,RVSUM_1:95
.= p by A22,Def6;
then
A32: Radical s divides s by A20,NAT_3:3;
reconsider s1 = s, t1 = t as non zero Element of NAT by ORDINAL1:def 12;
support ppf t = support pfexp t by NAT_3:def 9;
then
A33: support ppf t = support PFactors t by Def6;
A34: now
assume (support ppf s) meets (support ppf t);
then consider x being object such that
A35: x in support ppf s and
A36: x in support ppf t by XBOOLE_0:3;
x in support pfexp t by A36,NAT_3:def 9;
then
A37: x in support PFactors t by Def6;
x = p by A21,A35,TARSKI:def 1;
then p <= k by A23,A37,FINSEQ_1:1;
hence contradiction by NAT_1:13;
end;
s1,t1 are_coprime
proof
set u = s1 gcd t1;
A38: u divides t1 by NAT_D:def 5;
u <> 0 by INT_2:5;
then
A39: 0+1 <= u by NAT_1:13;
assume not s1,t1 are_coprime;
then s1 gcd t1 <> 1 by INT_2:def 3;
then u > 1 by A39,XXREAL_0:1;
then u >= 1+1 by NAT_1:13;
then consider r being Element of NAT such that
A40: r is prime and
A41: r divides u by INT_2:31;
u divides s1 by NAT_D:def 5;
then r divides s1 by A41,NAT_D:4;
then r divides p by A40,NAT_3:5;
then r = 1 or r = p by A12,INT_2:def 4;
then p divides t1 by A40,A41,A38,INT_2:def 4,NAT_D:4;
then p in support pfexp t by A12,NAT_3:37;
then p in support PFactors t by Def6;
then k+1 <= k by A23,FINSEQ_1:1;
hence contradiction by NAT_1:13;
end;
then Radical n = Product (PFactors s+PFactors t) by A14,Th50
.= Radical s * Radical t by A34,A19,A33,NAT_3:19;
hence thesis by A14,A32,A31,NAT_3:1;
end;
suppose
support PFactors n c= Seg k;
hence thesis by A4;
end;
end;
A42: P[ 0 ]
proof
let n be non zero Nat;
A43: {} c= support PFactors n;
assume support PFactors n c= Seg 0;
then support PFactors n = {} by A43;
then PFactors n = EmptyBag SetPrimes by PRE_POLY:81;
then Radical n = 1 by NAT_3:20;
hence thesis by NAT_D:6;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A42,A3);
hence thesis by A1,A2;
end;
theorem Th56:
for p being Prime, n being non zero Nat holds p
divides n iff p divides Radical n
proof
let p be Prime, n be non zero Nat;
thus p divides n implies p divides Radical n
proof
assume that
A1: p divides n and
A2: not p divides Radical n;
A3: p in support pfexp n by A1,NAT_3:37;
then
A4: p in support PFactors n by Def6;
then p in rng canFS support PFactors n by FUNCT_2:def 3;
then consider y being object such that
A5: y in dom canFS support PFactors n and
A6: p = (canFS support PFactors n).y by FUNCT_1:def 3;
consider f being FinSequence of COMPLEX such that
A7: Product PFactors n = Product f and
A8: f = (PFactors n) * canFS support PFactors n by NAT_3:def 5;
rng PFactors n c= NAT & rng f c= rng PFactors n by A8,RELAT_1:26
,VALUED_0:def 6;
then
A9: rng f c= NAT;
support PFactors n c= dom PFactors n by PRE_POLY:37;
then
A10: y in dom f by A4,A8,A5,A6,FUNCT_1:11;
reconsider f as FinSequence of NAT by A9,FINSEQ_1:def 4;
(PFactors n).p = p by A3,Def6;
then f.y = p by A8,A6,A10,FUNCT_1:12;
then p in rng f by A10,FUNCT_1:3;
hence contradiction by A2,A7,NAT_3:7;
end;
assume
A11: p divides Radical n;
Radical n divides n by Th55;
hence thesis by A11,NAT_D:4;
end;
theorem Th57:
for k being non zero Nat st k is square-free holds Radical k = k
proof
let k be non zero Nat;
assume
A1: k is square-free;
for i being object st i in SetPrimes holds (PFactors k).i = (ppf k).i
proof
let i be object;
assume i in SetPrimes;
then reconsider p = i as prime Element of NAT by NEWTON:def 6;
per cases;
suppose
A2: p in support pfexp k;
A3: p <> 1 by INT_2:def 4;
p |-count k <> 0
proof
assume p |-count k = 0;
then not p divides k by A3,NAT_3:27;
hence thesis by A2,NAT_3:36;
end;
then
A4: p |-count k >= 1 by NAT_1:14;
p |-count k <= 1 by A1,Th24;
then p |-count k = 1 by A4,XXREAL_0:1;
then (ppf k).p = p |^ 1 by A2,NAT_3:def 9
.= p;
hence thesis by A2,Def6;
end;
suppose
A5: not p in support pfexp k;
then not p in support PFactors k by Def6;
then
A6: (PFactors k).p = 0 by PRE_POLY:def 7;
not p in support ppf k by A5,NAT_3:def 9;
hence thesis by A6,PRE_POLY:def 7;
end;
end;
then PFactors k = ppf k by PBOOLE:3;
hence thesis by NAT_3:61;
end;
theorem
for n being non zero Nat holds Radical n <= n by Th55,NAT_D:7;
theorem
for p being Prime, n being non zero Nat holds
p |-count Radical n <= p |-count n by Th55,NAT_3:30;
theorem Th60:
for n being non zero Nat holds Radical n = 1 iff n = 1
proof
let n be non zero Nat;
thus Radical n = 1 implies n = 1
proof
A1: rng PFactors n c= NAT by VALUED_0:def 6;
consider f being FinSequence of COMPLEX such that
A2: Product PFactors n = Product f and
A3: f = (PFactors n) * canFS (support PFactors n) by NAT_3:def 5;
rng f c= rng PFactors n by A3,RELAT_1:26;
then rng f c= NAT by A1;
then reconsider f as FinSequence of NAT by FINSEQ_1:def 4;
assume
A4: Radical n = 1;
assume n <> 1;
then consider p being Prime such that
A5: p divides n by Th5;
A6: p in support pfexp n by A5,NAT_3:37;
then
A7: p in support PFactors n by Def6;
then p in rng canFS support PFactors n by FUNCT_2:def 3;
then consider y being object such that
A8: y in dom canFS support PFactors n & p = (canFS support PFactors n
).y by FUNCT_1:def 3;
(PFactors n).p = p by A6,Def6;
then
A9: f.y = p by A3,A8,FUNCT_1:13;
support PFactors n c= dom PFactors n by PRE_POLY:37;
then y in dom f by A3,A7,A8,FUNCT_1:11;
then 1 < p & p in rng f by A9,FUNCT_1:3,INT_2:def 4;
hence thesis by A4,A2,NAT_3:7,NAT_D:7;
end;
thus thesis by Th45,NAT_3:20;
end;
registration
reduce Radical 1 to 1;
reducibility by Th60;
end;
theorem Th61:
for p being Prime, n being non zero Nat holds p |-count Radical n <= 1
proof
defpred P[Nat] means for n being non zero Nat st
support PFactors n c= Seg $1 holds for p being Prime holds p |-count Radical n
<= 1;
let p be Prime, n be non zero Nat;
A1: ex mS being Element of NAT st support ppf n c= Seg mS by Th14;
A2: support ppf n = support pfexp n by NAT_3:def 9
.= support PFactors n by Def6;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A4: P[k];
let n be non zero Nat such that
A5: support PFactors n c= Seg (k+1);
A6: support pfexp n = support PFactors n by Def6;
per cases;
suppose
A7: not support PFactors n c= Seg k;
let p be Prime;
reconsider r = k+1 as non zero Element of NAT;
set e = r |-count n;
set s = r |^ e;
A8: now
assume
A9: not k+1 in support PFactors n;
support PFactors n c= Seg k
proof
let x be object;
assume
A10: x in support PFactors n;
then reconsider m = x as Nat;
m <= k+1 by A5,A10,FINSEQ_1:1;
then m < k+1 by A9,A10,XXREAL_0:1;
then
A11: m <= k by NAT_1:13;
x is Prime by A6,A10,NAT_3:34;
then 1 <= m by INT_2:def 4;
hence thesis by A11,FINSEQ_1:1;
end;
hence contradiction by A7;
end;
then
A12: r is Prime by A6,NAT_3:34;
then
A13: r > 1 by INT_2:def 4;
then s divides n by NAT_3:def 7;
then consider t being Nat such that
A14: n = s * t by NAT_D:def 3;
reconsider s, t as non zero Nat by A14;
reconsider s1 = s, t1 = t as non zero Element of NAT by ORDINAL1:def 12;
A15: support ppf s = support pfexp s by NAT_3:def 9;
then
A16: support ppf s = support PFactors s by Def6;
A17: support PFactors t c= Seg k
proof
set f = r |-count t;
let x be object;
assume
A18: x in support PFactors t;
then reconsider m = x as Nat;
A19: x in support pfexp t by A18,Def6;
A20: now
assume
A21: m = r;
(pfexp t).r = f by A12,NAT_3:def 8;
then f <> 0 by A19,A21,PRE_POLY:def 7;
then f >= 0+1 by NAT_1:13;
then consider g being Nat such that
A22: f = 1 + g by NAT_1:10;
r |^ f divides t by A13,NAT_3:def 7;
then consider u being Nat such that
A23: t = (r |^ f)*u by NAT_D:def 3;
reconsider g as Element of NAT by ORDINAL1:def 12;
n = s * (((r |^ g)*r)*u) by A14,A22,A23,NEWTON:6
.= s*r * ((r |^ g)*u)
.= (r |^ (e+1))*((r |^ g)*u) by NEWTON:6;
then r |^ (e+1) divides n by NAT_D:def 3;
hence contradiction by A13,NAT_3:def 7;
end;
support pfexp t c= support pfexp n by A14,NAT_3:45;
then support PFactors t c= support PFactors n by A6,Def6;
then m in support PFactors n by A18;
then m <= k+1 by A5,FINSEQ_1:1;
then m < r by A20,XXREAL_0:1;
then
A24: m <= k by NAT_1:13;
x is Prime by A19,NAT_3:34;
then 1 <= m by INT_2:def 4;
hence thesis by A24,FINSEQ_1:1;
end;
(pfexp n).r = e by A12,NAT_3:def 8;
then
A25: e <> 0 by A6,A8,PRE_POLY:def 7;
A26: p |-count Radical s <= 1
proof
per cases;
suppose
A27: p = r;
A28: p > 1 by INT_2:def 4;
Radical s = r by A25,A27,Th54;
hence thesis by A27,A28,NAT_3:22;
end;
suppose
p <> r;
then p, r are_coprime by A12,INT_2:30;
then
A29: not p divides r by PYTHTRIP:def 2;
A30: p > 1 by INT_2:def 4;
p |-count s = e * (p |-count r) by NAT_3:32
.= e * 0 by A29,A30,NAT_3:27
.= 0;
hence thesis by Th55,NAT_3:30;
end;
end;
A31: support ppf s = {r} by A12,A25,A15,NAT_3:42;
A32: now
assume (support ppf s) meets (support ppf t);
then consider x being object such that
A33: x in support ppf s and
A34: x in support ppf t by XBOOLE_0:3;
x in support pfexp t by A34,NAT_3:def 9;
then
A35: x in support PFactors t by Def6;
x = r by A31,A33,TARSKI:def 1;
then r <= k by A17,A35,FINSEQ_1:1;
hence contradiction by NAT_1:13;
end;
support ppf t = support pfexp t by NAT_3:def 9;
then
A36: support ppf t = support PFactors t by Def6;
A37: p |-count Radical s = 0 or p |-count Radical t = 0
proof
assume that
A38: p |-count Radical s <> 0 and
A39: p |-count Radical t <> 0;
p |-count t > 0 by A39,Th55,NAT_3:30;
then (PFactors t).p <> 0 by Th49;
then
A40: p in support PFactors t by PRE_POLY:def 7;
p |-count s > 0 by A38,Th55,NAT_3:30;
then (PFactors s).p <> 0 by Th49;
then p in support PFactors s by PRE_POLY:def 7;
hence thesis by A32,A16,A36,A40,XBOOLE_0:3;
end;
s1,t1 are_coprime
proof
set u = s1 gcd t1;
A41: u divides t1 by NAT_D:def 5;
u <> 0 by INT_2:5;
then
A42: 0+1 <= u by NAT_1:13;
assume not s1,t1 are_coprime;
then s1 gcd t1 <> 1 by INT_2:def 3;
then u > 1 by A42,XXREAL_0:1;
then u >= 1+1 by NAT_1:13;
then consider w being Element of NAT such that
A43: w is prime and
A44: w divides u by INT_2:31;
u divides s1 by NAT_D:def 5;
then w divides s1 by A44,NAT_D:4;
then w divides r by A43,NAT_3:5;
then w = 1 or w = r by A12,INT_2:def 4;
then r divides t1 by A43,A44,A41,INT_2:def 4,NAT_D:4;
then r in support pfexp t by A12,NAT_3:37;
then r in support PFactors t by Def6;
then k+1 <= k by A17,FINSEQ_1:1;
hence contradiction by NAT_1:13;
end;
then Radical n = Product (PFactors s+PFactors t) by A14,Th50
.= Radical s * Radical t by A32,A16,A36,NAT_3:19;
then p |-count Radical n = (p |-count Radical t) + (p |-count Radical s
) by NAT_3:28;
hence thesis by A4,A17,A37,A26;
end;
suppose
support PFactors n c= Seg k;
hence thesis by A4;
end;
end;
A45: P[ 0 ]
proof
let n be non zero Nat;
assume
A46: support PFactors n c= Seg 0;
let p be Prime;
{} c= support PFactors n;
then support PFactors n = {} by A46;
then
A47: PFactors n = EmptyBag SetPrimes by PRE_POLY:81;
not p divides Radical n
proof
assume p divides Radical n;
then
A48: p divides 1 by A47,NAT_3:20;
1 divides p by NAT_D:6;
then p = 1 by A48,NAT_D:5;
hence thesis by INT_2:def 4;
end;
hence thesis by Th6;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A45,A3);
hence thesis by A1,A2;
end;
Lm3: for n being non zero Nat, p being Prime holds not p |^2
divides Radical n
proof
let n be non zero Nat;
let p be Prime;
set PR = p |-count Radical n;
A1: p <> 1 by INT_2:def 4;
assume
A2: p|^2 divides Radical n;
A3: PR is non zero Element of NAT
proof
assume not PR is non zero Element of NAT;
then not p |^(0+1) divides Radical n by A1,NAT_3:def 7;
hence contradiction by A2,Th10;
end;
PR >= 2
proof
assume PR < 2;
then PR = 1 by A3,NAT_1:23;
then not p |^(1+1) divides Radical n by A1,NAT_3:def 7;
hence contradiction by A2;
end;
then PR > 1 by XXREAL_0:2;
hence contradiction by Th61;
end;
registration
let n be non zero Nat;
cluster Radical n -> square-free;
coherence by Lm3;
end;
theorem
for n being non zero Nat holds Radical Radical n = Radical n by Th57;
theorem
for n being non zero Nat, p being Prime holds
{ k where k is Element of NAT : 0 < k & k divides Radical n & p divides k }
c= Seg n
proof
let n be non zero Nat;
let p be Prime;
let x be object;
assume x in { k where k is Element of NAT : 0 < k & k divides Radical n & p
divides k };
then consider k being Element of NAT such that
A1: x = k and
A2: k > 0 and
A3: k divides Radical n and
p divides k;
A4: 1 <= k by A2,NAT_1:14;
A5: Radical n <= n by Th55,NAT_D:7;
k <= Radical n by A3,NAT_D:7;
then k <= n by A5,XXREAL_0:2;
hence thesis by A1,A4,FINSEQ_1:1;
end;
theorem
for n being non zero Nat, p being Prime holds { k where k
is Element of NAT : 0 < k & k divides Radical n & not p divides k } c= Seg n
proof
let n be non zero Nat;
let p be Prime;
let x be object;
assume x in { k where k is Element of NAT : 0 < k & k divides Radical n &
not p divides k };
then consider k being Element of NAT such that
A1: x = k and
A2: k > 0 and
A3: k divides Radical n and
not p divides k;
A4: 1 <= k by A2,NAT_1:14;
A5: Radical n <= n by Th55,NAT_D:7;
k <= Radical n by A3,NAT_D:7;
then k <= n by A5,XXREAL_0:2;
hence thesis by A1,A4,FINSEQ_1:1;
end;
Lm5: for m, n being non zero Nat st m divides n & m is square-free
holds m divides Radical n
proof
let m, n be non zero Nat;
assume that
A1: m divides n and
A2: m is square-free;
for p being Prime holds p |-count m <= p |-count Radical n
proof
let p be Prime;
A3: p > 1 by INT_2:def 4;
per cases;
suppose
p divides m;
then p divides n by A1,NAT_D:4;
then p divides Radical n by Th56;
then
A4: p |-count Radical n <> 0 by A3,NAT_3:27;
p |-count Radical n <= 1 by Th61;
then
A5: p |-count Radical n < 1 + 1 by NAT_1:13;
p |-count m <= 1 by A2,Th24;
hence thesis by A5,A4,NAT_1:23;
end;
suppose
not p divides m;
hence thesis by A3,NAT_3:27;
end;
end;
hence thesis by Th19;
end;
theorem Th65:
for k, n being non zero Nat holds
k divides n & k is square-free iff k divides Radical n
proof
let k, n be non zero Nat;
k divides Radical n implies k divides n & k is square-free
proof
assume
A2: k divides Radical n;
Radical n divides n by Th55;
hence thesis by A2,Th26,NAT_D:4;
end;
hence thesis by Lm5;
end;
theorem
for n being non zero Nat holds
{ k where k is Element of NAT : 0 < k & k divides n & k is square-free } =
{ k where k is Element of NAT : 0 < k & k divides Radical n }
proof
let n be non zero Nat;
thus { k where k is Element of NAT : 0 < k & k divides n & k is square-free
} c= { k where k is Element of NAT : 0 < k & k divides Radical n }
proof
let x be object;
assume x in { k where k is Element of NAT : 0 < k & k divides n & k is
square-free };
then consider k1 being Element of NAT such that
A1: k1 = x and
A2: 0 < k1 and
A3: k1 divides n & k1 is square-free;
k1 divides Radical n by A3,Th65;
hence thesis by A1,A2;
end;
let x be object;
assume x in { k where k is Element of NAT : 0 < k & k divides Radical n };
then consider k1 being Element of NAT such that
A4: x = k1 & 0 < k1 and
A5: k1 divides Radical n;
A6: k1 is square-free by A5,Th26;
Radical n divides n by Th55;
then k1 divides n by A5,NAT_D:4;
hence thesis by A4,A6;
end;
registration
let n be non trivial Nat;
cluster Radical n -> non trivial;
coherence
proof
n is non zero & n <> 1 by NAT_2:28; then
Radical n <> 1 by Th60;
hence thesis by NAT_2:28;
end;
end;
registration
let n be square-free Nat;
reduce Radical n to n;
reducibility by Th57;
end;