:: On Square-free Numbers :: by Adam Grabowski :: :: Received July 12, 2013 :: Copyright (c) 2013-2018 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, FINSEQ_2, INT_1, XREAL_0, NAT_1, MEMBERED, ORDINAL2, FINSEQ_1, FINSET_1, RVSUM_1, XXREAL_0, FUNCT_1, REALSET1, NAT_2, FUNCOP_1, NEWTON, SEQ_1, SEQM_3, XCMPLX_0, NUMBERS, MATRIX13, MOEBIUS1, SQUARE_1, ORDINAL1, PARTFUN3, FRAENKEL, CARD_1, STRUCT_0, PRE_POLY, NAT_3, UPROOTS, LATTICES, NAT_LAT, BINOP_1, CAYLDICK, LATTICE2, XBOOLE_0, VALUED_0, XXREAL_2, FUNCT_2, REAL_1, SUBSET_1, VALUED_1, SEQ_4; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions SERIES_1, FUNCOP_1, SEQM_3, CARD_1, ORDINAL1, RVSUM_1, FINSEQ_2, VALUED_0, TARSKI, PARTFUN3, XBOOLE_0, MOEBIUS1; equalities ORDINAL1, FUNCOP_1, 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 Nat 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,FUNCOP_1:13; 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) by FUNCOP_1:13; 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,MOEBIUS1:21; 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 Nat 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 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 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,RVSUM_1:95 .= 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,NAT_3:3,A20; 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 Nat 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 Nat 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 Nat 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 Nat 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 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 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,RVSUM_1:95 .= 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,NAT_3:3,A20; 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 NAT_D:18,Z2; then 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,NAT_D:3; 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;