moebius3.miz



    begin

    reserve n,i,k,m for Nat;

    reserve p for Prime;

    registration

      cluster non zero square non trivial for Nat;

      existence

      proof

        4 = (2 ^2 );

        then 4 is non zero square;

        hence thesis by NAT_2: 28;

      end;

    end

    registration

      let Z be Subset of REAL ;

      let f be PartFunc of Z, REAL ;

      let A be Subset of REAL ;

      cluster (f | A) -> A -defined;

      coherence ;

    end

    theorem :: MOEBIUS3:1

    for Z be Subset of REAL st 0 in Z holds (( id Z) " { 0 }) = { 0 }

    proof

      let Z be Subset of REAL ;

      assume 0 in Z;

      then { 0 } c= Z by ZFMISC_1: 31;

      hence thesis by FUNCT_2: 94;

    end;

    theorem :: MOEBIUS3:2

    

     Counter0: for Z be Subset of REAL st not 0 in Z holds (( id Z) " { 0 }) = {}

    proof

      let Z be Subset of REAL ;

      assume

       AA: not 0 in Z;

      (( id Z) " { 0 }) c= {}

      proof

        let x be object;

        assume x in (( id Z) " { 0 });

        then

         A2: x in ( dom ( id Z)) & (( id Z) . x) in { 0 } by FUNCT_1:def 7;

        then (( id Z) . x) = x by FUNCT_1: 17;

        hence thesis by A2, AA, TARSKI:def 1;

      end;

      hence thesis;

    end;

    theorem :: MOEBIUS3:3

    

     ContCut: for Z be open Subset of REAL , A be non empty closed_interval Subset of REAL st not 0 in Z & A c= Z holds ((( id Z) ^ ) | A) is continuous

    proof

      let Z be open Subset of REAL , A be non empty closed_interval Subset of REAL ;

      assume

       A1: not 0 in Z & A c= Z;

      then (( id Z) ^ ) is_differentiable_on Z by FDIFF_5: 4;

      then ((( id Z) ^ ) | Z) is continuous by FDIFF_1: 25;

      hence thesis by A1, FCONT_1: 16;

    end;

    theorem :: MOEBIUS3:4

    for Z be open Subset of REAL , A be non empty closed_interval Subset of REAL st Z = ( right_open_halfline 0 ) & A = [.1, (n + 1).] holds ( integral ((( id Z) ^ ),A)) = ( ln . (n + 1))

    proof

      let Z be open Subset of REAL , A be non empty closed_interval Subset of REAL ;

      assume

       Z1: Z = ( right_open_halfline 0 ) & A = [.1, (n + 1).];

      then

       N1: not 0 in Z by XXREAL_1: 4;

      

       A1: A c= Z

      proof

        let x be object;

        assume

         aa: x in A;

        then

        reconsider xx = x as Real;

        1 <= xx & xx <= (n + 1) by aa, Z1, XXREAL_1: 1;

        hence thesis by Z1, XXREAL_1: 235;

      end;

      set f = ( id Z);

      

       a3: ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2

      .= (Z \ {} ) by Counter0, N1

      .= Z;

      

       B1: ( lower_bound A) = 1 by Z1, XREAL_1: 31, XXREAL_2: 25;

      

       B2: ( upper_bound A) = (n + 1) by Z1, XREAL_1: 31, XXREAL_2: 29;

      ((( id Z) ^ ) | A) is continuous by ContCut, A1, N1;

      

      then ( integral ((( id Z) ^ ),A)) = (( ln . ( upper_bound A)) - ( ln . ( lower_bound A))) by A1, Z1, TAYLOR_1: 18, a3, INTEGRA9: 61

      .= (( ln . (n + 1)) - (1 - 1)) by ENTROPY1: 2, B1, B2

      .= ( ln . (n + 1));

      hence thesis;

    end;

    theorem :: MOEBIUS3:5

    for Z be open Subset of REAL , A be non empty closed_interval Subset of REAL st Z = ( right_open_halfline 0 ) & 0 < n & A = [.n, (n + 1).] holds ( integral ((( id Z) ^ ),A)) = ( ln . ((n + 1) / n))

    proof

      let Z be open Subset of REAL , A be non empty closed_interval Subset of REAL ;

      assume

       Z1: Z = ( right_open_halfline 0 ) & 0 < n & A = [.n, (n + 1).];

      

       N1: not 0 in Z by XXREAL_1: 4, Z1;

      

       A1: A c= Z

      proof

        let x be object;

        assume

         aa: x in A;

        then

        reconsider xx = x as Real;

        n <= xx & xx <= (n + 1) by aa, Z1, XXREAL_1: 1;

        hence thesis by XXREAL_1: 235, Z1;

      end;

      set f = ( id Z);

      

       a3: ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2

      .= (Z \ {} ) by Counter0, N1

      .= Z;

      

       B1: ( lower_bound A) = n by Z1, XREAL_1: 31, XXREAL_2: 25;

      

       B2: ( upper_bound A) = (n + 1) by Z1, XREAL_1: 31, XXREAL_2: 29;

      ((( id Z) ^ ) | A) is continuous by ContCut, A1, N1;

      

      then ( integral ((( id Z) ^ ),A)) = (( ln . ( upper_bound A)) - ( ln . ( lower_bound A))) by A1, Z1, TAYLOR_1: 18, a3, INTEGRA9: 61

      .= ( ln . ((n + 1) / n)) by Z1, DIFF_4: 4, B1, B2;

      hence thesis;

    end;

    theorem :: MOEBIUS3:6

    

     MacPositive: for x,r be Real st x > 0 & r > 0 holds ( Maclaurin ( exp_R , ].( - r), r.[,x)) is positive-yielding

    proof

      let x,r be Real;

      assume

       A0: x > 0 & r > 0 ;

      set f = ( Maclaurin ( exp_R , ].( - r), r.[,x));

      for r be Real st r in ( rng f) holds 0 < r

      proof

        let r be Real;

        assume r in ( rng f);

        then

        consider xx be object such that

         A1: xx in ( dom f) & r = (f . xx) by FUNCT_1:def 3;

        reconsider nn = xx as Element of NAT by A1;

        r = ((x |^ nn) / (nn ! )) by A1, TAYLOR_2: 8, A0;

        hence thesis by A0;

      end;

      hence thesis by PARTFUN3:def 1;

    end;

    theorem :: MOEBIUS3:7

    

     Th36: for f be summable Real_Sequence, n be Nat st f is positive-yielding holds ( Sum (f ^\ (n + 1))) > 0

    proof

      let f be summable Real_Sequence, n be Nat;

      assume

       A0: f is positive-yielding;

      set LS = (f ^\ (n + 1));

      

       A2: for i be Nat holds 0 <= (LS . i)

      proof

        let i be Nat;

        

         a1: (LS . i) = (f . ((n + 1) + i)) by NAT_1:def 3;

        ((n + 1) + i) in NAT by ORDINAL1:def 12;

        then ((n + 1) + i) in ( dom f) by FUNCT_2:def 1;

        then (f . ((n + 1) + i)) in ( rng f) by FUNCT_1: 3;

        hence thesis by PARTFUN3:def 1, A0, a1;

      end;

      ex i be Nat st i in ( dom LS) & 0 < (LS . i)

      proof

        consider j be Nat such that

         A3: (n + 1) <= j;

        (j - (n + 1)) in NAT by A3, INT_1: 5;

        then

        reconsider i = (j - (n + 1)) as Nat;

        take i;

        

         A4: ((n + 1) + i) = j;

        

         aa: ( dom LS) = NAT by FUNCT_2:def 1;

        

         A6: (LS . i) = (f . j) by NAT_1:def 3, A4;

        j in NAT by ORDINAL1:def 12;

        then j in ( dom f) by FUNCT_2:def 1;

        then (f . j) in ( rng f) by FUNCT_1: 3;

        hence thesis by aa, A6, A0, PARTFUN3:def 1, ORDINAL1:def 12;

      end;

      then

      consider k be Nat such that

       A6: k in ( dom LS) & (LS . k) > 0 ;

      LS is summable by SERIES_1: 12;

      hence thesis by A6, RSSPACE2: 3, A2;

    end;

    begin

    definition

      let n be Nat;

      :: MOEBIUS3:def1

      func Harmonic n -> Real equals (( Partial_Sums invNAT ) . n);

      coherence ;

    end

    theorem :: MOEBIUS3:8

    

     Harm0: ( Harmonic 0 ) = 0

    proof

      ( Harmonic 0 ) = ( invNAT . 0 ) by SERIES_1:def 1

      .= (1 / 0 ) by MOEBIUS2:def 2

      .= 0 ;

      hence thesis;

    end;

    theorem :: MOEBIUS3:9

    

     Harmon1: ( Harmonic (n + 1)) = (( Harmonic n) + (1 / (n + 1)))

    proof

      (( Partial_Sums invNAT ) . (n + 1)) = ((( Partial_Sums invNAT ) . n) + ( invNAT . (n + 1))) by SERIES_1:def 1

      .= (( Harmonic n) + (1 / (n + 1))) by MOEBIUS2:def 2;

      hence thesis;

    end;

    theorem :: MOEBIUS3:10

    

     Harm1: ( Harmonic 1) = 1

    proof

      ( Harmonic ( 0 + 1)) = (( Harmonic 0 ) + (1 / ( 0 + 1))) by Harmon1

      .= 1 by Harm0;

      hence thesis;

    end;

    theorem :: MOEBIUS3:11

    ( Harmonic 2) = (3 / 2)

    proof

      ( Harmonic (1 + 1)) = (( Harmonic 1) + (1 / (1 + 1))) by Harmon1

      .= (3 / 2) by Harm1;

      hence thesis;

    end;

    begin

    theorem :: MOEBIUS3:12

    

     LogZero: ( ln . 1) = 0

    proof

      

       A2: number_e <> 1 by TAYLOR_1: 11;

      

       A1: 1 in ( right_open_halfline 0 ) by XXREAL_1: 235;

      ( ln . 1) = ( log ( number_e ,1)) by A1, TAYLOR_1:def 2, TAYLOR_1:def 3

      .= 0 by TAYLOR_1: 11, A2, POWER: 51;

      hence thesis;

    end;

    theorem :: MOEBIUS3:13

    for x be Real st x > 0 holds ( exp_R . x) > (x + 1)

    proof

      let x be Real;

      assume

       AA: x > 0 ;

      set r = 1;

      set f = ( Maclaurin ( exp_R , ].( - r), r.[,x));

      

       A4: ( exp_R . x) = ( Sum f) by TAYLOR_2: 16;

      

       A2: (f . 0 ) = ((x |^ 0 ) / ( 0 ! )) by TAYLOR_2: 8

      .= 1 by NEWTON: 4, NEWTON: 12;

      

       A3: (f . 1) = ((x |^ 1) / (1 ! )) by TAYLOR_2: 8

      .= x by NEWTON: 13;

      

       SS: f is absolutely_summable by TAYLOR_2: 16;

      

      then

       A6: ( Sum f) = ((( Partial_Sums f) . 1) + ( Sum (f ^\ (1 + 1)))) by SERIES_1: 15

      .= (((( Partial_Sums f) . 0 ) + (f . ( 0 + 1))) + ( Sum (f ^\ (1 + 1)))) by SERIES_1:def 1

      .= ((1 + x) + ( Sum (f ^\ (1 + 1)))) by A2, A3, SERIES_1:def 1;

      f is positive-yielding & f is summable by MacPositive, AA, SS;

      hence thesis by A4, A6, XREAL_1: 29, Th36;

    end;

    theorem :: MOEBIUS3:14

    

     Diesel1: for x be Real st x > 0 holds ( ln . (x + 1)) < x

    proof

      let x be Real;

      assume x > 0 ;

      then (x + 1) > 1 by XREAL_1: 29;

      then ( ln . (x + 1)) < ((x + 1) - 1) by ENTROPY1: 2;

      hence thesis;

    end;

    theorem :: MOEBIUS3:15

    

     Diesel2: for n be Nat st n > 0 holds ( ln . ((n + 1) / n)) < (1 / n)

    proof

      let n be Nat;

      assume

       A1: n > 0 ;

      ((n + 1) / n) = ((n / n) + (1 / n)) by XCMPLX_1: 62

      .= (1 + (1 / n)) by A1, XCMPLX_1: 60;

      hence thesis by Diesel1, A1;

    end;

    theorem :: MOEBIUS3:16

    

     LogExp: for x be Real holds ( ln . ( exp_R . x)) = x

    proof

      let x be Real;

      

       A1: ( exp_R . x) in ( right_open_halfline 0 ) by XXREAL_1: 235, SIN_COS: 54;

      ( log ( number_e ,( exp_R . x))) = x by TAYLOR_1: 13;

      hence thesis by A1, TAYLOR_1:def 3, TAYLOR_1:def 2;

    end;

    theorem :: MOEBIUS3:17

    

     LogMono: for x,y be Real st 0 < x < y holds ( ln . x) < ( ln . y)

    proof

      let x,y be Real;

      assume

       A1: 0 < x < y;

      then

       A2: x in ( right_open_halfline 0 ) & y in ( right_open_halfline 0 ) by XXREAL_1: 235;

       number_e > 1 by XXREAL_0: 2, TAYLOR_1: 11;

      then ( log ( number_e ,x)) < ( log ( number_e ,y)) by A1, POWER: 57;

      then (( log_ number_e ) . x) < ( log ( number_e ,y)) by A2, TAYLOR_1:def 2;

      hence thesis by TAYLOR_1:def 3, TAYLOR_1:def 2, A2;

    end;

    theorem :: MOEBIUS3:18

    for n be non zero Nat holds ( ln . (n + 1)) > 0

    proof

      let n be non zero Nat;

      ( 0 + 1) < (n + 1) by XREAL_1: 8;

      hence thesis by LogZero, LogMono;

    end;

    theorem :: MOEBIUS3:19

    

     LogAdd: for x,y be Real st 0 < x & 0 < y holds ( ln . (x * y)) = (( ln . x) + ( ln . y))

    proof

      let x,y be Real;

      assume

       A1: 0 < x & 0 < y;

      then

       A2: x in ( right_open_halfline 0 ) & y in ( right_open_halfline 0 ) by XXREAL_1: 235;

      

       a2: (x * y) in ( right_open_halfline 0 ) by XXREAL_1: 235, A1;

      

       A3: number_e > 1 by XXREAL_0: 2, TAYLOR_1: 11;

      ( ln . (x * y)) = ( log ( number_e ,(x * y))) by a2, TAYLOR_1:def 2, TAYLOR_1:def 3

      .= (( log ( number_e ,x)) + ( log ( number_e ,y))) by POWER: 53, A1, A3

      .= (( log ( number_e ,x)) + (( log_ number_e ) . y)) by TAYLOR_1:def 2, A2

      .= (( ln . x) + ( ln . y)) by TAYLOR_1:def 3, TAYLOR_1:def 2, A2;

      hence thesis;

    end;

    theorem :: MOEBIUS3:20

    for x be Real holds ex y be non zero Nat st x < ( ln . ( ln . (y + 1)))

    proof

      let x be Real;

      set N = [/( exp_R . ( exp_R . x))\];

      

       A1: ( exp_R . ( exp_R . x)) > 0 by SIN_COS: 54;

      then N > 0 by INT_1:def 7;

      then N in NAT by INT_1: 3;

      then

      reconsider N as non zero Nat by SIN_COS: 54, INT_1:def 7;

      take N;

      

       A3: ( exp_R . x) > 0 by SIN_COS: 54;

      ( ln . ( exp_R . ( exp_R . x))) < ( ln . (N + 1)) by A1, LogMono, INT_1: 32;

      then ( exp_R . x) < ( ln . (N + 1)) by LogExp;

      then ( ln . ( exp_R . x)) < ( ln . ( ln . (N + 1))) by A3, LogMono;

      hence thesis by LogExp;

    end;

    theorem :: MOEBIUS3:21

    

     Diesel3: for A be non empty closed_interval Subset of REAL , Z be open Subset of REAL , n be non zero Nat st Z = ( right_open_halfline 0 ) & A = [.n, (n + 1).] holds ( integral ((( id Z) ^ ),A)) < (1 / n)

    proof

      let A be non empty closed_interval Subset of REAL , Z be open Subset of REAL , n be non zero Nat;

      assume

       aa: Z = ( right_open_halfline 0 ) & A = [.n, (n + 1).];

      

       N1: not 0 in Z by aa, XXREAL_1: 4;

      

       A1: A c= Z

      proof

        let x be object;

        assume

         BB: x in A;

        then

        reconsider xx = x as Real;

        n <= xx & xx <= (n + 1) by BB, aa, XXREAL_1: 1;

        hence thesis by aa, XXREAL_1: 235;

      end;

      set f = ( id Z);

      

       a3: ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2

      .= (Z \ {} ) by Counter0, N1

      .= Z;

      

       B1: ( lower_bound A) = n by aa, XREAL_1: 31, XXREAL_2: 25;

      

       B2: ( upper_bound A) = (n + 1) by aa, XREAL_1: 31, XXREAL_2: 29;

      ((( id Z) ^ ) | A) is continuous by ContCut, A1, N1;

      

      then ( integral ((( id Z) ^ ),A)) = (( ln . ( upper_bound A)) - ( ln . ( lower_bound A))) by A1, aa, TAYLOR_1: 18, a3, INTEGRA9: 61

      .= ( ln . ((n + 1) / n)) by B1, B2, DIFF_4: 4;

      hence thesis by Diesel2;

    end;

    theorem :: MOEBIUS3:22

    for n be non zero Nat holds ( ln . (n + 1)) < ( Harmonic n)

    proof

      let n be non zero Nat;

      set A = [.1, (n + 1).];

      ( 0 + 1) <= (n + 1) by XREAL_1: 31;

      then

      reconsider A as non empty closed_interval Subset of REAL by MEASURE5:def 3, XXREAL_1: 1;

      

       WA: A = ['1, (n + 1)'] by XREAL_1: 31, INTEGRA5:def 3;

      reconsider Z = ( right_open_halfline 0 ) as open Subset of REAL ;

      

       N1: not 0 in Z by XXREAL_1: 4;

      

       A1: A c= Z

      proof

        let x be object;

        assume

         a1: x in A;

        then

        reconsider xx = x as Real;

        1 <= xx & xx <= (n + 1) by a1, XXREAL_1: 1;

        hence thesis by XXREAL_1: 235;

      end;

      set f = ( id Z);

      

       NN: ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2

      .= (Z \ {} ) by Counter0, N1

      .= Z;

      

       B1: ( lower_bound A) = 1 by XREAL_1: 31, XXREAL_2: 25;

      

       B2: ( upper_bound A) = (n + 1) by XREAL_1: 31, XXREAL_2: 29;

      ((( id Z) ^ ) | A) is continuous by ContCut, A1, N1;

      

      then

       KL: ( integral ((( id Z) ^ ),A)) = (( ln . ( upper_bound A)) - ( ln . ( lower_bound A))) by A1, TAYLOR_1: 18, NN, INTEGRA9: 61

      .= (( ln . (n + 1)) - (1 - 1)) by ENTROPY1: 2, B1, B2

      .= ( ln . (n + 1));

      set g = (( id Z) ^ );

      defpred P[ Nat] means ( integral (g,1,($1 + 1))) < ( Harmonic $1);

      reconsider AA = ['1, (1 + 1)'] as non empty closed_interval Subset of REAL ;

      AA = [.1, (1 + 1).] by INTEGRA5:def 3;

      then ( integral (g,AA)) < (1 / 1) by Diesel3;

      then

       I1: P[1] by Harm1, INTEGRA5:def 4;

      

       I2: for k be non zero Nat st P[k] holds P[(k + 1)]

      proof

        let k be non zero Nat;

        assume

         s0: P[k];

        set a = 1, b = ((k + 1) + 1), c = (k + 1);

        

         W0: a <= b by XREAL_1: 31;

        

         Za: [.a, b.] c= ]. 0 , +infty .[ by XXREAL_1: 249;

        then

         W3: ['a, b'] c= ( dom g) by XREAL_1: 31, INTEGRA5:def 3, NN;

        set B = ['a, b'];

        B c= Z by Za, INTEGRA5:def 3, XREAL_1: 31;

        then

         v1: ((( id Z) ^ ) | B) is continuous by ContCut, N1;

        then

         W2: g is_integrable_on ['a, b'] by INTEGRA5: 11, W3;

        

         W4: (g | ['a, b']) is bounded by INTEGRA5: 10, W3, v1;

        a <= c & c <= b by XREAL_1: 31;

        then c in [.a, b.] by XXREAL_1: 1;

        then c in ['a, b'] by XREAL_1: 31, INTEGRA5:def 3;

        then

         W1: ( integral (g,a,b)) = (( integral (g,a,c)) + ( integral (g,c,b))) by W0, W2, W3, W4, INTEGRA6: 17;

        set AB = ['(k + 1), ((k + 1) + 1)'];

        AB = [.(k + 1), ((k + 1) + 1).] by INTEGRA5:def 3, NAT_1: 11;

        then ( integral (g,AB)) < (1 / (k + 1)) by Diesel3;

        then ( integral (g,(k + 1),((k + 1) + 1))) < (1 / (k + 1)) by NAT_1: 11, INTEGRA5:def 4;

        then (( integral (g,1,(k + 1))) + ( integral (g,(k + 1),((k + 1) + 1)))) < (( Harmonic k) + (1 / (k + 1))) by s0, XREAL_1: 8;

        hence thesis by Harmon1, W1;

      end;

      

       KK: for n be non zero Nat holds P[n] from NAT_1:sch 10( I1, I2);

      ( integral (g,1,(n + 1))) < ( Harmonic n) by KK;

      hence thesis by KL, INTEGRA5:def 4, WA, XREAL_1: 31;

    end;

    theorem :: MOEBIUS3:23

    for n1,n2 be Nat st (n1 ^2 ) = (n2 ^2 ) holds n1 = n2

    proof

      let n1,n2 be Nat;

      assume (n1 ^2 ) = (n2 ^2 );

      then n1 = ( sqrt (n2 ^2 )) by SQUARE_1: 22;

      hence thesis by SQUARE_1: 22;

    end;

    registration

      let n be non trivial Nat;

      cluster (n ^2 ) -> non trivial;

      coherence

      proof

        n >= (1 + 1) by NAT_2: 29;

        then

         A1: n > 1 by NAT_1: 13;

        then (n ^2 ) > n by SQUARE_1: 14;

        hence thesis by NAT_2: 28, A1;

      end;

    end

    ::$Notion-Name

    theorem :: MOEBIUS3:24

    

     Telescoping: for a,b,s be Real_Sequence st (for n be Nat holds (s . n) = ((a . n) + (b . n))) & (for k be Nat holds (b . k) = ( - (a . (k + 1)))) holds for n be Nat holds (( Partial_Sums s) . n) = ((a . 0 ) + (b . n))

    proof

      let a,b,s be Real_Sequence;

      assume that

       Z1: (for n be Nat holds (s . n) = ((a . n) + (b . n))) and

       Z2: (for k be Nat holds (b . k) = ( - (a . (k + 1))));

      let n be Nat;

      defpred P[ Nat] means (( Partial_Sums s) . $1) = ((a . 0 ) + (b . $1));

      (( Partial_Sums s) . 0 ) = (s . 0 ) by SERIES_1:def 1

      .= ((a . 0 ) + (b . 0 )) by Z1;

      then

       A1: P[ 0 ];

      

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

      proof

        let k be Nat;

        assume P[k];

        

        then (( Partial_Sums s) . (k + 1)) = (((a . 0 ) + (b . k)) + (s . (k + 1))) by SERIES_1:def 1

        .= (((a . 0 ) + (b . k)) + ((a . (k + 1)) + (b . (k + 1)))) by Z1

        .= (((a . 0 ) + ( - (a . (k + 1)))) + ((a . (k + 1)) + (b . (k + 1)))) by Z2

        .= ((a . 0 ) + (b . (k + 1)));

        hence thesis;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: MOEBIUS3:25

    

     Impor3: for f1,f2 be Real_Sequence, n be non trivial Nat st (for k be non trivial Nat st k <= n holds (f1 . k) < (f2 . k)) holds ( Sum (f1,n,1)) < ( Sum (f2,n,1))

    proof

      let f1,f2 be Real_Sequence, n be non trivial Nat;

      assume

       A1: for k be non trivial Nat st k <= n holds (f1 . k) < (f2 . k);

      defpred X[ Nat] means (for k be non trivial Nat st k <= $1 holds (f1 . k) < (f2 . k)) implies ((( Partial_Sums f1) . $1) - (( Partial_Sums f1) . 1)) < ((( Partial_Sums f2) . $1) - (( Partial_Sums f2) . 1));

      (( Partial_Sums f1) . 2) = ((( Partial_Sums f1) . 1) + (f1 . (1 + 1))) & (( Partial_Sums f2) . 2) = ((( Partial_Sums f2) . 1) + (f2 . (1 + 1))) by SERIES_1:def 1;

      then

       a1: X[2];

      

       A2: for n be non trivial Nat st X[n] holds X[(n + 1)]

      proof

        let n be non trivial Nat such that

         A3: X[n];

        assume

         B1: for k be non trivial Nat st k <= (n + 1) holds (f1 . k) < (f2 . k);

        

         A4: (f1 . (n + 1)) < (f2 . (n + 1)) by B1;

        

         ZZ: (( Partial_Sums f1) . (n + 1)) = ((( Partial_Sums f1) . n) + (f1 . (n + 1))) & (( Partial_Sums f2) . (n + 1)) = ((( Partial_Sums f2) . n) + (f2 . (n + 1))) by SERIES_1:def 1;

        

         G1: n <= (n + 1) by NAT_1: 11;

        for k be non trivial Nat st k <= n holds (f1 . k) < (f2 . k)

        proof

          let k be non trivial Nat;

          assume k <= n;

          then k <= (n + 1) by G1, XXREAL_0: 2;

          hence thesis by B1;

        end;

        then ((f1 . (n + 1)) + ((( Partial_Sums f1) . n) - (( Partial_Sums f1) . 1))) < ((f2 . (n + 1)) + ((( Partial_Sums f2) . n) - (( Partial_Sums f2) . 1))) by A3, A4, XREAL_1: 8;

        hence thesis by ZZ;

      end;

      for n be non trivial Nat holds X[n] from NAT_2:sch 2( a1, A2);

      hence thesis by A1;

    end;

    begin

    definition

      :: MOEBIUS3:def2

      func Reci-seq1 -> Real_Sequence means

      : MyDef: for n be Nat holds (it . n) = (1 / ((n ^2 ) - (1 / 4)));

      existence

      proof

        deffunc F( Nat) = (1 / (($1 ^2 ) - (1 / 4)));

        ex f be Real_Sequence st for n be Nat holds (f . n) = F(n) from SEQ_1:sch 1;

        hence thesis;

      end;

      uniqueness

      proof

        deffunc F( Nat) = (1 / (($1 ^2 ) - (1 / 4)));

        let f1,f2 be Real_Sequence such that

         A1: (f1 . n) = F(n) and

         A2: (f2 . n) = F(n);

        let n be Element of NAT ;

        

        thus (f1 . n) = F(n) by A1

        .= (f2 . n) by A2;

      end;

    end

    theorem :: MOEBIUS3:26

    

     Tele1: for n be Nat holds ( Reci-seq1 . n) = ((1 / (n - (1 / 2))) - (1 / (n + (1 / 2))))

    proof

      let n be Nat;

      set a = (1 / 2);

       not (1 / 2) is Nat

      proof

        assume

         A4: (1 / 2) is Nat;

         0 <= (1 / 2) & (1 / 2) <= ( 0 + 1);

        hence thesis by A4, NAT_1: 9;

      end;

      then

       A2: (n - a) <> 0 ;

      ((1 / (n - a)) - (1 / (n + a))) = (((1 * (n + a)) / ((n - a) * (n + a))) - (1 / (n + a))) by XCMPLX_1: 91

      .= (((1 * (n + a)) / ((n - a) * (n + a))) - ((1 * (n - a)) / ((n + a) * (n - a)))) by A2, XCMPLX_1: 91

      .= (((n + a) - (n - a)) / ((n + a) * (n - a))) by XCMPLX_1: 120

      .= (1 / ((n ^2 ) - (1 / 4)));

      hence thesis by MyDef;

    end;

    

     AlgDef: for n be Nat, a,b be Real holds (( rseq ( 0 ,1,a,b)) . n) = (1 / ((a * n) + b))

    proof

      let n be Nat, a,b be Real;

      (( rseq ( 0 ,1,a,b)) . n) = ((( 0 * n) + 1) / ((a * n) + b)) by BASEL_1: 5;

      hence thesis;

    end;

    

     Tele2: for n be Nat holds ( Reci-seq1 . n) = ((( rseq ( 0 ,1,1,( - (1 / 2)))) . n) + (( - ( rseq ( 0 ,1,1,(1 / 2)))) . n))

    proof

      let n be Nat;

      

       A3: ( Reci-seq1 . n) = ((1 / (n - (1 / 2))) - (1 / (n + (1 / 2)))) by Tele1

      .= ((1 / (n - (1 / 2))) + ( - (1 / (n + (1 / 2)))));

      

       A1: (( rseq ( 0 ,1,1,( - (1 / 2)))) . n) = (1 / ((1 * n) + ( - (1 / 2)))) by AlgDef;

      (( - ( rseq ( 0 ,1,1,(1 / 2)))) . n) = ( - (( rseq ( 0 ,1,1,(1 / 2))) . n)) by VALUED_1: 8

      .= ( - (1 / ((1 * n) + (1 / 2)))) by AlgDef;

      hence thesis by A1, A3;

    end;

    theorem :: MOEBIUS3:27

     Reci-seq1 = (( rseq ( 0 ,1,1,( - (1 / 2)))) + ( - ( rseq ( 0 ,1,1,(1 / 2))))) by SEQ_1: 7, Tele2;

    theorem :: MOEBIUS3:28

    for n be Nat holds (( Partial_Sums Reci-seq1 ) . n) < ( - 2)

    proof

      let n be Nat;

      set s = Reci-seq1 ;

      set a = ( rseq ( 0 ,1,1,( - (1 / 2))));

      set b = ( - ( rseq ( 0 ,1,1,(1 / 2))));

      

       ff: for k be Nat holds (b . k) = ( - (a . (k + 1)))

      proof

        let k be Nat;

        (b . k) = ( - (( rseq ( 0 ,1,1,(1 / 2))) . k)) by VALUED_1: 8

        .= ( - (1 / ((1 * k) + (1 / 2)))) by AlgDef

        .= ( - (1 / ((1 * (k + 1)) + ( - (1 / 2)))))

        .= ( - (a . (k + 1))) by AlgDef;

        hence thesis;

      end;

      

       w3: (a . 0 ) = (1 / ((1 * 0 ) + ( - (1 / 2)))) by AlgDef

      .= ( - 2);

      (b . n) = ( - (( rseq ( 0 ,1,1,(1 / 2))) . n)) by VALUED_1: 8

      .= ( - (1 / ((1 * n) + (1 / 2)))) by AlgDef

      .= ( - (1 / (n + (1 / 2))));

      then (( - 2) + (b . n)) < (( - 2) + 0 ) by XREAL_1: 8;

      hence thesis by w3, ff, Telescoping, Tele2;

    end;

    theorem :: MOEBIUS3:29

    

     Seq3: for n be Nat holds ( Sum ( Reci-seq1 ,n,1)) < (2 / 3)

    proof

      let n be Nat;

      set s = Reci-seq1 ;

      set a = ( rseq ( 0 ,1,1,( - (1 / 2))));

      set b = ( - ( rseq ( 0 ,1,1,(1 / 2))));

      

       ff: for k be Nat holds (b . k) = ( - (a . (k + 1)))

      proof

        let k be Nat;

        (b . k) = ( - (( rseq ( 0 ,1,1,(1 / 2))) . k)) by VALUED_1: 8

        .= ( - (1 / ((1 * k) + (1 / 2)))) by AlgDef

        .= ( - (1 / ((1 * (k + 1)) + ( - (1 / 2)))))

        .= ( - (a . (k + 1))) by AlgDef;

        hence thesis;

      end;

      

       W2: (a . 0 ) = (1 / ((1 * 0 ) + ( - (1 / 2)))) by AlgDef

      .= ( - 2);

      

       V1: (a . 1) = (1 / ((1 * 1) + ( - (1 / 2)))) by AlgDef

      .= 2;

      

       V2: (b . 0 ) = ( - (( rseq ( 0 ,1,1,(1 / 2))) . 0 )) by VALUED_1: 8

      .= ( - (1 / ((1 * 0 ) + (1 / 2)))) by AlgDef

      .= ( - 2);

      

       V3: (b . 1) = ( - (( rseq ( 0 ,1,1,(1 / 2))) . 1)) by VALUED_1: 8

      .= ( - (1 / ((1 * 1) + (1 / 2)))) by AlgDef

      .= ( - (2 / 3));

      (s . 0 ) = ((a . 0 ) + (b . 0 )) by Tele2;

      

      then

       V4: ((s . 0 ) + (s . 1)) = (((a . 0 ) + (b . 0 )) + ((a . 1) + (b . 1))) by Tele2

      .= (( - 2) + ( - (2 / 3))) by V1, V3, W2, V2;

      

       V5: (( Partial_Sums s) . 1) = ((( Partial_Sums s) . 0 ) + (s . ( 0 + 1))) by SERIES_1:def 1

      .= (( - 2) + ( - (2 / 3))) by V4, SERIES_1:def 1;

      

       W1: (b . n) = ( - (( rseq ( 0 ,1,1,(1 / 2))) . n)) by VALUED_1: 8

      .= ( - (1 / ((1 * n) + (1 / 2)))) by AlgDef

      .= ( - (1 / (n + (1 / 2))));

      

       W3: (( Partial_Sums s) . n) = (( - 2) + (b . n)) by W2, ff, Telescoping, Tele2;

      ((b . n) + (2 / 3)) < ( 0 + (2 / 3)) by XREAL_1: 8, W1;

      hence thesis by W3, V5;

    end;

    registration

      cluster Basel-seq -> summable;

      coherence

      proof

        for n be Nat st n >= 1 holds ( Basel-seq . n) = (1 / (n to_power 2))

        proof

          let n be Nat;

          assume n >= 1;

          ( Basel-seq . n) = (1 / (n ^2 )) by BASEL_1: 31

          .= (1 / (n to_power 2)) by NEWTON: 81;

          hence thesis;

        end;

        hence thesis by SERIES_1: 32;

      end;

    end

    theorem :: MOEBIUS3:30

    for n be Nat holds (( Partial_Sums Reci-seq1 ) . n) = (( - 2) + ( - (1 / (n + (1 / 2)))))

    proof

      let n be Nat;

      set s = Reci-seq1 ;

      set a = ( rseq ( 0 ,1,1,( - (1 / 2))));

      set b = ( - ( rseq ( 0 ,1,1,(1 / 2))));

      

       ff: for k be Nat holds (b . k) = ( - (a . (k + 1)))

      proof

        let k be Nat;

        (b . k) = ( - (( rseq ( 0 ,1,1,(1 / 2))) . k)) by VALUED_1: 8

        .= ( - (1 / ((1 * k) + (1 / 2)))) by AlgDef

        .= ( - (1 / ((1 * (k + 1)) + ( - (1 / 2)))))

        .= ( - (a . (k + 1))) by AlgDef;

        hence thesis;

      end;

      

       W2: (a . 0 ) = (1 / ((1 * 0 ) + ( - (1 / 2)))) by AlgDef

      .= ( - 2);

      (b . n) = ( - (( rseq ( 0 ,1,1,(1 / 2))) . n)) by VALUED_1: 8

      .= ( - (1 / ((1 * n) + (1 / 2)))) by AlgDef

      .= ( - (1 / (n + (1 / 2))));

      hence thesis by W2, ff, Telescoping, Tele2;

    end;

    theorem :: MOEBIUS3:31

    

     Impor2: for n be non trivial Nat holds ( Sum ( Basel-seq ,n,1)) < ( Sum ( Reci-seq1 ,n,1))

    proof

      let n be non trivial Nat;

      for k be non trivial Nat st k <= n holds ( Basel-seq . k) < ( Reci-seq1 . k)

      proof

        let k be non trivial Nat;

        assume k <= n;

        

         Z1: ( Basel-seq . k) = (1 / (k ^2 )) by BASEL_1: 31;

        

         Z2: ( Reci-seq1 . k) = (1 / ((k ^2 ) - (1 / 4))) by MyDef;

        k >= (1 + 1) by NAT_2: 29;

        then k > 1 by NAT_1: 13;

        then (k ^2 ) > (1 ^2 ) by SQUARE_1: 16;

        then ((k ^2 ) - (1 / 4)) > (1 - (1 / 4)) by XREAL_1: 14;

        then ((k ^2 ) - (1 / 4)) > (3 / 4);

        hence thesis by Z1, Z2, XREAL_1: 76, XREAL_1: 44;

      end;

      hence thesis by Impor3;

    end;

    theorem :: MOEBIUS3:32

    

     Important: for n be non trivial Nat holds ( Sum ( Basel-seq ,n)) < (5 / 3)

    proof

      let n be non trivial Nat;

      

       Z2: ( Sum ( Basel-seq ,n)) = ((( Partial_Sums Basel-seq ) . ( 0 + 1)) + ((( Partial_Sums Basel-seq ) . n) - (( Partial_Sums Basel-seq ) . 1)))

      .= (((( Partial_Sums Basel-seq ) . 0 ) + ( Basel-seq . 1)) + ((( Partial_Sums Basel-seq ) . n) - (( Partial_Sums Basel-seq ) . 1))) by SERIES_1:def 1

      .= ((( Basel-seq . 0 ) + ( Basel-seq . 1)) + ((( Partial_Sums Basel-seq ) . n) - (( Partial_Sums Basel-seq ) . 1))) by SERIES_1:def 1

      .= (((1 / ( 0 ^2 )) + ( Basel-seq . 1)) + ( Sum ( Basel-seq ,n,1))) by BASEL_1: 31

      .= (((1 / 0 ) + (1 / (1 ^2 ))) + ( Sum ( Basel-seq ,n,1))) by BASEL_1: 31

      .= (1 + ( Sum ( Basel-seq ,n,1)));

      

       Z5: ( Sum ( Basel-seq ,n)) < (1 + ( Sum ( Reci-seq1 ,n,1))) by Z2, XREAL_1: 8, Impor2;

      (1 + ( Sum ( Reci-seq1 ,n,1))) < (1 + (2 / 3)) by XREAL_1: 8, Seq3;

      hence thesis by Z5, XXREAL_0: 2;

    end;

    theorem :: MOEBIUS3:33

    (( Partial_Sums Basel-seq ) . n) < (5 / 3)

    proof

      per cases by NAT_2: 28;

        suppose n is non trivial;

        then ( Sum ( Basel-seq ,n)) < (5 / 3) by Important;

        hence thesis;

      end;

        suppose n = 0 ;

        

        then (( Partial_Sums Basel-seq ) . n) = ( Basel-seq . 0 ) by SERIES_1:def 1

        .= (1 / ( 0 ^2 )) by BASEL_1: 31

        .= 0 ;

        hence thesis;

      end;

        suppose

         F: n = 1;

        (( Partial_Sums Basel-seq ) . ( 0 + 1)) = ((( Partial_Sums Basel-seq ) . 0 ) + ( Basel-seq . 1)) by SERIES_1:def 1

        .= (( Basel-seq . 0 ) + ( Basel-seq . 1)) by SERIES_1:def 1

        .= ((1 / ( 0 ^2 )) + ( Basel-seq . 1)) by BASEL_1: 31

        .= ( 0 + ( Basel-seq . 1))

        .= ( 0 + (1 / (1 ^2 ))) by BASEL_1: 31

        .= 1;

        hence thesis by F;

      end;

    end;

    definition

      :: MOEBIUS3:def3

      func Reci-seq2 -> Real_Sequence means

      : My3Def: for n be Nat holds (it . n) = (1 + (1 / ( primenumber n)));

      existence

      proof

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

        ex f be Real_Sequence st for n be Nat holds (f . n) = F(n) from SEQ_1:sch 1;

        hence thesis;

      end;

      uniqueness

      proof

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

        let f1,f2 be Real_Sequence such that

         A1: (f1 . n) = F(n) and

         A2: (f2 . n) = F(n);

        let n be Element of NAT ;

        

        thus (f1 . n) = F(n) by A1

        .= (f2 . n) by A2;

      end;

    end

    theorem :: MOEBIUS3:34

    ( Sum ( Sgm {1})) = 1

    proof

      ( Sum <*1*>) = 1;

      hence thesis by FINSEQ_3: 44;

    end;

    definition

      let n be Nat;

      :: MOEBIUS3:def4

      func SetPrimes n -> Subset of NAT equals ( SetPrimes /\ ( Seg n));

      coherence ;

    end

    registration

      let n be Nat;

      cluster ( SetPrimes n) -> finite;

      coherence ;

    end

    theorem :: MOEBIUS3:35

    for m,n be Nat st m <= n holds ( SetPrimes m) c= ( SetPrimes n) by XBOOLE_1: 26, FINSEQ_1: 5;

    theorem :: MOEBIUS3:36

    

     PrimesSet: not (n + 1) is Prime implies ( SetPrimes (n + 1)) = ( SetPrimes n)

    proof

      

       A1: ( SetPrimes (n + 1)) = ( SetPrimes /\ (( Seg n) \/ {(n + 1)})) by FINSEQ_1: 9

      .= (( SetPrimes n) \/ ( SetPrimes /\ {(n + 1)})) by XBOOLE_1: 23;

      assume not (n + 1) is Prime;

      then not (n + 1) in SetPrimes by NEWTON:def 6;

      then ( SetPrimes /\ {(n + 1)}) = {} by XBOOLE_0:def 7, ZFMISC_1: 50;

      hence ( SetPrimes (n + 1)) = ( SetPrimes n) by A1;

    end;

    theorem :: MOEBIUS3:37

    

     SetPrime1: ( SetPrimes 0 ) = {} & ( SetPrimes 1) = {}

    proof

       not ( 0 + 1) is Prime by INT_2:def 4;

      then ( SetPrimes ( 0 + 1)) = ( SetPrimes 0 ) by PrimesSet;

      hence thesis;

    end;

    theorem :: MOEBIUS3:38

    

     PrimesSet2: (n + 1) is Prime implies ( SetPrimes (n + 1)) = (( SetPrimes n) \/ {(n + 1)})

    proof

      

       A1: ( SetPrimes (n + 1)) = ( SetPrimes /\ (( Seg n) \/ {(n + 1)})) by FINSEQ_1: 9

      .= (( SetPrimes n) \/ ( SetPrimes /\ {(n + 1)})) by XBOOLE_1: 23;

      assume (n + 1) is Prime;

      then (n + 1) in SetPrimes by NEWTON:def 6;

      hence thesis by A1, ZFMISC_1: 46;

    end;

    theorem :: MOEBIUS3:39

    

     P1NotPrime: for p be Prime st p > 2 holds not (p + 1) is Prime

    proof

      let p be Prime;

      assume

       S1: p > 2;

      then (p + 1) > (2 + 1) by XREAL_1: 8;

      then

       S3: (p + 1) > 2 by XXREAL_0: 2;

      p is odd by S1, PEPIN: 17;

      hence thesis by S3, PEPIN: 17;

    end;

    theorem :: MOEBIUS3:40

    

     Set2: ( SetPrimes 2) = {2}

    proof

       not 1 is Prime by INT_2:def 4;

      then

       A1: not 1 in SetPrimes by NEWTON:def 6;

      2 in SetPrimes by NEWTON:def 6, INT_2: 28;

      hence thesis by ZFMISC_1: 54, A1, FINSEQ_1: 2;

    end;

    theorem :: MOEBIUS3:41

     not (n + 1) in ( SetPrimes n)

    proof

      assume (n + 1) in ( SetPrimes n);

      then (n + 1) in ( Seg n) by XBOOLE_0:def 4;

      then (n + 1) <= n by FINSEQ_1: 1;

      hence thesis by NAT_1: 13;

    end;

    definition

      let n be Nat;

      :: MOEBIUS3:def5

      func indexp n -> Nat equals ( card ( SetPrimes n));

      coherence ;

    end

    theorem :: MOEBIUS3:42

    

     Krzys1: for n be Nat holds ( indexp n) <= n

    proof

      let n be Nat;

      ( card ( SetPrimes n)) <= ( card ( Seg n)) by NAT_1: 43, XBOOLE_1: 17;

      hence thesis;

    end;

    begin

    theorem :: MOEBIUS3:43

    for n be non zero Nat holds n = (( TSqF n) * (n div ( TSqF n)))

    proof

      let n be non zero Nat;

      ( TSqF n) divides n by MOEBIUS2: 53;

      then

       A2: (n mod ( TSqF n)) = 0 by INT_1: 62;

      set i2 = ( TSqF n);

      n = (((n div i2) * i2) + (n mod i2)) by INT_1: 59

      .= ((n div i2) * i2) by A2;

      hence thesis;

    end;

    theorem :: MOEBIUS3:44

    

     Skup: for n be non zero Nat holds (( SqF n) |^ 2) divides n

    proof

      deffunc F( non zero Nat) = (( Product ( SqFactors $1)) |^ 2);

      deffunc F1( non zero Nat) = ( Product ( SqFactors $1));

      deffunc G( non zero Nat) = ( SqFactors $1);

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

      let n be non zero Nat;

      

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

      

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

      .= ( support G(n)) by MOEBIUS2:def 3;

      

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

      proof

        let k be Nat;

        assume

         A4: P[k];

        let n be non zero Nat such that

         A5: ( support G(n)) c= ( Seg (k + 1));

        

         A6: ( support ( pfexp n)) = ( support G(n)) by MOEBIUS2:def 3;

        per cases ;

          suppose

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

          set p = (k + 1);

          set e = (p |-count n);

          set s = (p |^ e);

           A8:

          now

            assume

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

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

            proof

              let x be object;

              assume

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

              then

              reconsider m = x as Nat;

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

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

              then

               A11: m <= k by NAT_1: 13;

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

              then 1 <= m by INT_2:def 4;

              hence thesis by A11, FINSEQ_1: 1;

            end;

            hence contradiction by A7;

          end;

          then

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

          then

           A13: p > 1 by INT_2:def 4;

          then s divides n by NAT_3:def 7;

          then

          consider t be Nat such that

           A14: n = (s * t);

          reconsider s, t as non zero Nat by A14;

          consider f be FinSequence of COMPLEX such that

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

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

          

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

          

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

          then

           A19: ( support ( ppf s)) = ( support G(s)) by MOEBIUS2:def 3;

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

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

          then

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

          then

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

          

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

          proof

            set f = (p |-count t);

            let x be object;

            assume

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

            then

            reconsider m = x as Nat;

            

             A25: x in ( support ( pfexp t)) by A24, MOEBIUS2:def 3;

             A26:

            now

              assume

               A27: m = p;

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

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

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

              then

              consider g be Nat such that

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

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

              then

              consider u be Nat such that

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

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

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

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

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

              hence contradiction by A13, NAT_3:def 7;

            end;

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

            then ( support G(t)) c= ( support G(n)) by A6, MOEBIUS2:def 3;

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

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

            then m < p by A26, XXREAL_0: 1;

            then

             A30: m <= k by NAT_1: 13;

            x is Prime by A25, NAT_3: 34;

            then 1 <= m by INT_2:def 4;

            hence thesis by A30, FINSEQ_1: 1;

          end;

          then

           A31: F(t) divides t by A4;

          ( support G(s)) = {p} by A18, A21, MOEBIUS2:def 3;

          

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

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

          

          then

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

          .= (p |^ ((p |-count s) div 2)) by A22, MOEBIUS2:def 3;

          

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

          set j = (p |-count s);

          j = ((2 * (j div 2)) + (j mod 2)) by NAT_D: 2;

          then

           Sb: (2 * (j div 2)) <= j by NAT_1: 11;

          ((p |^ ((p |-count s) div 2)) |^ 2) = (p |^ (((p |-count s) div 2) * 2)) by NEWTON: 9;

          then

           ZZ: ((p |^ ((p |-count s) div 2)) |^ 2) divides (p |^ e) by Sb, NEWTON: 89, H2, XXREAL_0: 2;

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

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

          then

           A33: ( support ( ppf t)) = ( support G(t)) by MOEBIUS2:def 3;

           A34:

          now

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

            then

            consider x be object such that

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

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

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

            then

             A37: x in ( support G(t)) by MOEBIUS2:def 3;

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

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

            hence contradiction by NAT_1: 13;

          end;

          (s1,t1) are_coprime

          proof

            set u = (s1 gcd t1);

            

             A38: u divides t1 by NAT_D:def 5;

            

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

            assume not (s1,t1) are_coprime ;

            then u > 1 by A39, XXREAL_0: 1;

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

            then

            consider r be Element of NAT such that

             A40: r is prime and

             A41: r divides u by INT_2: 31;

            u divides s1 by NAT_D:def 5;

            then r divides s1 by A41, NAT_D: 4;

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

            then p in ( support ( pfexp t)) by NAT_3: 37, A40, A41, A38, NAT_D: 4;

            then p in ( support G(t)) by MOEBIUS2:def 3;

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

            hence contradiction by NAT_1: 13;

          end;

          

          then F(n) = (( Product ( G(s) + G(t))) |^ 2) by A14, MOEBIUS2: 44

          .= (( F1(s) * F1(t)) |^ 2) by A34, A19, A33, NAT_3: 19

          .= ( F(s) * F(t)) by NEWTON: 7;

          hence thesis by A14, h1, ZZ, A31, NAT_3: 1;

        end;

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

          hence thesis by A4;

        end;

      end;

      

       A42: P[ 0 ]

      proof

        let n be non zero Nat;

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

        then ( support G(n)) = {} ;

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

        

        then F(n) = (1 |^ 2) by NAT_3: 20

        .= 1;

        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 :: MOEBIUS3:45

    

     KeyValue: for m be finite-support natural-valued ManySortedSet of SetPrimes , p be Prime st ( support m) = {p} holds ( Product m) = (m . p)

    proof

      let m be finite-support natural-valued ManySortedSet of SetPrimes , p be Prime;

      assume

       A1: ( support m) = {p};

      consider f be FinSequence of COMPLEX such that

       A15: ( Product m) = ( Product f) and

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

      

       Z1: (m * <*p*>) = <*(m . p)*>

      proof

        

         D1: ( rng <*p*>) = {p} by FINSEQ_1: 39;

        

         d2: p in SetPrimes by NEWTON:def 6;

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

        

        then

         B1: ( dom (m * <*p*>)) = ( dom <*p*>) by D1, d2, RELAT_1: 27, ZFMISC_1: 31

        .= ( Seg 1) by FINSEQ_1: 38;

        

         B2: ( dom (m * <*p*>)) = ( dom <*(m . p)*>) by B1, FINSEQ_1: 38;

        for x be object st x in ( dom (m * <*p*>)) holds ((m * <*p*>) . x) = ( <*(m . p)*> . x)

        proof

          let x be object;

          assume

           C1: x in ( dom (m * <*p*>));

          then

           C2: x = 1 by B1, TARSKI:def 1, FINSEQ_1: 2;

          

          then ((m * <*p*>) . x) = (m . ( <*p*> . 1)) by FUNCT_1: 12, C1

          .= ( <*(m . p)*> . x) by C2;

          hence thesis;

        end;

        hence thesis by B2, FUNCT_1: 2;

      end;

      f = <*(m . p)*> by Z1, FINSEQ_1: 94, A16, A1;

      hence thesis by RVSUM_1: 95, A15;

    end;

    theorem :: MOEBIUS3:46

    

     Cosik: for n be non zero Nat holds (( SqF n) |^ 2) = ( TSqF n)

    proof

      deffunc F( non zero Nat) = (( Product ( SqFactors $1)) |^ 2);

      deffunc F1( non zero Nat) = ( Product ( SqFactors $1));

      deffunc G( non zero Nat) = ( SqFactors $1);

      deffunc H( non zero Nat) = ( Product ( TSqFactors $1));

      defpred P[ Nat] means for n be non zero Nat st ( support G(n)) c= ( Seg $1) holds F(n) = H(n);

      let n be non zero Nat;

      

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

      

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

      .= ( support G(n)) by MOEBIUS2:def 3;

      

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

      proof

        let k be Nat;

        assume

         A4: P[k];

        let n be non zero Nat such that

         A5: ( support G(n)) c= ( Seg (k + 1));

        

         A6: ( support ( pfexp n)) = ( support G(n)) by MOEBIUS2:def 3;

        per cases ;

          suppose

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

          set p = (k + 1);

          set e = (p |-count n);

          set s = (p |^ e);

           A8:

          now

            assume

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

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

            proof

              let x be object;

              assume

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

              then

              reconsider m = x as Nat;

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

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

              then

               A11: m <= k by NAT_1: 13;

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

              then 1 <= m by INT_2:def 4;

              hence thesis by A11, FINSEQ_1: 1;

            end;

            hence contradiction by A7;

          end;

          then

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

          then

           A13: p > 1 by INT_2:def 4;

          then s divides n by NAT_3:def 7;

          then

          consider t be Nat such that

           A14: n = (s * t);

          reconsider s, t as non zero Nat by A14;

          consider f be FinSequence of COMPLEX such that

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

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

          

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

          

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

          then

           A19: ( support ( ppf s)) = ( support G(s)) by MOEBIUS2:def 3;

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

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

          then

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

          then

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

          

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

          proof

            set f = (p |-count t);

            let x be object;

            assume

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

            then

            reconsider m = x as Nat;

            

             A25: x in ( support ( pfexp t)) by A24, MOEBIUS2:def 3;

             A26:

            now

              assume

               A27: m = p;

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

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

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

              then

              consider g be Nat such that

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

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

              then

              consider u be Nat such that

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

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

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

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

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

              hence contradiction by A13, NAT_3:def 7;

            end;

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

            then ( support G(t)) c= ( support G(n)) by A6, MOEBIUS2:def 3;

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

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

            then m < p by A26, XXREAL_0: 1;

            then

             A30: m <= k by NAT_1: 13;

            x is Prime by A25, NAT_3: 34;

            then 1 <= m by INT_2:def 4;

            hence thesis by A30, FINSEQ_1: 1;

          end;

          then

           A31: F(t) = H(t) by A4;

          

           a21: ( support G(s)) = {p} by A18, A21, MOEBIUS2:def 3;

          

           Aa1: ( support ( TSqFactors s)) = {p} by A18, A21, MOEBIUS2:def 8;

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

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

          

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

          .= (p |^ ((p |-count s) div 2)) by A22, MOEBIUS2:def 3;

          

          then

           aa1: (( Product G(s)) |^ 2) = (p |^ (2 * ((p |-count s) div 2))) by NEWTON: 9

          .= (( TSqFactors s) . p) by A22, MOEBIUS2:def 8

          .= ( Product ( TSqFactors s)) by A12, KeyValue, Aa1;

          set j = (p |-count s);

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

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

          then

           A33: ( support ( ppf t)) = ( support G(t)) by MOEBIUS2:def 3;

           A34:

          now

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

            then

            consider x be object such that

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

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

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

            then

             A37: x in ( support G(t)) by MOEBIUS2:def 3;

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

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

            hence contradiction by NAT_1: 13;

          end;

          

           ZZ: (s1,t1) are_coprime

          proof

            set u = (s1 gcd t1);

            

             A38: u divides t1 by NAT_D:def 5;

            

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

            assume not (s1,t1) are_coprime ;

            then u > 1 by A39, XXREAL_0: 1;

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

            then

            consider r be Element of NAT such that

             A40: r is prime and

             A41: r divides u by INT_2: 31;

            u divides s1 by NAT_D:def 5;

            then r divides s1 by A41, NAT_D: 4;

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

            then p in ( support ( pfexp t)) by NAT_3: 37, A40, A41, A38, NAT_D: 4;

            then p in ( support G(t)) by MOEBIUS2:def 3;

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

            hence contradiction by NAT_1: 13;

          end;

          ( support ( TSqFactors s)) = ( support ( pfexp s)) & ( support ( TSqFactors t)) = ( support ( pfexp t)) by MOEBIUS2:def 8;

          then

           za: ( support ( TSqFactors s)) = ( support ( ppf s)) & ( support ( TSqFactors t)) = ( support ( ppf t)) by NAT_3:def 9;

           F(n) = (( Product ( G(s) + G(t))) |^ 2) by A14, MOEBIUS2: 44, ZZ

          .= (( F1(s) * F1(t)) |^ 2) by A34, A19, A33, NAT_3: 19

          .= (( F1(s) |^ 2) * ( F1(t) |^ 2)) by NEWTON: 7

          .= ( Product (( TSqFactors s) + ( TSqFactors t))) by za, NAT_3: 19, aa1, A31, A34

          .= H(n) by A14, ZZ, MOEBIUS2: 52;

          hence thesis;

        end;

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

          hence thesis by A4;

        end;

      end;

      

       A42: P[ 0 ]

      proof

        let n be non zero Nat;

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

        then

         J1: ( support G(n)) = {} ;

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

        

        then

         BB: F(n) = (1 |^ 2) by NAT_3: 20

        .= 1;

        ( support ( TSqFactors n)) = ( support ( pfexp n)) by MOEBIUS2:def 8

        .= ( support G(n)) by MOEBIUS2:def 3;

        then ( TSqFactors n) = ( EmptyBag SetPrimes ) by PRE_POLY: 81, J1;

        hence thesis by BB, NAT_3: 20;

      end;

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

      hence thesis by A1, A2;

    end;

    registration

      let n be non zero Nat;

      cluster (n div (( SqF n) |^ 2)) -> square-free;

      coherence

      proof

        set TS = (( SqF n) |^ 2);

        TS = ( TSqF n) by Cosik;

        hence thesis;

      end;

    end

    definition

      let n be non zero Nat;

      :: MOEBIUS3:def6

      func SquarefreePart n -> non zero Nat equals (n div ( TSqF n));

      coherence

      proof

        (( SqF n) |^ 2) divides n by Skup;

        then ( TSqF n) divides n by Cosik;

        then n = (( TSqF n) * (n div ( TSqF n))) by NAT_D: 3;

        hence thesis;

      end;

    end

    registration

      let n be non zero Nat;

      cluster ( SquarefreePart n) -> square-free;

      coherence ;

    end

    theorem :: MOEBIUS3:47

    

     Canonical: for n be non zero Nat holds n = (( SquarefreePart n) * (( SqF n) ^2 ))

    proof

      let n be non zero Nat;

      (( SqF n) |^ 2) divides n by Skup;

      then ( TSqF n) divides n by Cosik;

      

      then n = (( TSqF n) * (n div ( TSqF n))) by NAT_D: 3

      .= ((( SqF n) |^ 2) * (n div ( TSqF n))) by Cosik

      .= ((( SqF n) ^2 ) * (n div ( TSqF n))) by NEWTON: 81;

      hence thesis;

    end;

    theorem :: MOEBIUS3:48

    for n be non zero Nat holds ( support ( pfexp n)) c= ( Seg n)

    proof

      let n be non zero Nat;

      let x be object;

      assume

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

      then

      reconsider k = x as Prime by NAT_3: 34;

      

       A3: 1 < k by INT_2:def 4;

      k <= n by NAT_D: 7, A1, NAT_3: 36;

      hence thesis by FINSEQ_1: 1, A3;

    end;

    theorem :: MOEBIUS3:49

    for n be non zero Nat holds ( support ( ppf n)) c= ( Seg n)

    proof

      let n be non zero Nat;

      let x be object;

      assume x in ( support ( ppf n));

      then

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

      then

      reconsider k = x as Prime by NAT_3: 34;

      

       A3: 1 < k by INT_2:def 4;

      k <= n by NAT_D: 7, A1, NAT_3: 36;

      hence thesis by FINSEQ_1: 1, A3;

    end;

    theorem :: MOEBIUS3:50

    for n be non zero Nat holds ( Seg ( SquarefreePart n)) c= ( Seg n)

    proof

      let n be non zero Nat;

      n = (( SquarefreePart n) * (( SqF n) ^2 )) by Canonical;

      then ( SquarefreePart n) divides n;

      then ( SquarefreePart n) <= n by NAT_D: 7;

      hence thesis by FINSEQ_1: 5;

    end;

    

     Surprise: for n,m be non zero Nat st (m ^2 ) divides ( SquarefreePart n) holds m = 1

    proof

      let n,m be non zero Nat;

      assume

       A0: (m ^2 ) divides ( SquarefreePart n);

      assume m <> 1;

      then

      consider p be Prime such that

       A1: p divides m by MOEBIUS1: 5;

      p in NAT & m in NAT by ORDINAL1:def 12;

      then (p ^2 ) divides (m ^2 ) by A1, PYTHTRIP: 6;

      then (p ^2 ) divides ( SquarefreePart n) by A0, NAT_D: 4;

      then (p |^ 2) divides ( SquarefreePart n) by NEWTON: 81;

      then (1 + 1) <= (p |-count ( SquarefreePart n)) by MOEBIUS2: 40;

      hence thesis by MOEBIUS1: 24, NAT_1: 13;

    end;

    theorem :: MOEBIUS3:51

    for k,n be non zero Nat holds (k ^2 ) divides ( SquarefreePart n) iff k = 1 by Surprise, NAT_D: 6;

    theorem :: MOEBIUS3:52

    for m,n be non zero Nat st ( SquarefreePart n) = ( SquarefreePart m) & ( TSqF m) = ( TSqF n) holds m = n

    proof

      let m,n be non zero Nat;

      assume

       A1: ( SquarefreePart n) = ( SquarefreePart m) & ( TSqF m) = ( TSqF n);

      m = (( SquarefreePart m) * (( SqF m) ^2 )) by Canonical

      .= (( SquarefreePart m) * (( SqF m) |^ 2)) by NEWTON: 81

      .= (( SquarefreePart n) * ( TSqF n)) by A1, Cosik

      .= (( SquarefreePart n) * (( SqF n) |^ 2)) by Cosik

      .= (( SquarefreePart n) * (( SqF n) ^2 )) by NEWTON: 81

      .= n by Canonical;

      hence thesis;

    end;

    begin

    definition

      let A be finite Subset of SetPrimes ;

      :: MOEBIUS3:def7

      func A -bag -> bag of SetPrimes equals (( EmptyBag SetPrimes ) +* ( id A));

      coherence

      proof

        set f = (( EmptyBag SetPrimes ) +* ( id A));

        ( dom f) = (( dom ( EmptyBag SetPrimes )) \/ ( dom ( id A))) by FUNCT_4:def 1

        .= ( SetPrimes \/ ( dom ( id A))) by PARTFUN1:def 2

        .= SetPrimes by XBOOLE_1: 12;

        then

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

        ( support f) c= A

        proof

          let x be object;

          assume

           a10: x in ( support f);

          x in A

          proof

            assume not x in A;

            then not x in ( dom ( id A));

            

            then (f . x) = (( EmptyBag SetPrimes ) . x) by FUNCT_4: 11

            .= 0 by PBOOLE: 5;

            hence thesis by a10, PRE_POLY:def 7;

          end;

          hence thesis;

        end;

        hence thesis by PRE_POLY:def 8;

      end;

    end

    theorem :: MOEBIUS3:53

    

     BagSupport: for A be finite Subset of SetPrimes holds ( support (A -bag )) = A

    proof

      let A be finite Subset of SetPrimes ;

      set f = (A -bag );

      

       B1: ( support f) c= A

      proof

        let x be object;

        assume

         a10: x in ( support f);

        x in A

        proof

          assume not x in A;

          then not x in ( dom ( id A));

          

          then (f . x) = (( EmptyBag SetPrimes ) . x) by FUNCT_4: 11

          .= 0 by PBOOLE: 5;

          hence thesis by a10, PRE_POLY:def 7;

        end;

        hence thesis;

      end;

      A c= ( support f)

      proof

        let x be object;

        assume

         E1: x in A;

        then x in ( dom ( id A));

        

        then (f . x) = (( id A) . x) by FUNCT_4: 13

        .= x by E1, FUNCT_1: 17;

        then (f . x) is Prime by NEWTON:def 6, E1;

        hence thesis by PRE_POLY:def 7;

      end;

      hence thesis by B1, XBOOLE_0:def 10;

    end;

    theorem :: MOEBIUS3:54

    for A be finite Subset of SetPrimes st A = {} holds (A -bag ) = ( EmptyBag SetPrimes )

    proof

      let A be finite Subset of SetPrimes ;

      assume A = {} ;

      then ( support (A -bag )) = {} by BagSupport;

      hence thesis by PRE_POLY: 81;

    end;

    theorem :: MOEBIUS3:55

    

     BagValue: for A be finite Subset of SetPrimes holds for i be object st i in ( support (A -bag )) holds ((A -bag ) . i) = i

    proof

      let A be finite Subset of SetPrimes ;

      let i be object;

      assume

       aa: i in ( support (A -bag ));

      then

       A2: i in A by BagSupport;

      

       A1: i in ( dom ( id A)) by aa, BagSupport;

      ((A -bag ) . i) = (( id A) . i) by A1, FUNCT_4: 13

      .= i by A2, FUNCT_1: 17;

      hence thesis;

    end;

    theorem :: MOEBIUS3:56

    for A,B be finite Subset of SetPrimes st (A -bag ) = (B -bag ) holds A = B

    proof

      let A,B be finite Subset of SetPrimes ;

      assume (A -bag ) = (B -bag );

      then A = ( support (B -bag )) by BagSupport;

      hence thesis by BagSupport;

    end;

    registration

      let A be finite Subset of SetPrimes ;

      cluster (A -bag ) -> prime-factorization-like;

      coherence

      proof

        for x be Prime st x in ( support (A -bag )) holds ex n be Nat st 0 < n & ((A -bag ) . x) = (x |^ n)

        proof

          let x be Prime;

          assume x in ( support (A -bag ));

          then ((A -bag ) . x) = (x |^ 1) by BagValue;

          hence thesis;

        end;

        hence thesis by INT_7:def 1;

      end;

    end

    

     ProdSqF: for A be finite Subset of SetPrimes holds ( Product (A -bag )) is square-free

    proof

      let A be finite Subset of SetPrimes ;

      set n = ( Product (A -bag ));

      reconsider n as non zero Nat by MOEBIUS2: 26;

      

       C2: ( Product (A -bag )) = ( Product ( ppf n)) by NAT_3: 61;

      

       ZW: ( ppf n) = (A -bag ) by INT_7: 15, C2;

       not ex p be Prime st (p |^ 2) divides n

      proof

        given p1 be Prime such that

         K1: (p1 |^ 2) divides n;

        

         K2: (p1 |-count (p1 |^ 2)) <= (p1 |-count n) by NAT_3: 30, K1;

        set m = (p1 |-count n);

        

         W2: m >= 2 by K2, NAT_3: 25, INT_2:def 4;

        (p1 |^ 1) divides (p1 |^ 2) by NEWTON: 89;

        then

         V1: p1 in ( support ( pfexp n)) by NAT_3: 37, K1, NAT_D: 4;

        then

         W1: (( ppf n) . p1) = (p1 |^ m) by NAT_3:def 9;

        p1 in ( support ( ppf n)) by V1, NAT_3:def 9;

        then p1 = (p1 |^ m) by W1, BagValue, ZW;

        hence thesis by PREPOWER: 13, W2, INT_2:def 4;

      end;

      hence thesis by MOEBIUS1:def 1;

    end;

    registration

      let A be finite Subset of SetPrimes ;

      cluster ( Product (A -bag )) -> square-free;

      coherence by ProdSqF;

    end

    theorem :: MOEBIUS3:57

    for n be non zero Nat holds for x be object st x in ( bool ( SetPrimes n)) holds x is finite Subset of SetPrimes

    proof

      let n be non zero Nat;

      let x be object;

      assume

       G1: x in ( bool ( SetPrimes n));

      reconsider g1 = x as Subset of ( SetPrimes n) by G1;

      ( SetPrimes n) c= SetPrimes by XBOOLE_1: 17;

      then g1 c= SetPrimes ;

      hence thesis;

    end;

    theorem :: MOEBIUS3:58

    for n be non zero Nat holds for x be object st x in [:( bool ( SetPrimes n)), ( Seg n):] holds (x `1 ) is finite Subset of SetPrimes

    proof

      let n be non zero Nat;

      let x be object;

      assume

       G1: x in [:( bool ( SetPrimes n)), ( Seg n):];

      x is pair by CARDFIL4: 4, G1;

      then x = [(x `1 ), (x `2 )];

      then

      reconsider g1 = (x `1 ) as Subset of ( SetPrimes n) by G1, ZFMISC_1: 87;

      ( SetPrimes n) c= SetPrimes by XBOOLE_1: 17;

      then g1 c= SetPrimes ;

      hence thesis;

    end;

    theorem :: MOEBIUS3:59

    ( rseq ( 0 ,1,1, 0 )) = invNAT

    proof

      for n be Element of NAT holds (( rseq ( 0 ,1,1, 0 )) . n) = ( invNAT . n)

      proof

        let n be Element of NAT ;

        (( rseq ( 0 ,1,1, 0 )) . n) = (1 / ((1 * n) + 0 )) by AlgDef

        .= ( invNAT . n) by MOEBIUS2:def 2;

        hence thesis;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: MOEBIUS3:60

    ( indexp 0 ) = 0 ;

    theorem :: MOEBIUS3:61

    

     GreaterProduct: for n be Nat holds (( Partial_Product Reci-seq2 ) . n) > 0

    proof

      let n be Nat;

      for k be Nat holds ( Reci-seq2 . k) > 0

      proof

        let k be Nat;

        ( Reci-seq2 . k) = (1 + (1 / ( primenumber k))) by My3Def;

        hence thesis;

      end;

      hence thesis by SERIES_3: 43;

    end;

    theorem :: MOEBIUS3:62

    

     Crucial5X: for n be Nat holds ( ln . (( Partial_Product Reci-seq2 ) . n)) <= (( Partial_Sums ReciPrime ) . n)

    proof

      let n be Nat;

      defpred P[ Nat] means ( ln . (( Partial_Product Reci-seq2 ) . $1)) <= (( Partial_Sums ReciPrime ) . $1);

      

       B1: (( Partial_Product Reci-seq2 ) . 0 ) = ( Reci-seq2 . 0 ) by SERIES_3:def 1

      .= (1 + (1 / 2)) by MOEBIUS2: 8, My3Def;

      (( Partial_Sums ReciPrime ) . 0 ) = ( ReciPrime . 0 ) by SERIES_1:def 1

      .= (1 / 2) by MOEBIUS2: 8, MOEBIUS2:def 1;

      then

       A1: P[ 0 ] by B1, Diesel1;

      

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

      proof

        let k be Nat;

        assume

         B1: P[k];

        

         C1: (( Partial_Product Reci-seq2 ) . k) > 0 by GreaterProduct;

        

         C2: ( Reci-seq2 . (k + 1)) > 0

        proof

          ( Reci-seq2 . (k + 1)) = (1 + (1 / ( primenumber (k + 1)))) by My3Def;

          hence thesis;

        end;

        (( Partial_Product Reci-seq2 ) . (k + 1)) = ((( Partial_Product Reci-seq2 ) . k) * ( Reci-seq2 . (k + 1))) by SERIES_3:def 1;

        then ( ln . (( Partial_Product Reci-seq2 ) . (k + 1))) = (( ln . (( Partial_Product Reci-seq2 ) . k)) + ( ln . ( Reci-seq2 . (k + 1)))) by LogAdd, C1, C2;

        then

         D5: ( ln . (( Partial_Product Reci-seq2 ) . (k + 1))) <= ((( Partial_Sums ReciPrime ) . k) + ( ln . ( Reci-seq2 . (k + 1)))) by XREAL_1: 7, B1;

        

         D3: (( Partial_Sums ReciPrime ) . (k + 1)) = ((( Partial_Sums ReciPrime ) . k) + ( ReciPrime . (k + 1))) by SERIES_1:def 1;

        ( ln . ( Reci-seq2 . (k + 1))) < ( ReciPrime . (k + 1))

        proof

          

           D1: ( Reci-seq2 . (k + 1)) = (1 + (1 / ( primenumber (k + 1)))) by My3Def;

          ( ReciPrime . (k + 1)) = (1 / ( primenumber (k + 1))) by MOEBIUS2:def 1;

          hence thesis by D1, Diesel1;

        end;

        then ((( Partial_Sums ReciPrime ) . k) + ( ln . ( Reci-seq2 . (k + 1)))) < ((( Partial_Sums ReciPrime ) . k) + ( ReciPrime . (k + 1))) by XREAL_1: 8;

        hence thesis by D5, XXREAL_0: 2, D3;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: MOEBIUS3:63

    for n be Nat holds ( ln . (( Partial_Product Reci-seq2 ) . ( indexp n))) <= (( Partial_Sums ReciPrime ) . n)

    proof

      let n be Nat;

      

       A1: ( ln . (( Partial_Product Reci-seq2 ) . ( indexp n))) <= (( Partial_Sums ReciPrime ) . ( indexp n)) by Crucial5X;

      for i be Nat holds ( ReciPrime . i) >= 0

      proof

        let i be Nat;

        ( ReciPrime . i) = (1 / ( primenumber i)) by MOEBIUS2:def 1;

        hence thesis;

      end;

      then (( Partial_Sums ReciPrime ) . ( indexp n)) <= (( Partial_Sums ReciPrime ) . n) by Krzys1, CATALAN2: 52;

      hence thesis by A1, XXREAL_0: 2;

    end;

    definition

      :: MOEBIUS3:def8

      func Reci-Sqf -> Real_Sequence means

      : MySumDef: (it . 0 ) = 0 & for i be non zero Nat holds (it . i) = (1 / ( SquarefreePart i));

      existence

      proof

        deffunc G( Nat, object) = ( In ((1 / ( SquarefreePart ($1 + 1))), REAL ));

        deffunc A() = ( In ( 0 , REAL ));

        consider f be sequence of REAL such that

         A1: (f . 0 ) = A() & for n be Nat holds (f . (n + 1)) = G(n,.) from NAT_1:sch 12;

        reconsider f as Real_Sequence;

        take f;

        thus (f . 0 ) = 0 by A1;

        let n be non zero Nat;

        consider k be Nat such that

         A2: (k + 1) = n by NAT_1: 6;

        (f . (k + 1)) = G(k,.) by A1

        .= (1 / ( SquarefreePart (k + 1)));

        hence thesis by A2;

      end;

      uniqueness

      proof

        let f1,f2 be Real_Sequence such that

         A1: (f1 . 0 ) = 0 & for i be non zero Nat holds (f1 . i) = (1 / ( SquarefreePart i)) and

         A2: (f2 . 0 ) = 0 & for i be non zero Nat holds (f2 . i) = (1 / ( SquarefreePart i));

        for n be Element of NAT holds (f1 . n) = (f2 . n)

        proof

          let n be Element of NAT ;

          per cases ;

            suppose n = 0 ;

            hence thesis by A2, A1;

          end;

            suppose n <> 0 ;

            then

            reconsider nn = n as non zero Nat;

            (f1 . nn) = (1 / ( SquarefreePart nn)) by A1

            .= (f2 . nn) by A2;

            hence thesis;

          end;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      :: MOEBIUS3:def9

      func Reci-TSq -> Real_Sequence means

      : MySum2Def: (it . 0 ) = 0 & for i be non zero Nat holds (it . i) = (1 / ( TSqF i));

      existence

      proof

        deffunc G( Nat, object) = ( In ((1 / ( TSqF ($1 + 1))), REAL ));

        deffunc A() = ( In ( 0 , REAL ));

        consider f be sequence of REAL such that

         A1: (f . 0 ) = A() & for n be Nat holds (f . (n + 1)) = G(n,.) from NAT_1:sch 12;

        reconsider f as Real_Sequence;

        take f;

        thus (f . 0 ) = 0 by A1;

        let n be non zero Nat;

        consider k be Nat such that

         A2: (k + 1) = n by NAT_1: 6;

        (f . (k + 1)) = G(k,.) by A1

        .= (1 / ( TSqF (k + 1)));

        hence thesis by A2;

      end;

      uniqueness

      proof

        let f1,f2 be Real_Sequence such that

         A1: (f1 . 0 ) = 0 & for i be non zero Nat holds (f1 . i) = (1 / ( TSqF i)) and

         A2: (f2 . 0 ) = 0 & for i be non zero Nat holds (f2 . i) = (1 / ( TSqF i));

        for n be Element of NAT holds (f1 . n) = (f2 . n)

        proof

          let n be Element of NAT ;

          per cases ;

            suppose n = 0 ;

            hence thesis by A2, A1;

          end;

            suppose n <> 0 ;

            then

            reconsider nn = n as non zero Nat;

            (f1 . nn) = (1 / ( TSqF nn)) by A1

            .= (f2 . nn) by A2;

            hence thesis;

          end;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: MOEBIUS3:64

    

     Core1: ( rseq ( 0 ,1,1, 0 )) = ( Reci-Sqf (#) Reci-TSq )

    proof

      for n be Nat holds (( rseq ( 0 ,1,1, 0 )) . n) = (( Reci-Sqf . n) * ( Reci-TSq . n))

      proof

        let n be Nat;

        

         A1: (( rseq ( 0 ,1,1, 0 )) . n) = (1 / ((1 * n) + 0 )) by AlgDef;

        per cases ;

          suppose

           A2: n = 0 ;

          

          then (( rseq ( 0 ,1,1, 0 )) . n) = (1 / ((1 * 0 ) + 0 )) by AlgDef

          .= (( Reci-Sqf . n) * 0 )

          .= (( Reci-Sqf . n) * ( Reci-TSq . n)) by MySum2Def, A2;

          hence thesis;

        end;

          suppose n <> 0 ;

          then

          reconsider nn = n as non zero Nat;

          

           A3: ( TSqF nn) = (( SqF nn) |^ 2) by Cosik

          .= (( SqF nn) ^2 ) by NEWTON: 81;

          

           A4: ( Reci-TSq . nn) = (1 / ( TSqF nn)) by MySum2Def;

          (1 / nn) = (1 / (( SquarefreePart nn) * ( TSqF nn))) by Canonical, A3

          .= ((1 / ( SquarefreePart nn)) * (1 / ( TSqF nn))) by XCMPLX_1: 102;

          hence thesis by MySumDef, A1, A4;

        end;

      end;

      hence thesis by SEQ_1: 8;

    end;

    reserve s,s1,s2 for Real_Sequence;

    theorem :: MOEBIUS3:65

    

     Seqs1: for n be Nat holds ( Reci-Sqf . n) >= 0

    proof

      let n be Nat;

      per cases ;

        suppose n = 0 ;

        hence thesis by MySumDef;

      end;

        suppose n <> 0 ;

        then

        reconsider nn = n as non zero Nat;

        ( Reci-Sqf . n) = (1 / ( SquarefreePart nn)) by MySumDef;

        hence thesis;

      end;

    end;

    theorem :: MOEBIUS3:66

    

     Seqs4: for n be Nat holds ( Reci-TSq . n) >= 0

    proof

      let n be Nat;

      per cases ;

        suppose n = 0 ;

        hence thesis by MySum2Def;

      end;

        suppose n <> 0 ;

        then

        reconsider nn = n as non zero Nat;

        ( Reci-TSq . n) = (1 / ( TSqF nn)) by MySum2Def;

        hence thesis;

      end;

    end;

    theorem :: MOEBIUS3:67

    for n be Nat holds ( Basel-seq . n) >= 0

    proof

      let n be Nat;

      ( Basel-seq . n) = (1 / (n ^2 )) by BASEL_1: 31;

      hence thesis;

    end;

    theorem :: MOEBIUS3:68

    for n be Nat holds (( Partial_Sums ( rseq ( 0 ,1,1, 0 ))) . n) <= ((( Partial_Sums Reci-Sqf ) . n) * (( Partial_Sums Reci-TSq ) . n)) by SERIES_3: 39, Seqs1, Seqs4, Core1;

    definition

      let n be non zero Nat;

      :: MOEBIUS3:def10

      func Compose n -> Function of [:( bool ( SetPrimes n)), ( Seg n):], NAT means for x be Element of [:( bool ( SetPrimes n)), ( Seg n):], A be finite Subset of SetPrimes , k be Nat st x = [A, k] holds (it . x) = (( Product ((A,1) -bag )) * (k ^2 ));

      existence

      proof

        defpred P[ object, object, object] means for A be finite Subset of SetPrimes , k be Nat st A = $1 & k = $2 holds $3 = (( Product ((A,1) -bag )) * (k ^2 ));

        

         A1: for x,y,z1,z2 be object st x in ( bool ( SetPrimes n)) & y in ( Seg n) & P[x, y, z1] & P[x, y, z2] holds z1 = z2

        proof

          let x,y,z1,z2 be object;

          assume

           a1: x in ( bool ( SetPrimes n)) & y in ( Seg n) & P[x, y, z1] & P[x, y, z2];

          then

          reconsider xa = x as Subset of ( SetPrimes n);

          

           a4: ( SetPrimes n) c= SetPrimes by XBOOLE_1: 17;

          xa c= SetPrimes by a4;

          then

          reconsider S = xa as finite Subset of SetPrimes ;

          set xx = ((S,1) -bag );

          reconsider yy = y as Nat by a1;

          z1 = (( Product xx) * (yy ^2 )) by a1;

          hence thesis by a1;

        end;

        

         A2: for x,y be object st x in ( bool ( SetPrimes n)) & y in ( Seg n) holds ex z be object st P[x, y, z]

        proof

          let x,y be object;

          assume

           a1: x in ( bool ( SetPrimes n)) & y in ( Seg n);

          

           a4: ( SetPrimes n) c= SetPrimes by XBOOLE_1: 17;

          reconsider xx = x as Subset of ( SetPrimes n) by a1;

          xx c= SetPrimes by a4;

          then

          reconsider xx = x as finite Subset of SetPrimes ;

          reconsider yy = y as Nat by a1;

          ex z be object st P[x, y, z]

          proof

            take (( Product ((xx,1) -bag )) * (yy ^2 ));

            thus thesis;

          end;

          hence thesis;

        end;

        ex f be Function st ( dom f) = [:( bool ( SetPrimes n)), ( Seg n):] & for x,y be object st x in ( bool ( SetPrimes n)) & y in ( Seg n) holds P[x, y, (f . (x,y))] from FUNCT_3:sch 1( A1, A2);

        then

        consider f be Function such that

         D1: ( dom f) = [:( bool ( SetPrimes n)), ( Seg n):] & for x,y be object st x in ( bool ( SetPrimes n)) & y in ( Seg n) holds P[x, y, (f . (x,y))];

        ( rng f) c= NAT

        proof

          let g be object;

          assume g in ( rng f);

          then

          consider gg be object such that

           E1: gg in ( dom f) & g = (f . gg) by FUNCT_1:def 3;

          

           G0: gg is pair by CARDFIL4: 4, E1, D1;

          then

           G3: gg = [(gg `1 ), (gg `2 )];

          then

           Z1: (gg `1 ) in ( bool ( SetPrimes n)) by E1, D1, ZFMISC_1: 87;

          reconsider g1 = (gg `1 ) as Subset of ( SetPrimes n) by G3, E1, D1, ZFMISC_1: 87;

          

           a4: ( SetPrimes n) c= SetPrimes by XBOOLE_1: 17;

          g1 c= SetPrimes by a4;

          then

          reconsider g1 = (gg `1 ) as finite Subset of SetPrimes ;

          

           Z2: (gg `2 ) in ( Seg n) by E1, D1, G3, ZFMISC_1: 87;

          then

          reconsider yy = (gg `2 ) as Nat;

          (f . (g1,yy)) = (( Product ((g1,1) -bag )) * (yy ^2 )) by Z1, D1, Z2;

          hence thesis by E1, G0;

        end;

        then

        reconsider f as Function of [:( bool ( SetPrimes n)), ( Seg n):], NAT by D1, FUNCT_2: 2;

        take f;

        let x be Element of [:( bool ( SetPrimes n)), ( Seg n):], A be finite Subset of SetPrimes , k be Nat;

        assume

         D2: x = [A, k];

        then

         D3: A in ( bool ( SetPrimes n)) by ZFMISC_1: 87;

        k in ( Seg n) by D2, ZFMISC_1: 87;

        then P[A, k, (f . (A,k))] by D3, D1;

        hence thesis by D2;

      end;

      uniqueness

      proof

        let f1,f2 be Function of [:( bool ( SetPrimes n)), ( Seg n):], NAT ;

        assume that

         A1: for x be Element of [:( bool ( SetPrimes n)), ( Seg n):], A be finite Subset of SetPrimes , k be Nat st x = [A, k] holds (f1 . x) = (( Product ((A,1) -bag )) * (k ^2 )) and

         A2: for x be Element of [:( bool ( SetPrimes n)), ( Seg n):], A be finite Subset of SetPrimes , k be Nat st x = [A, k] holds (f2 . x) = (( Product ((A,1) -bag )) * (k ^2 ));

        for x be object st x in [:( bool ( SetPrimes n)), ( Seg n):] holds (f1 . x) = (f2 . x)

        proof

          let x be object;

          assume

           G1: x in [:( bool ( SetPrimes n)), ( Seg n):];

          then

           G0: x is pair by CARDFIL4: 4;

          then

           G3: x = [(x `1 ), (x `2 )];

          then

          reconsider xx = (x `1 ) as Subset of ( SetPrimes n) by G1, ZFMISC_1: 87;

          

           a4: ( SetPrimes n) c= SetPrimes by XBOOLE_1: 17;

          xx c= SetPrimes by a4;

          then

          reconsider xx = (x `1 ) as finite Subset of SetPrimes ;

          (x `2 ) in ( Seg n) by G1, G3, ZFMISC_1: 87;

          then

          reconsider yy = (x `2 ) as Nat;

          

           G2: x = [xx, yy] by G0;

          

          then (f1 . x) = (( Product ((xx,1) -bag )) * (yy ^2 )) by G1, A1

          .= (f2 . x) by A2, G1, G2;

          hence thesis;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: MOEBIUS3:69

    (( Partial_Sums Basel-seq ) . n) >= 0

    proof

      for n be Nat holds ( Basel-seq . n) >= 0

      proof

        let n be Nat;

        ( Basel-seq . n) = (1 / (n ^2 )) by BASEL_1: 31;

        hence thesis;

      end;

      hence thesis by SERIES_3: 34;

    end;

    begin

    definition

      let n be Nat;

      :: MOEBIUS3:def11

      func ReciProducts n -> Subset of REAL equals the set of all (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes n);

      coherence

      proof

        set Y = the set of all (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes n);

        Y c= REAL

        proof

          let x be object;

          assume x in Y;

          then

          consider X be Subset of ( SetPrimes n) such that

           A1: x = (1 / ( Product ( Sgm X)));

          thus thesis by A1, XREAL_0:def 1;

        end;

        hence thesis;

      end;

    end

    registration

      let n be Nat;

      cluster ( ReciProducts n) -> finite;

      correctness

      proof

        set Y = ( ReciProducts n);

        deffunc F( Subset of ( SetPrimes n)) = (1 / ( Product ( Sgm $1)));

        

         A3: Y c= { F(X) where X be Element of ( bool ( SetPrimes n)) : X in ( bool ( SetPrimes n)) }

        proof

          let x be object;

          assume x in Y;

          then

          consider X be Subset of ( SetPrimes n) such that

           B1: x = (1 / ( Product ( Sgm X)));

          thus thesis by B1;

        end;

        

         A1: ( bool ( SetPrimes n)) is finite;

        { F(w) where w be Element of ( bool ( SetPrimes n)) : w in ( bool ( SetPrimes n)) } is finite from FRAENKEL:sch 21( A1);

        hence thesis by A3;

      end;

    end

    theorem :: MOEBIUS3:70

    ( ReciProducts 0 ) = {1}

    proof

       the set of all (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes 0 ) = {1}

      proof

        

         T1: the set of all (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes 0 ) c= {1}

        proof

          let x be object;

          assume x in the set of all (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes 0 );

          then

          consider X be Subset of ( SetPrimes 0 ) such that

           C1: x = (1 / ( Product ( Sgm X)));

          ( Sgm X) = {} by FINSEQ_3: 43;

          hence thesis by TARSKI:def 1, C1, RVSUM_1: 94;

        end;

         {1} c= the set of all (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes 0 )

        proof

          let x be object;

          assume x in {1};

          then

           S1: x = (1 / ( Product ( Sgm {} ))) by FINSEQ_3: 43, RVSUM_1: 94, TARSKI:def 1;

           {} c= ( SetPrimes 0 );

          hence thesis by S1;

        end;

        hence thesis by T1, TARSKI: 2;

      end;

      hence thesis;

    end;

    theorem :: MOEBIUS3:71

    for p be Prime st p > 2 holds ( ReciProducts (p + 1)) = ( ReciProducts p)

    proof

      let p be Prime;

      assume p > 2;

      then not (p + 1) is prime by P1NotPrime;

      then ( SetPrimes (p + 1)) = ( SetPrimes p) by PrimesSet;

      hence thesis;

    end;

    theorem :: MOEBIUS3:72

    for p be Nat st not (p + 1) is Prime holds ( ReciProducts (p + 1)) = ( ReciProducts p)

    proof

      let p be Nat;

      assume not (p + 1) is Prime;

      then ( SetPrimes (p + 1)) = ( SetPrimes p) by PrimesSet;

      hence thesis;

    end;

    theorem :: MOEBIUS3:73

    ( ReciProducts 1) = {1}

    proof

       the set of all (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes 1) = {1}

      proof

        

         T1: the set of all (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes 1) c= {1}

        proof

          let x be object;

          assume x in the set of all (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes 1);

          then

          consider X be Subset of ( SetPrimes 1) such that

           C1: x = (1 / ( Product ( Sgm X)));

          ( Sgm X) = {} by FINSEQ_3: 43, SetPrime1;

          hence thesis by TARSKI:def 1, C1, RVSUM_1: 94;

        end;

         {1} c= the set of all (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes 1)

        proof

          let x be object;

          assume x in {1};

          then

           S1: x = (1 / ( Product ( Sgm {} ))) by FINSEQ_3: 43, RVSUM_1: 94, TARSKI:def 1;

           {} c= ( SetPrimes 1);

          hence thesis by S1;

        end;

        hence thesis by T1, TARSKI: 2;

      end;

      hence thesis;

    end;

    theorem :: MOEBIUS3:74

    ( ReciProducts 2) = {(1 / 2), 1}

    proof

      ( Sgm {2}) = <*2*> by FINSEQ_3: 44;

      then

       A2: (1 / ( Product ( Sgm {2}))) = (1 / 2) by RVSUM_1: 95;

       {2} c= ( SetPrimes 2) by Set2;

      then

       S1: (1 / 2) in ( ReciProducts 2) by A2;

       {} c= ( Seg 1);

      then

       A4: ( Product ( Sgm {} )) = 1 by RVSUM_1: 94, FINSEQ_1: 51;

      

       Z1: {} c= ( SetPrimes 2);

      (1 / ( Product ( Sgm {} ))) = 1 by A4;

      then 1 in ( ReciProducts 2) by Z1;

      then

       ZZ: {(1 / 2), 1} c= ( ReciProducts 2) by ZFMISC_1: 32, S1;

      ( ReciProducts 2) c= {(1 / 2), 1}

      proof

        let x be object;

        assume x in ( ReciProducts 2);

        then

        consider X be Subset of ( SetPrimes 2) such that

         N1: x = (1 / ( Product ( Sgm X)));

        X = {} or X = {2} by ZFMISC_1: 33, Set2;

        hence thesis by TARSKI:def 2, N1, A4, A2;

      end;

      hence thesis by TARSKI: 2, ZZ;

    end;

    theorem :: MOEBIUS3:75

    

     ReciSubset: for n be Nat holds ( ReciProducts n) c= ( ReciProducts (n + 1))

    proof

      let n be Nat;

      let x be object;

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

      then

       A0: ( SetPrimes n) c= ( SetPrimes (n + 1)) by XBOOLE_1: 26, FINSEQ_1: 5;

      assume x in ( ReciProducts n);

      then

      consider X be Subset of ( SetPrimes n) such that

       A1: x = (1 / ( Product ( Sgm X)));

      X c= ( SetPrimes (n + 1)) by A0;

      hence thesis by A1;

    end;

    theorem :: MOEBIUS3:76

    for n be Nat st (n + 1) is Prime holds ( ReciProducts (n + 1)) = (( ReciProducts n) \/ { (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes (n + 1)) : (n + 1) in X })

    proof

      let n be Nat;

      assume

       A0: (n + 1) is Prime;

      

       T1: ( ReciProducts (n + 1)) c= (( ReciProducts n) \/ { (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes (n + 1)) : (n + 1) in X })

      proof

        let x be object;

        assume x in ( ReciProducts (n + 1));

        then

        consider X be Subset of ( SetPrimes (n + 1)) such that

         A1: x = (1 / ( Product ( Sgm X)));

        X c= ( SetPrimes (n + 1));

        then

         A2: X c= (( SetPrimes n) \/ {(n + 1)}) by A0, PrimesSet2;

        per cases ;

          suppose (n + 1) in X;

          then x in { (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes (n + 1)) : (n + 1) in X } by A1;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose not (n + 1) in X;

          then X c= ( SetPrimes n) by A2, ZFMISC_1: 135;

          then x in ( ReciProducts n) by A1;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      (( ReciProducts n) \/ { (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes (n + 1)) : (n + 1) in X }) c= ( ReciProducts (n + 1))

      proof

        let x be object;

        assume x in (( ReciProducts n) \/ { (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes (n + 1)) : (n + 1) in X });

        per cases by XBOOLE_0:def 3;

          suppose

           Z1: x in ( ReciProducts n);

          ( ReciProducts n) c= ( ReciProducts (n + 1)) by ReciSubset;

          hence thesis by Z1;

        end;

          suppose x in { (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes (n + 1)) : (n + 1) in X };

          then

          consider X be Subset of ( SetPrimes (n + 1)) such that

           B1: x = (1 / ( Product ( Sgm X))) & (n + 1) in X;

          thus thesis by B1;

        end;

      end;

      hence thesis by T1, TARSKI: 2;

    end;

    theorem :: MOEBIUS3:77

    for n be Nat st (n + 1) is Prime holds ( ReciProducts (n + 1)) = ({ (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes n) : not (n + 1) in X } \/ { (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes (n + 1)) : (n + 1) in X })

    proof

      let n be Nat;

      assume

       A0: (n + 1) is Prime;

      

       T1: ( ReciProducts (n + 1)) c= ({ (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes n) : not (n + 1) in X } \/ { (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes (n + 1)) : (n + 1) in X })

      proof

        let x be object;

        assume x in ( ReciProducts (n + 1));

        then

        consider X be Subset of ( SetPrimes (n + 1)) such that

         A1: x = (1 / ( Product ( Sgm X)));

        X c= ( SetPrimes (n + 1));

        then

         A2: X c= (( SetPrimes n) \/ {(n + 1)}) by A0, PrimesSet2;

        per cases ;

          suppose (n + 1) in X;

          then x in { (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes (n + 1)) : (n + 1) in X } by A1;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose

           SS: not (n + 1) in X;

          then X c= ( SetPrimes n) by A2, ZFMISC_1: 135;

          then x in { (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes n) : not (n + 1) in X } by SS, A1;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      ({ (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes n) : not (n + 1) in X } \/ { (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes (n + 1)) : (n + 1) in X }) c= ( ReciProducts (n + 1))

      proof

        let x be object;

        assume x in ({ (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes n) : not (n + 1) in X } \/ { (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes (n + 1)) : (n + 1) in X });

        per cases by XBOOLE_0:def 3;

          suppose x in { (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes n) : not (n + 1) in X };

          then

          consider X be Subset of ( SetPrimes n) such that

           I1: x = (1 / ( Product ( Sgm X))) & not (n + 1) in X;

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

          then ( SetPrimes n) c= ( SetPrimes (n + 1)) by XBOOLE_1: 26, FINSEQ_1: 5;

          then X c= ( SetPrimes (n + 1));

          hence thesis by I1;

        end;

          suppose x in { (1 / ( Product ( Sgm X))) where X be Subset of ( SetPrimes (n + 1)) : (n + 1) in X };

          then

          consider X be Subset of ( SetPrimes (n + 1)) such that

           B1: x = (1 / ( Product ( Sgm X))) & (n + 1) in X;

          thus thesis by B1;

        end;

      end;

      hence thesis by T1, TARSKI: 2;

    end;