:: On Square-free Numbers
:: by Adam Grabowski
::
:: Received July 12, 2013
:: Copyright (c) 2013-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 ORDINAL2, FINSEQ_1, ARYTM_3, ARYTM_1, RELAT_1, FUNCT_1, FINSEQ_2,
INT_1, SQUARE_1, SEQ_1, REALSET1, SERIES_1, SEQ_2, NAT_LAT, FINSET_1,
CARD_1, MOEBIUS1, LATTICES, PRE_POLY, XXREAL_2, MSAFREE, MOEBIUS2,
NEWTON, XXREAL_0, XBOOLE_0, INT_2, TARSKI, PARTFUN3, NAT_1, BINOP_1,
EQREL_1, PBOOLE, NAT_3, CARD_3, FUNCT_2, VALUED_0, UPROOTS, QUOFIELD,
MEMBERED, INT_7, STRUCT_0, XCMPLX_0, COMPLEX1, ORDINAL1, SUBSET_1,
ZFMISC_1, NUMBERS, REAL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, CARD_1, XXREAL_0,
XCMPLX_0, MEMBERED, ENUMSET1, ZFMISC_1, FINSET_1, MCART_1, SQUARE_1,
COMPLEX1, ABSVALUE, INT_1, INT_2, NAT_1, XREAL_0, REAL_1, RELAT_1,
FUNCT_1, FUNCT_2, VALUED_0, VALUED_1, FINSEQ_1, REALSET1, FUNCOP_1,
CARD_2, PARTFUN3, PRE_POLY, PBOOLE, NAT_D, SEQ_1, SEQ_2, FINSEQ_2,
FINSEQ_4, RVSUM_1, STRUCT_0, BINOP_1, LATTICES, NAT_LAT, BINARITH,
NEWTON, SERIES_1, SEQM_3, COMSEQ_2, INT_7, WSIERP_1, NAT_3, POLYNOM1,
PEPIN, MOEBIUS1, PARTFUN1;
constructors PARTFUN1, WELLORD2, SQUARE_1, NAT_1, BINOP_2, FINSEQOP, SEQ_1,
VALUED_1, SIN_COS, POLYNOM2, UPROOTS, INT_7, SERIES_3, COMSEQ_2,
ZFMISC_1, CARD_1, CARD_2, MCART_1, MOEBIUS1, ABSVALUE, COMPLEX1,
FINSEQ_4, FINSOP_1, SETWOP_2, RVSUM_1, INT_2, NEWTON, BINARITH, BAGORDER,
ENUMSET1, LATTICES, NAT_LAT, STRUCT_0, BINOP_1, REALSET1, SERIES_1,
ORDINAL1, XXREAL_0, POWER, SEQ_2, REAL_1, PARTFUN3, PEPIN, PBOOLE, NAT_3,
POLYNOM1, POLYEQ_3, RELSET_1, WSIERP_1, RSSPACE, ASYMPT_1, FUNCOP_1,
SEQM_3, FUNCT_7, NAT_D, RECDEF_1, NUMBERS, XCMPLX_0, XREAL_0, FUNCT_2;
registrations RELSET_1, INT_1, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, FINSET_1,
RVSUM_1, XXREAL_0, FUNCT_1, REALSET1, FUNCOP_1, NEWTON, XCMPLX_0,
NUMBERS, MOEBIUS1, SQUARE_1, ORDINAL1, PARTFUN3, FRAENKEL, CARD_1,
STRUCT_0, PRE_POLY, NAT_3, LATTICES, NAT_LAT, CAYLDICK, LATTICE2,
XBOOLE_0, VALUED_0, FUNCT_2, SUBSET_1, VALUED_1, SEQ_4;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions VALUED_0, TARSKI, PARTFUN3;
equalities ORDINAL1, FINSEQ_2, SERIES_1, SQUARE_1, BINOP_1, LATTICES,
REALSET1;
expansions TARSKI, INT_2, LATTICES, NAT_D, SEQ_2;
theorems FINSEQ_2, RVSUM_1, XCMPLX_1, ORDINAL1, SQUARE_1, NAT_1, NEWTON,
XREAL_1, FINSEQ_1, RELAT_1, XREAL_0, SEQ_2, SERIES_1, FUNCT_2, SEQ_4,
FUNCOP_1, SEQM_3, XXREAL_0, CARD_1, CARD_2, INT_2, PEPIN, FUNCT_1,
ABSVALUE, RINFSUP1, PBOOLE, TARSKI, NAT_3, MOEBIUS1, NAT_D, INT_1,
XBOOLE_1, XBOOLE_0, PARTFUN1, PARTFUN3, WSIERP_1, ENUMSET1, LATTICES,
NAT_2, INT_6, INT_4, NAT_LAT, BINOP_1, VALUED_0, ZFMISC_1, PRE_POLY,
INT_7, NAT_4, SUBSET_1, CARD_FIN, PREPOWER;
schemes NAT_1, SEQ_1, FUNCT_2, FUNCT_1, SUBSET_1, NUMPOLY1;
begin :: Preliminaries
registration let a, b be non zero Nat;
cluster a gcd b -> non zero;
coherence by INT_2:5;
cluster a lcm b -> non zero;
coherence by INT_2:4;
end;
registration
let n be Nat;
reduce 0 -' n to 0;
reducibility
proof
per cases;
suppose 0 - n >= 0; then
0 - n = 0;
hence thesis by XREAL_1:233;
end;
suppose 0 - n < 0;
hence thesis by XREAL_0:def 2;
end;
end;
end;
theorem
for n, i being Nat st n >= 2 |^ (2 * i + 2) holds
n / 2 >= (2 |^ i) * sqrt n
proof
let n, i be Nat;
assume
A1: n >= 2 |^ (2 * i + 2);
assume n / 2 < (2 |^ i) * sqrt n; then
n / 2 * 2 < (2 |^ i) * sqrt n * 2 by XREAL_1:68; then
n < 2 * (2 |^ i) * sqrt n; then
n < (2 |^ (i + 1)) * sqrt n by NEWTON:6; then
n ^2 < ((2 |^ (i + 1)) * sqrt n) ^2 by SQUARE_1:16; then
n ^2 < (2 |^ (i + 1)) ^2 * (sqrt n) ^2; then
n ^2 < (2 |^ (i + 1)) ^2 * n by SQUARE_1:def 2; then
n ^2 < (2 |^ (i + 1)) |^2 * n by NEWTON:81; then
n ^2 < (2 |^ (2 * (i + 1))) * n by NEWTON:9; then
(n ^2) / n < (2 |^ (2 * i + 2)) * n / n by A1,XREAL_1:74; then
n < (2 |^ (2 * i + 2)) * n / n by A1,XCMPLX_1:89;
hence thesis by A1,XCMPLX_1:89;
end;
theorem
for n being Nat holds support pfexp n c= SetPrimes
proof
let n be Nat;
let x be object;
assume x in support pfexp n; then
x is Prime by NAT_3:34;
hence thesis by NEWTON:def 6;
end;
theorem FOT1:
for n being non zero Nat holds
n - (n div 2) * 2 <= 1
proof
let n be non zero Nat;
A2: n = 2 * (n div 2) + (n mod 2) by NAT_D:2;
per cases by NAT_1:23,NAT_D:1;
suppose n mod 2 = 0;
hence thesis by A2;
end;
suppose n mod 2 = 1;
hence thesis by A2;
end;
end;
theorem FOTN:
for a,n being non zero Nat holds
(n div a) * a <= n
proof
let a,n be non zero Nat;
n = a * (n div a) + (n mod a) by NAT_D:2;
hence thesis by NAT_1:11;
end;
theorem RelPrimeEx:
for a, b being non zero Nat st
not a, b are_coprime holds
ex k being non zero Nat st k <> 1 & k divides a & k divides b
proof
let a, b be non zero Nat;
assume
Z1: not a, b are_coprime;
set k = a gcd b;
k divides a & k divides b by NAT_D:def 5;
hence thesis by Z1;
end;
theorem DivNonZero:
for n,a being non zero Nat st a divides n holds
n div a <> 0
proof
let n,a be non zero Nat;
assume
A0: a divides n;
assume n div a = 0; then
n < a by NAT_2:12;
hence thesis by NAT_D:7,A0;
end;
theorem INT615:
for i,j being Nat st i,j are_coprime holds i lcm j = i * j
proof
let i, j be Nat;
reconsider ii = i, jj = j as Integer;
|.ii * jj.| = ii * jj by ABSVALUE:def 1;
hence thesis by INT_6:15;
end;
registration let f be natural-valued FinSequence;
cluster Product f -> natural;
coherence
proof
rng f c= NAT by VALUED_0:def 6; then
reconsider g = f as FinSequence of NAT by FINSEQ_1:def 4;
Product g is Element of NAT;
hence thesis;
end;
end;
begin :: Prime Numbers
theorem
primenumber 0 = 2
proof
0 = card SetPrimenumber 2;
hence thesis by INT_2:28,NEWTON:def 8;
end;
theorem LS2:
SetPrimenumber 3 = {2}
proof
A1: {2} is Subset of NAT by ZFMISC_1:31;
for q being Nat holds q in {2} iff q < 3 & q is prime
proof
let q be Nat;
hereby assume q in {2}; then
q = 2 by TARSKI:def 1;
hence q < 3 & q is prime by INT_2:28;
end;
assume
Z: q < 3 & q is prime; then
q < 2 + 1; then
q <= 2 by NAT_1:13; then
q = 0 or ... or q = 2;
hence thesis by TARSKI:def 1,Z;
end;
hence thesis by A1,NEWTON:def 7;
end;
theorem
primenumber 1 = 3
proof
1 = card SetPrimenumber 3 by LS2,CARD_2:42;
hence thesis by PEPIN:41,NEWTON:def 8;
end;
theorem LS3:
SetPrimenumber 5 = {2, 3}
proof
A1: {2, 3} is Subset of NAT by ZFMISC_1:32;
for q being Nat holds q in {2,3} iff q < 5 & q is prime
proof
let q be Nat;
hereby assume q in {2,3}; then
q = 2 or q = 3 by TARSKI:def 2;
hence q < 5 & q is prime by INT_2:28,PEPIN:41;
end;
assume
Z: q < 5 & q is prime; then
q < 4 + 1; then
q <= 4 by NAT_1:13; then
q = 0 or ... or q = 4;
hence thesis by TARSKI:def 2,Z,INT_2:29;
end;
hence thesis by A1,NEWTON:def 7;
end;
theorem
primenumber 2 = 5
proof
2 = card SetPrimenumber 5 by LS3,CARD_2:57;
hence thesis by PEPIN:59,NEWTON:def 8;
end;
lem6: 2 divides 2*3;
lem8: 2 divides 2*4;
lem9: 3 divides 3*3;
lem10: 2 divides 2*5;
lem12: 2 divides 2*6;
theorem
SetPrimenumber 6 = {2, 3, 5}
proof
A1: {2, 3, 5} c= NAT
proof
let x be object;
assume x in {2,3,5}; then
x = 2 or x = 3 or x = 5 by ENUMSET1:def 1;
hence thesis;
end;
for q being Nat holds q in {2,3,5} iff q < 6 & q is prime
proof
let q be Nat;
hereby assume q in {2,3,5}; then
q = 2 or q = 3 or q = 5 by ENUMSET1:def 1;
hence q < 6 & q is prime by INT_2:28,PEPIN:41,59;
end;
assume
Z: q < 6 & q is prime; then
q = 0 or ... or q = 6;
hence thesis by ENUMSET1:def 1,Z,INT_2:29;
end;
hence thesis by A1,NEWTON:def 7;
end;
theorem LS4:
SetPrimenumber 7 = {2, 3, 5}
proof
A1: {2, 3, 5} c= NAT
proof
let x be object;
assume x in {2,3,5}; then
x = 2 or x = 3 or x = 5 by ENUMSET1:def 1;
hence thesis;
end;
for q being Nat holds q in {2,3,5} iff q < 7 & q is prime
proof
let q be Nat;
hereby assume q in {2,3,5}; then
q = 2 or q = 3 or q = 5 by ENUMSET1:def 1;
hence q < 7 & q is prime by INT_2:28,PEPIN:41,59;
end;
assume
Z: q < 7 & q is prime; then
q < 6 + 1; then
q <= 6 by NAT_1:13; then
q = 0 or ... or q = 6;
hence thesis by ENUMSET1:def 1,Z,INT_2:29,lem6;
end;
hence thesis by A1,NEWTON:def 7;
end;
theorem
primenumber 3 = 7
proof
3 = card SetPrimenumber 7 by LS4,CARD_2:58;
hence thesis by NAT_4:26,NEWTON:def 8;
end;
theorem LS11:
SetPrimenumber 11 = {2, 3, 5, 7}
proof
A1: {2, 3, 5, 7} c= NAT
proof
let x be object;
assume x in {2,3,5,7}; then
x = 2 or x = 3 or x = 5 or x = 7 by ENUMSET1:def 2;
hence thesis;
end;
for q being Nat holds q in {2,3,5,7} iff q < 11 & q is prime
proof
let q be Nat;
hereby assume q in {2,3,5,7}; then
q = 2 or q = 3 or q = 5 or q = 7 by ENUMSET1:def 2;
hence q < 11 & q is prime by INT_2:28,PEPIN:41,59,NAT_4:26;
end;
assume
Z: q < 11 & q is prime; then
q < 10 + 1; then
q <= 10 by NAT_1:13; then
q = 0 or ... or q = 10;
hence thesis by ENUMSET1:def 2,Z,INT_2:29,lem6,lem8,lem9,lem10;
end;
hence thesis by A1,NEWTON:def 7;
end;
theorem
primenumber 4 = 11
proof
4 = card SetPrimenumber 11 by CARD_2:59,LS11;
hence thesis by NAT_4:27,NEWTON:def 8;
end;
theorem LS13:
SetPrimenumber 13 = {2, 3, 5, 7, 11}
proof
A1: {2, 3, 5, 7, 11} c= NAT
proof
let x be object;
assume x in {2,3,5,7,11}; then
x = 2 or x = 3 or x = 5 or x = 7 or x = 11 by ENUMSET1:def 3;
hence thesis;
end;
for q being Nat holds q in {2,3,5,7,11} iff q < 13 & q is prime
proof
let q be Nat;
hereby assume q in {2,3,5,7,11}; then
q = 2 or q = 3 or q = 5 or q = 7 or q = 11 by ENUMSET1:def 3;
hence q < 13 & q is prime by INT_2:28,PEPIN:41,59,NAT_4:26,NAT_4:27;
end;
assume
Z: q < 13 & q is prime; then
q < 12 + 1; then
q <= 12 by NAT_1:13; then
q = 0 or ... or q = 12;
hence thesis
by ENUMSET1:def 3,Z,INT_2:29,lem6,lem8,lem9,lem12,lem10;
end;
hence thesis by A1,NEWTON:def 7;
end;
theorem
primenumber 5 = 13
proof
2,3,5,7,11 are_mutually_distinct by ZFMISC_1:def 7;
then 5 = card SetPrimenumber 13 by LS13,CARD_2:63;
hence thesis by NAT_4:28,NEWTON:def 8;
end;
theorem
for m, n being Nat holds
SetPrimenumber m c= SetPrimenumber n
or SetPrimenumber n c= SetPrimenumber m
proof
let m, n be Nat;
m <= n or n <= m;
hence thesis by NEWTON:69;
end;
theorem Cosik1:
for n, m being Nat holds n < m iff primenumber n < primenumber m
proof
let n, m be Nat;
AA: for n, m being Nat st n < m holds primenumber n < primenumber m
proof
let n, m be Nat;
assume
A2: n < m;
assume
A3: primenumber n >= primenumber m;
n = card SetPrimenumber primenumber n by NEWTON:def 8; then
A4: card SetPrimenumber primenumber n < card SetPrimenumber primenumber m
by A2,NEWTON:def 8;
Segm card SetPrimenumber primenumber m c=
Segm card SetPrimenumber primenumber n by CARD_1:11,A3,NEWTON:69;
hence contradiction by A4,NAT_1:39;
end;
hence n < m implies primenumber n < primenumber m;
assume
A1: primenumber n < primenumber m;
assume m <= n; then
m < n or m = n by XXREAL_0:1;
hence thesis by A1,AA;
end;
begin :: Prime Reciprocals
reserve n,i for Nat;
definition
func ReciPrime -> Real_Sequence means :ReciPr:
for i being Nat holds
it.i = 1 / primenumber i;
correctness
proof
deffunc F(Nat) = 1 / primenumber $1;
thus (ex seq being Real_Sequence st
for n being Nat holds seq.n=F(n)) &
(for seq1, seq2 being Real_Sequence st
(for n being Nat holds seq1.n=F(n)) &
(for n being Nat holds seq2.n=F(n)) holds seq1=seq2)
from NUMPOLY1:sch 1;
end;
end;
notation let f be Real_Sequence;
antonym f is divergent for f is convergent;
end;
registration
cluster ReciPrime -> decreasing bounded_below;
coherence
proof
set f = ReciPrime;
for n,m being Nat st n < m holds f.m < f.n
proof
let n,m be Nat;
assume A1: n < m;
f.n = 1 / primenumber n & f.m = 1 / primenumber m by ReciPr;
hence thesis by A1,Cosik1,XREAL_1:76;
end;
hence f is decreasing by SEQM_3:4;
for n being Nat holds f.n > 0
proof
let n be Nat;
f.n = 1 / primenumber n by ReciPr;
hence thesis;
end;
hence thesis;
end;
end;
registration
cluster ReciPrime -> convergent;
coherence;
end;
definition
func invNAT -> Real_Sequence means :DefRec:
for i being Nat holds it.i = 1 / i;
correctness
proof
deffunc F(Nat) = 1 / $1;
thus (ex seq being Real_Sequence st
for n being Nat holds seq.n = F(n)) &
(for seq1, seq2 being Real_Sequence st
(for n being Nat holds seq1.n = F(n)) &
(for n being Nat holds seq2.n = F(n)) holds seq1 = seq2)
from NUMPOLY1:sch 1;
end;
end;
registration
cluster invNAT -> nonnegative-yielding;
coherence
proof
let r be Real;
assume r in rng invNAT; then
consider p being object such that
A1: p in dom invNAT & r = invNAT.p by FUNCT_1:def 3;
reconsider p as Nat by A1;
r = 1 / p by DefRec,A1;
hence thesis;
end;
end;
registration
cluster invNAT -> convergent;
coherence
proof
for n being Nat holds invNAT.n = 1 / (n + 0) by DefRec;
hence thesis by SEQ_4:31;
end;
end;
theorem LimId:
lim invNAT = 0
proof
for n being Nat holds invNAT.n = 1 / (n + 0) by DefRec;
hence thesis by SEQ_4:31;
end;
theorem RecSub:
ReciPrime is subsequence of invNAT
proof
deffunc F(Nat) = primenumber $1;
consider f being Real_Sequence such that
A1: for i being Nat holds f.i = F(i) from SEQ_1:sch 1;
reconsider f as Function of NAT, REAL;
A3: for n being Nat holds f.n is Element of NAT
proof
let n be Nat;
f.n = primenumber n by A1;
hence thesis;
end;
for n,m being Nat st n < m holds f.n < f.m
proof
let n,m be Nat;
assume
C1: n < m;
f.n = primenumber n & f.m = primenumber m by A1;
hence thesis by Cosik1,C1;
end; then
reconsider f as increasing sequence of NAT by A3,SEQM_3:13,1;
take f;
ReciPrime = invNAT * f
proof
for x being Element of NAT holds ReciPrime.x = (invNAT * f).x
proof
let x be Element of NAT;
dom f = NAT by FUNCT_2:def 1; then
(invNAT * f).x = invNAT.(f.x) by FUNCT_1:13
.= invNAT.(primenumber x) by A1
.= 1 / primenumber x by DefRec;
hence thesis by ReciPr;
end;
hence thesis by FUNCT_2:def 8;
end;
hence thesis;
end;
registration let f be nonnegative-yielding Real_Sequence;
cluster -> nonnegative-yielding for subsequence of f;
coherence
proof
let g be subsequence of f;
let r be Real;
rng g c= rng f by VALUED_0:21;
hence thesis by PARTFUN3:def 4;
end;
end;
registration
cluster ReciPrime -> nonnegative-yielding;
coherence by RecSub;
end;
theorem
lim ReciPrime = 0 by LimId,RecSub,SEQ_4:17;
registration
cluster Partial_Sums ReciPrime -> non-decreasing for Real_Sequence;
coherence
proof
for n be Nat holds 0 <= ReciPrime.n
proof
let n be Nat;
ReciPrime.n in rng ReciPrime by FUNCT_2:4,ORDINAL1:def 12;
hence thesis by PARTFUN3:def 4;
end;
hence thesis by SERIES_1:16;
end;
end;
theorem
for f being nonnegative-yielding Real_Sequence st f is summable holds
for p being Real st p > 0 holds
ex i being Element of NAT st Sum (f ^\ i) < p
proof
let f be nonnegative-yielding Real_Sequence;
assume
A1: f is summable;
let p be Real;
assume
B1: p > 0;
assume
O1: for i being Element of NAT holds Sum (f ^\ i) >= p;
set S = Sum f;
Partial_Sums f is convergent by A1,SERIES_1:def 2; then
consider n being Nat such that
D1: for m being Nat st n <= m holds
|. (Partial_Sums f.m - S) .| < p by B1,SEQ_2:def 7;
reconsider m = n + 1 as Element of NAT;
reconsider m1 = m + 1 as Element of NAT;
x1: Partial_Sums f.m + Sum (f ^\ m1) = S by A1,SERIES_1:15;
set R = f ^\ m1;
Y1: R is summable by A1,SERIES_1:12;
for n being Nat holds 0 <= R.n by RINFSUP1:def 3;
then Sum (f ^\ m1) >= 0 by Y1,SERIES_1:18; then
-(S - Partial_Sums f.m) <= -0 by x1; then
per cases;
suppose
X3: Partial_Sums f.m - S < 0;
|. (Partial_Sums f.m - S) .| < p by D1,NAT_1:11; then
-(Partial_Sums f.m - S) < p by X3,ABSVALUE:def 1;
hence thesis by O1,x1;
end;
suppose
Partial_Sums f.m - S = 0;
hence thesis by O1,x1,B1;
end;
end;
begin :: Square Factors
definition let n be non zero Nat;
func SqFactors n -> ManySortedSet of SetPrimes means :SqDef:
support it = support pfexp n &
for p being Nat st p in support pfexp n holds
it.p = p |^ ((p |-count n) div 2);
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) div 2)) &
(not p in support pfexp n implies $2 = 0);
A1: for x,y1,y2 being object st
x in SetPrimes & P[x,y1] & P[x,y2] holds y1 = y2
proof
let x,y1,y2 be object such that
A2: x in SetPrimes and
A3: P[x,y1] and
A4: P[x,y2];
reconsider p = x as prime Element of NAT by A2,NEWTON:def 6;
y1 = y2
proof
per cases;
suppose Z1: p in support pfexp n;
hence y1 = p |^ ((p |-count n) div 2) by A3 .= y2 by Z1,A4;
end;
suppose Z1: not p in support pfexp n;
hence y1 = 0 by A3 .= y2 by A4,Z1;
end;
end;
hence y1 = y2;
end;
A5: for x being object st x in SetPrimes ex y being object st P[x,y]
proof
let x be object such that
A6: x in SetPrimes;
reconsider i = x as prime Element of NAT by A6,NEWTON:def 6;
per cases;
suppose A7: i in support pfexp n;
take i |^ ((i |-count n) div 2);
let p be Prime; assume p = x;
hence thesis by A7;
end;
suppose A8: not i in support pfexp n;
take 0;
let p be Prime; assume p = x;
hence thesis by A8;
end;
end;
consider f being Function such that
A9: dom f = SetPrimes and
A10: for x being object st x in SetPrimes holds P[x,f.x]
from FUNCT_1:sch 2(A1, A5);
A11: support f c= SetPrimes by A9,PRE_POLY:37;
A12: support f c= support pfexp n
proof
let x be object;
assume
A13: x in support f;
then x in SetPrimes by A11;
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 A10,A11,A13;
hence contradiction by A13,PRE_POLY:def 7;
end;
reconsider f as SetPrimes-defined Function by A9,RELAT_1:def 18;
reconsider f as ManySortedSet of SetPrimes by A9,PARTFUN1:def 2;
take f;
support pfexp n c= support f
proof
let x be object;
assume
J0: x in support pfexp n; then
reconsider p = x as Prime by NAT_3:34;
f.x = p |^ ((p |-count n) div 2) by A10,J0;
hence thesis by PRE_POLY:def 7;
end;
hence support f = support pfexp n by A12,XBOOLE_0:def 10;
let p be Nat;
assume
A15: p in support pfexp n; then
p is Prime by NAT_3:34;
hence f.p = p |^ ((p |-count n) div 2) by A15,A10;
end;
uniqueness
proof
let f1, f2 be ManySortedSet of SetPrimes such that
A16: support f1 = support pfexp n and
A17: for p being Nat st p in support pfexp n holds
f1.p = p|^((p|-count n) div 2) and
A18: support f2 = support pfexp n and
A19: for p being Nat st p in support pfexp n holds
f2.p = p|^((p|-count n) div 2);
now let i be object such that
A20: i in SetPrimes;
reconsider p = i as Prime by A20,NEWTON:def 6;
per cases;
suppose A21: p in support pfexp n;
hence f1.i = p|^((p|-count n) div 2) by A17
.= f2.i by A19,A21;
end;
suppose
A22: not p in support pfexp n;
hence f1.i = 0 by A16,PRE_POLY:def 7
.= f2.i by A18,A22,PRE_POLY:def 7;
end;
end;
hence thesis by PBOOLE:3;
end;
end;
registration let n be non zero Nat;
cluster SqFactors n -> finite-support natural-valued;
coherence
proof
A1: support SqFactors n c= support pfexp n by SqDef;
rng SqFactors n c= NAT
proof
let y be object;
assume y in rng SqFactors n; then
consider x being object such that
C1: x in dom SqFactors n & y = (SqFactors n).x by FUNCT_1:def 3;
dom SqFactors n = SetPrimes by PARTFUN1:def 2; then
reconsider p = x as Nat by C1;
per cases;
suppose p in support pfexp n; then
(SqFactors n).p = p |^ ((p |-count n) div 2) by SqDef;
hence thesis by C1,ORDINAL1:def 12;
end;
suppose not p in support pfexp n; then
not p in support (SqFactors n) by SqDef; then
(SqFactors n).p = 0 by PRE_POLY:def 7;
hence thesis by C1;
end;
end;
hence thesis by PRE_POLY:def 8,A1,VALUED_0:def 6;
end;
end;
registration let n be non zero Nat;
cluster -> natural for Element of support SqFactors n;
coherence;
end;
definition let n be non zero Nat;
func SqF n -> Nat equals
Product SqFactors n;
coherence;
end;
theorem Matsu:
for f being bag of SetPrimes holds Product f <> 0
proof
let f be bag of SetPrimes;
consider g being FinSequence of COMPLEX such that
A2: Product f = Product g & g = f*canFS(support f) by NAT_3:def 5;
assume Product f = 0; then
consider k be Nat such that
H1: k in dom g & g.k = 0 by A2,RVSUM_1:103;
h1: dom g c= dom canFS support f by A2,RELAT_1:25; then
H3: f.((canFS support f).k) = 0 by A2,H1,FUNCT_1:13;
(canFS support f).k in rng canFS support f by FUNCT_1:3,H1,h1; then
(canFS support f).k in support f by FUNCT_2:def 3;
hence thesis by H3,PRE_POLY:def 7;
end;
registration let n be non zero Nat;
cluster SqF n -> non zero;
coherence by Matsu;
end;
definition let p be Prime;
func FreeGen p -> Subset of NAT means :FG:
for n being Nat holds n in it iff
n is square-free & for i being Prime st i divides n holds i <= p;
existence
proof
defpred P[set] means
ex n being Nat st n = $1 &
n is square-free & for i being Prime st i divides n holds i <= p;
ex X being Subset of NAT st for x being Element of NAT holds x in X iff
P[x] from SUBSET_1:sch 3; then
consider X being Subset of NAT such that
A1: for x being Element of NAT holds x in X iff P[x];
take X;
let n be Nat;
hereby assume n in X; then
consider m being Nat such that
B1: m = n &
m is square-free & for i being Prime st i divides m holds i <= p by A1;
thus
n is square-free & for i being Prime st i divides n holds i <= p by B1;
end;
assume
b2: n is square-free & for i being Prime st i divides n holds i <= p;
n in NAT by ORDINAL1:def 12;
hence thesis by A1,b2;
end;
uniqueness
proof
let A1, A2 be Subset of NAT such that
A1: for n being Nat holds n in A1 iff
n is square-free & for i being Prime st i divides n holds i <= p and
A2: for n being Nat holds n in A2 iff
n is square-free & for i being Prime st i divides n holds i <= p;
for x being Element of NAT holds x in A1 iff x in A2
proof
let x be Element of NAT;
x in A1 iff x is square-free &
for i being Prime st i divides x holds i <= p by A1;
hence thesis by A2;
end;
hence thesis by SUBSET_1:3;
end;
end;
reserve p for Prime;
theorem Ex1:
1 in FreeGen p
proof
for i being Prime st i divides 1 holds i <= p
proof
let i be Prime;
assume i divides 1; then
i = 1 by WSIERP_1:15;
hence thesis by INT_2:def 4;
end;
hence thesis by FG,MOEBIUS1:22;
end;
theorem
not 0 in FreeGen p by MOEBIUS1:21,FG;
registration
cluster square-free non zero for Nat;
existence by MOEBIUS1:22;
end;
registration let p;
cluster positive-yielding for bag of Seg p;
existence
proof
set f = p |-> p;
reconsider f as bag of Seg p;
f is positive-yielding;
hence thesis;
end;
end;
theorem Thds:
for f being positive-yielding bag of Seg p holds
dom f = support f
proof
let f be positive-yielding bag of Seg p;
Y1: dom f = Seg p by PARTFUN1:def 2;
Seg p c= support f
proof
let x be object;
assume x in Seg p; then
f.x in rng f by Y1,FUNCT_1:3;
hence thesis by PRE_POLY:def 7;
end;
hence thesis by Y1,XBOOLE_0:def 10;
end;
theorem domcanFS:
dom canFS Seg p = Seg p
proof
len canFS Seg p = card Seg p by FINSEQ_1:93
.= p by FINSEQ_1:57;
hence thesis by FINSEQ_1:def 3;
end;
theorem
for A being finite set holds
dom canFS A = Seg card A
proof
let A be finite set;
len canFS A = card A by FINSEQ_1:93;
hence thesis by FINSEQ_1:def 3;
end;
theorem ThCon:
for g being positive-yielding bag of Seg p st g = p |-> p holds
g = g * canFS support g
proof
let f be positive-yielding bag of Seg p;
assume A0: f = p |-> p;
Y1: dom f = Seg p by A0; then
yy: support f = Seg p by Thds;
set g = f * canFS Seg p;
R5: rng canFS Seg p = Seg p by FUNCT_2:def 3;
R3: dom canFS Seg p = Seg p by domcanFS;
R4: dom g = dom canFS Seg p by RELAT_1:27,R5,Y1
.= Seg p by domcanFS; then
GG: dom g = dom (p |-> p);
for x being object st x in dom g holds g.x = (p |-> p).x
proof
let x be object;
assume
Z2: x in dom g;
hence g.x = f.((canFS Seg p).x) by FUNCT_1:12
.= p by Z2,FUNCOP_1:7,A0,R5,R3,R4,FUNCT_1:3
.= (p |-> p).x by FUNCOP_1:7,Z2,R4;
end;
hence thesis by A0,yy,FUNCT_1:2,GG;
end;
theorem
for f being positive-yielding bag of Seg p st f = p |-> p holds
Product f = p |^ p
proof
let f be positive-yielding bag of Seg p;
assume
A0: f = p |-> p;
consider g being FinSequence of COMPLEX such that
A1: Product f = Product g & g = f * canFS support f by NAT_3:def 5;
g = f by ThCon,A0,A1;
hence thesis by A1,A0,NEWTON:def 1;
end;
theorem Lm1:
for n being non zero Nat st n in FreeGen p holds
support pfexp n c= Seg p
proof
let n be non zero Nat;
assume n in FreeGen p; then
A2: for i being Prime st i divides n holds i <= p by FG;
let x be object;
assume
A1: x in support pfexp n; then
reconsider k = x as Prime by NAT_3:34;
A3: 1 < k by INT_2:def 4;
k divides n by A1,NAT_3:36;
hence thesis by A3,FINSEQ_1:1,A2;
end;
theorem
for n being non zero Nat st n in FreeGen p holds
card support pfexp n <= p
proof
let n be non zero Nat;
assume n in FreeGen p; then
card support pfexp n <= card Seg p by NAT_1:43,Lm1;
hence thesis by FINSEQ_1:57;
end;
theorem LmRng:
for n being square-free non zero Nat holds
rng pfexp n c= 2
proof
let n be square-free non zero Nat;
let y be object;
assume y in rng pfexp n; then
consider x being object such that
A1: x in dom pfexp n & y = (pfexp n).x by FUNCT_1:def 3;
reconsider x as Prime by A1,NAT_3:33;
A2: y = x |-count n by A1,NAT_3:def 8;
reconsider y1 = y as Nat by A1;
y = 0 or y = 1 by NAT_1:25,MOEBIUS1:24,A2;
hence thesis by CARD_1:50,TARSKI:def 2;
end;
theorem WOW:
for m, n being non zero Nat st pfexp m = pfexp n holds
m = n
proof
let m, n be non zero Nat;
K1: dom pfexp m = SetPrimes by PARTFUN1:def 2
.= dom ppf m by PARTFUN1:def 2;
K2: dom pfexp n = SetPrimes by PARTFUN1:def 2
.= dom ppf n by PARTFUN1:def 2;
assume
SS: pfexp m = pfexp n;
for x being object st x in dom ppf m holds
(ppf m).x = (ppf n).x
proof
let x be object;
assume x in dom ppf m; then
reconsider y = x as Prime by K1,NAT_3:33;
per cases;
suppose
B1: y in support pfexp m & y in support pfexp n; then
B2: (ppf m).y = y |^ (y |-count m) by NAT_3:def 9;
y |-count m = (pfexp m).y by NAT_3:def 8
.= y |-count n by NAT_3:def 8,SS;
hence thesis by B2,B1,NAT_3:def 9;
end;
suppose not y in support pfexp m & y in support pfexp n;
hence thesis by SS;
end;
suppose y in support pfexp m & not y in support pfexp n;
hence thesis by SS;
end;
suppose not y in support pfexp m & not y in support pfexp n; then
KS: not y in support ppf m & not y in support ppf n by NAT_3:def 9;
hence (ppf m).x = 0 by PRE_POLY:def 7
.= (ppf n).x by KS,PRE_POLY:def 7;
end;
end; then
ppf m = ppf n by SS,K1,K2,FUNCT_1:2; then
m = Product ppf n by NAT_3:61;
hence thesis by NAT_3:61;
end;
registration let p be Prime;
cluster FreeGen p -> non empty;
coherence by Ex1;
end;
registration let p be Prime;
cluster -> non empty for Element of FreeGen p;
coherence by MOEBIUS1:21,FG;
end;
definition let p be Prime;
func BoolePrime p -> set equals
Funcs ((Seg p) /\ SetPrimes, 2);
coherence;
end;
registration let p be Prime;
cluster BoolePrime p -> finite;
coherence;
end;
definition let p be Prime;
func canHom p -> Function of FreeGen p, BoolePrime p means :canH:
for x being Element of FreeGen p holds
it.x = (pfexp x) | (Seg p /\ SetPrimes);
existence
proof
deffunc F(Nat) = (pfexp $1) | (Seg p /\ SetPrimes);
A0: for x being Element of FreeGen p holds
F(x) in BoolePrime p
proof
let x be Element of FreeGen p;
dom pfexp x = SetPrimes by PARTFUN1:def 2; then
J1: dom ((pfexp x) | (Seg p /\ SetPrimes)) =
SetPrimes /\ ((Seg p) /\ SetPrimes) by RELAT_1:61
.= (Seg p) /\ SetPrimes by XBOOLE_1:17,XBOOLE_1:28;
set SP = (Seg p) /\ SetPrimes;
rng ((pfexp x) | SP) c= 2
proof
x is square-free & for i being Prime st i divides x holds i <= p
by FG; then
l1: rng pfexp x c= 2 by LmRng;
rng ((pfexp x) | SP) c= rng pfexp x by RELAT_1:70;
hence thesis by l1;
end; then
(pfexp x) | SP is Function of (Seg p) /\ SetPrimes, 2
by J1,FUNCT_2:2;
hence thesis by FUNCT_2:8;
end;
consider f being Function of FreeGen p, BoolePrime p such that
A1: for x being Element of FreeGen p holds f.x = F(x) from FUNCT_2:sch 8(A0);
thus thesis by A1;
end;
uniqueness
proof
let f1, f2 be Function of FreeGen p, BoolePrime p
such that
A1: for x being Element of FreeGen p holds
f1.x = (pfexp x) | (Seg p /\ SetPrimes) and
A2: for x being Element of FreeGen p holds
f2.x = (pfexp x) | (Seg p /\ SetPrimes);
for x being Element of FreeGen p holds f1.x = f2.x
proof
let x be Element of FreeGen p;
thus f1.x = (pfexp x) | (Seg p /\ SetPrimes) by A1 .= f2.x by A2;
end;
hence thesis by FUNCT_2:def 8;
end;
end;
registration let p be Prime;
cluster canHom p -> one-to-one;
coherence
proof
set X = FreeGen p;
defpred P[non zero Nat, object] means
$2 = (pfexp $1) | ((Seg p) /\ SetPrimes);
set f = canHom p;
for x1,x2 being object st
x1 in X & x2 in X & f.x1 = f.x2 holds x1 = x2
proof
let x1,x2 be object;
assume
I0: x1 in X & x2 in X & f.x1 = f.x2; then
reconsider m1 = x1, m2 = x2 as non zero Nat by MOEBIUS1:21;
II: P[m1,f.x1] & P[m2,f.x2] by I0,canH;
u1: dom pfexp m1 = SetPrimes & dom pfexp m2 = SetPrimes
by PARTFUN1:def 2;
ki: support pfexp m1 c= Seg p & support pfexp m2 c= Seg p by Lm1,I0;
kk: support pfexp m1 = support pfexp m2
proof
assume not thesis; then
consider z being object such that
JJ: not (z in support pfexp m1 iff z in support pfexp m2) by TARSKI:2;
per cases by JJ;
suppose
he: z in support pfexp m1 & not z in support pfexp m2; then
hh: (pfexp m1).z <> 0 & (pfexp m2).z = 0 by PRE_POLY:def 7;
xk: z in SetPrimes /\ Seg p by XBOOLE_0:def 4,he,ki; then
((pfexp m1) | (SetPrimes /\ Seg p)).z = (pfexp m1).z
by FUNCT_1:49;
hence thesis by xk,FUNCT_1:49,I0,II,hh;
end;
suppose
he: z in support pfexp m2 & not z in support pfexp m1; then
hh: (pfexp m2).z <> 0 & (pfexp m1).z = 0 by PRE_POLY:def 7;
xk: z in SetPrimes /\ Seg p by XBOOLE_0:def 4,he,ki; then
((pfexp m2) | (SetPrimes /\ Seg p)).z <> 0 by hh,FUNCT_1:49;
hence thesis by hh,xk,FUNCT_1:49,I0,II;
end;
end;
for x being object st
x in dom pfexp m1 holds (pfexp m1).x = (pfexp m2).x
proof
let x be object;
assume x in dom pfexp m1;
per cases;
suppose
GG: x in SetPrimes /\ Seg p;
hence (pfexp m1).x =
((pfexp m1) | (SetPrimes /\ Seg p)).x by FUNCT_1:49
.= (pfexp m2).x by FUNCT_1:49,GG,I0,II;
end;
suppose not x in SetPrimes /\ Seg p; then
zo: not x in support pfexp m1 by ki,XBOOLE_0:def 4; then
(pfexp m1).x = 0 by PRE_POLY:def 7;
hence thesis by PRE_POLY:def 7,kk,zo;
end;
end;
hence thesis by WOW,FUNCT_1:2,u1;
end;
hence thesis by FUNCT_2:19;
end;
end;
theorem FinCar:
card FreeGen p c= card BoolePrime p
proof
A1: dom canHom p = FreeGen p by FUNCT_2:def 1;
rng canHom p c= BoolePrime p by RELAT_1:def 19;
hence thesis by A1,CARD_1:10;
end;
LmX:
card FreeGen p c= 2 |^ p
proof
A1: card FreeGen p c= card BoolePrime p by FinCar;
A2: card ((Seg p) /\ SetPrimes) <= card Seg p by NAT_1:43,XBOOLE_1:17;
card BoolePrime p =
(card 2) |^ (card (((Seg p) /\ SetPrimes))) by CARD_FIN:4
.= 2 |^ (card ((Seg p) /\ SetPrimes)); then
card BoolePrime p <= 2 |^ (card Seg p) by PREPOWER:93,A2; then
card BoolePrime p <= 2 |^ p by FINSEQ_1:57; then
Segm card BoolePrime p c= Segm (2 |^ p) by NAT_1:39;
hence thesis by A1;
end;
registration let p be Prime;
cluster FreeGen p -> finite;
coherence
proof
card FreeGen p c= 2 |^ p by LmX;
hence thesis;
end;
end;
theorem
card FreeGen p <= 2 |^ p
proof
Segm card FreeGen p c= Segm (2 |^ p) by LmX;
hence thesis by NAT_1:39;
end;
theorem Ciek: :: MOEBIUS1:9 inverted
n <> 0 & (p |^ i) divides n implies i <= p |-count n
proof
assume A0: n <> 0;
assume A1: (p |^ i) divides n;
reconsider b = p |^ i as non zero Nat;
reconsider a = n as non zero Nat by A0;
p |-count b <= p |-count a by A1,NAT_3:30;
hence thesis by NAT_3:25,INT_2:def 4;
end;
theorem MoInv: :: MOEBIUS1:24 inverted
n <> 0 & (for p being Prime holds p |-count n <= 1) implies
n is square-free
proof
assume
A1: n <> 0 & for p being Prime holds p |-count n <= 1;
assume n is square-containing; then
consider p being Prime such that
A2: p |^ 2 divides n by MOEBIUS1:def 1;
p |-count n >= 1 + 1 by A1,A2,Ciek;
hence thesis by A1,NAT_1:13;
end;
theorem MB148:
for p being Prime, n being non zero Nat st
p |-count n = 0 holds (SqFactors 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 SqFactors n by SqDef;
hence thesis by PRE_POLY:def 7;
end;
theorem MB149:
for n being non zero Nat, p being Prime st
p |-count n <> 0 holds
(SqFactors n).p = p |^ ((p |-count n) div 2)
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 SqDef;
end;
theorem MB150:
for m, n being non zero Nat st
m, n are_coprime holds
SqFactors (m * n) = SqFactors m + SqFactors n
proof
let a, b be non zero Nat;
reconsider an = a, bn = b as non zero Nat;
assume
A1: a, b are_coprime;
deffunc F(non zero Nat) = SqFactors $1;
now
let i be object;
assume i in SetPrimes;
then reconsider p = i as Prime by NEWTON:def 6;
A2: p |-count (an*bn) = (p |-count a) + (p |-count b) by NAT_3:28;
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 (F(a*b)).i = 0 by A5,MB148
.= 0 + (F(b)).i by A6,MB148
.= (F(a)).i + (F(b)).i by A7,MB148
.= (F(a) + F(b)).i by PRE_POLY:def 5;
end;
suppose
A8: p |-count (a*b) <> 0;
thus (F(a*b)).i = (F(a) + F(b)).i
proof
per cases by A2,A8;
suppose
A9: (p |-count a) <> 0;
A10: (p |-count b) = 0
proof
consider ka being Nat such that
A11: (p |-count a) = ka+1 by A9,NAT_1:6;
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;
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 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;
b = p*((p|^kb)*lb) by A15;
then p divides b;
then p divides 1 by A1,A13,NAT_D:def 5;
hence contradiction by INT_2:def 4,NAT_D:7;
end;
thus (F(a*b)).i = p |^ ((p |-count (a*b)) div 2) by A8,MB149
.= (F(a)).p + 0 by A9,MB149,A10,A2
.= (F(a)).p + (F(b)).p by A10,MB148
.= (F(a) + F(b)).i by PRE_POLY:def 5;
end;
suppose
A16: (p |-count b) <> 0;
A17: (p |-count a) = 0
proof
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 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;
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 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;
b = p*((p|^kb)*lb) by A22;
then p divides b;
then p divides 1 by A1,A20,NAT_D:def 5;
hence contradiction by INT_2:def 4,NAT_D:7;
end;
thus (F(a*b)).i = p |^ ((p |-count (a*b)) div 2) by A8,MB149
.= 0+(F(b)).p by A16,MB149,A17,A2
.= (F(a)).p + (F(b)).p by A17,MB148
.= (F(a) + F(b)).i by PRE_POLY:def 5;
end;
end;
end;
end;
hence thesis by PBOOLE:3;
end;
theorem
for n being non zero Nat holds SqF n divides n
proof
deffunc F(non zero Nat) = Product SqFactors $1;
deffunc G(non zero Nat) = SqFactors $1;
defpred P[Nat] means for n being non zero Nat st
support G(n) c= Seg $1 holds F(n) divides n;
let n be non zero Nat;
A1: ex mS being Element of NAT st support ppf n c= Seg mS by MOEBIUS1:14;
A2: support ppf n = support pfexp n by NAT_3:def 9
.= support G(n) by SqDef;
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 G(n) c= Seg (k+1);
A6: support pfexp n = support G(n) by SqDef;
per cases;
suppose
A7: not support G(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 G(n);
support G(n) c= Seg k
proof
let x be object;
assume
A10: x in support G(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;
reconsider s, t as non zero Nat by A14;
consider f being FinSequence of COMPLEX such that
A15: Product G(s) = Product f and
A16: f = (G(s))*canFS(support G(s)) by NAT_3:def 5;
A17: dom G(s) = SetPrimes by PARTFUN1:def 2;
A18: support ppf s = support pfexp s by NAT_3:def 9; then
A19: support ppf s = support G(s) by SqDef;
(pfexp n).p = e by A12,NAT_3:def 8; then
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 G(t) c= Seg k
proof
set f = p |-count t;
let x be object;
assume
A24: x in support G(t);
then reconsider m = x as Nat;
A25: x in support pfexp t by A24,SqDef;
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;
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;
hence contradiction by A13,NAT_3:def 7;
end;
support pfexp t c= support pfexp n by A14,NAT_3:45;
then support G(t) c= support G(n) by A6,SqDef;
then m in support G(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: F(t) divides t by A4;
support G(s) = {p} by A18,A21,SqDef;
then f = (G(s))*<*p*> by A16,FINSEQ_1:94
.= <* (G(s)).p *> by FINSEQ_2:34,A17,A8; then
h1: Product G(s) = (G(s)).p by A15
.= p |^ ((p |-count s) div 2) by A22,SqDef;
H2: (p |-count s) <= (p |-count n) by A12,NAT_3:25,INT_2:def 4;
p |-count s = 0 iff not p divides s by NAT_3:27,A13; then
(p |-count s) div 2 <= (p |-count s) by INT_1:56; then
ZZ: p |^ ((p |-count s) div 2) divides p |^ e by NEWTON:89,H2,XXREAL_0:2;
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 G(t) by SqDef;
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 G(t) by SqDef;
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;
A39: 0+1 <= u by NAT_1:13;
assume not s1,t1 are_coprime;
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 = 1 or r = p by A12,INT_2:def 4,A40,NAT_3:5;
then p in support pfexp t
by NAT_3:37,A40,A41,A38,NAT_D:4;
then p in support G(t) by SqDef;
then k+1 <= k by A23,FINSEQ_1:1;
hence contradiction by NAT_1:13;
end;
then F(n) = Product (G(s)+G(t)) by A14,MB150
.= F(s) * F(t) by A34,A19,A33,NAT_3:19;
hence thesis by A14,h1,ZZ,A31,NAT_3:1;
end;
suppose
support G(n) c= Seg k;
hence thesis by A4;
end;
end;
A42: P[0]
proof
let n be non zero Nat;
assume support G(n) c= Seg 0;
then support G(n) = {};
then G(n) = EmptyBag SetPrimes by PRE_POLY:81;
then F(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;
registration let n be non zero Nat;
cluster PFactors n -> prime-factorization-like;
coherence
proof
set p = PFactors n;
for x being Prime st x in support p
ex n be Nat st 0 < n & p.x = x |^n
proof
let x be Prime;
assume x in support p; then
a1: x in support pfexp n by MOEBIUS1:def 6;
x = x |^ 1;
hence thesis by a1,MOEBIUS1:def 6;
end;
hence thesis by INT_7:def 1;
end;
end;
theorem Matsu0:
for f being bag of SetPrimes
ex g being FinSequence of NAT st
Product f = Product g & g = f*canFS(support f)
proof
let f be bag of SetPrimes;
consider g being FinSequence of COMPLEX such that
A2: Product f = Product g & g = f*canFS(support f) by NAT_3:def 5;
rng g c= NAT by A2,VALUED_0:def 6; then
g is FinSequence of NAT by FINSEQ_1:def 4;
hence thesis by A2;
end;
theorem Matsu1:
for f being bag of SetPrimes st f.p = p |^ n holds
p |^ n divides Product f
proof
let f be bag of SetPrimes;
assume
AA: f.p = p |^ n;
consider g being FinSequence of NAT such that
A2: Product f = Product g & g = f*canFS(support f) by Matsu0;
reconsider PP = Product g as Nat;
p in SetPrimes by NEWTON:def 6; then
B0: p in dom f by PARTFUN1:def 2;
B1: p in support f by AA,PRE_POLY:def 7;
rng canFS support f = support f by FUNCT_2:def 3; then
consider y being object such that
B2: y in dom canFS support f & p = (canFS support f).y by B1,FUNCT_1:def 3;
B3: y in dom g by A2,FUNCT_1:11,B2,B0;
f.p = g.y by A2,B2,FUNCT_1:13; then
f.p in rng g by FUNCT_1:3,B3;
hence thesis by A2,AA,NAT_3:7;
end;
theorem BZE:
for f being bag of SetPrimes st f.p = p |^ n holds
p |-count Product f >= n
proof
let f be bag of SetPrimes;
assume
AA: f.p = p |^ n;
Product f <> 0 by Matsu;
hence thesis by Ciek,AA,Matsu1;
end;
begin :: Extracting Square-Containing and Square-Free Part of a Number
definition let n be non zero Nat;
func TSqFactors n -> ManySortedSet of SetPrimes means :TSqDef:
support it = support pfexp n &
for p being Nat st p in support pfexp n holds
it.p = p |^ (2 * ((p |-count n) div 2));
existence
proof
defpred P[object,object] means
for p being Prime st $1 = p holds
(p in support pfexp n implies $2 = p |^ (2 * ((p |-count n) div 2))) &
(not p in support pfexp n implies $2 = 0);
A1: for x,y1,y2 being object st
x in SetPrimes & P[x,y1] & P[x,y2] holds y1 = y2
proof
let x,y1,y2 be object such that
A2: x in SetPrimes and
A3: P[x,y1] and
A4: P[x,y2];
reconsider p = x as Prime by A2,NEWTON:def 6;
y1 = y2
proof
per cases;
suppose
Z1: p in support pfexp n;
hence y1 = p |^ (2 * ((p |-count n) div 2)) by A3 .= y2 by Z1,A4;
end;
suppose
Z1: not p in support pfexp n;
hence y1 = 0 by A3 .= y2 by A4,Z1;
end;
end;
hence y1 = y2;
end;
A5: for x being object st x in SetPrimes ex y being object st P[x,y]
proof
let x be object such that
A6: x in SetPrimes;
reconsider i = x as prime Element of NAT by A6,NEWTON:def 6;
per cases;
suppose
A7: i in support pfexp n;
take i |^ (2 * ((i |-count n) div 2));
let p be Prime;
assume p = x;
hence thesis by A7;
end;
suppose
A8: not i in support pfexp n;
take 0;
let p be Prime; assume p = x;
hence thesis by A8;
end;
end;
consider f being Function such that
A9: dom f = SetPrimes and
A10: for x being object st x in SetPrimes holds P[x,f.x]
from FUNCT_1:sch 2(A1, A5);
A11: support f c= SetPrimes by A9,PRE_POLY:37;
A12: support f c= support pfexp n
proof
let x be object;
assume
A13: x in support f;
then reconsider i = x as Prime by A11,NEWTON:def 6;
assume not x in support pfexp n;
then f.i = 0 by A10,A11,A13;
hence contradiction by A13,PRE_POLY:def 7;
end;
reconsider f as SetPrimes-defined Function by A9,RELAT_1:def 18;
reconsider f as ManySortedSet of SetPrimes by A9,PARTFUN1:def 2;
take f;
support pfexp n c= support f
proof
let x be object;
assume
J0: x in support pfexp n; then
reconsider p = x as Prime by NAT_3:34;
f.x = p |^ (2 * ((p |-count n) div 2)) by A10,J0;
hence thesis by PRE_POLY:def 7;
end;
hence support f = support pfexp n by A12,XBOOLE_0:def 10;
let p be Nat;
assume
A15: p in support pfexp n; then
p is Prime by NAT_3:34;
hence f.p = p |^ (2 * ((p |-count n) div 2)) by A15,A10;
end;
uniqueness
proof
let f1, f2 be ManySortedSet of SetPrimes such that
A16: support f1 = support pfexp n and
A17: for p being Nat st p in support pfexp n holds
f1.p = p |^ (2 * ((p|-count n) div 2)) and
A18: support f2 = support pfexp n and
A19: for p being Nat st p in support pfexp n holds
f2.p = p |^ (2 * ((p|-count n) div 2));
now let i be object such that
A20: i in SetPrimes;
reconsider p = i as Prime by A20,NEWTON:def 6;
per cases;
suppose
A21: p in support pfexp n;
hence f1.i = p |^ (2 * ((p|-count n) div 2)) by A17
.= f2.i by A19,A21;
end;
suppose
A22: not p in support pfexp n;
hence f1.i = 0 by A16,PRE_POLY:def 7
.= f2.i by A18,A22,PRE_POLY:def 7;
end;
end;
hence thesis by PBOOLE:3;
end;
end;
theorem
for n being non zero Nat holds
TSqFactors n = (SqFactors n) |^ 2
proof
let n be non zero Nat;
A0: dom ((SqFactors n) |^ 2) = SetPrimes by PARTFUN1:def 2;
AA: dom TSqFactors n = SetPrimes &
dom (SqFactors n) = SetPrimes by PARTFUN1:def 2;
for x being object st x in dom TSqFactors n holds
(TSqFactors n).x = ((SqFactors n) |^ 2).x
proof
let x be object;
assume x in dom TSqFactors n; then
reconsider p = x as Prime by AA,NEWTON:def 6;
per cases;
suppose
J1: x in support pfexp n;
hence (TSqFactors n).x = p |^ (2 * ((p |-count n) div 2)) by TSqDef
.= (p |^ (((p |-count n) div 2))) |^ 2 by NEWTON:9
.= ((SqFactors n).x) |^ 2 by SqDef,J1
.= ((SqFactors n) |^ 2).x by NAT_3:def 6;
end;
suppose
J0: not x in support pfexp n; then
not x in support TSqFactors n by TSqDef; then
J3: (TSqFactors n).x = 0 by PRE_POLY:def 7;
not x in support SqFactors n by J0,SqDef; then
(SqFactors n).x = 0 by PRE_POLY:def 7; then
((SqFactors n).x) |^ 2 = 0 by NEWTON:11;
hence thesis by J3,NAT_3:def 6;
end;
end;
hence thesis by FUNCT_1:2,A0,PARTFUN1:def 2;
end;
registration let n be non zero Nat;
cluster TSqFactors n -> finite-support natural-valued;
coherence
proof
a2: support TSqFactors n c= support pfexp n by TSqDef;
rng TSqFactors n c= NAT
proof
let y be object;
assume y in rng TSqFactors n; then
consider x being object such that
C1: x in dom TSqFactors n & y = (TSqFactors n).x by FUNCT_1:def 3;
dom TSqFactors n = SetPrimes by PARTFUN1:def 2; then
reconsider p = x as Nat by C1;
per cases;
suppose p in support pfexp n; then
(TSqFactors n).p = p |^ (2 * ((p |-count n) div 2)) by TSqDef;
hence thesis by C1,ORDINAL1:def 12;
end;
suppose not p in support pfexp n; then
not p in support TSqFactors n by TSqDef; then
(TSqFactors n).p = 0 by PRE_POLY:def 7;
hence thesis by C1;
end;
end;
hence thesis by PRE_POLY:def 8,a2,VALUED_0:def 6;
end;
end;
definition let n be non zero Nat;
func TSqF n -> Nat equals
Product TSqFactors n;
coherence;
end;
registration let n be non zero Nat;
cluster TSqF n -> non zero;
coherence by Matsu;
end;
theorem MB148T:
for p being Prime, n being non zero Nat holds
p |-count n = 0 implies (TSqFactors 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 TSqFactors n by TSqDef;
hence thesis by PRE_POLY:def 7;
end;
theorem MB149T:
for n being non zero Nat, p being Prime st
p |-count n <> 0 holds
(TSqFactors n).p = p |^ (2 * ((p |-count n) div 2))
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 TSqDef;
end;
theorem MB150T:
for m, n being non zero Nat st
m, n are_coprime holds
TSqFactors (m * n) = TSqFactors m + TSqFactors n
proof
let a, b be non zero Nat;
reconsider an = a, bn = b as non zero Nat;
assume
A1: a, b are_coprime;
deffunc F(non zero Nat) = TSqFactors $1;
now
let i be object;
assume i in SetPrimes;
then reconsider p = i as Prime by NEWTON:def 6;
A2: p |-count (an*bn) = (p |-count a) + (p |-count b) by NAT_3:28;
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 (F(a*b)).i = 0 by A5,MB148T
.= 0 + (F(b)).i by A6,MB148T
.= (F(a)).i + (F(b)).i by A7,MB148T
.= (F(a) + F(b)).i by PRE_POLY:def 5;
end;
suppose
A8: p |-count (a*b) <> 0;
thus (F(a*b)).i = (F(a) + F(b)).i
proof
per cases by A2,A8;
suppose
A9: (p |-count a) <> 0;
A10: (p |-count b) = 0
proof
consider ka being Nat such that
A11: (p |-count a) = ka+1 by A9,NAT_1:6;
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;
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 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;
b = p*((p|^kb)*lb) by A15;
then p divides b;
then p divides 1 by A1,A13,NAT_D:def 5;
hence contradiction by INT_2:def 4,NAT_D:7;
end;
thus (F(a*b)).i = p |^ (2 * ((p |-count (a*b)) div 2)) by A8,MB149T
.= (F(a)).p + 0 by A9,MB149T,A10,A2
.= (F(a)).p + (F(b)).p by A10,MB148T
.= (F(a) + F(b)).i by PRE_POLY:def 5;
end;
suppose
A16: (p |-count b) <> 0;
A17: (p |-count a) = 0
proof
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;
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 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;
b = p*((p|^kb)*lb) by A22;
then p divides b;
then p divides 1 by A1,A20,NAT_D:def 5;
hence contradiction by INT_2:def 4,NAT_D:7;
end;
thus (F(a*b)).i = p |^ (2 * ((p |-count (a*b)) div 2)) by A8,MB149T
.= 0+(F(b)).p by A16,MB149T,A17,A2
.= (F(a)).p + (F(b)).p by A17,MB148T
.= (F(a) + F(b)).i by PRE_POLY:def 5;
end;
end;
end;
end;
hence thesis by PBOOLE:3;
end;
registration let n be non zero Nat;
cluster support TSqFactors n -> natural-membered;
coherence;
end;
theorem Skup:
for n being non zero Nat holds TSqF n divides n
proof
deffunc F(non zero Nat) = Product TSqFactors $1;
deffunc G(non zero Nat) = TSqFactors $1;
defpred P[Nat] means for n being non zero Nat st
support G(n) c= Seg $1 holds F(n) divides n;
let n be non zero Nat;
A1: ex mS being Element of NAT st support ppf n c= Seg mS by MOEBIUS1:14;
A2: support ppf n = support pfexp n by NAT_3:def 9
.= support G(n) by TSqDef;
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 G(n) c= Seg (k+1);
A6: support pfexp n = support G(n) by TSqDef;
per cases;
suppose
A7: not support G(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 G(n);
support G(n) c= Seg k
proof
let x be object;
assume
A10: x in support G(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;
reconsider s, t as non zero Nat by A14;
consider f being FinSequence of COMPLEX such that
A15: Product G(s) = Product f and
A16: f = (G(s))*canFS(support G(s)) by NAT_3:def 5;
A17: dom G(s) = SetPrimes by PARTFUN1:def 2;
A18: support ppf s = support pfexp s by NAT_3:def 9; then
A19: support ppf s = support G(s) by TSqDef;
(pfexp n).p = e by A12,NAT_3:def 8; then
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 G(t) c= Seg k
proof
set f = p |-count t;
let x be object;
assume
A24: x in support G(t);
then reconsider m = x as Nat;
A25: x in support pfexp t by A24,TSqDef;
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;
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;
hence contradiction by A13,NAT_3:def 7;
end;
support pfexp t c= support pfexp n by A14,NAT_3:45;
then support G(t) c= support G(n) by A6,TSqDef;
then m in support G(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: F(t) divides t by A4;
support G(s) = {p} by A18,A21,TSqDef;
then f = (G(s))*<*p*> by A16,FINSEQ_1:94
.= <* (G(s)).p *> by FINSEQ_2:34,A17,A8; then
h1: Product G(s) = (G(s)).p by A15
.= p |^ (2 * ((p |-count s) div 2)) by A22,TSqDef;
H2: p |-count s <= p |-count n by A12,NAT_3:25,INT_2:def 4;
p |-count s = 0 iff not p divides s by NAT_3:27,A13; then
(2 * ((p |-count s) div 2)) <= p |-count s by FOTN; then
ZZ: p |^ (2 * ((p |-count s) div 2)) divides p |^ e
by NEWTON:89,H2,XXREAL_0:2;
reconsider s1 = s, t1 = t as non zero Nat;
support ppf t = support pfexp t by NAT_3:def 9; then
A33: support ppf t = support G(t) by TSqDef;
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 G(t) by TSqDef;
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;
A39: 0+1 <= u by NAT_1:13;
assume not s1,t1 are_coprime;
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 = 1 or r = p by A12,INT_2:def 4,A40,NAT_3:5;
then p in support pfexp t
by NAT_3:37,A40,A41,A38,NAT_D:4;
then p in support G(t) by TSqDef;
then k+1 <= k by A23,FINSEQ_1:1;
hence contradiction by NAT_1:13;
end;
then F(n) = Product (G(s)+G(t)) by A14,MB150T
.= F(s) * F(t) by A34,A19,A33,NAT_3:19;
hence thesis by A14,h1,ZZ,A31,NAT_3:1;
end;
suppose
support G(n) c= Seg k;
hence thesis by A4;
end;
end;
A42: P[0]
proof
let n be non zero Nat;
assume support G(n) c= Seg 0;
then support G(n) = {};
then G(n) = EmptyBag SetPrimes by PRE_POLY:81;
then F(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;
registration
let n be non zero Nat;
cluster n div TSqF n -> square-free for Nat;
coherence
proof
consider k being Nat such that
Z2: n = (TSqF n) * k by NAT_D:def 3,Skup;
n div (TSqF n) = k by Z2;
Z1: n div (TSqF n) <> 0 by Z2;
for p being Prime holds p |-count (n div (TSqF n)) <= 1
proof
let p be Prime;
XX: p <> 1 by INT_2:def 4;
reconsider b = TSqF n as non zero Nat;
S1: p |-count (n div b) = (p |-count n) -' (p |-count b) by Skup,NAT_3:31;
set h = 2 * ((p |-count n) div 2);
per cases;
suppose
K1: p in support pfexp n; then
s: (TSqFactors n).p = p |^ h by TSqDef;
p divides n by K1,NAT_3:36; then
p |-count n <> 0 by NAT_3:27,XX; then
S4: (p |-count n) - h <= 1 by FOT1;
(p |-count n) - (p |-count b) <= (p |-count n) - h
by s,BZE,XREAL_1:10; then
(p |-count n) - (p |-count b) <= 1 by S4,XXREAL_0:2;
hence thesis by S1,XREAL_0:def 2;
end;
suppose not p in support pfexp n; then
not p divides n by NAT_3:37; then
p |-count n = 0 by XX,NAT_3:27;
hence thesis by S1;
end;
end;
hence thesis by Z1,MoInv;
end;
end;
theorem SqCon1:
for n,k being non zero Nat st
k <> 1 & k ^2 divides n holds
n is square-containing
proof
let n, k be non zero Nat;
assume
A1: k <> 1 & k ^2 divides n; then
k |^ 2 divides n by NEWTON:81;
hence thesis by A1,MOEBIUS1:20;
end;
theorem DivRelPrime:
for n being square-free non zero Nat,
a being non zero Nat st a divides n holds
a, n div a are_coprime
proof
let n be square-free non zero Nat,
a be non zero Nat;
assume
A0: a divides n;
assume
Z1: not a, n div a are_coprime;
Z2: n div a <> 0
proof
assume n div a = 0; then
n < a by NAT_2:12;
hence thesis by NAT_D:7,A0;
end;
consider k being non zero Nat such that
A1: k <> 1 & k divides a & k divides n div a by RelPrimeEx,Z1,Z2;
a * (n div a) = n by A0; then
k ^2 divides n by A1,NAT_3:1;
hence thesis by A1,SqCon1;
end;
begin :: Binary Operations
theorem CutComm:
for A, C being non empty set,
L being commutative BinOp of A,
LC being BinOp of C st
C c= A & LC = L || C holds
LC is commutative
proof
let A, C be non empty set;
let L be commutative BinOp of A,
LC be BinOp of C;
assume
Z1: C c= A & LC = L || C;
for a, b being Element of C holds LC.(a,b) = LC.(b,a)
proof
let a, b be Element of C;
reconsider aa = a, bb = b as Element of A by Z1;
ZZ: L.(aa,bb) = L.(bb,aa) by BINOP_1:def 2;
thus LC.(a,b) = L.[aa,bb] by ZFMISC_1:87,FUNCT_1:49,Z1
.= LC.(b,a) by ZZ,ZFMISC_1:87,FUNCT_1:49,Z1;
end;
hence thesis by BINOP_1:def 2;
end;
theorem CutAssoc:
for A, C being non empty set,
L being associative BinOp of A,
LC being BinOp of C st
C c= A & LC = L || C holds
LC is associative
proof
let A, C be non empty set;
let L be associative BinOp of A,
LC be BinOp of C;
assume
Z1: C c= A & LC = L || C;
A1: dom LC = [:C,C:] by FUNCT_2:def 1;
for a, b, c being Element of C holds
LC.(a,LC.(b,c)) = LC.(LC.(a,b),c)
proof
let a, b, c be Element of C;
reconsider aa = a, bb = b, cc = c as Element of A by Z1;
W2: LC.(aa,bb) = L.(a,b) by ZFMISC_1:87,FUNCT_1:49,Z1;
ZZ: L.(aa,L.(bb,cc)) = L.(L.(aa,bb),cc) by BINOP_1:def 3;
set y = [aa,LC.[bb,cc]];
thus LC.(a,LC.(b,c)) = L.y by FUNCT_1:49,Z1,ZFMISC_1:87
.= L.(L.(aa,bb),cc) by ZZ,ZFMISC_1:87,FUNCT_1:49,Z1
.= LC.(LC.(a,b),c) by FUNCT_1:47,A1,Z1,W2,ZFMISC_1:87;
end;
hence thesis by BINOP_1:def 3;
end;
registration let C be non empty set;
let L be commutative BinOp of C,
M be BinOp of C;
cluster LattStr (# C, L, M #) -> join-commutative;
coherence by BINOP_1:def 2;
end;
registration let C be non empty set;
let L be BinOp of C,
M be commutative BinOp of C;
cluster LattStr (# C, L, M #) -> meet-commutative;
coherence by BINOP_1:def 2;
end;
registration let C be non empty set;
let L be associative BinOp of C,
M be BinOp of C;
cluster LattStr (# C, L, M #) -> join-associative;
coherence by BINOP_1:def 3;
end;
registration let C be non empty set;
let L be BinOp of C,
M be associative BinOp of C;
cluster LattStr (# C, L, M #) -> meet-associative;
coherence by BINOP_1:def 3;
end;
begin :: On the Natural Divisors
theorem DivInPlus:
for n being non zero Nat holds NatDivisors n c= NATPLUS by NAT_LAT:def 6;
theorem LCMDiv:
for n being non zero Nat,
x, y being Nat st x in NatDivisors n & y in NatDivisors n holds
x lcm y in NatDivisors n
proof
let n be non zero Nat;
let x, y be Nat;
assume
a0: x in NatDivisors n & y in NatDivisors n; then
x divides n & y divides n & x > 0 & y > 0 by MOEBIUS1:39; then
x lcm y divides n by NAT_D:def 4;
hence thesis by a0,MOEBIUS1:39;
end;
theorem GCDDiv:
for n being non zero Nat,
x, y being Nat st x in NatDivisors n & y in NatDivisors n holds
x gcd y in NatDivisors n
proof
let n be non zero Nat;
let x, y be Nat;
assume x in NatDivisors n & y in NatDivisors n; then
A0: x divides n & y divides n & x > 0 & y > 0 by MOEBIUS1:39;
x gcd y divides x by NAT_D:def 5;
hence thesis by A0,MOEBIUS1:39,NAT_D:4;
end;
registration let n be non zero Nat;
cluster NatDivisors n -> non empty;
coherence by MOEBIUS1:39;
end;
registration
cluster hcflat -> commutative associative;
coherence by NAT_LAT:def 3;
cluster lcmlat -> commutative associative;
coherence by NAT_LAT:def 3;
end;
theorem HcfLat:
hcflatplus = hcflat || NATPLUS
proof
set hp = hcflatplus;
set h = hcflat;
set N = NATPLUS;
[:N,N:] c= [:NAT,NAT:]; then
A0: [:N,N:] c= dom h by FUNCT_2:def 1;
hp = h | [:N,N:]
proof
A1: dom hp = [:N,N:] by FUNCT_2:def 1
.= dom (h | [:N,N:]) by RELAT_1:62,A0;
for x being object st x in dom hp holds
hp.x = (h | [:N,N:]).x
proof
let x be object;
assume x in dom hp; then
A2: x in [:N,N:] by FUNCT_2:def 1; then
consider x1, x2 being object such that
B1: x1 in N & x2 in N & x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1, x2 as NatPlus by B1;
thus hp.x = hp.(x1,x2) by B1
.= x1 gcd x2 by NAT_LAT:def 8
.= h.(x1,x2) by NAT_LAT:def 1
.= (h | [:N,N:]).x by A2,FUNCT_1:49,B1;
end;
hence thesis by A1,FUNCT_1:2;
end;
hence thesis;
end;
theorem LcmLat:
lcmlatplus = lcmlat || NATPLUS
proof
set hp = lcmlatplus;
set h = lcmlat;
set N = NATPLUS;
[:N,N:] c= [:NAT,NAT:]; then
A0: [:N,N:] c= dom h by FUNCT_2:def 1;
hp = h | [:N,N:]
proof
A1: dom hp = [:N,N:] by FUNCT_2:def 1
.= dom (h | [:N,N:]) by RELAT_1:62,A0;
for x being object st x in dom hp holds
hp.x = (h | [:N,N:]).x
proof
let x be object;
assume x in dom hp; then
A2: x in [:N,N:] by FUNCT_2:def 1; then
consider x1, x2 being object such that
B1: x1 in N & x2 in N & x = [x1,x2] by ZFMISC_1:def 2;
reconsider x1, x2 as NatPlus by B1;
thus hp.x = hp.(x1,x2) by B1
.= x1 lcm x2 by NAT_LAT:def 9
.= h.(x1,x2) by NAT_LAT:def 2
.= (h | [:N,N:]).x by A2,FUNCT_1:49,B1;
end;
hence thesis by A1,FUNCT_1:2;
end;
hence thesis;
end;
registration
cluster hcflatplus -> commutative;
coherence by CutComm,HcfLat;
cluster lcmlatplus -> commutative;
coherence by CutComm,LcmLat;
cluster hcflatplus -> associative;
coherence by CutAssoc,HcfLat;
cluster lcmlatplus -> associative;
coherence by CutAssoc,LcmLat;
end;
begin :: The Lattice of Natural Divisors
::$N The lattice of natural divisors
definition let n be non zero Nat;
func Divisors_Lattice n -> strict SubLattice of NatPlus_Lattice means
:DivLat:
the carrier of it = NatDivisors n;
existence
proof
set L = NatPlus_Lattice;
set C = NatDivisors n;
set LJ = (the L_join of L) || NatDivisors n;
set LM = (the L_meet of L) || NatDivisors n;
A0: C c= the carrier of L by NAT_LAT:def 6,def 10;
dom the L_join of L = [:the carrier of L,the carrier of L:]
by FUNCT_2:def 1; then
A1: dom LJ = [:C,C:] by RELAT_1:62,A0,ZFMISC_1:96;
rng LJ c= C
proof
let y be object;
assume y in rng LJ; then
consider x being object such that
B1: x in dom LJ & y = LJ.x by FUNCT_1:def 3;
consider x1, x2 being object such that
B2: x1 in C & x2 in C & x = [x1,x2] by ZFMISC_1:def 2,A1,B1;
reconsider xx1 = x1, xx2 = x2 as Nat by B2;
reconsider xx1, xx2 as NatPlus by B2,NAT_LAT:def 6;
y = lcmlatplus.(x1,x2) by NAT_LAT:def 10,B1,A1,B2,FUNCT_1:49; then
y = xx1 lcm xx2 by NAT_LAT:def 9;
hence thesis by LCMDiv,B2;
end; then
reconsider LJ as BinOp of C by FUNCT_2:2,A1;
dom the L_meet of L = [:the carrier of L,the carrier of L:]
by FUNCT_2:def 1; then
A1: dom LM = [:C,C:] by RELAT_1:62,A0,ZFMISC_1:96;
rng LM c= C
proof
let y be object;
assume y in rng LM; then
consider x being object such that
B1: x in dom LM & y = LM.x by FUNCT_1:def 3;
consider x1, x2 being object such that
B2: x1 in C & x2 in C & x = [x1,x2] by ZFMISC_1:def 2,A1,B1;
reconsider xx1 = x1, xx2 = x2 as Nat by B2;
reconsider xx1, xx2 as NatPlus by B2,NAT_LAT:def 6;
y = hcflatplus.(x1,x2) by NAT_LAT:def 10,B1,A1,B2,FUNCT_1:49; then
y = xx1 gcd xx2 by NAT_LAT:def 8;
hence thesis by GCDDiv,B2;
end; then
reconsider LM as BinOp of C by FUNCT_2:2,A1;
set DD = LattStr (# C, LJ, LM #);
reconsider DD as non empty LattStr;
SS: for a, b being Element of DD, aa, bb being Nat st
a = aa & b = bb holds LJ.(a,b) = aa lcm bb
proof
let a, b be Element of DD;
let aa, bb be Nat;
assume
Z1: a = aa & b = bb;
reconsider a1 = a, b1 = b as NatPlus by NAT_LAT:def 6;
thus LJ.(a,b) = lcmlatplus.(a,b) by NAT_LAT:def 10,ZFMISC_1:87,FUNCT_1:49
.= a1 lcm b1 by NAT_LAT:def 9
.= aa lcm bb by Z1;
end;
ss: for a, b being Element of DD, aa, bb being Nat st
a = aa & b = bb holds LM.(a,b) = aa gcd bb
proof
let a, b be Element of DD;
let aa, bb be Nat;
assume
Z1: a = aa & b = bb;
reconsider a1 = a, b1 = b as NatPlus by NAT_LAT:def 6;
thus LM.(a,b) = hcflatplus.(a,b) by NAT_LAT:def 10,ZFMISC_1:87,FUNCT_1:49
.= a1 gcd b1 by NAT_LAT:def 8
.= aa gcd bb by Z1;
end;
set LL = the L_join of L;
d3: LJ is commutative by CutComm,DivInPlus,NAT_LAT:def 10;
set ll = the L_meet of L;
d2: LM is commutative by CutComm,NAT_LAT:def 10,DivInPlus;
d4: LM is associative by CutAssoc,NAT_LAT:def 10,DivInPlus;
d5: LJ is associative by CutAssoc,NAT_LAT:def 10,DivInPlus;
for a,b being Element of DD holds a "/\" (a "\/" b) = a
proof
let a, b be Element of DD;
reconsider aa = a, bb = b as Nat;
[a,b] in [:C,C:] by ZFMISC_1:87; then
reconsider jj = LJ.(a,b) as Element of DD by FUNCT_2:5;
reconsider lj = jj as Nat;
thus a "/\" (a "\/" b) = aa gcd lj by ss
.= aa gcd (aa lcm bb) by SS
.= a by NEWTON:54;
end; then
D1: DD is join-absorbing;
for a,b being Element of DD holds (a "/\" b) "\/" b = b
proof
let a, b be Element of DD;
reconsider aa = a, bb = b as Nat;
[a,b] in [:C,C:] by ZFMISC_1:87; then
reconsider jj = LM.(a,b) as Element of DD by FUNCT_2:5;
reconsider lj = jj as Nat;
thus (a "/\" b) "\/" b = lj lcm bb by SS
.= (aa gcd bb) lcm bb by ss
.= b by NEWTON:53;
end; then
DD is meet-absorbing; then
DD is SubLattice of L
by DivInPlus,NAT_LAT:def 10,NAT_LAT:def 12,D1,d2,d3,d4,d5;
hence thesis;
end;
uniqueness
proof
let L1, L2 be strict SubLattice of NatPlus_Lattice such that
A1: the carrier of L1 = NatDivisors n and
A2: the carrier of L2 = NatDivisors n;
set L = NatPlus_Lattice;
A3: the L_meet of L1
= (the L_meet of L) || the carrier of L1 by NAT_LAT:def 12
.= the L_meet of L2 by NAT_LAT:def 12,A1,A2;
the L_join of L1
= (the L_join of L) || the carrier of L1 by NAT_LAT:def 12
.= the L_join of L2 by NAT_LAT:def 12,A1,A2;
hence thesis by A3,A1,A2;
end;
end;
registration let n be non zero Nat;
cluster the carrier of Divisors_Lattice n -> natural-membered;
coherence
proof
the carrier of Divisors_Lattice n = NatDivisors n by DivLat;
hence thesis;
end;
end;
theorem OperLat:
for n being non zero Nat,
a, b being Element of Divisors_Lattice n holds
a "\/" b = a lcm b &
a "/\" b = a gcd b
proof
let n be non zero Nat,
a, b be Element of Divisors_Lattice n;
set L = Divisors_Lattice n;
set K = NatPlus_Lattice;
A0: the carrier of L c= the carrier of K by NAT_LAT:def 12;
reconsider aa = a, bb = b as Element of K by A0;
the L_join of L = (the L_join of K) ||
the carrier of L by NAT_LAT:def 12;
hence a "\/" b = aa "\/" bb by FUNCT_1:49,ZFMISC_1:87
.= a lcm b;
the L_meet of L = (the L_meet of K) ||
the carrier of L by NAT_LAT:def 12;
hence a "/\" b = aa "/\" bb by FUNCT_1:49,ZFMISC_1:87
.= a gcd b;
end;
registration
let n be non zero Nat;
let p,q be Element of Divisors_Lattice n;
identify p "\/" q with p lcm q;
correctness by OperLat;
identify p "/\" q with p gcd q;
correctness by OperLat;
end;
registration let n be non zero Nat;
cluster Divisors_Lattice n -> non empty;
coherence;
end;
registration let n be non zero Nat;
cluster Divisors_Lattice n -> distributive bounded;
coherence
proof
set L = Divisors_Lattice n;
TT: ex c being Element of L st
for a being Element of L holds c"\/"a = c & a"\/"c = c
proof
n in NatDivisors n by MOEBIUS1:39; then
reconsider c = n as Element of L by DivLat;
take c;
let a be Element of L;
a in the carrier of L; then
a in NatDivisors n by DivLat;
hence thesis by NEWTON:44,MOEBIUS1:39;
end;
ex c being Element of L st
for a being Element of L holds c"/\"a = c & a"/\"c = c
proof
1 in NatDivisors n by MOEBIUS1:39,NAT_D:6; then
reconsider c = 1 as Element of L by DivLat;
take c;
thus thesis by NEWTON:51;
end; then
t1: L is lower-bounded upper-bounded by TT;
for a,b,c being Element of L holds
a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
proof
let a,b,c be Element of L;
a in the carrier of L; then
a1: a in NatDivisors n by DivLat;
b in the carrier of L; then
a2: b in NatDivisors n by DivLat;
c in the carrier of L; then
c in NatDivisors n by DivLat; then
reconsider n1 = a, n2 = b, n3 = c as non zero Nat by a1,a2;
(n3 gcd n1) lcm (n2 gcd n1) = (n3 lcm n2) gcd n1 by INT_4:46;
hence thesis;
end;
hence thesis by t1;
end;
end;
theorem TopBot:
for n being non zero Nat holds
Top Divisors_Lattice n = n &
Bottom Divisors_Lattice n = 1
proof
let n be non zero Nat;
set L = Divisors_Lattice n;
n in NatDivisors n by MOEBIUS1:39; then
reconsider TT = n as Element of L by DivLat;
a1: for a being Element of L holds TT "\/" a = TT & a "\/" TT = TT
proof
let a be Element of L;
a in the carrier of L; then
a in NatDivisors n by DivLat;
hence thesis by NEWTON:44,MOEBIUS1:39;
end;
1 in NatDivisors n by MOEBIUS1:39,NAT_D:6; then
reconsider TT = 1 as Element of L by DivLat;
for a being Element of L holds TT "/\" a = TT & a "/\" TT = TT
by NEWTON:51;
hence thesis by a1,LATTICES:def 16,def 17;
end;
SquareBool0:
for n being square-free non zero Nat holds
Divisors_Lattice n is Boolean
proof
let n be square-free non zero Nat;
set L = Divisors_Lattice n;
L is complemented
proof
for b being Element of L
ex a being Element of L st a is_a_complement_of b
proof
let b be Element of L;
b in the carrier of L; then
aa: b in NatDivisors n by DivLat; then
A1: n = b * (n div b) by NAT_D:3,MOEBIUS1:39;
set a = n div b;
n div b <> 0 by DivNonZero,aa,MOEBIUS1:39; then
a in NatDivisors n by MOEBIUS1:39,A1,NAT_D:def 3; then
reconsider a as Element of L by DivLat;
take a;
reconsider aa = a, bb = b as non zero Element of NAT
by DivNonZero,aa,MOEBIUS1:39;
S1: aa, bb are_coprime by aa,MOEBIUS1:39,DivRelPrime; then
a lcm b = n by A1,INT615;
hence thesis by S1,TopBot;
end;
hence thesis;
end;
hence thesis;
end;
registration let n be square-free non zero Nat;
cluster Divisors_Lattice n -> Boolean;
coherence by SquareBool0;
end;
registration let n be non zero Nat;
cluster -> non zero for Element of Divisors_Lattice n;
coherence
proof
let a be Element of Divisors_Lattice n;
a in the carrier of Divisors_Lattice n; then
a in NatDivisors n by DivLat;
hence thesis;
end;
end;
theorem
for n being non zero Nat holds
Divisors_Lattice n is Boolean iff n is square-free
proof
let n be non zero Nat;
set L = Divisors_Lattice n;
thus L is Boolean implies n is square-free
proof
assume
A0: L is Boolean;
assume n is square-containing; then
consider p being Prime such that
A1: p |^ 2 divides n by MOEBIUS1:def 1;
a1: p * p divides n by A1,NEWTON:81;
A2: p <> 1 by INT_2:def 4;
p divides p * p; then
p divides p |^ 2 by NEWTON:81; then
p in NatDivisors n by MOEBIUS1:39,A1,NAT_D:4; then
reconsider pp = p as Element of L by DivLat;
not ex a being Element of L st a is_a_complement_of pp
proof
given a being Element of L such that
C1: a is_a_complement_of pp;
C2: a lcm p = n & a gcd p = 1 by C1,TopBot;
a, p are_coprime by C1,TopBot; then
a lcm p = a * p by INT615; then
p divides a by C2,a1,INT_4:7; then
p divides a gcd p by NAT_D:def 5; then
C5: p <= a gcd p by NAT_D:7;
a gcd p <> 1
proof
assume a gcd p = 1; then
p < 1 + 1 by C5,NAT_1:13;
hence thesis by A2,NAT_1:23;
end;
hence thesis by C1,TopBot;
end;
hence thesis by A0,LATTICES:def 19;
end;
thus thesis;
end;