:: On Square-free Numbers
::  by Adam Grabowski
::
:: Received July 12, 2013
:: Copyright (c) 2013-2016 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:28;
  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:29;
  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;