moebius2.miz



    begin

    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 :: MOEBIUS2:1

    for n,i be 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 :: MOEBIUS2:2

    for n be 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 :: MOEBIUS2:3

    

     FOT1: for n be 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 :: MOEBIUS2:4

    

     FOTN: for a,n be 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 :: MOEBIUS2:5

    

     RelPrimeEx: for a,b be non zero Nat st not (a,b) are_coprime holds ex k be 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 :: MOEBIUS2:6

    

     DivNonZero: for n,a be 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 :: MOEBIUS2:7

    

     INT615: for i,j be 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

    theorem :: MOEBIUS2:8

    ( primenumber 0 ) = 2

    proof

       0 = ( card ( SetPrimenumber 2));

      hence thesis by INT_2: 28, NEWTON:def 8;

    end;

    theorem :: MOEBIUS2:9

    

     LS2: ( SetPrimenumber 3) = {2}

    proof

      

       A1: {2} is Subset of NAT by ZFMISC_1: 31;

      for q be 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 :: MOEBIUS2:10

    ( primenumber 1) = 3

    proof

      1 = ( card ( SetPrimenumber 3)) by LS2, CARD_2: 42;

      hence thesis by PEPIN: 41, NEWTON:def 8;

    end;

    theorem :: MOEBIUS2:11

    

     LS3: ( SetPrimenumber 5) = {2, 3}

    proof

      

       A1: {2, 3} is Subset of NAT by ZFMISC_1: 32;

      for q be 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 :: MOEBIUS2:12

    ( 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 :: MOEBIUS2:13

    ( 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 be 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, PEPIN: 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 :: MOEBIUS2:14

    

     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 be 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, PEPIN: 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 :: MOEBIUS2:15

    ( primenumber 3) = 7

    proof

      3 = ( card ( SetPrimenumber 7)) by LS4, CARD_2: 58;

      hence thesis by NAT_4: 26, NEWTON:def 8;

    end;

    theorem :: MOEBIUS2:16

    

     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 be 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, PEPIN: 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 :: MOEBIUS2:17

    ( primenumber 4) = 11

    proof

      4 = ( card ( SetPrimenumber 11)) by CARD_2: 59, LS11;

      hence thesis by NAT_4: 27, NEWTON:def 8;

    end;

    theorem :: MOEBIUS2:18

    

     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 be 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, PEPIN: 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 :: MOEBIUS2:19

    ( 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 :: MOEBIUS2:20

    for m,n be 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 :: MOEBIUS2:21

    

     Cosik1: for n,m be Nat holds n < m iff ( primenumber n) < ( primenumber m)

    proof

      let n,m be Nat;

      

       AA: for n,m be 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

    reserve n,i for Nat;

    definition

      :: MOEBIUS2:def1

      func ReciPrime -> Real_Sequence means

      : ReciPr: for i be Nat holds (it . i) = (1 / ( primenumber i));

      correctness

      proof

        deffunc F( Nat) = (1 / ( primenumber $1));

        thus (ex seq be Real_Sequence st for n be Nat holds (seq . n) = F(n)) & (for seq1,seq2 be Real_Sequence st (for n be Nat holds (seq1 . n) = F(n)) & (for n be 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 be 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 be 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

      :: MOEBIUS2:def2

      func invNAT -> Real_Sequence means

      : DefRec: for i be Nat holds (it . i) = (1 / i);

      correctness

      proof

        deffunc F( Nat) = (1 / $1);

        thus (ex seq be Real_Sequence st for n be Nat holds (seq . n) = F(n)) & (for seq1,seq2 be Real_Sequence st (for n be Nat holds (seq1 . n) = F(n)) & (for n be 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 be 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 be Nat holds ( invNAT . n) = (1 / (n + 0 )) by DefRec;

        hence thesis by SEQ_4: 31;

      end;

    end

    theorem :: MOEBIUS2:22

    

     LimId: ( lim invNAT ) = 0

    proof

      for n be Nat holds ( invNAT . n) = (1 / (n + 0 )) by DefRec;

      hence thesis by SEQ_4: 31;

    end;

    theorem :: MOEBIUS2:23

    

     RecSub: ReciPrime is subsequence of invNAT

    proof

      deffunc F( Nat) = ( primenumber $1);

      consider f be Real_Sequence such that

       A1: for i be Nat holds (f . i) = F(i) from SEQ_1:sch 1;

      reconsider f as Function of NAT , REAL ;

      

       A3: for n be 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 be 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, SEQM_3: 1;

      take f;

       ReciPrime = ( invNAT * f)

      proof

        for x be 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 :: MOEBIUS2:24

    ( lim ReciPrime ) = 0 by LimId, RecSub, SEQ_4: 17;

    registration

      cluster ( Partial_Sums ReciPrime ) -> non-decreasing;

      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 :: MOEBIUS2:25

    for f be nonnegative-yielding Real_Sequence st f is summable holds for p be Real st p > 0 holds ex i be 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 be 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 be Nat such that

       D1: for m be 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 be 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;

      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

    definition

      let n be non zero Nat;

      :: MOEBIUS2:def3

      func SqFactors n -> ManySortedSet of SetPrimes means

      : SqDef: ( support it ) = ( support ( pfexp n)) & for p be 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 be 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 be 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 be object st x in SetPrimes holds ex y be 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 be Function such that

         A9: ( dom f) = SetPrimes and

         A10: for x be 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 be 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 be 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 be 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;

      :: MOEBIUS2:def4

      func SqF n -> Nat equals ( Product ( SqFactors n));

      coherence ;

    end

    theorem :: MOEBIUS2:26

    

     Matsu: for f be bag of SetPrimes holds ( Product f) <> 0

    proof

      let f be bag of SetPrimes ;

      consider g be 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;

      :: MOEBIUS2:def5

      func FreeGen p -> Subset of NAT means

      : FG: for n be Nat holds n in it iff n is square-free & for i be Prime st i divides n holds i <= p;

      existence

      proof

        defpred P[ set] means ex n be Nat st n = $1 & n is square-free & for i be Prime st i divides n holds i <= p;

        ex X be Subset of NAT st for x be Element of NAT holds x in X iff P[x] from SUBSET_1:sch 3;

        then

        consider X be Subset of NAT such that

         A1: for x be Element of NAT holds x in X iff P[x];

        take X;

        let n be Nat;

        hereby

          assume n in X;

          then

          consider m be Nat such that

           B1: m = n & m is square-free & for i be Prime st i divides m holds i <= p by A1;

          thus n is square-free & for i be Prime st i divides n holds i <= p by B1;

        end;

        assume

         b2: n is square-free & for i be 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 be Nat holds n in A1 iff n is square-free & for i be Prime st i divides n holds i <= p and

         A2: for n be Nat holds n in A2 iff n is square-free & for i be Prime st i divides n holds i <= p;

        for x be 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 be 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 :: MOEBIUS2:27

    

     Ex1: 1 in ( FreeGen p)

    proof

      for i be 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 :: MOEBIUS2:28

     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 :: MOEBIUS2:29

    

     Thds: for f be 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 :: MOEBIUS2:30

    

     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 :: MOEBIUS2:31

    for A be 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 :: MOEBIUS2:32

    

     ThCon: for g be positive-yielding bag of ( Seg p) st g = (p |-> p) holds g = (g * ( canFS ( support g)))

    proof

      let f be positive-yielding bag of ( Seg p);

      assume

       A0: f = (p |-> p);

      

       Y1: ( dom f) = ( Seg p) by A0;

      then

       yy: ( support f) = ( Seg p) by Thds;

      set g = (f * ( canFS ( Seg p)));

      

       R5: ( rng ( canFS ( Seg p))) = ( Seg p) by FUNCT_2:def 3;

      

       R3: ( dom ( canFS ( Seg p))) = ( Seg p) by domcanFS;

      

       R4: ( dom g) = ( dom ( canFS ( Seg p))) by RELAT_1: 27, R5, Y1

      .= ( Seg p) by domcanFS;

      then

       GG: ( dom g) = ( dom (p |-> p));

      for x be 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 :: MOEBIUS2:33

    for f be 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 be 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 :: MOEBIUS2:34

    

     Lm1: for n be 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 be 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 :: MOEBIUS2:35

    for n be 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 :: MOEBIUS2:36

    

     LmRng: for n be 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 be 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 :: MOEBIUS2:37

    

     WOW: for m,n be 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 be 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;

      :: MOEBIUS2:def6

      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;

      :: MOEBIUS2:def7

      func canHom p -> Function of ( FreeGen p), ( BoolePrime p) means

      : canH: for x be 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 be 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 be 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 be Function of ( FreeGen p), ( BoolePrime p) such that

         A1: for x be 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 be Element of ( FreeGen p) holds (f1 . x) = (( pfexp x) | (( Seg p) /\ SetPrimes )) and

         A2: for x be Element of ( FreeGen p) holds (f2 . x) = (( pfexp x) | (( Seg p) /\ SetPrimes ));

        for x be 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 be 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 be 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 be 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 :: MOEBIUS2:38

    

     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 :: MOEBIUS2:39

    ( card ( FreeGen p)) <= (2 |^ p)

    proof

      ( Segm ( card ( FreeGen p))) c= ( Segm (2 |^ p)) by LmX;

      hence thesis by NAT_1: 39;

    end;

    theorem :: MOEBIUS2:40

    

     Ciek: 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 :: MOEBIUS2:41

    

     MoInv: n <> 0 & (for p be Prime holds (p |-count n) <= 1) implies n is square-free

    proof

      assume

       A1: n <> 0 & for p be Prime holds (p |-count n) <= 1;

      assume n is square-containing;

      then

      consider p be 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 :: MOEBIUS2:42

    

     MB148: for p be Prime, n be 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 :: MOEBIUS2:43

    

     MB149: for n be non zero Nat, p be 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 :: MOEBIUS2:44

    

     MB150: for m,n be 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(*) . 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(*) . 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 be 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 be 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 be 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 be 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(*) . 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 be 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 be Nat such that

                 A19: a = ((p * (p |^ ka)) * la);

                a = (p * ((p |^ ka) * la)) by A19;

                then

                 A20: p divides a;

                consider kb be 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 be 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(*) . 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 :: MOEBIUS2:45

    for n be 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 be non zero Nat st ( support G(n)) c= ( Seg $1) holds F(n) divides n;

      let n be non zero Nat;

      

       A1: ex mS be 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 be 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 be Nat such that

           A14: n = (s * t);

          reconsider s, t as non zero Nat by A14;

          consider f be 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 be Nat such that

               A28: f = (1 + g) by NAT_1: 10;

              (p |^ f) divides t by A13, NAT_3:def 7;

              then

              consider u be Nat such that

               A29: t = ((p |^ f) * u);

              n = (s * (((p |^ g) * p) * u)) by A14, A28, A29, NEWTON: 6

              .= ((s * p) * ((p |^ g) * u))

              .= ((p |^ (e + 1)) * ((p |^ g) * u)) by NEWTON: 6;

              then (p |^ (e + 1)) divides n;

              hence contradiction by A13, NAT_3:def 7;

            end;

            ( support ( pfexp t)) c= ( support ( pfexp n)) by A14, NAT_3: 45;

            then ( support G(t)) c= ( support G(n)) by A6, SqDef;

            then m in ( support G(n)) by A24;

            then m <= (k + 1) by A5, FINSEQ_1: 1;

            then m < p by A26, XXREAL_0: 1;

            then

             A30: m <= k by NAT_1: 13;

            x is Prime by A25, NAT_3: 34;

            then 1 <= m by INT_2:def 4;

            hence thesis by A30, FINSEQ_1: 1;

          end;

          then

           A31: F(t) divides t by A4;

          ( support G(s)) = {p} by A18, A21, SqDef;

          

          then f = ( G(s) * <*p*>) by A16, FINSEQ_1: 94

          .= <*( G(s) . p)*> by FINSEQ_2: 34, A17, A8;

          

          then

           h1: ( Product G(s)) = ( G(s) . p) by A15

          .= (p |^ ((p |-count s) div 2)) by A22, SqDef;

          

           H2: (p |-count s) <= (p |-count n) by A12, NAT_3: 25, INT_2:def 4;

          (p |-count s) = 0 iff not p divides s by NAT_3: 27, A13;

          then ((p |-count s) div 2) <= (p |-count s) by INT_1: 56, 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 be 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 be 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 be 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 be Prime st x in ( support p) holds 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 :: MOEBIUS2:46

    

     Matsu0: for f be bag of SetPrimes holds ex g be FinSequence of NAT st ( Product f) = ( Product g) & g = (f * ( canFS ( support f)))

    proof

      let f be bag of SetPrimes ;

      consider g be 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 :: MOEBIUS2:47

    

     Matsu1: for f be 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 be 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 be 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 :: MOEBIUS2:48

    

     BZE: for f be 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

    definition

      let n be non zero Nat;

      :: MOEBIUS2:def8

      func TSqFactors n -> ManySortedSet of SetPrimes means

      : TSqDef: ( support it ) = ( support ( pfexp n)) & for p be 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 be 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 be 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 be object st x in SetPrimes holds ex y be 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 be Function such that

         A9: ( dom f) = SetPrimes and

         A10: for x be 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 be 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 be 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 :: MOEBIUS2:49

    for n be 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 be 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 be 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;

      :: MOEBIUS2:def9

      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 :: MOEBIUS2:50

    

     MB148T: for p be Prime, n be 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 :: MOEBIUS2:51

    

     MB149T: for n be non zero Nat, p be 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 :: MOEBIUS2:52

    

     MB150T: for m,n be 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(*) . 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(*) . 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 be 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 be 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 be 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 be 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(*) . 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 be 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 be Nat such that

                 A19: a = ((p * (p |^ ka)) * la);

                a = (p * ((p |^ ka) * la)) by A19;

                then

                 A20: p divides a;

                consider kb be 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 be 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(*) . 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 :: MOEBIUS2:53

    

     Skup: for n be 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 be non zero Nat st ( support G(n)) c= ( Seg $1) holds F(n) divides n;

      let n be non zero Nat;

      

       A1: ex mS be 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 be 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 be Nat such that

           A14: n = (s * t);

          reconsider s, t as non zero Nat by A14;

          consider f be 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 be Nat such that

               A28: f = (1 + g) by NAT_1: 10;

              (p |^ f) divides t by A13, NAT_3:def 7;

              then

              consider u be Nat such that

               A29: t = ((p |^ f) * u);

              reconsider g as Element of NAT by ORDINAL1:def 12;

              n = (s * (((p |^ g) * p) * u)) by A14, A28, A29, NEWTON: 6

              .= ((s * p) * ((p |^ g) * u))

              .= ((p |^ (e + 1)) * ((p |^ g) * u)) by NEWTON: 6;

              then (p |^ (e + 1)) divides n;

              hence contradiction by A13, NAT_3:def 7;

            end;

            ( support ( pfexp t)) c= ( support ( pfexp n)) by A14, NAT_3: 45;

            then ( support G(t)) c= ( support G(n)) by A6, TSqDef;

            then m in ( support G(n)) by A24;

            then m <= (k + 1) by A5, FINSEQ_1: 1;

            then m < p by A26, XXREAL_0: 1;

            then

             A30: m <= k by NAT_1: 13;

            x is Prime by A25, NAT_3: 34;

            then 1 <= m by INT_2:def 4;

            hence thesis by A30, FINSEQ_1: 1;

          end;

          then

           A31: F(t) divides t by A4;

          ( support G(s)) = {p} by A18, A21, TSqDef;

          

          then f = ( G(s) * <*p*>) by A16, FINSEQ_1: 94

          .= <*( G(s) . p)*> by FINSEQ_2: 34, A17, A8;

          

          then

           h1: ( Product G(s)) = ( G(s) . p) by A15

          .= (p |^ (2 * ((p |-count s) div 2))) by A22, TSqDef;

          

           H2: (p |-count s) <= (p |-count n) by A12, NAT_3: 25, INT_2:def 4;

          (p |-count s) = 0 iff not p divides s by NAT_3: 27, A13;

          then (2 * ((p |-count s) div 2)) <= (p |-count s) by FOTN, 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 be 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 be 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 be 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;

      coherence

      proof

        consider k be 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 be 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 :: MOEBIUS2:54

    

     SqCon1: for n,k be 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 :: MOEBIUS2:55

    

     DivRelPrime: for n be square-free non zero Nat, a be 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 be 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

    theorem :: MOEBIUS2:56

    

     CutComm: for A,C be non empty set, L be commutative BinOp of A, LC be 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 be 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 :: MOEBIUS2:57

    

     CutAssoc: for A,C be non empty set, L be associative BinOp of A, LC be 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 be 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

    theorem :: MOEBIUS2:58

    

     DivInPlus: for n be non zero Nat holds ( NatDivisors n) c= NATPLUS by NAT_LAT:def 6;

    theorem :: MOEBIUS2:59

    

     LCMDiv: for n be non zero Nat, x,y be 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 :: MOEBIUS2:60

    

     GCDDiv: for n be non zero Nat, x,y be 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 :: MOEBIUS2:61

    

     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 be 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 be 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 :: MOEBIUS2:62

    

     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 be 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 be 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

    ::$Notion-Name

    definition

      let n be non zero Nat;

      :: MOEBIUS2:def10

      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, NAT_LAT: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 be object such that

           B1: x in ( dom LJ) & y = (LJ . x) by FUNCT_1:def 3;

          consider x1,x2 be 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 be object such that

           B1: x in ( dom LM) & y = (LM . x) by FUNCT_1:def 3;

          consider x1,x2 be 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 be Element of DD, aa,bb be 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 be Element of DD, aa,bb be 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 be 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 be 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 :: MOEBIUS2:63

    

     OperLat: for n be non zero Nat, a,b be 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 lcm q with p "\/" q;

      correctness by OperLat;

      identify p gcd q with p "/\" 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 be Element of L st for a be 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 be Element of L st for a be 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 be 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 :: MOEBIUS2:64

    

     TopBot: for n be 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 be 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 be Element of L holds (TT "/\" a) = TT & (a "/\" TT) = TT by NEWTON: 51;

      hence thesis by a1, LATTICES:def 16, LATTICES:def 17;

    end;

    

     SquareBool0: for n be 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 be Element of L holds ex a be 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 :: MOEBIUS2:65

    for n be 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 be 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 be Element of L st a is_a_complement_of pp

        proof

          given a be 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;