moebius1.miz



    begin

    

     Lm1: for X,Y,Z,x be set st X misses Y holds x in (X /\ Z) implies not x in (Y /\ Z) by XBOOLE_1: 76, XBOOLE_0: 3;

    scheme :: MOEBIUS1:sch1

    LambdaNATC { A() -> Element of NAT , B() -> set , F( object) -> set } :

ex f be sequence of B() st (f . 0 ) = A() & for x be non zero Element of NAT holds (f . x) = F(x)

      provided

       A1: A() in B()

       and

       A2: for x be non zero Element of NAT holds F(x) in B();

      deffunc G( object) = A();

      defpred C[ object] means $1 = 0 ;

      

       A3: for x be object st x in NAT holds ( C[x] implies G(x) in B()) & ( not C[x] implies F(x) in B()) by A1, A2;

      ex f be sequence of B() st for x be object st x in NAT holds ( C[x] implies (f . x) = G(x)) & ( not C[x] implies (f . x) = F(x)) from FUNCT_2:sch 5( A3);

      then

      consider f be sequence of B() such that

       A4: for x be object st x in NAT holds ( C[x] implies (f . x) = G(x)) & ( not C[x] implies (f . x) = F(x));

      take f;

      thus (f . 0 ) = A() by A4;

      let x be non zero Element of NAT ;

      thus thesis by A4;

    end;

    registration

      cluster non prime non zero for Element of NAT ;

      existence by INT_2: 29;

    end

    theorem :: MOEBIUS1:1

    

     Th1: for n be non zero Nat holds n <> 1 implies n >= 2

    proof

      let n be non zero Nat;

      assume

       A1: n <> 1;

      assume n < 2;

      then n < (1 + 1);

      then n <= ( 0 + 1) by NAT_1: 13;

      hence contradiction by A1, NAT_1: 8;

    end;

    theorem :: MOEBIUS1:2

    for k,n,i be Nat st 1 <= k holds i in ( Seg n) iff (k * i) in ( Seg (k * n))

    proof

      let k,n,i be Nat;

      assume

       A1: 1 <= k;

      hereby

        assume

         A2: i in ( Seg n);

        then i <= n by FINSEQ_1: 1;

        then

         A3: (k * i) <= (k * n) by NAT_1: 4;

        1 <= i by A2, FINSEQ_1: 1;

        then (1 * 1) <= (k * i) by A1, XREAL_1: 66;

        hence (k * i) in ( Seg (k * n)) by A3, FINSEQ_1: 1;

      end;

      assume

       A4: (k * i) in ( Seg (k * n));

      then 0 < i by FINSEQ_1: 1;

      then

       A5: ( 0 + 1) <= i by NAT_1: 13;

      (k * i) <= (k * n) by A4, FINSEQ_1: 1;

      then i <= n by A1, XREAL_1: 68;

      hence thesis by A5, FINSEQ_1: 1;

    end;

    theorem :: MOEBIUS1:3

    for m,n be Element of NAT st (m,n) are_coprime holds m > 0 or n > 0

    proof

      let a,b be Element of NAT ;

      assume (a,b) are_coprime ;

      then a is odd or b is odd by PYTHTRIP: 10;

      hence thesis by ABIAN: 12;

    end;

    

     Lm2: for n be Nat st n <> 1 holds ex p be Prime st p divides n

    proof

      let n be Nat;

      assume

       A1: n <> 1;

      per cases ;

        suppose n is zero;

        hence thesis by INT_2: 28, NAT_D: 6;

      end;

        suppose n is non zero;

        then ex p be Element of NAT st p is prime & p divides n by A1, Th1, INT_2: 31;

        hence thesis;

      end;

    end;

    theorem :: MOEBIUS1:4

    

     Th4: for n be non prime Element of NAT st n <> 1 holds ex p be Prime st p divides n & p <> n

    proof

      let n be non prime Element of NAT ;

      assume n <> 1;

      then ex p be Prime st p divides n by Lm2;

      hence thesis;

    end;

    theorem :: MOEBIUS1:5

    

     Th5: for n be Nat st n <> 1 holds ex p be Prime st p divides n

    proof

      let n be Nat;

      

       A1: n in NAT by ORDINAL1:def 12;

      assume

       A2: n <> 1;

      per cases ;

        suppose n is Prime;

        hence thesis;

      end;

        suppose not n is Prime;

        then ex p be Prime st p divides n & p <> n by A1, A2, Th4;

        hence thesis;

      end;

    end;

    theorem :: MOEBIUS1:6

    

     Th6: for p be Prime, n be non zero Nat holds p divides n iff (p |-count n) > 0

    proof

      let p be Prime, n be non zero Nat;

      

       A1: p <> 1 by INT_2:def 4;

      thus p divides n implies (p |-count n) > 0

      proof

        assume

         A2: p divides n;

        (p |-count n) >= 1

        proof

          assume (p |-count n) < 1;

          then (p |-count n) = 0 by NAT_1: 25;

          then not (p |^ ( 0 + 1)) divides n by A1, NAT_3:def 7;

          hence contradiction by A2;

        end;

        hence thesis;

      end;

      assume (p |-count n) > 0 ;

      then

      reconsider d = (p |-count n) as non zero Nat;

      p <> 1 by INT_2:def 4;

      then (p |^ d) divides n by NAT_3:def 7;

      then (p |^ ( 0 + 1)) divides n by NAT_3: 4;

      hence thesis;

    end;

    theorem :: MOEBIUS1:7

    

     Th7: ( support ( ppf 1)) = {}

    proof

      ( support ( pfexp 1)) = {} ;

      hence thesis by NAT_3:def 9;

    end;

    theorem :: MOEBIUS1:8

    

     Th8: for p be Prime holds ( support ( ppf p)) = {p}

    proof

      let p be Prime;

      ( support ( pfexp p)) = {p} by NAT_3: 43;

      hence thesis by NAT_3:def 9;

    end;

    reserve m,n for Nat;

    theorem :: MOEBIUS1:9

    

     Th9: for p be Prime st n <> 0 & m <= (p |-count n) holds (p |^ m) divides n

    proof

      let p be Prime;

      assume that

       A1: n <> 0 and

       A2: m <= (p |-count n);

      

       A3: (p |^ m) divides (p |^ (p |-count n)) by A2, NEWTON: 89;

      p > 1 by INT_2:def 4;

      then (p |^ (p |-count n)) divides n by A1, NAT_3:def 7;

      hence thesis by A3, NAT_D: 4;

    end;

    theorem :: MOEBIUS1:10

    

     Th10: for a be Element of NAT , p be Prime holds (p |^ 2) divides a implies p divides a

    proof

      let a be Element of NAT ;

      let p be Prime;

      assume (p |^ 2) divides a;

      then

      consider t be Nat such that

       A1: a = ((p |^ 2) * t) by NAT_D:def 3;

      a = ((p * p) * t) by A1, WSIERP_1: 1

      .= (p * (p * t));

      hence thesis by NAT_D:def 3;

    end;

    theorem :: MOEBIUS1:11

    

     Th11: for p be prime Element of NAT , m,n be non zero Element of NAT st (m,n) are_coprime & (p |^ 2) divides (m * n) holds (p |^ 2) divides m or (p |^ 2) divides n

    proof

      let p be prime Element of NAT , a,b be non zero Element of NAT ;

      assume that

       A1: (a,b) are_coprime and

       A2: (p |^ 2) divides (a * b);

      p divides (p |^ 2) by NAT_3: 3;

      then

       A3: p divides (a * b) by A2, NAT_D: 4;

      per cases by A3, NEWTON: 80;

        suppose p divides a;

        then

         A4: not p divides b by A1, PYTHTRIP:def 2;

        (p,b) are_coprime

        proof

          reconsider k = (p gcd b) as Element of NAT by ORDINAL1:def 12;

          assume not (p,b) are_coprime ;

          then

           A5: k <> 1 by INT_2:def 3;

          k divides p & k divides b by NAT_D:def 5;

          hence contradiction by A4, A5, INT_2:def 4;

        end;

        then ((p * p),b) are_coprime by EULER_1: 14;

        then ((p |^ 2),b) are_coprime by WSIERP_1: 1;

        hence thesis by A2, EULER_1: 13;

      end;

        suppose p divides b;

        then

         A6: not p divides a by A1, PYTHTRIP:def 2;

        (p,a) are_coprime

        proof

          reconsider k = (p gcd a) as Element of NAT by ORDINAL1:def 12;

          assume not (p,a) are_coprime ;

          then

           A7: k <> 1 by INT_2:def 3;

          k divides p & k divides a by NAT_D:def 5;

          hence contradiction by A6, A7, INT_2:def 4;

        end;

        then ((p * p),a) are_coprime by EULER_1: 14;

        then ((p |^ 2),a) are_coprime by WSIERP_1: 1;

        hence thesis by A2, EULER_1: 13;

      end;

    end;

    theorem :: MOEBIUS1:12

    

     Th12: for N be Rbag of NAT st ( support N) = {n} holds ( Sum N) = (N . n)

    proof

      let N be Rbag of NAT ;

      reconsider Nn = (N . n) as Element of REAL by XREAL_0:def 1;

      reconsider F = <*Nn*> as FinSequence of REAL ;

      assume

       A1: ( support N) = {n};

       {n} c= ( dom N) by PRE_POLY: 37, A1;

      then n in ( dom N) by ZFMISC_1: 31;

      

      then

       A2: F = (N * <*n*>) by FINSEQ_2: 34

      .= (N * ( canFS ( support N))) by A1, FINSEQ_1: 94;

      ( Sum F) = (N . n) by FINSOP_1: 11;

      hence thesis by A2, UPROOTS:def 3;

    end;

    registration

      cluster ( canFS {} ) -> empty;

      coherence ;

    end

    theorem :: MOEBIUS1:13

    for p be Prime st p divides n holds { d where d be Element of NAT : d > 0 & d divides n & p divides d } = { (p * d) where d be Element of NAT : d > 0 & d divides (n div p) }

    proof

      let p be Prime;

      assume

       A1: p divides n;

      set B = { (p * d) where d be Element of NAT : d > 0 & d divides (n div p) };

      set A = { d where d be Element of NAT : d > 0 & d divides n & p divides d };

      thus A c= B

      proof

        let x be object;

        assume x in A;

        then

        consider d be Element of NAT such that

         A2: d = x and

         A3: d > 0 and

         A4: d divides n and

         A5: p divides d;

        consider d1 be Nat such that

         A6: d = (p * d1) by A5, NAT_D:def 3;

        consider d2 be Nat such that

         A7: n = (d * d2) by A4, NAT_D:def 3;

        n = (p * (d1 * d2)) by A6, A7;

        then p divides n by NAT_D:def 3;

        then (p * (n div p)) = (p * (d1 * d2)) by A6, A7, NAT_D: 3;

        then (n div p) = (d1 * d2) by XCMPLX_1: 5;

        then

         A8: d1 divides (n div p) by NAT_D:def 3;

        d1 in NAT & d1 > 0 by A3, A6, ORDINAL1:def 12;

        hence thesis by A2, A6, A8;

      end;

      let x be object;

      assume x in B;

      then

      consider d be Element of NAT such that

       A9: (p * d) = x and

       A10: d > 0 and

       A11: d divides (n div p);

      reconsider d1 = x as Element of NAT by A9, ORDINAL1:def 12;

      consider d2 be Nat such that

       A12: (n div p) = (d * d2) by A11, NAT_D:def 3;

      ((n div p) * p) = ((d * d2) * p) by A12;

      then n = (d2 * (d * p)) by A1, NAT_D: 3;

      then

       A13: d1 divides n by A9, NAT_D:def 3;

      p divides d1 by A9, NAT_D:def 3;

      hence thesis by A9, A10, A13;

    end;

    theorem :: MOEBIUS1:14

    

     Th14: for n be non zero Nat holds ex k be Element of NAT st ( support ( ppf n)) c= ( Seg k)

    proof

      let n be non zero Nat;

      

       A1: ( support ( ppf n)) = ( support ( pfexp n)) by NAT_3:def 9;

      per cases ;

        suppose

         A2: ( support ( ppf n)) is empty;

        take 0 ;

        thus thesis by A2;

      end;

        suppose ( support ( ppf n)) is non empty;

        then

        reconsider S = ( support ( ppf n)) as finite non empty Subset of NAT by XBOOLE_1: 1;

        take ( max S);

        

         A3: ( max S) is Element of NAT by ORDINAL1:def 12;

        ( support ( ppf n)) c= ( Seg ( max S))

        proof

          let x be object;

          assume

           A4: x in ( support ( ppf n));

          then

          reconsider m = x as Nat;

          x is Prime by A1, A4, NAT_3: 34;

          then

           A5: 1 <= m by INT_2:def 4;

          m <= ( max S) by A4, XXREAL_2:def 8;

          hence thesis by A5, FINSEQ_1: 1;

        end;

        hence thesis by A3;

      end;

    end;

    theorem :: MOEBIUS1:15

    

     Th15: for n be non zero Element of NAT , p be Prime st not p in ( support ( ppf n)) holds (p |-count n) = 0

    proof

      let n be non zero Element of NAT , p be Prime;

      assume

       A1: not p in ( support ( ppf n));

      assume (p |-count n) <> 0 ;

      then (( ppf n) . p) = (p |^ (p |-count n)) by NAT_3: 56;

      hence thesis by A1, PRE_POLY:def 7;

    end;

    theorem :: MOEBIUS1:16

    

     Th16: for k be Nat, n be non zero Element of NAT st ( support ( ppf n)) c= ( Seg (k + 1)) & not ( support ( ppf n)) c= ( Seg k) holds (k + 1) is Prime

    proof

      let k be Nat, n be non zero Element of NAT ;

      assume that

       A1: ( support ( ppf n)) c= ( Seg (k + 1)) and

       A2: not ( support ( ppf n)) c= ( Seg k);

      (k + 1) in ( support ( ppf n))

      proof

        assume not (k + 1) in ( support ( ppf n));

        then

         A3: {(k + 1)} misses ( support ( ppf n)) by ZFMISC_1: 50;

        (( support ( ppf n)) \ {(k + 1)}) c= (( Seg (k + 1)) \ {(k + 1)}) by A1, XBOOLE_1: 33;

        then ( support ( ppf n)) c= (( Seg (k + 1)) \ {(k + 1)}) by A3, XBOOLE_1: 83;

        hence thesis by A2, FINSEQ_1: 10;

      end;

      then (k + 1) in ( support ( pfexp n)) by NAT_3:def 9;

      hence thesis by NAT_3: 34;

    end;

    theorem :: MOEBIUS1:17

    

     Th17: for m,n be non zero Nat st (for p be Prime holds (p |-count m) <= (p |-count n)) holds ( support ( ppf m)) c= ( support ( ppf n))

    proof

      let m,n be non zero Nat;

      assume

       A1: for p be Prime holds (p |-count m) <= (p |-count n);

      let x be object;

      assume

       A2: x in ( support ( ppf m));

      then x in ( support ( pfexp m)) by NAT_3:def 9;

      then

      reconsider p = x as Prime by NAT_3: 34;

      (( ppf m) . p) <> 0 by A2, PRE_POLY:def 7;

      then (p |-count m) <> 0 by NAT_3: 55;

      then (p |-count n) > 0 by A1;

      then (( ppf n) . p) = (p |^ (p |-count n)) by NAT_3: 56;

      hence thesis by PRE_POLY:def 7;

    end;

    theorem :: MOEBIUS1:18

    

     Th18: for k be Nat, n be non zero Element of NAT st ( support ( ppf n)) c= ( Seg (k + 1)) holds ex m be non zero Element of NAT , e be Element of NAT st ( support ( ppf m)) c= ( Seg k) & n = (m * ((k + 1) |^ e)) & for p be Prime holds (p in ( support ( ppf m)) implies (p |-count m) = (p |-count n)) & ( not p in ( support ( ppf m)) implies (p |-count m) <= (p |-count n))

    proof

      let k be Nat, n be non zero Element of NAT ;

      assume

       A1: ( support ( ppf n)) c= ( Seg (k + 1));

      per cases ;

        suppose

         A2: ( support ( ppf n)) c= ( Seg k);

        take n;

        take e = 0 ;

        ((k + 1) |^ e) = 1 by NEWTON: 4;

        hence thesis by A2;

      end;

        suppose

         A3: not ( support ( ppf n)) c= ( Seg k);

        reconsider r = (k + 1) as non zero Element of NAT ;

        set e = (r |-count n);

        set s = (r |^ e);

        now

          assume

           A4: not (k + 1) in ( support ( ppf n));

          ( support ( ppf n)) c= ( Seg k)

          proof

            let x be object;

            assume

             A5: x in ( support ( ppf n));

            then

            reconsider m = x as Nat;

            x in ( support ( pfexp n)) by A5, NAT_3:def 9;

            then x is Prime by NAT_3: 34;

            then

             A6: 1 <= m by INT_2:def 4;

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

            then m < (k + 1) by A4, A5, XXREAL_0: 1;

            then m <= k by NAT_1: 13;

            hence thesis by A6, FINSEQ_1: 1;

          end;

          hence contradiction by A3;

        end;

        then (k + 1) in ( support ( pfexp n)) by NAT_3:def 9;

        then

         A7: r is Prime by NAT_3: 34;

        then

         A8: r > 1 by INT_2:def 4;

        then s divides n by NAT_3:def 7;

        then

        consider t be Nat such that

         A9: n = (s * t) by NAT_D:def 3;

        reconsider s, t as non zero Element of NAT by A9, ORDINAL1:def 12;

        

         A10: ( support ( ppf t)) = ( support ( pfexp t)) by NAT_3:def 9;

        

         A11: ( support ( ppf t)) c= ( Seg k)

        proof

          set f = (r |-count t);

          let x be object;

          assume

           A12: x in ( support ( ppf t));

          then

          reconsider m = x as Nat;

          

           A13: x in ( support ( pfexp t)) by A12, NAT_3:def 9;

           A14:

          now

            assume

             A15: m = r;

            (( pfexp t) . r) = f by A7, NAT_3:def 8;

            then f <> 0 by A13, A15, PRE_POLY:def 7;

            then f >= ( 0 + 1) by NAT_1: 13;

            then

            consider g be Nat such that

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

            (r |^ f) divides t by A8, NAT_3:def 7;

            then

            consider u be Nat such that

             A17: t = ((r |^ f) * u) by NAT_D:def 3;

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

            n = (s * (((r |^ g) * r) * u)) by A9, A16, A17, NEWTON: 6

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

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

            then (r |^ (e + 1)) divides n by NAT_D:def 3;

            hence contradiction by A8, NAT_3:def 7;

          end;

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

          then ( support ( ppf t)) c= ( support ( ppf n)) by A10, NAT_3:def 9;

          then m in ( support ( ppf n)) by A12;

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

          then m < r by A14, XXREAL_0: 1;

          then

           A18: m <= k by NAT_1: 13;

          x is Prime by A13, NAT_3: 34;

          then 1 <= m by INT_2:def 4;

          hence thesis by A18, FINSEQ_1: 1;

        end;

        

         A19: e <> 0

        proof

          assume e = 0 ;

          then n = (1 * t) by A9, NEWTON: 4;

          hence thesis by A3, A11;

        end;

        take m = t;

        take e = ((k + 1) |-count n);

        ( support ( ppf s)) = ( support ( pfexp s)) by NAT_3:def 9;

        then

         A20: ( support ( ppf s)) = {r} by A7, A19, NAT_3: 42;

         A21:

        now

          assume ( support ( ppf s)) meets ( support ( ppf t));

          then

          consider x be object such that

           A22: x in ( support ( ppf s)) and

           A23: x in ( support ( ppf t)) by XBOOLE_0: 3;

          x = r by A20, A22, TARSKI:def 1;

          then r <= k by A11, A23, FINSEQ_1: 1;

          hence contradiction by NAT_1: 13;

        end;

        for p be Prime holds (p in ( support ( ppf m)) implies (p |-count m) = (p |-count n)) & ( not p in ( support ( ppf m)) implies (p |-count m) <= (p |-count n))

        proof

          let p be Prime;

          hereby

            assume p in ( support ( ppf m));

            then not p in ( support ( ppf s)) by A21, XBOOLE_0: 3;

            then

             A24: (p |-count s) = 0 by Th15;

            (p |-count n) = ((p |-count (r |^ e)) + (p |-count t)) by A9, NAT_3: 28;

            hence (p |-count m) = (p |-count n) by A24;

          end;

          assume not p in ( support ( ppf m));

          hence thesis by Th15;

        end;

        hence thesis by A9, A11;

      end;

    end;

    theorem :: MOEBIUS1:19

    

     Th19: for m,n be non zero Nat st (for p be Prime holds (p |-count m) <= (p |-count n)) holds m divides n

    proof

      defpred P[ Nat] means for k,l be non zero Element of NAT st ( support ( ppf k)) c= ( Seg $1) & ( support ( ppf l)) c= ( Seg $1) & (for p be Prime holds (p |-count k) <= (p |-count l)) holds k divides l;

      let m,n be non zero Nat;

      

       A1: m is Element of NAT & n is Element of NAT by ORDINAL1:def 12;

      consider k be Element of NAT such that

       A2: ( support ( ppf n)) c= ( Seg k) by Th14;

      

       A3: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A4: P[k];

        let m,n be non zero Element of NAT ;

        assume that

         A5: ( support ( ppf m)) c= ( Seg (k + 1)) and

         A6: ( support ( ppf n)) c= ( Seg (k + 1)) and

         A7: for p be Prime holds (p |-count m) <= (p |-count n);

        per cases ;

          suppose

           A8: not ( support ( ppf n)) c= ( Seg k) & ( support ( ppf m)) c= ( Seg k);

          reconsider r = (k + 1) as non zero Element of NAT ;

          set e = (r |-count n);

          set s = (r |^ e);

          now

            assume

             A9: not (k + 1) in ( support ( ppf n));

            ( support ( ppf n)) c= ( Seg k)

            proof

              let x be object;

              assume

               A10: x in ( support ( ppf n));

              then

              reconsider m = x as Nat;

              x in ( support ( pfexp n)) by A10, NAT_3:def 9;

              then x is Prime by NAT_3: 34;

              then

               A11: 1 <= m by INT_2:def 4;

              m <= (k + 1) by A6, A10, FINSEQ_1: 1;

              then m < (k + 1) by A9, A10, XXREAL_0: 1;

              then m <= k by NAT_1: 13;

              hence thesis by A11, FINSEQ_1: 1;

            end;

            hence contradiction by A8;

          end;

          then

           A12: (k + 1) in ( support ( pfexp n)) by NAT_3:def 9;

          then

           A13: r is Prime by NAT_3: 34;

          then

           A14: r > 1 by INT_2:def 4;

          then s divides n by NAT_3:def 7;

          then

          consider t be Nat such that

           A15: n = (s * t) by NAT_D:def 3;

          

           A16: t divides n by A15, NAT_D:def 3;

          reconsider s, t as non zero Element of NAT by A15, ORDINAL1:def 12;

          

           A17: ( support ( ppf t)) = ( support ( pfexp t)) by NAT_3:def 9;

          

           A18: ( support ( ppf t)) c= ( Seg k)

          proof

            set f = (r |-count t);

            let x be object;

            assume

             A19: x in ( support ( ppf t));

            then

            reconsider m = x as Nat;

            

             A20: x in ( support ( pfexp t)) by A19, NAT_3:def 9;

             A21:

            now

              assume

               A22: m = r;

              (( pfexp t) . r) = f by A13, NAT_3:def 8;

              then f <> 0 by A20, A22, PRE_POLY:def 7;

              then f >= ( 0 + 1) by NAT_1: 13;

              then

              consider g be Nat such that

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

              (r |^ f) divides t by A14, NAT_3:def 7;

              then

              consider u be Nat such that

               A24: t = ((r |^ f) * u) by NAT_D:def 3;

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

              n = (s * (((r |^ g) * r) * u)) by A15, A23, A24, NEWTON: 6

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

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

              then (r |^ (e + 1)) divides n by NAT_D:def 3;

              hence contradiction by A14, NAT_3:def 7;

            end;

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

            then ( support ( ppf t)) c= ( support ( ppf n)) by A17, NAT_3:def 9;

            then m in ( support ( ppf n)) by A19;

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

            then m < r by A21, XXREAL_0: 1;

            then

             A25: m <= k by NAT_1: 13;

            x is Prime by A20, NAT_3: 34;

            then 1 <= m by INT_2:def 4;

            hence thesis by A25, FINSEQ_1: 1;

          end;

          

           A26: ( support ( ppf s)) = ( support ( pfexp s)) by NAT_3:def 9;

          e <> 0

          proof

            assume e = 0 ;

            then not r divides n by A14, NAT_3: 27;

            hence thesis by A12, NAT_3: 36;

          end;

          then

           A27: ( support ( ppf s)) = {r} by A13, A26, NAT_3: 42;

           A28:

          now

            assume ( support ( ppf s)) meets ( support ( ppf t));

            then

            consider x be object such that

             A29: x in ( support ( ppf s)) and

             A30: x in ( support ( ppf t)) by XBOOLE_0: 3;

            x = r by A27, A29, TARSKI:def 1;

            then r <= k by A18, A30, FINSEQ_1: 1;

            hence contradiction by NAT_1: 13;

          end;

          

           A31: ( support ( ppf m)) c= ( Seg k) & ( support ( ppf t)) c= ( Seg k) & (for p be Prime holds (p |-count m) <= (p |-count t)) implies m divides t by A4;

          ( support ( ppf n)) = ( support ( pfexp n)) & ( support ( ppf t)) = ( support ( pfexp t)) by NAT_3:def 9;

          then

           A32: ( support ( ppf n)) = (( support ( ppf s)) \/ ( support ( ppf t))) by A15, A26, NAT_3: 46;

          

           A33: for p be Prime holds (p |-count m) <= (p |-count t)

          proof

            let p be Prime;

            

             A34: (p |-count n) = ((p |-count (r |^ e)) + (p |-count t)) by A15, NAT_3: 28;

            per cases ;

              suppose

               A35: p in ( support ( ppf n));

              per cases by A32, A35, XBOOLE_0:def 3;

                suppose p in ( support ( ppf s));

                then

                 A36: p = (k + 1) by A27, TARSKI:def 1;

                per cases ;

                  suppose p in ( support ( ppf m));

                  then p <= k by A8, FINSEQ_1: 1;

                  hence thesis by A36, NAT_1: 13;

                end;

                  suppose not p in ( support ( ppf m));

                  hence thesis by Th15;

                end;

              end;

                suppose p in ( support ( ppf t));

                then not p in ( support ( ppf s)) by A28, XBOOLE_0: 3;

                then (p |-count s) = 0 by Th15;

                hence thesis by A7, A34;

              end;

            end;

              suppose not p in ( support ( ppf n));

              then (p |-count n) = 0 by Th15;

              hence thesis by A7;

            end;

          end;

          then ( support ( ppf m)) c= ( support ( ppf t)) by Th17;

          hence thesis by A16, A18, A33, A31, NAT_D: 4;

        end;

          suppose

           A37: not ( support ( ppf n)) c= ( Seg k) & not ( support ( ppf m)) c= ( Seg k);

          then

          reconsider w = (k + 1) as Prime by A5, Th16;

          consider m1 be non zero Element of NAT , e1 be Element of NAT such that

           A38: ( support ( ppf m1)) c= ( Seg k) and

           A39: m = (m1 * ((k + 1) |^ e1)) and

           A40: for p be Prime holds (p in ( support ( ppf m1)) implies (p |-count m1) = (p |-count m)) & ( not p in ( support ( ppf m1)) implies (p |-count m1) <= (p |-count m)) by A5, Th18;

          consider m2 be non zero Element of NAT , e2 be Element of NAT such that

           A41: ( support ( ppf m2)) c= ( Seg k) and

           A42: n = (m2 * ((k + 1) |^ e2)) and

           A43: for p be Prime holds (p in ( support ( ppf m2)) implies (p |-count m2) = (p |-count n)) & ( not p in ( support ( ppf m2)) implies (p |-count m2) <= (p |-count n)) by A6, Th18;

          

           A44: not w divides m2

          proof

            assume w divides m2;

            then w in ( support ( pfexp m2)) by NAT_3: 37;

            then w in ( support ( ppf m2)) by NAT_3:def 9;

            then w <= k by A41, FINSEQ_1: 1;

            hence thesis by NAT_1: 13;

          end;

          

           A45: (k + 1) is Prime by A5, A37, Th16;

          for p be Prime holds (p |-count m1) <= (p |-count m2)

          proof

            let p be Prime;

            per cases ;

              suppose p in ( support ( ppf m1)) & p in ( support ( ppf m2));

              then (p |-count m1) = (p |-count m) & (p |-count m2) = (p |-count n) by A40, A43;

              hence thesis by A7;

            end;

              suppose not p in ( support ( ppf m1)) & p in ( support ( ppf m2));

              hence thesis by Th15;

            end;

              suppose

               A46: p in ( support ( ppf m1)) & not p in ( support ( ppf m2));

              m1 divides m by A39, NAT_D:def 3;

              then

               A47: (p |-count m1) <= (p |-count m) by NAT_3: 30;

              

               A48: p > 1 by INT_2:def 4;

              p in ( support ( pfexp m1)) by A46, NAT_3:def 9;

              then p divides m1 by NAT_3: 36;

              then (p |-count m1) <> 0 by A48, NAT_3: 27;

              then (p |-count m1) > 0 ;

              then (p |-count n) > 0 by A7, A47;

              then

               A49: p divides n by A48, NAT_3: 27;

              (p |-count m2) = 0 by A46, Th15;

              then not p divides m2 by A48, NAT_3: 27;

              then p divides ((k + 1) |^ e2) by A42, A49, NEWTON: 80;

              then p divides (k + 1) by NAT_3: 5;

              then

               A50: p = (k + 1) by A45, A48, INT_2:def 4;

              k < (k + 1) by NAT_1: 13;

              hence thesis by A38, A46, A50, FINSEQ_1: 1;

            end;

              suppose not p in ( support ( ppf m1)) & not p in ( support ( ppf m2));

              hence thesis by Th15;

            end;

          end;

          then

           A51: m1 divides m2 by A4, A38, A41;

          

           A52: not w divides m1

          proof

            assume w divides m1;

            then w in ( support ( pfexp m1)) by NAT_3: 37;

            then w in ( support ( ppf m1)) by NAT_3:def 9;

            then w <= k by A38, FINSEQ_1: 1;

            hence thesis by NAT_1: 13;

          end;

          

           A53: w > 1 by INT_2:def 4;

          then (w |-count (w |^ e2)) = e2 by NAT_3: 25;

          

          then

           A54: (w |-count n) = ((w |-count m2) + e2) by A42, NAT_3: 28

          .= ( 0 + e2) by A53, A44, NAT_3: 27

          .= e2;

          (w |-count (w |^ e1)) = e1 by A53, NAT_3: 25;

          

          then (w |-count m) = ((w |-count m1) + e1) by A39, NAT_3: 28

          .= ( 0 + e1) by A53, A52, NAT_3: 27

          .= e1;

          then ((k + 1) |^ e1) divides ((k + 1) |^ e2) by A7, A54, NEWTON: 89;

          hence thesis by A39, A42, A51, NAT_3: 1;

        end;

          suppose

           A55: ( support ( ppf n)) c= ( Seg k);

          ( support ( ppf m)) c= ( support ( ppf n)) by A7, Th17;

          then ( support ( ppf m)) c= ( Seg k) by A55;

          hence thesis by A4, A7, A55;

        end;

      end;

      

       A56: P[ 0 ]

      proof

        let k,l be non zero Element of NAT ;

        assume that

         A57: ( support ( ppf k)) c= ( Seg 0 ) and ( support ( ppf l)) c= ( Seg 0 ) and for p be Prime holds (p |-count k) <= (p |-count l);

        ( support ( ppf k)) = {} by A57, XBOOLE_1: 3;

        then

         A58: ( support ( pfexp k)) = {} by NAT_3:def 9;

        per cases ;

          suppose k <> 1;

          then ex p be Prime st p divides k by Lm2;

          hence thesis by A58, NAT_3: 37;

        end;

          suppose k = 1;

          hence thesis by NAT_D: 6;

        end;

      end;

      

       A59: for k be Nat holds P[k] from NAT_1:sch 2( A56, A3);

      assume

       A60: for p be Prime holds (p |-count m) <= (p |-count n);

      then ( support ( ppf m)) c= ( support ( ppf n)) by Th17;

      then ( support ( ppf m)) c= ( Seg k) by A2;

      hence thesis by A60, A59, A2, A1;

    end;

    begin

    definition

      let x be Nat;

      :: MOEBIUS1:def1

      attr x is square-containing means ex p be Prime st (p |^ 2) divides x;

    end

    theorem :: MOEBIUS1:20

    

     Th20: for n be Nat st ex p be non zero Nat st p <> 1 & (p |^ 2) divides n holds n is square-containing

    proof

      let n be Nat;

      given p be non zero Nat such that

       A1: p <> 1 and

       A2: (p |^ 2) divides n;

      consider r be Prime such that

       A3: r divides p by A1, Lm2;

      (r |^ 2) divides (p |^ 2) by A3, WSIERP_1: 14;

      then (r |^ 2) divides n by A2, NAT_D: 4;

      hence thesis;

    end;

    notation

      let x be Nat;

      antonym x is square-free for x is square-containing;

    end

    theorem :: MOEBIUS1:21

    

     Th21: 0 is square-containing

    proof

      set p = the Prime;

      (p |^ 2) divides 0 by NAT_D: 6;

      hence thesis;

    end;

    theorem :: MOEBIUS1:22

    

     Th22: 1 is square-free

    proof

      assume 1 is square-containing;

      then

      consider n be Prime such that

       A1: (n |^ 2) divides 1;

      (n * n) divides 1 by A1, WSIERP_1: 1;

      then n = 1 or n = ( - 1) by WSIERP_1: 15, XCMPLX_1: 182;

      hence contradiction by INT_2:def 4;

    end;

    theorem :: MOEBIUS1:23

    

     Th23: for p be Prime holds p is square-free

    proof

      let p be Prime;

      assume p is square-containing;

      then

      consider n be Prime such that

       A1: (n |^ 2) divides p;

      

       A2: n divides (n |^ 2) by NAT_3: 3;

      then

       A3: n divides p by A1, NAT_D: 4;

      per cases by A3, INT_2:def 4;

        suppose n = 1;

        hence contradiction by INT_2:def 4;

      end;

        suppose n = p;

        then n = (n |^ 2) by A1, A2, NAT_D: 5;

        then (n |^ 1) = (n |^ 2);

        then n <= 1 by PEPIN: 30;

        hence contradiction by INT_2:def 4;

      end;

    end;

    registration

      cluster prime -> square-free for Element of NAT ;

      coherence by Th23;

    end

    definition

      :: MOEBIUS1:def2

      func SCNAT -> Subset of NAT means

      : Def2: for n be Nat holds n in it iff n is square-free;

      existence

      proof

        defpred P[ Nat] means $1 is square-free;

        consider X be Subset of NAT such that

         A1: for n be Element of NAT holds n in X iff P[n] from SUBSET_1:sch 3;

        take X;

        let n be Nat;

        thus n in X implies n is square-free by A1;

        assume

         A2: n is square-free;

        n is Element of NAT by INT_1: 3;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of NAT ;

        defpred P[ Nat] means $1 is square-free;

        assume that

         A3: for n be Nat holds n in X1 iff n is square-free and

         A4: for n be Nat holds n in X2 iff n is square-free;

        

         A5: for y be Element of NAT holds y in X2 iff P[y] by A4;

        

         A6: for y be Element of NAT holds y in X1 iff P[y] by A3;

        thus X1 = X2 from SUBSET_1:sch 2( A6, A5);

      end;

    end

    registration

      cluster square-free for Nat;

      existence by Th22;

      cluster square-containing for Nat;

      existence

      proof

        take 4;

        (2 |^ 2) = (2 * 2) by NEWTON: 81

        .= 4;

        hence thesis by INT_2: 28;

      end;

    end

    registration

      cluster square non trivial -> square-containing for Nat;

      coherence

      proof

        let n be Nat;

        assume

         A1: n is square non trivial;

        then

        consider m be Nat such that

         A2: n = (m ^2 ) by PYTHTRIP:def 3;

        

         A3: (m |^ 2) divides n by A2, WSIERP_1: 1;

        m <> (1 ^2 ) & m <> ( 0 ^2 ) by A1, A2, NAT_2: 28;

        hence thesis by A3, Th20;

      end;

    end

    theorem :: MOEBIUS1:24

    

     Th24: n is square-free implies for p be Prime holds (p |-count n) <= 1

    proof

      assume

       A1: n is square-free;

      given p be Prime such that

       A2: (p |-count n) > 1;

      (p |-count n) >= (1 + 1) by A2, NAT_1: 13;

      then (p |^ 2) divides n by A1, Th9, Th21;

      hence thesis by A1;

    end;

    theorem :: MOEBIUS1:25

    

     Th25: (m * n) is square-free implies m is square-free by NAT_D: 9;

    theorem :: MOEBIUS1:26

    

     Th26: m is square-free & n divides m implies n is square-free

    proof

      assume that

       A1: m is square-free and

       A2: n divides m;

      ex x be Nat st m = (n * x) by A2, NAT_D:def 3;

      hence thesis by A1, Th25;

    end;

    theorem :: MOEBIUS1:27

    

     Th27: for p be Prime, m,d be Nat st m is square-free & p divides m & d divides (m div p) holds d divides m & not p divides d

    proof

      let p be Prime, m,d be Nat;

      assume that

       A1: m is square-free and

       A2: p divides m;

      assume d divides (m div p);

      then

      consider z be Nat such that

       A3: (m div p) = (d * z) by NAT_D:def 3;

      

       A4: ((m div p) * p) = ((d * z) * p) by A3;

      then m = (d * (z * p)) by A2, NAT_D: 3;

      hence d divides m by NAT_D:def 3;

      assume p divides d;

      then

      consider w be Nat such that

       A5: d = (p * w) by NAT_D:def 3;

      m = ((w * (p * p)) * z) by A2, A4, A5, NAT_D: 3

      .= ((w * (p |^ 2)) * z) by WSIERP_1: 1

      .= ((p |^ 2) * (w * z));

      then (p |^ 2) divides m by NAT_D:def 3;

      hence thesis by A1;

    end;

    theorem :: MOEBIUS1:28

    

     Th28: for p be Prime, m,d be Nat st p divides m & d divides m & not p divides d holds d divides (m div p)

    proof

      let p be Prime, m,d be Nat;

      assume that

       A1: p divides m and

       A2: d divides m and

       A3: not p divides d;

      consider z be Nat such that

       A4: m = (d * z) by A2, NAT_D:def 3;

      p divides z by A1, A3, A4, NEWTON: 80;

      then

      consider u be Nat such that

       A5: z = (p * u) by NAT_D:def 3;

      m = ((d * u) * p) by A4, A5;

      then (m div p) = (d * u) by NAT_D: 18;

      hence thesis by NAT_D:def 3;

    end;

    theorem :: MOEBIUS1:29

    for p be Prime, m be Nat st m is square-free & p divides m holds { d where d be Element of NAT : 0 < d & d divides m & not p divides d } = { d where d be Element of NAT : 0 < d & d divides (m div p) }

    proof

      let p be Prime, m be Nat;

      assume that

       A1: m is square-free and

       A2: p divides m;

      set B = { d where d be Element of NAT : 0 < d & d divides (m div p) };

      set A = { d where d be Element of NAT : 0 < d & d divides m & not p divides d };

      thus A c= B

      proof

        let x be object;

        assume x in A;

        then

        consider d be Element of NAT such that

         A3: d = x & 0 < d and

         A4: d divides m & not p divides d;

        d divides (m div p) by A2, A4, Th28;

        hence thesis by A3;

      end;

      let x be object;

      assume x in B;

      then

      consider d be Element of NAT such that

       A5: d = x & 0 < d and

       A6: d divides (m div p);

      d divides m & not p divides d by A1, A2, A6, Th27;

      hence thesis by A5;

    end;

    begin

    definition

      let n be Nat;

      ::$Notion-Name

      :: MOEBIUS1:def3

      func Moebius n -> Real means

      : Def3: it = 0 if n is square-containing

      otherwise ex n9 be non zero Nat st n9 = n & it = (( - 1) |^ ( card ( support ( ppf n9))));

      consistency ;

      existence

      proof

        thus n is square-containing implies ex r be Real st r = 0 ;

        n is square-free implies ex n9 be non zero Nat st n9 = n & ex r be Real st r = (( - 1) |^ ( card ( support ( ppf n9))))

        proof

          assume

           A1: n is square-free;

          n is non zero Nat

          proof

            set p = the Prime;

            assume not n is non zero Nat;

            then (p |^ 2) divides n by NAT_D: 6;

            hence contradiction by A1;

          end;

          then

          reconsider n9 = n as non zero Nat;

          ex r be Real st r = (( - 1) |^ ( card ( support ( ppf n9))));

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness ;

    end

    theorem :: MOEBIUS1:30

    

     Th30: ( Moebius 1) = 1

    proof

      ( Moebius 1) = (( - 1) |^ ( card {} )) by Def3, Th7, Th22

      .= 1 by NEWTON: 4;

      hence thesis;

    end;

    theorem :: MOEBIUS1:31

    ( Moebius 2) = ( - 1)

    proof

      ( Moebius 2) = (( - 1) |^ ( card ( support ( ppf 2)))) by Def3, INT_2: 28

      .= (( - 1) |^ ( card {2})) by Th8, INT_2: 28

      .= (( - 1) |^ 1) by CARD_1: 30;

      hence thesis;

    end;

    theorem :: MOEBIUS1:32

    ( Moebius 3) = ( - 1)

    proof

      ( Moebius 3) = (( - 1) |^ ( card ( support ( ppf 3)))) by Def3, PEPIN: 41

      .= (( - 1) |^ ( card {3})) by Th8, PEPIN: 41

      .= (( - 1) |^ 1) by CARD_1: 30;

      hence thesis;

    end;

    theorem :: MOEBIUS1:33

    

     Th33: for n be Nat st n is square-free holds ( Moebius n) <> 0

    proof

      let n be Nat;

      assume n is square-free;

      then

      consider n9 be non zero Nat such that

       A1: n9 = n & ( Moebius n) = (( - 1) |^ ( card ( support ( ppf n9)))) by Def3;

      ( Moebius n) = (( - 1) |^ ( card ( support ( ppf n9)))) by A1;

      hence thesis by CARD_4: 3;

    end;

    registration

      let n be square-free Nat;

      cluster ( Moebius n) -> non zero;

      coherence by Th33;

    end

    theorem :: MOEBIUS1:34

    

     Th34: for p be Prime holds ( Moebius p) = ( - 1)

    proof

      let p be Prime;

      reconsider p1 = p as prime Element of NAT by ORDINAL1:def 12;

      ( Moebius p) = (( - 1) |^ ( card ( support ( ppf p1)))) by Def3

      .= (( - 1) |^ ( card {p})) by Th8

      .= (( - 1) |^ 1) by CARD_1: 30;

      hence thesis;

    end;

    theorem :: MOEBIUS1:35

    

     Th35: for m,n be non zero Element of NAT st (m,n) are_coprime holds ( Moebius (m * n)) = (( Moebius m) * ( Moebius n))

    proof

      let a,b be non zero Element of NAT ;

      assume

       A1: (a,b) are_coprime ;

      per cases ;

        suppose

         A2: a is square-free & b is square-free;

        

         A3: (a * b) is square-free

        proof

          assume (a * b) is square-containing;

          then

          consider p be Prime such that

           A4: (p |^ 2) divides (a * b);

          p in NAT by ORDINAL1:def 12;

          then (p |^ 2) divides a or (p |^ 2) divides b by A1, A4, Th11;

          hence contradiction by A2;

        end;

        

         A5: ( Moebius a) = (( - 1) |^ ( card ( support ( ppf a)))) by A2, Def3;

        ( card ( support ( pfexp (a * b)))) = (( card ( support ( pfexp a))) + ( card ( support ( pfexp b)))) by A1, NAT_3: 47;

        

        then ( card ( support ( ppf (a * b)))) = (( card ( support ( pfexp a))) + ( card ( support ( pfexp b)))) by NAT_3:def 9

        .= (( card ( support ( pfexp a))) + ( card ( support ( ppf b)))) by NAT_3:def 9

        .= (( card ( support ( ppf a))) + ( card ( support ( ppf b)))) by NAT_3:def 9;

        

        then ( Moebius (a * b)) = (( - 1) |^ (( card ( support ( ppf a))) + ( card ( support ( ppf b))))) by A3, Def3

        .= ((( - 1) |^ ( card ( support ( ppf a)))) * (( - 1) |^ ( card ( support ( ppf b))))) by NEWTON: 8;

        hence thesis by A2, A5, Def3;

      end;

        suppose

         A6: a is square-free & b is square-containing;

        then

        consider p be Prime such that

         A7: (p |^ 2) divides b;

        (p |^ 2) divides (a * b) by A7, NAT_D: 9;

        then

         A8: (a * b) is square-containing;

        ( Moebius b) = 0 by A6, Def3;

        hence thesis by A8, Def3;

      end;

        suppose

         A9: a is square-containing & b is square-free;

        then

        consider p be Prime such that

         A10: (p |^ 2) divides a;

        (p |^ 2) divides (a * b) by A10, NAT_D: 9;

        then

         A11: (a * b) is square-containing;

        ( Moebius a) = 0 by A9, Def3;

        hence thesis by A11, Def3;

      end;

        suppose

         A12: a is square-containing & b is square-containing;

        then

        consider p be Prime such that

         A13: (p |^ 2) divides a;

        (p |^ 2) divides (a * b) by A13, NAT_D: 9;

        then

         A14: (a * b) is square-containing;

        ( Moebius a) = 0 by A12, Def3;

        hence thesis by A14, Def3;

      end;

    end;

    theorem :: MOEBIUS1:36

    for p be Prime, n be Element of NAT st 1 <= n & (n * p) is square-free holds ( Moebius (n * p)) = ( - ( Moebius n))

    proof

      let p be Prime, a be Element of NAT ;

      assume that

       A1: 1 <= a and

       A2: (a * p) is square-free;

      

       A3: p in NAT by ORDINAL1:def 12;

      (a,p) are_coprime

      proof

        assume not (a,p) are_coprime ;

        then

        consider q be prime Nat such that

         A4: q divides a and

         A5: q divides p by PYTHTRIP:def 2;

        q = 1 or q = p by A5, INT_2:def 4;

        then (p * p) divides (a * p) by A3, A4, INT_2:def 4, PYTHTRIP: 7;

        then (p |^ 2) divides (a * p) by WSIERP_1: 1;

        hence thesis by A2;

      end;

      

      then ( Moebius (a * p)) = (( Moebius a) * ( Moebius p)) by A1, A3, Th35

      .= (( Moebius a) * ( - 1)) by Th34;

      hence thesis;

    end;

    theorem :: MOEBIUS1:37

    for m,n be non zero Element of NAT st not (m,n) are_coprime holds ( Moebius (m * n)) = 0

    proof

      let m,n be non zero Element of NAT ;

      assume not (m,n) are_coprime ;

      then

      consider p be prime Nat such that

       A1: p divides m & p divides n by PYTHTRIP:def 2;

      reconsider p as prime Element of NAT by ORDINAL1:def 12;

      (p * p) divides (m * n) by A1, NAT_3: 1;

      then (p |^ 2) divides (m * n) by WSIERP_1: 1;

      then (m * n) is square-containing;

      hence thesis by Def3;

    end;

    theorem :: MOEBIUS1:38

    

     Th38: for n be Nat holds n in SCNAT iff ( Moebius n) <> 0

    proof

      let n be Nat;

      hereby

        assume n in SCNAT ;

        then n is square-free by Def2;

        hence ( Moebius n) <> 0 ;

      end;

      assume ( Moebius n) <> 0 ;

      then n is square-free by Def3;

      hence thesis by Def2;

    end;

    begin

    definition

      let n be Nat;

      :: MOEBIUS1:def4

      func NatDivisors n -> Subset of NAT equals { k where k be Element of NAT : k <> 0 & k divides n };

      coherence

      proof

        { k where k be Element of NAT : k <> 0 & k divides n } c= NAT

        proof

          let x be object;

          assume x in { k where k be Element of NAT : k <> 0 & k divides n };

          then ex k be Element of NAT st k = x & k <> 0 & k divides n;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: MOEBIUS1:39

    for n,k be Nat holds k in ( NatDivisors n) iff 0 < k & k divides n

    proof

      let n,k be Nat;

      hereby

        assume k in ( NatDivisors n);

        then ex l be Element of NAT st l = k & l <> 0 & l divides n;

        hence 0 < k & k divides n;

      end;

      assume

       A1: 0 < k & k divides n;

      k is Element of NAT by ORDINAL1:def 12;

      hence thesis by A1;

    end;

    theorem :: MOEBIUS1:40

    

     Th40: for n be non zero Nat holds ( NatDivisors n) c= ( Seg n)

    proof

      let n be non zero Nat;

      let x be object;

      assume x in ( NatDivisors n);

      then

      consider k be Element of NAT such that

       A1: x = k and

       A2: k <> 0 & k divides n;

      1 <= k & k <= n by A2, NAT_1: 14, NAT_D: 7;

      hence thesis by A1, FINSEQ_1: 1;

    end;

    registration

      let n be non zero Nat;

      cluster ( NatDivisors n) -> finite with_non-empty_elements;

      coherence

      proof

        set P = ( NatDivisors n);

        

         A1: not 0 in P

        proof

          assume 0 in P;

          then ex k be Element of NAT st k = 0 & k <> 0 & k divides n;

          hence contradiction;

        end;

        P c= ( Seg n) by Th40;

        hence thesis by A1, MEASURE6:def 2;

      end;

    end

    theorem :: MOEBIUS1:41

    

     Th41: ( NatDivisors 1) = {1}

    proof

      thus ( NatDivisors 1) c= {1}

      proof

        let x be object;

        assume x in ( NatDivisors 1);

        then

        consider k be Element of NAT such that

         A1: x = k and k <> 0 and

         A2: k divides 1;

        k = 1 by A2, WSIERP_1: 15;

        hence thesis by A1, ZFMISC_1: 31;

      end;

      let x be object;

      assume

       A3: x in {1};

      then

      reconsider m = x as Element of NAT ;

      m <> 0 & m divides 1 by A3, TARSKI:def 1;

      hence thesis;

    end;

    begin

    definition

      let X be set;

      :: MOEBIUS1:def5

      func SMoebius X -> ManySortedSet of NAT means

      : Def5: ( support it ) = (X /\ SCNAT ) & for k be Element of NAT st k in ( support it ) holds (it . k) = ( Moebius k);

      existence

      proof

        defpred R[ object] means $1 in (X /\ SCNAT );

        deffunc G( Element of NAT ) = 0 ;

        deffunc F( Element of NAT ) = ( Moebius $1);

        ex f be ManySortedSet of NAT st for i be Element of NAT st i in NAT holds ( R[i] implies (f . i) = F(i)) & ( not R[i] implies (f . i) = G(i)) from PRE_CIRC:sch 2;

        then

        consider f be ManySortedSet of NAT such that

         A1: for i be Element of NAT st i in NAT holds ( R[i] implies (f . i) = F(i)) & ( not R[i] implies (f . i) = G(i));

        

         A2: ( support f) c= SCNAT

        proof

          ( dom f) = NAT by PARTFUN1:def 2;

          then

           A3: ( support f) c= NAT by PRE_POLY: 37;

          let x be object;

          assume

           A4: x in ( support f);

          then

           A5: (f . x) <> 0 by PRE_POLY:def 7;

          per cases ;

            suppose R[x];

            hence thesis by XBOOLE_0:def 4;

          end;

            suppose not R[x];

            hence thesis by A1, A4, A5, A3;

          end;

        end;

        

         A6: ( support f) = (X /\ SCNAT )

        proof

          thus ( support f) c= (X /\ SCNAT )

          proof

            let x be object;

            assume

             A7: x in ( support f);

            then x in SCNAT by A2;

            then

            reconsider i = x as Element of NAT ;

            assume not x in (X /\ SCNAT );

            then (f . i) = 0 by A1;

            hence contradiction by A7, PRE_POLY:def 7;

          end;

          let x be object;

          assume

           A8: x in (X /\ SCNAT );

          then

          reconsider i = x as Element of NAT ;

          x in SCNAT by A8, XBOOLE_0:def 4;

          then

           A9: ( Moebius i) <> 0 by Th38;

          (f . i) = ( Moebius i) by A1, A8;

          hence thesis by A9, PRE_POLY:def 7;

        end;

        reconsider f as ManySortedSet of NAT ;

        take f;

        thus ( support f) = (X /\ SCNAT ) by A6;

        let k be Element of NAT ;

        assume k in ( support f);

        hence thesis by A1, A6;

      end;

      uniqueness

      proof

        let f,g be ManySortedSet of NAT such that

         A10: ( support f) = (X /\ SCNAT ) and

         A11: for k be Element of NAT st k in ( support f) holds (f . k) = ( Moebius k) and

         A12: ( support g) = (X /\ SCNAT ) and

         A13: for k be Element of NAT st k in ( support g) holds (g . k) = ( Moebius k);

        for i be object st i in NAT holds (f . i) = (g . i)

        proof

          let i be object;

          assume i in NAT ;

          then

          reconsider j = i as Element of NAT ;

          per cases ;

            suppose

             A14: j in ( support f);

            

            hence (f . i) = ( Moebius j) by A11

            .= (g . i) by A10, A12, A13, A14;

          end;

            suppose

             A15: not j in ( support f);

            

            hence (f . i) = 0 by PRE_POLY:def 7

            .= (g . i) by A10, A12, A15, PRE_POLY:def 7;

          end;

        end;

        hence thesis by PBOOLE: 3;

      end;

    end

    registration

      let X be set;

      cluster ( SMoebius X) -> real-valued;

      coherence

      proof

        ( rng ( SMoebius X)) c= REAL

        proof

          let y be object;

          assume y in ( rng ( SMoebius X));

          then

          consider i be object such that

           A1: i in ( dom ( SMoebius X)) and

           A2: (( SMoebius X) . i) = y by FUNCT_1:def 3;

          ( dom ( SMoebius X)) = NAT by PARTFUN1:def 2;

          then

          reconsider i as Nat by A1;

          per cases ;

            suppose

             A3: i in ( support ( SMoebius X));

            then i in (X /\ SCNAT ) by Def5;

            then y = ( Moebius i) by A2, A3, Def5;

            hence thesis by XREAL_0:def 1;

          end;

            suppose not i in ( support ( SMoebius X));

            then (( SMoebius X) . i) = ( In ( 0 , REAL )) by PRE_POLY:def 7;

            hence thesis by A2;

          end;

        end;

        hence thesis by VALUED_0:def 3;

      end;

    end

    registration

      let X be finite set;

      cluster ( SMoebius X) -> finite-support;

      coherence

      proof

        ( support ( SMoebius X)) = (X /\ SCNAT ) by Def5;

        hence thesis by PRE_POLY:def 8;

      end;

    end

    theorem :: MOEBIUS1:42

    ( Sum ( SMoebius ( NatDivisors 1))) = 1

    proof

      reconsider J = 1 as Element of NAT ;

      reconsider M = (( {1},1) -bag ) as Rbag of NAT ;

      

       A1: 1 in {1} by TARSKI:def 1;

      

       A2: 1 in SCNAT by Def2, Th22;

      J in {1} by TARSKI:def 1;

      then J in ( {1} /\ SCNAT ) by A2, XBOOLE_0:def 4;

      then J in ( support ( SMoebius {1})) by Def5;

      then

       A3: (( SMoebius {1}) . 1) = 1 by Def5, Th30;

       {1} c= SCNAT by A2, ZFMISC_1: 31;

      then

       A4: ( {1} /\ SCNAT ) = {1} by XBOOLE_1: 28;

      for x be object st x in NAT holds (( SMoebius {1}) . x) = (M . x)

      proof

        let x be object;

        per cases ;

          suppose

           A5: x in {1};

          then x = 1 by TARSKI:def 1;

          hence thesis by A3, A5, UPROOTS: 7;

        end;

          suppose

           A6: not x in {1};

          then

           A7: not x in ( support ( SMoebius {1})) by A4, Def5;

          (M . x) = 0 by A6, UPROOTS: 6

          .= (( SMoebius {1}) . x) by A7, PRE_POLY:def 7;

          hence thesis;

        end;

      end;

      then ( support M) = {1} & ( SMoebius {1}) = M by PBOOLE: 3, UPROOTS: 8;

      

      then ( Sum ( SMoebius ( NatDivisors 1))) = (M . 1) by Th12, Th41

      .= 1 by A1, UPROOTS: 7;

      hence thesis;

    end;

    theorem :: MOEBIUS1:43

    for X,Y be finite Subset of NAT st X misses Y holds (( support ( SMoebius X)) \/ ( support ( SMoebius Y))) = ( support (( SMoebius X) + ( SMoebius Y)))

    proof

      let X,Y be finite Subset of NAT ;

      assume

       A1: X misses Y;

      thus (( support ( SMoebius X)) \/ ( support ( SMoebius Y))) c= ( support (( SMoebius X) + ( SMoebius Y)))

      proof

        let x be object;

        ( support ( SMoebius X)) = (X /\ SCNAT ) & ( support ( SMoebius Y)) = (Y /\ SCNAT ) by Def5;

        then

         A2: ( support ( SMoebius X)) misses ( support ( SMoebius Y)) by A1, XBOOLE_1: 76;

        assume

         A3: x in (( support ( SMoebius X)) \/ ( support ( SMoebius Y)));

        per cases by A3, XBOOLE_0:def 3;

          suppose

           A4: x in ( support ( SMoebius X));

          then not x in ( support ( SMoebius Y)) by A2, XBOOLE_0: 3;

          then (( SMoebius Y) . x) = 0 by PRE_POLY:def 7;

          then ((( SMoebius X) . x) + (( SMoebius Y) . x)) <> 0 by A4, PRE_POLY:def 7;

          then ((( SMoebius X) + ( SMoebius Y)) . x) <> 0 by PRE_POLY:def 5;

          hence thesis by PRE_POLY:def 7;

        end;

          suppose

           A5: x in ( support ( SMoebius Y));

          then not x in ( support ( SMoebius X)) by A2, XBOOLE_0: 3;

          then (( SMoebius X) . x) = 0 by PRE_POLY:def 7;

          then ((( SMoebius X) . x) + (( SMoebius Y) . x)) <> 0 by A5, PRE_POLY:def 7;

          then ((( SMoebius X) + ( SMoebius Y)) . x) <> 0 by PRE_POLY:def 5;

          hence thesis by PRE_POLY:def 7;

        end;

      end;

      thus thesis by PRE_POLY: 75;

    end;

    theorem :: MOEBIUS1:44

    for X,Y be finite Subset of NAT st X misses Y holds ( SMoebius (X \/ Y)) = (( SMoebius X) + ( SMoebius Y))

    proof

      let X,Y be finite Subset of NAT ;

      

       A1: ( support ( SMoebius (X \/ Y))) = ((X \/ Y) /\ SCNAT ) by Def5

      .= ((X /\ SCNAT ) \/ (Y /\ SCNAT )) by XBOOLE_1: 23;

      assume

       A2: X misses Y;

      for x be object st x in NAT holds (( SMoebius (X \/ Y)) . x) = ((( SMoebius X) + ( SMoebius Y)) . x)

      proof

        let x be object;

        per cases ;

          suppose

           A3: x in ( support ( SMoebius (X \/ Y)));

          per cases by A1, A3, XBOOLE_0:def 3;

            suppose

             A4: x in (X /\ SCNAT );

            then

            reconsider k = x as Element of NAT ;

            

             A5: k in ( support ( SMoebius X)) by A4, Def5;

             not x in (Y /\ SCNAT ) by A2, A4, Lm1;

            then

             A6: not k in ( support ( SMoebius Y)) by Def5;

            (( SMoebius (X \/ Y)) . x) = (( Moebius k) + 0 qua Nat) by A3, Def5

            .= (( Moebius k) + (( SMoebius Y) . k)) by A6, PRE_POLY:def 7

            .= ((( SMoebius X) . k) + (( SMoebius Y) . k)) by A5, Def5

            .= ((( SMoebius X) + ( SMoebius Y)) . x) by PRE_POLY:def 5;

            hence thesis;

          end;

            suppose

             A7: x in (Y /\ SCNAT );

            then

            consider k be Element of NAT such that

             A8: k = x;

             not x in (X /\ SCNAT ) by A2, A7, Lm1;

            then

             A9: not k in ( support ( SMoebius X)) by A8, Def5;

            

             A10: k in ( support ( SMoebius Y)) by A7, A8, Def5;

            (( SMoebius (X \/ Y)) . x) = (( Moebius k) + 0 qua Nat) by A3, A8, Def5

            .= (( Moebius k) + (( SMoebius X) . k)) by A9, PRE_POLY:def 7

            .= ((( SMoebius Y) . k) + (( SMoebius X) . k)) by A10, Def5

            .= ((( SMoebius X) + ( SMoebius Y)) . x) by A8, PRE_POLY:def 5;

            hence thesis;

          end;

        end;

          suppose

           A11: not x in ( support ( SMoebius (X \/ Y)));

          then not x in (Y /\ SCNAT ) by A1, XBOOLE_0:def 3;

          then

           A12: not x in ( support ( SMoebius Y)) by Def5;

           not x in (X /\ SCNAT ) by A1, A11, XBOOLE_0:def 3;

          then

           A13: not x in ( support ( SMoebius X)) by Def5;

          (( SMoebius (X \/ Y)) . x) = 0 by A11, PRE_POLY:def 7

          .= ((( SMoebius Y) . x) + 0 ) by A12, PRE_POLY:def 7

          .= ((( SMoebius Y) . x) + (( SMoebius X) . x)) by A13, PRE_POLY:def 7

          .= ((( SMoebius X) + ( SMoebius Y)) . x) by PRE_POLY:def 5;

          hence thesis;

        end;

      end;

      hence thesis by PBOOLE: 3;

    end;

    begin

    definition

      let n be non zero Nat;

      :: MOEBIUS1:def6

      func PFactors n -> ManySortedSet of SetPrimes means

      : Def6: ( support it ) = ( support ( pfexp n)) & for p be Nat st p in ( support ( pfexp n)) holds (it . p) = p;

      existence

      proof

        defpred P[ object, object] means for p be Prime st $1 = p holds (p in ( support ( pfexp n)) implies $2 = p) & ( not p in ( support ( pfexp n)) implies $2 = 0 );

        

         A1: for x be object st x in SetPrimes holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in SetPrimes ;

          then

          reconsider i = x as prime Element of NAT by NEWTON:def 6;

          per cases ;

            suppose

             A2: i in ( support ( pfexp n));

            take i;

            let p be Prime;

            assume p = x;

            hence thesis by A2;

          end;

            suppose

             A3: not i in ( support ( pfexp n));

            take 0 ;

            let p be Prime;

            assume p = x;

            hence thesis by A3;

          end;

        end;

        consider f be Function such that

         A4: ( dom f) = SetPrimes and

         A5: for x be object st x in SetPrimes holds P[x, (f . x)] from CLASSES1:sch 1( A1);

        

         A6: ( support f) c= SetPrimes by A4, PRE_POLY: 37;

         A7:

        now

          let x be object;

          hereby

            assume

             A8: x in ( support f);

            then x in SetPrimes by A6;

            then

            reconsider i = x as prime Element of NAT by NEWTON:def 6;

            assume not x in ( support ( pfexp n));

            then (f . i) = 0 by A5, A6, A8;

            hence contradiction by A8, PRE_POLY:def 7;

          end;

          assume

           A9: x in ( support ( pfexp n));

          then x in SetPrimes ;

          then

          reconsider i = x as prime Element of NAT by NEWTON:def 6;

          (f . i) = i by A5, A9;

          hence x in ( support f) by PRE_POLY:def 7;

        end;

        reconsider f as ManySortedSet of SetPrimes by A4, PARTFUN1:def 2, RELAT_1:def 18;

        take f;

        thus ( support f) = ( support ( pfexp n)) by A7, TARSKI: 2;

        let p be Nat;

        assume

         A10: p in ( support ( pfexp n));

        then p is Prime by NAT_3: 34;

        hence thesis by A5, A10;

      end;

      uniqueness

      proof

        let it1,it2 be ManySortedSet of SetPrimes such that

         A11: ( support it1) = ( support ( pfexp n)) and

         A12: for p be Nat st p in ( support ( pfexp n)) holds (it1 . p) = p and

         A13: ( support it2) = ( support ( pfexp n)) and

         A14: for p be Nat st p in ( support ( pfexp n)) holds (it2 . p) = p;

        now

          let i be object;

          assume i in SetPrimes ;

          then

          reconsider p = i as prime Element of NAT by NEWTON:def 6;

          per cases ;

            suppose

             A15: p in ( support ( pfexp n));

            

            hence (it1 . i) = p by A12

            .= (it2 . i) by A14, A15;

          end;

            suppose

             A16: not p in ( support ( pfexp n));

            

            hence (it1 . i) = 0 by A11, PRE_POLY:def 7

            .= (it2 . i) by A13, A16, PRE_POLY:def 7;

          end;

        end;

        hence it1 = it2 by PBOOLE: 3;

      end;

    end

    registration

      let n be non zero Nat;

      cluster ( PFactors n) -> finite-support natural-valued;

      coherence

      proof

        

         A1: ( rng ( PFactors n)) c= NAT

        proof

          let x be object;

          assume x in ( rng ( PFactors n));

          then

          consider y be object such that

           A2: y in ( dom ( PFactors n)) and

           A3: (( PFactors n) . y) = x by FUNCT_1:def 3;

          

           A4: y in SetPrimes by A2, PARTFUN1:def 2;

          per cases ;

            suppose y in ( support ( pfexp n));

            then x = y by A3, Def6;

            hence thesis by A4;

          end;

            suppose not y in ( support ( pfexp n));

            then not y in ( support ( PFactors n)) by Def6;

            then x = 0 by A3, PRE_POLY:def 7;

            hence thesis;

          end;

        end;

        ( support ( PFactors n)) = ( support ( pfexp n)) by Def6;

        hence thesis by A1, PRE_POLY:def 8, VALUED_0:def 6;

      end;

    end

    theorem :: MOEBIUS1:45

    

     Th45: ( PFactors 1) = ( EmptyBag SetPrimes )

    proof

      set f = ( PFactors 1);

      for z be object st z in ( dom f) holds (f . z) = 0

      proof

        let z be object;

        assume z in ( dom f);

        then z in SetPrimes by PARTFUN1:def 2;

        then

        reconsider z as Element of NAT ;

        ( support ( pfexp 1)) = {} ;

        then not z in ( support f) by Def6;

        hence thesis by PRE_POLY:def 7;

      end;

      then

       A1: f = (( dom f) --> 0 ) by FUNCOP_1: 11;

      ( dom f) = SetPrimes by PARTFUN1:def 2;

      hence thesis by A1, PBOOLE:def 3;

    end;

    theorem :: MOEBIUS1:46

    

     Th46: for p be Prime holds (( PFactors p) * <*p*>) = <*p*>

    proof

      let p be Prime;

      set f = <*p*>, g = ( PFactors p);

      

       A1: ( dom (g * f)) = {1}

      proof

        thus ( dom (g * f)) c= {1}

        proof

          let x be object;

          assume x in ( dom (g * f));

          then x in ( dom f) by FUNCT_1: 11;

          hence thesis by FINSEQ_1: 2, FINSEQ_1: 38;

        end;

        let x be object;

        assume

         A2: x in {1};

        then x = 1 by TARSKI:def 1;

        then (f . x) = p by FINSEQ_1:def 8;

        then (f . x) in SetPrimes by NEWTON:def 6;

        then

         A3: (f . x) in ( dom g) by PARTFUN1:def 2;

        x in ( dom f) by A2, FINSEQ_1: 2, FINSEQ_1: 38;

        hence thesis by A3, FUNCT_1: 11;

      end;

      

       A4: for x be object st x in ( dom (g * f)) holds ((g * f) . x) = (f . x)

      proof

        let x be object;

        (( pfexp p) . p) <> 0 by NAT_3: 38;

        then

         A5: p in ( support ( pfexp p)) by PRE_POLY:def 7;

        assume

         A6: x in ( dom (g * f));

        then

         A7: x = 1 by A1, TARSKI:def 1;

        

        then ((g * f) . 1) = (g . (f . 1)) by A6, FUNCT_1: 12

        .= (g . p) by FINSEQ_1:def 8

        .= p by A5, Def6

        .= (f . 1) by FINSEQ_1:def 8;

        hence thesis by A7;

      end;

      ( dom f) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      hence thesis by A1, A4, FUNCT_1: 2;

    end;

    theorem :: MOEBIUS1:47

    

     Th47: for p be Prime, n be non zero Nat holds (( PFactors (p |^ n)) * <*p*>) = <*p*>

    proof

      let p be Prime, n be non zero Nat;

      set s = (p |^ n);

      set f = <*p*>, g = ( PFactors s);

      

       A1: ( dom f) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      

       A2: ( dom (g * f)) = {1}

      proof

        thus ( dom (g * f)) c= {1} by A1, FUNCT_1: 11;

        let x be object;

        assume

         A3: x in {1};

        then x = 1 by TARSKI:def 1;

        then (f . x) = p by FINSEQ_1:def 8;

        then (f . x) in SetPrimes by NEWTON:def 6;

        then

         A4: (f . x) in ( dom g) by PARTFUN1:def 2;

        x in ( dom f) by A3, FINSEQ_1: 2, FINSEQ_1: 38;

        hence thesis by A4, FUNCT_1: 11;

      end;

      

       A5: for x be object st x in ( dom (g * f)) holds ((g * f) . x) = (f . x)

      proof

        let x be object;

        (( pfexp p) . p) <> 0 by NAT_3: 38;

        then p in ( support ( pfexp p)) by PRE_POLY:def 7;

        then

         A6: p in ( support ( pfexp s)) by NAT_3: 48;

        assume

         A7: x in ( dom (g * f));

        then

         A8: x = 1 by A2, TARSKI:def 1;

        

        then ((g * f) . 1) = (g . (f . 1)) by A7, FUNCT_1: 12

        .= (g . p) by FINSEQ_1:def 8

        .= p by A6, Def6

        .= (f . 1) by FINSEQ_1:def 8;

        hence thesis by A8;

      end;

      ( dom (g * f)) = ( dom f) by A2, FINSEQ_1: 2, FINSEQ_1: 38;

      hence thesis by A5, FUNCT_1: 2;

    end;

    theorem :: MOEBIUS1:48

    

     Th48: for p be Prime, n be non zero Nat holds (p |-count n) = 0 implies (( PFactors n) . p) = 0

    proof

      let p be Prime, n be non zero Nat;

      assume (p |-count n) = 0 ;

      then (( pfexp n) . p) = 0 by NAT_3:def 8;

      then not p in ( support ( pfexp n)) by PRE_POLY:def 7;

      then not p in ( support ( PFactors n)) by Def6;

      hence thesis by PRE_POLY:def 7;

    end;

    theorem :: MOEBIUS1:49

    

     Th49: for n be non zero Nat, p be Prime st (p |-count n) <> 0 holds (( PFactors n) . p) = p

    proof

      let n be non zero Nat, p be Prime;

      assume (p |-count n) <> 0 ;

      then (( pfexp n) . p) <> 0 by NAT_3:def 8;

      then p in ( support ( pfexp n)) by PRE_POLY:def 7;

      hence thesis by Def6;

    end;

    theorem :: MOEBIUS1:50

    

     Th50: for m,n be non zero Element of NAT st (m,n) are_coprime holds ( PFactors (m * n)) = (( PFactors m) + ( PFactors n))

    proof

      let a,b be non zero Element of NAT ;

      reconsider an = a, bn = b as non zero Nat;

      assume

       A1: (a,b) are_coprime ;

      now

        let i be object;

        assume i in SetPrimes ;

        then

        reconsider p = i as prime Element of NAT by NEWTON:def 6;

        

         A2: (p |-count (an * bn)) = ((p |-count a) + (p |-count b)) by NAT_3: 28;

        

         A3: (a gcd b) = 1 by A1, INT_2:def 3;

        

         A4: p > 1 by INT_2:def 4;

        per cases ;

          suppose

           A5: (p |-count (a * b)) = 0 ;

          then

           A6: (p |-count b) = 0 by A2;

          

           A7: (p |-count a) = 0 by A2, A5;

          

          thus (( PFactors (a * b)) . i) = 0 by A5, Th48

          .= ( 0 + (( PFactors b) . i)) by A6, Th48

          .= ((( PFactors a) . i) + (( PFactors b) . i)) by A7, Th48

          .= ((( PFactors a) + ( PFactors b)) . i) by PRE_POLY:def 5;

        end;

          suppose

           A8: (p |-count (a * b)) <> 0 ;

          thus (( PFactors (a * b)) . i) = ((( PFactors a) + ( PFactors b)) . i)

          proof

            per cases by A2, A8;

              suppose

               A9: (p |-count a) <> 0 ;

               A10:

              now

                consider ka be Nat such that

                 A11: (p |-count a) = (ka + 1) by A9, NAT_1: 6;

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

                (p |^ (p |-count a)) divides a by A4, NAT_3:def 7;

                then (p * (p |^ ka)) divides a by A11, NEWTON: 6;

                then

                consider la be Nat such that

                 A12: a = ((p * (p |^ ka)) * la) by NAT_D:def 3;

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

                then

                 A13: p divides a by NAT_D:def 3;

                assume (p |-count b) <> 0 ;

                then

                consider kb be Nat such that

                 A14: (p |-count b) = (kb + 1) by NAT_1: 6;

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

                (p |^ (p |-count b)) divides b by A4, NAT_3:def 7;

                then (p * (p |^ kb)) divides b by A14, NEWTON: 6;

                then

                consider lb be Nat such that

                 A15: b = ((p * (p |^ kb)) * lb) by NAT_D:def 3;

                b = (p * ((p |^ kb) * lb)) by A15;

                then p divides b by NAT_D:def 3;

                then p divides 1 by A3, A13, NAT_D:def 5;

                hence contradiction by A4, NAT_D: 7;

              end;

              

              thus (( PFactors (a * b)) . i) = p by A8, Th49

              .= ((( PFactors a) . p) + 0 ) by A9, Th49

              .= ((( PFactors a) . p) + (( PFactors b) . p)) by A10, Th48

              .= ((( PFactors a) + ( PFactors b)) . i) by PRE_POLY:def 5;

            end;

              suppose

               A16: (p |-count b) <> 0 ;

               A17:

              now

                assume (p |-count a) <> 0 ;

                then

                consider ka 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) by NAT_D:def 3;

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

                then

                 A20: p divides a by NAT_D:def 3;

                consider kb be Nat such that

                 A21: (p |-count b) = (kb + 1) by A16, NAT_1: 6;

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

                (p |^ (p |-count b)) divides b by A4, NAT_3:def 7;

                then (p * (p |^ kb)) divides b by A21, NEWTON: 6;

                then

                consider lb be Nat such that

                 A22: b = ((p * (p |^ kb)) * lb) by NAT_D:def 3;

                b = (p * ((p |^ kb) * lb)) by A22;

                then p divides b by NAT_D:def 3;

                then p divides 1 by A3, A20, NAT_D:def 5;

                hence contradiction by A4, NAT_D: 7;

              end;

              

              thus (( PFactors (a * b)) . i) = p by A8, Th49

              .= ( 0 + (( PFactors b) . p)) by A16, Th49

              .= ((( PFactors a) . p) + (( PFactors b) . p)) by A17, Th48

              .= ((( PFactors a) + ( PFactors b)) . i) by PRE_POLY:def 5;

            end;

          end;

        end;

      end;

      hence thesis by PBOOLE: 3;

    end;

    theorem :: MOEBIUS1:51

    for n be non zero Element of NAT , A be finite Subset of NAT st A = { k where k be Element of NAT : 0 < k & k divides n & k is square-containing } holds ( SMoebius A) = ( EmptyBag NAT )

    proof

      let n be non zero Element of NAT , A be finite Subset of NAT ;

      assume

       A1: A = { k where k be Element of NAT : 0 < k & k divides n & k is square-containing };

      

       A2: A misses SCNAT

      proof

        assume A meets SCNAT ;

        then

        consider x be object such that

         A3: x in A and

         A4: x in SCNAT by XBOOLE_0: 3;

        ex k be Element of NAT st k = x & 0 < k & k divides n & k is square-containing by A1, A3;

        hence thesis by A4, Def2;

      end;

      for x be object st x in NAT holds (( SMoebius A) . x) = (( EmptyBag NAT ) . x)

      proof

        let x be object;

        assume x in NAT ;

        then

        reconsider k = x as Element of NAT ;

        ( support ( SMoebius A)) = (A /\ SCNAT ) by Def5

        .= {} by A2;

        then (( SMoebius A) . k) = 0 by PRE_POLY:def 7;

        hence thesis by PBOOLE: 5;

      end;

      hence thesis by PBOOLE: 3;

    end;

    begin

    definition

      let n be non zero Nat;

      :: MOEBIUS1:def7

      func Radical n -> Element of NAT equals ( Product ( PFactors n));

      coherence ;

    end

    theorem :: MOEBIUS1:52

    

     Th52: for n be non zero Nat holds ( Radical n) > 0

    proof

      let n be non zero Nat;

      assume ( Radical n) <= 0 ;

      then ( Product ( PFactors n)) = 0 ;

      then

      consider f be FinSequence of COMPLEX such that

       A1: ( Product f) = 0 and

       A2: f = (( PFactors n) * ( canFS ( support ( PFactors n)))) by NAT_3:def 5;

       not ex k be Nat st k in ( dom f) & (f . k) = 0

      proof

        given k be Nat such that

         A3: k in ( dom f) and

         A4: (f . k) = 0 ;

        k in ( dom ( canFS ( support ( PFactors n)))) by A2, A3, FUNCT_1: 11;

        then

         A5: ( rng ( canFS ( support ( PFactors n)))) c= ( support ( PFactors n)) & (( canFS ( support ( PFactors n))) . k) in ( rng ( canFS ( support ( PFactors n)))) by FINSEQ_1:def 4, FUNCT_1: 3;

        then (( canFS ( support ( PFactors n))) . k) in ( support ( PFactors n));

        then

        reconsider p = (( canFS ( support ( PFactors n))) . k) as prime Element of NAT by NEWTON:def 6;

        p in ( support ( PFactors n)) by A5;

        then

         A6: p in ( support ( pfexp n)) by Def6;

        (f . k) = (( PFactors n) . p) by A2, A3, FUNCT_1: 12

        .= p by A6, Def6;

        hence thesis by A4;

      end;

      hence contradiction by A1, RVSUM_1: 103;

    end;

    registration

      let n be non zero Nat;

      cluster ( Radical n) -> non zero;

      coherence by Th52;

    end

    theorem :: MOEBIUS1:53

    for p be Prime holds p = ( Radical p)

    proof

      let p be Prime;

      

       A1: ( support ( PFactors p)) = ( support ( pfexp p)) by Def6

      .= {p} by NAT_3: 43;

      reconsider p as prime Element of NAT by ORDINAL1:def 12;

      reconsider f = <*p*> as FinSequence of NAT ;

      ( rng f) c= NAT by FINSEQ_1:def 4;

      then ( rng f) c= COMPLEX by NUMBERS: 20;

      then

       A2: ( Product f) = p & f is FinSequence of COMPLEX by FINSEQ_1:def 4, RVSUM_1: 95;

      f = (( PFactors p) * <*p*>) by Th46

      .= (( PFactors p) * ( canFS {p})) by FINSEQ_1: 94;

      hence thesis by A1, A2, NAT_3:def 5;

    end;

    theorem :: MOEBIUS1:54

    

     Th54: for p be Prime, n be non zero Element of NAT holds ( Radical (p |^ n)) = p

    proof

      let p be Prime, n be non zero Element of NAT ;

      reconsider p as prime Element of NAT by ORDINAL1:def 12;

      reconsider f = <*p*> as FinSequence of NAT ;

      set s = (p |^ n);

      

       A1: f = (( PFactors s) * <*p*>) by Th47

      .= (( PFactors s) * ( canFS {p})) by FINSEQ_1: 94;

      ( rng f) c= NAT by FINSEQ_1:def 4;

      then ( rng f) c= COMPLEX by NUMBERS: 20;

      then

       A2: ( Product f) = p & f is FinSequence of COMPLEX by FINSEQ_1:def 4, RVSUM_1: 95;

      ( support ( PFactors s)) = ( support ( pfexp s)) by Def6

      .= ( support ( pfexp p)) by NAT_3: 48

      .= {p} by NAT_3: 43;

      hence thesis by A1, A2, NAT_3:def 5;

    end;

    theorem :: MOEBIUS1:55

    

     Th55: for n be non zero Nat holds ( Radical n) divides n

    proof

      defpred P[ Nat] means for n be non zero Nat st ( support ( PFactors n)) c= ( Seg $1) holds ( Radical n) divides n;

      let n be non zero Nat;

      

       A1: ex mS be Element of NAT st ( support ( ppf n)) c= ( Seg mS) by Th14;

      

       A2: ( support ( ppf n)) = ( support ( pfexp n)) by NAT_3:def 9

      .= ( support ( PFactors n)) by Def6;

      

       A3: for k 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 ( PFactors n)) c= ( Seg (k + 1));

        

         A6: ( support ( pfexp n)) = ( support ( PFactors n)) by Def6;

        per cases ;

          suppose

           A7: not ( support ( PFactors n)) c= ( Seg k);

          set p = (k + 1);

          set e = (p |-count n);

          set s = (p |^ e);

           A8:

          now

            assume

             A9: not (k + 1) in ( support ( PFactors n));

            ( support ( PFactors n)) c= ( Seg k)

            proof

              let x be object;

              assume

               A10: x in ( support ( PFactors n));

              then

              reconsider m = x as Nat;

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

              then m < (k + 1) by A9, A10, XXREAL_0: 1;

              then

               A11: m <= k by NAT_1: 13;

              x is Prime by A6, A10, NAT_3: 34;

              then 1 <= m by INT_2:def 4;

              hence thesis by A11, FINSEQ_1: 1;

            end;

            hence contradiction by A7;

          end;

          then

           A12: p is Prime by A6, NAT_3: 34;

          then

           A13: p > 1 by INT_2:def 4;

          then s divides n by NAT_3:def 7;

          then

          consider t be Nat such that

           A14: n = (s * t) by NAT_D:def 3;

          reconsider s, t as non zero Nat by A14;

          consider f be FinSequence of COMPLEX such that

           A15: ( Product ( PFactors s)) = ( Product f) and

           A16: f = (( PFactors s) * ( canFS ( support ( PFactors s)))) by NAT_3:def 5;

          

           A17: ( dom ( PFactors s)) = SetPrimes by PARTFUN1:def 2;

          

           A18: ( support ( ppf s)) = ( support ( pfexp s)) by NAT_3:def 9;

          then

           A19: ( support ( ppf s)) = ( support ( PFactors s)) by Def6;

          (( pfexp n) . p) = e by A12, NAT_3:def 8;

          then

           A20: e <> 0 by A6, A8, PRE_POLY:def 7;

          then

           A21: ( support ( ppf s)) = {p} by A12, A18, NAT_3: 42;

          then

           A22: p in ( support ( pfexp s)) by A18, TARSKI:def 1;

          

           A23: ( support ( PFactors t)) c= ( Seg k)

          proof

            set f = (p |-count t);

            let x be object;

            assume

             A24: x in ( support ( PFactors t));

            then

            reconsider m = x as Nat;

            

             A25: x in ( support ( pfexp t)) by A24, Def6;

             A26:

            now

              assume

               A27: m = p;

              (( pfexp t) . p) = f by A12, NAT_3:def 8;

              then f <> 0 by A25, A27, PRE_POLY:def 7;

              then f >= ( 0 + 1) by NAT_1: 13;

              then

              consider g 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) by NAT_D:def 3;

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

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

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

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

              then (p |^ (e + 1)) divides n by NAT_D:def 3;

              hence contradiction by A13, NAT_3:def 7;

            end;

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

            then ( support ( PFactors t)) c= ( support ( PFactors n)) by A6, Def6;

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

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

            then m < p by A26, XXREAL_0: 1;

            then

             A30: m <= k by NAT_1: 13;

            x is Prime by A25, NAT_3: 34;

            then 1 <= m by INT_2:def 4;

            hence thesis by A30, FINSEQ_1: 1;

          end;

          then

           A31: ( Radical t) divides t by A4;

          ( support ( PFactors s)) = {p} by A18, A21, Def6;

          

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

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

          

          then ( Product ( PFactors s)) = (( PFactors s) . p) by A15, RVSUM_1: 95

          .= p by A22, Def6;

          then

           A32: ( Radical s) divides s by A20, NAT_3: 3;

          reconsider s1 = s, t1 = t as non zero Element of NAT by ORDINAL1:def 12;

          ( support ( ppf t)) = ( support ( pfexp t)) by NAT_3:def 9;

          then

           A33: ( support ( ppf t)) = ( support ( PFactors t)) by Def6;

           A34:

          now

            assume ( support ( ppf s)) meets ( support ( ppf t));

            then

            consider x 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 ( PFactors t)) by Def6;

            x = p by A21, A35, TARSKI:def 1;

            then p <= k by A23, A37, FINSEQ_1: 1;

            hence contradiction by NAT_1: 13;

          end;

          (s1,t1) are_coprime

          proof

            set u = (s1 gcd t1);

            

             A38: u divides t1 by NAT_D:def 5;

            u <> 0 by INT_2: 5;

            then

             A39: ( 0 + 1) <= u by NAT_1: 13;

            assume not (s1,t1) are_coprime ;

            then (s1 gcd t1) <> 1 by INT_2:def 3;

            then u > 1 by A39, XXREAL_0: 1;

            then u >= (1 + 1) by NAT_1: 13;

            then

            consider r 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 divides p by A40, NAT_3: 5;

            then r = 1 or r = p by A12, INT_2:def 4;

            then p divides t1 by A40, A41, A38, INT_2:def 4, NAT_D: 4;

            then p in ( support ( pfexp t)) by A12, NAT_3: 37;

            then p in ( support ( PFactors t)) by Def6;

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

            hence contradiction by NAT_1: 13;

          end;

          

          then ( Radical n) = ( Product (( PFactors s) + ( PFactors t))) by A14, Th50

          .= (( Radical s) * ( Radical t)) by A34, A19, A33, NAT_3: 19;

          hence thesis by A14, A32, A31, NAT_3: 1;

        end;

          suppose ( support ( PFactors n)) c= ( Seg k);

          hence thesis by A4;

        end;

      end;

      

       A42: P[ 0 ]

      proof

        let n be non zero Nat;

        

         A43: {} c= ( support ( PFactors n));

        assume ( support ( PFactors n)) c= ( Seg 0 );

        then ( support ( PFactors n)) = {} by A43;

        then ( PFactors n) = ( EmptyBag SetPrimes ) by PRE_POLY: 81;

        then ( Radical n) = 1 by NAT_3: 20;

        hence thesis by NAT_D: 6;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A42, A3);

      hence thesis by A1, A2;

    end;

    theorem :: MOEBIUS1:56

    

     Th56: for p be Prime, n be non zero Nat holds p divides n iff p divides ( Radical n)

    proof

      let p be Prime, n be non zero Nat;

      thus p divides n implies p divides ( Radical n)

      proof

        assume that

         A1: p divides n and

         A2: not p divides ( Radical n);

        

         A3: p in ( support ( pfexp n)) by A1, NAT_3: 37;

        then

         A4: p in ( support ( PFactors n)) by Def6;

        then p in ( rng ( canFS ( support ( PFactors n)))) by FUNCT_2:def 3;

        then

        consider y be object such that

         A5: y in ( dom ( canFS ( support ( PFactors n)))) and

         A6: p = (( canFS ( support ( PFactors n))) . y) by FUNCT_1:def 3;

        consider f be FinSequence of COMPLEX such that

         A7: ( Product ( PFactors n)) = ( Product f) and

         A8: f = (( PFactors n) * ( canFS ( support ( PFactors n)))) by NAT_3:def 5;

        ( rng ( PFactors n)) c= NAT & ( rng f) c= ( rng ( PFactors n)) by A8, RELAT_1: 26, VALUED_0:def 6;

        then

         A9: ( rng f) c= NAT ;

        ( support ( PFactors n)) c= ( dom ( PFactors n)) by PRE_POLY: 37;

        then

         A10: y in ( dom f) by A4, A8, A5, A6, FUNCT_1: 11;

        reconsider f as FinSequence of NAT by A9, FINSEQ_1:def 4;

        (( PFactors n) . p) = p by A3, Def6;

        then (f . y) = p by A8, A6, A10, FUNCT_1: 12;

        then p in ( rng f) by A10, FUNCT_1: 3;

        hence contradiction by A2, A7, NAT_3: 7;

      end;

      assume

       A11: p divides ( Radical n);

      ( Radical n) divides n by Th55;

      hence thesis by A11, NAT_D: 4;

    end;

    theorem :: MOEBIUS1:57

    

     Th57: for k be non zero Nat st k is square-free holds ( Radical k) = k

    proof

      let k be non zero Nat;

      assume

       A1: k is square-free;

      for i be object st i in SetPrimes holds (( PFactors k) . i) = (( ppf k) . i)

      proof

        let i be object;

        assume i in SetPrimes ;

        then

        reconsider p = i as prime Element of NAT by NEWTON:def 6;

        per cases ;

          suppose

           A2: p in ( support ( pfexp k));

          

           A3: p <> 1 by INT_2:def 4;

          (p |-count k) <> 0

          proof

            assume (p |-count k) = 0 ;

            then not p divides k by A3, NAT_3: 27;

            hence thesis by A2, NAT_3: 36;

          end;

          then

           A4: (p |-count k) >= 1 by NAT_1: 14;

          (p |-count k) <= 1 by A1, Th24;

          then (p |-count k) = 1 by A4, XXREAL_0: 1;

          

          then (( ppf k) . p) = (p |^ 1) by A2, NAT_3:def 9

          .= p;

          hence thesis by A2, Def6;

        end;

          suppose

           A5: not p in ( support ( pfexp k));

          then not p in ( support ( PFactors k)) by Def6;

          then

           A6: (( PFactors k) . p) = 0 by PRE_POLY:def 7;

           not p in ( support ( ppf k)) by A5, NAT_3:def 9;

          hence thesis by A6, PRE_POLY:def 7;

        end;

      end;

      then ( PFactors k) = ( ppf k) by PBOOLE: 3;

      hence thesis by NAT_3: 61;

    end;

    theorem :: MOEBIUS1:58

    for n be non zero Nat holds ( Radical n) <= n by Th55, NAT_D: 7;

    theorem :: MOEBIUS1:59

    for p be Prime, n be non zero Nat holds (p |-count ( Radical n)) <= (p |-count n) by Th55, NAT_3: 30;

    theorem :: MOEBIUS1:60

    for n be non zero Nat holds ( Radical n) = 1 iff n = 1

    proof

      let n be non zero Nat;

      thus ( Radical n) = 1 implies n = 1

      proof

        

         A1: ( rng ( PFactors n)) c= NAT by VALUED_0:def 6;

        consider f be FinSequence of COMPLEX such that

         A2: ( Product ( PFactors n)) = ( Product f) and

         A3: f = (( PFactors n) * ( canFS ( support ( PFactors n)))) by NAT_3:def 5;

        ( rng f) c= ( rng ( PFactors n)) by A3, RELAT_1: 26;

        then ( rng f) c= NAT by A1;

        then

        reconsider f as FinSequence of NAT by FINSEQ_1:def 4;

        assume

         A4: ( Radical n) = 1;

        assume n <> 1;

        then

        consider p be Prime such that

         A5: p divides n by Th5;

        

         A6: p in ( support ( pfexp n)) by A5, NAT_3: 37;

        then

         A7: p in ( support ( PFactors n)) by Def6;

        then p in ( rng ( canFS ( support ( PFactors n)))) by FUNCT_2:def 3;

        then

        consider y be object such that

         A8: y in ( dom ( canFS ( support ( PFactors n)))) & p = (( canFS ( support ( PFactors n))) . y) by FUNCT_1:def 3;

        (( PFactors n) . p) = p by A6, Def6;

        then

         A9: (f . y) = p by A3, A8, FUNCT_1: 13;

        ( support ( PFactors n)) c= ( dom ( PFactors n)) by PRE_POLY: 37;

        then y in ( dom f) by A3, A7, A8, FUNCT_1: 11;

        then 1 < p & p in ( rng f) by A9, FUNCT_1: 3, INT_2:def 4;

        hence thesis by A4, A2, NAT_3: 7, NAT_D: 7;

      end;

      thus thesis by Th45, NAT_3: 20;

    end;

    theorem :: MOEBIUS1:61

    

     Th61: for p be Prime, n be non zero Nat holds (p |-count ( Radical n)) <= 1

    proof

      defpred P[ Nat] means for n be non zero Nat st ( support ( PFactors n)) c= ( Seg $1) holds for p be Prime holds (p |-count ( Radical n)) <= 1;

      let p be Prime, n be non zero Nat;

      

       A1: ex mS be Element of NAT st ( support ( ppf n)) c= ( Seg mS) by Th14;

      

       A2: ( support ( ppf n)) = ( support ( pfexp n)) by NAT_3:def 9

      .= ( support ( PFactors n)) by Def6;

      

       A3: for k 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 ( PFactors n)) c= ( Seg (k + 1));

        

         A6: ( support ( pfexp n)) = ( support ( PFactors n)) by Def6;

        per cases ;

          suppose

           A7: not ( support ( PFactors n)) c= ( Seg k);

          let p be Prime;

          reconsider r = (k + 1) as non zero Element of NAT ;

          set e = (r |-count n);

          set s = (r |^ e);

           A8:

          now

            assume

             A9: not (k + 1) in ( support ( PFactors n));

            ( support ( PFactors n)) c= ( Seg k)

            proof

              let x be object;

              assume

               A10: x in ( support ( PFactors n));

              then

              reconsider m = x as Nat;

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

              then m < (k + 1) by A9, A10, XXREAL_0: 1;

              then

               A11: m <= k by NAT_1: 13;

              x is Prime by A6, A10, NAT_3: 34;

              then 1 <= m by INT_2:def 4;

              hence thesis by A11, FINSEQ_1: 1;

            end;

            hence contradiction by A7;

          end;

          then

           A12: r is Prime by A6, NAT_3: 34;

          then

           A13: r > 1 by INT_2:def 4;

          then s divides n by NAT_3:def 7;

          then

          consider t be Nat such that

           A14: n = (s * t) by NAT_D:def 3;

          reconsider s, t as non zero Nat by A14;

          reconsider s1 = s, t1 = t as non zero Element of NAT by ORDINAL1:def 12;

          

           A15: ( support ( ppf s)) = ( support ( pfexp s)) by NAT_3:def 9;

          then

           A16: ( support ( ppf s)) = ( support ( PFactors s)) by Def6;

          

           A17: ( support ( PFactors t)) c= ( Seg k)

          proof

            set f = (r |-count t);

            let x be object;

            assume

             A18: x in ( support ( PFactors t));

            then

            reconsider m = x as Nat;

            

             A19: x in ( support ( pfexp t)) by A18, Def6;

             A20:

            now

              assume

               A21: m = r;

              (( pfexp t) . r) = f by A12, NAT_3:def 8;

              then f <> 0 by A19, A21, PRE_POLY:def 7;

              then f >= ( 0 + 1) by NAT_1: 13;

              then

              consider g be Nat such that

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

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

              then

              consider u be Nat such that

               A23: t = ((r |^ f) * u) by NAT_D:def 3;

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

              n = (s * (((r |^ g) * r) * u)) by A14, A22, A23, NEWTON: 6

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

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

              then (r |^ (e + 1)) divides n by NAT_D:def 3;

              hence contradiction by A13, NAT_3:def 7;

            end;

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

            then ( support ( PFactors t)) c= ( support ( PFactors n)) by A6, Def6;

            then m in ( support ( PFactors n)) by A18;

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

            then m < r by A20, XXREAL_0: 1;

            then

             A24: m <= k by NAT_1: 13;

            x is Prime by A19, NAT_3: 34;

            then 1 <= m by INT_2:def 4;

            hence thesis by A24, FINSEQ_1: 1;

          end;

          (( pfexp n) . r) = e by A12, NAT_3:def 8;

          then

           A25: e <> 0 by A6, A8, PRE_POLY:def 7;

          

           A26: (p |-count ( Radical s)) <= 1

          proof

            per cases ;

              suppose

               A27: p = r;

              

               A28: p > 1 by INT_2:def 4;

              ( Radical s) = r by A25, A27, Th54;

              hence thesis by A27, A28, NAT_3: 22;

            end;

              suppose p <> r;

              then (p,r) are_coprime by A12, INT_2: 30;

              then

               A29: not p divides r by PYTHTRIP:def 2;

              

               A30: p > 1 by INT_2:def 4;

              (p |-count s) = (e * (p |-count r)) by NAT_3: 32

              .= (e * 0 ) by A29, A30, NAT_3: 27

              .= 0 ;

              hence thesis by Th55, NAT_3: 30;

            end;

          end;

          

           A31: ( support ( ppf s)) = {r} by A12, A25, A15, NAT_3: 42;

           A32:

          now

            assume ( support ( ppf s)) meets ( support ( ppf t));

            then

            consider x be object such that

             A33: x in ( support ( ppf s)) and

             A34: x in ( support ( ppf t)) by XBOOLE_0: 3;

            x in ( support ( pfexp t)) by A34, NAT_3:def 9;

            then

             A35: x in ( support ( PFactors t)) by Def6;

            x = r by A31, A33, TARSKI:def 1;

            then r <= k by A17, A35, FINSEQ_1: 1;

            hence contradiction by NAT_1: 13;

          end;

          ( support ( ppf t)) = ( support ( pfexp t)) by NAT_3:def 9;

          then

           A36: ( support ( ppf t)) = ( support ( PFactors t)) by Def6;

          

           A37: (p |-count ( Radical s)) = 0 or (p |-count ( Radical t)) = 0

          proof

            assume that

             A38: (p |-count ( Radical s)) <> 0 and

             A39: (p |-count ( Radical t)) <> 0 ;

            (p |-count t) > 0 by A39, Th55, NAT_3: 30;

            then (( PFactors t) . p) <> 0 by Th49;

            then

             A40: p in ( support ( PFactors t)) by PRE_POLY:def 7;

            (p |-count s) > 0 by A38, Th55, NAT_3: 30;

            then (( PFactors s) . p) <> 0 by Th49;

            then p in ( support ( PFactors s)) by PRE_POLY:def 7;

            hence thesis by A32, A16, A36, A40, XBOOLE_0: 3;

          end;

          (s1,t1) are_coprime

          proof

            set u = (s1 gcd t1);

            

             A41: u divides t1 by NAT_D:def 5;

            u <> 0 by INT_2: 5;

            then

             A42: ( 0 + 1) <= u by NAT_1: 13;

            assume not (s1,t1) are_coprime ;

            then (s1 gcd t1) <> 1 by INT_2:def 3;

            then u > 1 by A42, XXREAL_0: 1;

            then u >= (1 + 1) by NAT_1: 13;

            then

            consider w be Element of NAT such that

             A43: w is prime and

             A44: w divides u by INT_2: 31;

            u divides s1 by NAT_D:def 5;

            then w divides s1 by A44, NAT_D: 4;

            then w divides r by A43, NAT_3: 5;

            then w = 1 or w = r by A12, INT_2:def 4;

            then r divides t1 by A43, A44, A41, INT_2:def 4, NAT_D: 4;

            then r in ( support ( pfexp t)) by A12, NAT_3: 37;

            then r in ( support ( PFactors t)) by Def6;

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

            hence contradiction by NAT_1: 13;

          end;

          

          then ( Radical n) = ( Product (( PFactors s) + ( PFactors t))) by A14, Th50

          .= (( Radical s) * ( Radical t)) by A32, A16, A36, NAT_3: 19;

          then (p |-count ( Radical n)) = ((p |-count ( Radical t)) + (p |-count ( Radical s))) by NAT_3: 28;

          hence thesis by A4, A17, A37, A26;

        end;

          suppose ( support ( PFactors n)) c= ( Seg k);

          hence thesis by A4;

        end;

      end;

      

       A45: P[ 0 ]

      proof

        let n be non zero Nat;

        assume

         A46: ( support ( PFactors n)) c= ( Seg 0 );

        let p be Prime;

         {} c= ( support ( PFactors n));

        then ( support ( PFactors n)) = {} by A46;

        then

         A47: ( PFactors n) = ( EmptyBag SetPrimes ) by PRE_POLY: 81;

         not p divides ( Radical n)

        proof

          assume p divides ( Radical n);

          then

           A48: p divides 1 by A47, NAT_3: 20;

          1 divides p by NAT_D: 6;

          then p = 1 by A48, NAT_D: 5;

          hence thesis by INT_2:def 4;

        end;

        hence thesis by Th6;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A45, A3);

      hence thesis by A1, A2;

    end;

    

     Lm3: for n be non zero Nat, p be Prime holds not (p |^ 2) divides ( Radical n)

    proof

      let n be non zero Nat;

      let p be Prime;

      set PR = (p |-count ( Radical n));

      

       A1: p <> 1 by INT_2:def 4;

      assume

       A2: (p |^ 2) divides ( Radical n);

      

       A3: PR is non zero Element of NAT

      proof

        assume not PR is non zero Element of NAT ;

        then not (p |^ ( 0 + 1)) divides ( Radical n) by A1, NAT_3:def 7;

        then not p divides ( Radical n);

        hence contradiction by A2, Th10;

      end;

      PR >= 2

      proof

        assume PR < 2;

        then PR = 1 by A3, NAT_1: 23;

        then not (p |^ (1 + 1)) divides ( Radical n) by A1, NAT_3:def 7;

        hence contradiction by A2;

      end;

      then PR > 1 by XXREAL_0: 2;

      hence contradiction by Th61;

    end;

    

     Lm4: for n be non zero Nat holds ( Radical n) is square-free by Lm3;

    registration

      let n be non zero Nat;

      cluster ( Radical n) -> square-free;

      coherence by Lm4;

    end

    theorem :: MOEBIUS1:62

    for n be non zero Nat holds ( Radical ( Radical n)) = ( Radical n) by Th57;

    theorem :: MOEBIUS1:63

    for n be non zero Element of NAT , p be Prime holds { k where k be Element of NAT : 0 < k & k divides ( Radical n) & p divides k } c= ( Seg n)

    proof

      let n be non zero Element of NAT ;

      let p be Prime;

      let x be object;

      assume x in { k where k be Element of NAT : 0 < k & k divides ( Radical n) & p divides k };

      then

      consider k be Element of NAT such that

       A1: x = k and

       A2: k > 0 and

       A3: k divides ( Radical n) and p divides k;

      

       A4: 1 <= k by A2, NAT_1: 14;

      

       A5: ( Radical n) <= n by Th55, NAT_D: 7;

      k <= ( Radical n) by A3, NAT_D: 7;

      then k <= n by A5, XXREAL_0: 2;

      hence thesis by A1, A4, FINSEQ_1: 1;

    end;

    theorem :: MOEBIUS1:64

    for n be non zero Element of NAT , p be Prime holds { k where k be Element of NAT : 0 < k & k divides ( Radical n) & not p divides k } c= ( Seg n)

    proof

      let n be non zero Element of NAT ;

      let p be Prime;

      let x be object;

      assume x in { k where k be Element of NAT : 0 < k & k divides ( Radical n) & not p divides k };

      then

      consider k be Element of NAT such that

       A1: x = k and

       A2: k > 0 and

       A3: k divides ( Radical n) and not p divides k;

      

       A4: 1 <= k by A2, NAT_1: 14;

      

       A5: ( Radical n) <= n by Th55, NAT_D: 7;

      k <= ( Radical n) by A3, NAT_D: 7;

      then k <= n by A5, XXREAL_0: 2;

      hence thesis by A1, A4, FINSEQ_1: 1;

    end;

    

     Lm5: for m,n be non zero Element of NAT st m divides n & m is square-free holds m divides ( Radical n)

    proof

      let m,n be non zero Element of NAT ;

      assume that

       A1: m divides n and

       A2: m is square-free;

      for p be Prime holds (p |-count m) <= (p |-count ( Radical n))

      proof

        let p be Prime;

        

         A3: p > 1 by INT_2:def 4;

        per cases ;

          suppose p divides m;

          then p divides n by A1, NAT_D: 4;

          then p divides ( Radical n) by Th56;

          then

           A4: (p |-count ( Radical n)) <> 0 by A3, NAT_3: 27;

          (p |-count ( Radical n)) <= 1 by Th61;

          then

           A5: (p |-count ( Radical n)) < (1 + 1) by NAT_1: 13;

          (p |-count m) <= 1 by A2, Th24;

          hence thesis by A5, A4, NAT_1: 23;

        end;

          suppose not p divides m;

          hence thesis by A3, NAT_3: 27;

        end;

      end;

      hence thesis by Th19;

    end;

    theorem :: MOEBIUS1:65

    

     Th65: for k,n be non zero Nat holds k divides n & k is square-free iff k divides ( Radical n)

    proof

      let k,n be non zero Nat;

      

       A1: k divides ( Radical n) implies k divides n & k is square-free

      proof

        assume

         A2: k divides ( Radical n);

        ( Radical n) divides n by Th55;

        hence thesis by A2, Th26, NAT_D: 4;

      end;

      k is non zero Element of NAT & n is non zero Element of NAT by ORDINAL1:def 12;

      hence thesis by A1, Lm5;

    end;

    theorem :: MOEBIUS1:66

    for n be non zero Nat holds { k where k be Element of NAT : 0 < k & k divides n & k is square-free } = { k where k be Element of NAT : 0 < k & k divides ( Radical n) }

    proof

      let n be non zero Nat;

      thus { k where k be Element of NAT : 0 < k & k divides n & k is square-free } c= { k where k be Element of NAT : 0 < k & k divides ( Radical n) }

      proof

        let x be object;

        assume x in { k where k be Element of NAT : 0 < k & k divides n & k is square-free };

        then

        consider k1 be Element of NAT such that

         A1: k1 = x and

         A2: 0 < k1 and

         A3: k1 divides n & k1 is square-free;

        k1 divides ( Radical n) by A2, A3, Th65;

        hence thesis by A1, A2;

      end;

      let x be object;

      assume x in { k where k be Element of NAT : 0 < k & k divides ( Radical n) };

      then

      consider k1 be Element of NAT such that

       A4: x = k1 & 0 < k1 and

       A5: k1 divides ( Radical n);

      

       A6: k1 is square-free by A5, Th26;

      ( Radical n) divides n by Th55;

      then k1 divides n by A5, NAT_D: 4;

      hence thesis by A4, A6;

    end;