liouvil1.miz



    begin

    theorem :: LIOUVIL1:1

    

     Th1: for x,y be Nat st x > 1 & y > 1 holds (x * y) >= (x + y)

    proof

      let x,y be Nat;

      assume

       A1: x > 1 & y > 1;

      per cases ;

        suppose

         A2: x >= y;

        (y - 0 ) > 1 by A1;

        then (y - 1) >= ( 0 + 1) by INT_1: 7, XREAL_1: 12;

        then (x * (y - 1)) >= (y * 1) by A2, XREAL_1: 66;

        then (((x * y) - x) + x) >= (y + x) by XREAL_1: 6;

        hence thesis;

      end;

        suppose

         A3: x < y;

        (x - 0 ) > 1 by A1;

        then (x - 1) >= ( 0 + 1) by XREAL_1: 12, INT_1: 7;

        then (y * (x - 1)) >= (x * 1) by A3, XREAL_1: 66;

        then (((x * y) - y) + y) >= (x + y) by XREAL_1: 6;

        hence thesis;

      end;

    end;

    

     Th2: for n be Nat holds (n ! ) >= 1

    proof

      let n be Nat;

      (n ! ) >= ( 0 + 1) by NAT_1: 13;

      hence thesis;

    end;

    theorem :: LIOUVIL1:2

    

     ADDC1: for n be Nat holds n <= (n ! )

    proof

      let n be Nat;

      (n + 1) <= 3 or 3 <= n by INT_1: 7;

      then ((n + 1) - 1) <= (3 - 1) or 3 <= n by XREAL_1: 9;

      then

       CCS: (n = 0 or ... or n = 2) or 3 <= n;

      per cases by CCS;

        suppose n = 0 ;

        hence thesis;

      end;

        suppose n = 1;

        hence thesis by NEWTON: 13;

      end;

        suppose n = 2;

        hence thesis by NEWTON: 14;

      end;

        suppose n >= 3;

        hence thesis by ASYMPT_1: 59;

      end;

    end;

    theorem :: LIOUVIL1:3

    

     Th3: for n be Nat holds (n * (n ! )) = (((n + 1) ! ) - (n ! ))

    proof

      let n be Nat;

      set a = (n ! );

      

      thus (n * a) = (((n + 1) * a) - a)

      .= (((n + 1) ! ) - a) by NEWTON: 15;

    end;

    theorem :: LIOUVIL1:4

    for n be Nat st n >= 1 holds 2 <= ((n + 1) ! )

    proof

      let n be Nat;

      assume n >= 1;

      then (n + 1) >= (1 + 1) by XREAL_1: 7;

      then 1 < ((n + 1) ! ) by ASYMPT_1: 55;

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

      hence thesis;

    end;

    

     Th4: for n be Nat st n >= 1 holds ((n + 1) ! ) >= ((n ! ) + 1)

    proof

      let n be Nat;

      assume

       A1: n >= 1;

      (n ! ) >= 1 by Th2;

      then (n * (n ! )) >= (1 * 1) by A1, XREAL_1: 66;

      then (((n + 1) ! ) - (n ! )) >= 1 by Th3;

      then ((((n + 1) ! ) - (n ! )) + (n ! )) >= (1 + (n ! )) by XREAL_1: 6;

      hence thesis;

    end;

    

     Th5: for n be Nat st n >= 2 holds ((n + 1) ! ) > ((n ! ) + 1)

    proof

      let n be Nat;

      assume n >= 2;

      then n >= (1 + 1);

      then

       A1: n > 1 by NAT_1: 13;

      (n ! ) >= n by NEWTON: 38;

      then (n ! ) > 1 by A1, XXREAL_0: 2;

      then (n * (n ! )) > (1 * 1) by A1, XREAL_1: 96;

      then (((n + 1) ! ) - (n ! )) > 1 by Th3;

      then ((((n + 1) ! ) - (n ! )) + (n ! )) > (1 + (n ! )) by XREAL_1: 6;

      hence thesis;

    end;

    

     Th6: for n be Nat st n > 1 holds ((n + 2) ! ) > ((n ! ) + 2)

    proof

      let n be Nat;

      assume

       A1: n > 1;

      then

       A2: (n + 1) > (1 + 1) by XREAL_1: 8;

      then

       A3: (n + 1) > 1 by XXREAL_0: 2;

      (n ! ) >= n by NEWTON: 38;

      then

       A4: (n ! ) > 1 by XXREAL_0: 2, A1;

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

      then

       A5: ((n + 1) ! ) <= ((n + 2) ! ) by ASYMPT_1: 56;

      ((n + 1) ! ) <> ((n + 2) ! )

      proof

        assume ((n + 1) ! ) = ((n + 2) ! );

        then (((n + 1) ! ) * 1) = (((n + 1) ! ) * ((n + 1) + 1)) by NEWTON: 15;

        then 1 = ((n + 1) + 1) by XCMPLX_1: 5;

        then 0 = (n + 1);

        hence thesis;

      end;

      then

       A6: ((n + 1) ! ) < ((n + 2) ! ) by XXREAL_0: 1, A5;

      ((n + 1) ! ) = ((n + 1) * (n ! )) by NEWTON: 15;

      then

       A7: ((n + 1) ! ) >= ((n + 1) + (n ! )) by A3, Th1, A4;

      ((n + 1) + (n ! )) > ((n ! ) + 2) by XREAL_1: 8, A2;

      then ((n + 1) ! ) >= ((n ! ) + 2) by A7, XXREAL_0: 2;

      hence thesis by A6, XXREAL_0: 2;

    end;

    

     Th7: for n,i be Nat st n > 1 & i > 1 holds ((n + i) ! ) >= ((n ! ) + i)

    proof

      let n,i be Nat;

      assume

       A1: n > 1 & i > 1;

      then

       A2: i >= (1 + 1) by NAT_1: 13;

      

       A3: ((n + i) ! ) >= ((n ! ) * (i ! )) by NEWTON04: 70;

      n >= (1 + 1) by A1, NAT_1: 13;

      then (n ! ) > 1 & (i ! ) > 1 by A2, ASYMPT_1: 55;

      then

       A5: ((n ! ) * (i ! )) >= ((n ! ) + (i ! )) by Th1;

      per cases by A2, XXREAL_0: 1;

        suppose i = 2;

        hence thesis by A1, Th6;

      end;

        suppose i > 2;

        then

         A6: i >= (2 + 1) by NAT_1: 13;

        (i ! ) > i by ASYMPT_1: 59, A6;

        then ((n ! ) + (i ! )) > ((n ! ) + i) by XREAL_1: 6;

        then ((n ! ) * (i ! )) > ((n ! ) + i) by A5, XXREAL_0: 2;

        hence thesis by A3, XXREAL_0: 2;

      end;

    end;

    theorem :: LIOUVIL1:5

    

     Th8: for n,i be Nat st n >= 1 & i >= 1 holds ((n + i) ! ) >= ((n ! ) + i)

    proof

      let n,i be Nat;

      assume n >= 1 & i >= 1;

      per cases by XXREAL_0: 1;

        suppose n >= 1 & i > 1;

        per cases by XXREAL_0: 1;

          suppose n > 1 & i > 1;

          hence thesis by Th7;

        end;

          suppose n = 1 & i > 1;

          hence thesis by NEWTON: 13, NEWTON: 38;

        end;

      end;

        suppose n >= 1 & i = 1;

        hence thesis by Th4;

      end;

    end;

    theorem :: LIOUVIL1:6

    for n,i be Nat st n >= 2 & i >= 1 holds ((n + i) ! ) > ((n ! ) + i)

    proof

      let n,i be Nat;

      assume n >= 2 & i >= 1;

      per cases by XXREAL_0: 1;

        suppose n >= 2 & i > 1;

        per cases by XXREAL_0: 1;

          suppose

           A1: n > 2 & i > 1;

          then

           A2: i >= (1 + 1) by NAT_1: 13;

          

           A3: ((n + i) ! ) >= ((n ! ) * (i ! )) by NEWTON04: 70;

          (n ! ) > 1 & (i ! ) > 1 by A2, A1, ASYMPT_1: 55;

          then

           A5: ((n ! ) * (i ! )) >= ((n ! ) + (i ! )) by Th1;

          per cases by A2, XXREAL_0: 1;

            suppose

             A6: i = 2;

            n > 1 by A1, XXREAL_0: 2;

            hence thesis by A6, Th6;

          end;

            suppose i > 2;

            then

             A7: i >= (2 + 1) by NAT_1: 13;

            (i ! ) > i by ASYMPT_1: 59, A7;

            then ((n ! ) + (i ! )) > ((n ! ) + i) by XREAL_1: 6;

            then ((n ! ) * (i ! )) > ((n ! ) + i) by A5, XXREAL_0: 2;

            hence thesis by A3, XXREAL_0: 2;

          end;

        end;

          suppose

           A8: n = 2 & i > 1;

          then (2 + i) >= (2 + 1) by XREAL_1: 7;

          hence thesis by A8, NEWTON: 14, ASYMPT_1: 59;

        end;

      end;

        suppose n >= 2 & i = 1;

        hence thesis by Th5;

      end;

    end;

    theorem :: LIOUVIL1:7

    

     Th9: for b be Nat st b > 1 holds |.(1 / b).| < 1

    proof

      let b be Nat;

      assume b > 1;

      then (1 / b) < (1 / 1) by XREAL_1: 76;

      hence thesis;

    end;

    theorem :: LIOUVIL1:8

    

     Th10: for d be Integer holds ex n be non zero Nat st (2 to_power (n - 1)) > d

    proof

      let d be Integer;

      per cases ;

        suppose

         A1: d <= 0 ;

        take n = 1;

        thus thesis by A1, POWER: 24;

      end;

        suppose

         A2: d > 0 ;

        then d >= (1 + 0 ) by INT_1: 7;

        per cases by XXREAL_0: 1;

          suppose

           A3: d = 1;

          take n = 2;

          (2 to_power (n - 1)) = (2 to_power 1)

          .= 2;

          hence thesis by A3;

        end;

          suppose d > 1;

          then ( log (2,d)) > 0 by ENTROPY1: 4;

          then

           A4: [/( log (2,d))\] > 0 by INT_1:def 7;

          set n = ( [/( log (2,d))\] + 2);

          n in NAT by A4, INT_1: 3;

          then

          reconsider n as Nat;

          reconsider n as non zero Nat by A4;

          take n;

          (n - 1) = ( [/( log (2,d))\] + 1);

          then (2 to_power (n - 1)) > (2 to_power ( log (2,d))) by POWER: 39, INT_1: 32;

          hence thesis by A2, POWER:def 3;

        end;

      end;

    end;

    registration

      let a be Integer, b be Nat;

      cluster (a to_power b) -> integer;

      coherence

      proof

        per cases ;

          suppose a >= 0 ;

          then a in NAT by INT_1: 3;

          then

          reconsider aa = a as Nat;

          (aa to_power b) is Integer;

          hence thesis;

        end;

          suppose a < 0 ;

          then

          reconsider aa = ( - a) as Element of NAT by INT_1: 3;

          per cases ;

            suppose b is odd;

            then (( - aa) |^ b) = ( - (aa |^ b)) by POWER: 2;

            hence thesis;

          end;

            suppose b is even;

            then (( - aa) |^ b) = (aa |^ b) by POWER: 1;

            hence thesis;

          end;

        end;

      end;

    end

    begin

    theorem :: LIOUVIL1:9

    

     Th11: for s1,s2 be Real_Sequence st (for n be Nat holds 0 <= (s1 . n) & (s1 . n) <= (s2 . n)) & (ex n be Nat st 1 <= n & (s1 . n) < (s2 . n)) & s2 is summable holds s1 is summable & ( Sum s1) < ( Sum s2)

    proof

      let s1,s2 be Real_Sequence;

      assume that

       A1: for n be Nat holds 0 <= (s1 . n) & (s1 . n) <= (s2 . n) and

       A2: ex n be Nat st 1 <= n & (s1 . n) < (s2 . n) and

       A3: s2 is summable;

      consider N be Nat such that

       A4: 1 <= N & (s1 . N) < (s2 . N) by A2;

      

       A5: for n be Nat st 0 <= n holds (s1 . n) <= (s2 . n) by A1;

      hence s1 is summable by A1, A3, SERIES_1: 19;

      (N - 1) in NAT by A4, INT_1: 5;

      then

      reconsider N1 = (N - 1) as Nat;

      

       A6: (N1 + 1) = N;

      then

       A7: (( Partial_Sums s1) . N) = ((( Partial_Sums s1) . N1) + (s1 . N)) by SERIES_1:def 1;

      

       A8: ( Sum s1) = ((( Partial_Sums s1) . N) + ( Sum (s1 ^\ (N + 1)))) by A1, A3, A5, SERIES_1: 15, SERIES_1: 19;

      

       A9: (( Partial_Sums s2) . N) = ((( Partial_Sums s2) . N1) + (s2 . N)) by A6, SERIES_1:def 1;

      

       A10: ( Sum s2) = ((( Partial_Sums s2) . N) + ( Sum (s2 ^\ (N + 1)))) by SERIES_1: 15, A3;

      

       A11: for n be Nat holds 0 <= ((s1 ^\ (N + 1)) . n)

      proof

        let n be Nat;

        ((s1 ^\ (N + 1)) . n) = (s1 . (n + (N + 1))) by NAT_1:def 3;

        hence thesis by A1;

      end;

      

       A12: (s2 ^\ (N + 1)) is summable by A3, SERIES_1: 12;

      for n be Nat holds ((s1 ^\ (N + 1)) . n) <= ((s2 ^\ (N + 1)) . n)

      proof

        let n be Nat;

        

         A13: ((s1 ^\ (N + 1)) . n) = (s1 . (n + (N + 1))) by NAT_1:def 3;

        ((s2 ^\ (N + 1)) . n) = (s2 . (n + (N + 1))) by NAT_1:def 3;

        hence thesis by A1, A13;

      end;

      then

       A14: ( Sum (s1 ^\ (N + 1))) <= ( Sum (s2 ^\ (N + 1))) by A11, A12, SERIES_1: 20;

      ((( Partial_Sums s1) . N1) + (s1 . N)) < ((( Partial_Sums s2) . N1) + (s2 . N)) by XREAL_1: 8, A4, A1, SERIES_1: 14;

      hence thesis by A7, A8, A9, A10, A14, XREAL_1: 8;

    end;

    theorem :: LIOUVIL1:10

    

     Th12: for f be Real_Sequence st ex n be Nat st (for k be Nat st k >= n holds (f . k) = 0 ) holds f is summable

    proof

      let f be Real_Sequence;

      given n be Nat such that

       A1: for k be Nat st k >= n holds (f . k) = 0 ;

      set p = ( Partial_Sums f);

      reconsider pk = (p . n) as Real;

      set r = ( seq_const pk);

      for k be Nat st k >= n holds (p . k) = (r . k)

      proof

        let k be Nat;

        assume

         A2: k >= n;

        defpred P[ Nat] means (p . $1) = (r . $1);

        

         A3: P[n] by SEQ_1: 57;

        

         A4: for i be Nat st n <= i holds P[i] implies P[(i + 1)]

        proof

          let i be Nat;

          assume

           A5: n <= i;

          assume

           A6: P[i];

          (p . (i + 1)) = ((p . i) + (f . (i + 1))) by SERIES_1:def 1

          .= ((r . i) + 0 ) by A1, A5, A6, NAT_1: 12

          .= pk by SEQ_1: 57

          .= (r . (i + 1));

          hence thesis;

        end;

        for k be Nat st n <= k holds P[k] from NAT_1:sch 8( A3, A4);

        hence thesis by A2;

      end;

      hence thesis by SEQ_4: 18;

    end;

    theorem :: LIOUVIL1:11

    

     Th13: for b be Nat st b > 1 holds ( Sum ((1 / b) GeoSeq )) = (b / (b - 1))

    proof

      let b be Nat;

      assume

       A0: b > 1;

      then

       A1: |.(1 / b).| < 1 by Th9;

      ( Sum ((1 / b) GeoSeq )) = (1 / (1 - (1 / b))) by A1, SERIES_1: 24

      .= (1 / ((b / b) - (1 / b))) by XCMPLX_1: 60, A0

      .= (1 / ((b - 1) / b)) by XCMPLX_1: 120

      .= (b / (b - 1)) by XCMPLX_1: 57;

      hence thesis;

    end;

    registration

      let n be Nat;

      cluster ( seq_const n) -> NAT -valued;

      coherence

      proof

        n in NAT by ORDINAL1:def 12;

        hence thesis;

      end;

    end

    registration

      let r be positive Nat;

      cluster ( seq_const r) -> positive-yielding;

      coherence ;

    end

    registration

      cluster NAT -valued INT -valued for Real_Sequence;

      existence

      proof

        take f = ( seq_const 0 );

        thus thesis;

      end;

    end

    theorem :: LIOUVIL1:12

    

     Th14: for F be Real_Sequence, n be Nat, a be Real st (for k be Nat holds (F . k) = a) holds (( Partial_Sums F) . n) = (a * (n + 1))

    proof

      let F be Real_Sequence, n be Nat, a be Real;

      assume

       A1: for k be Nat holds (F . k) = a;

      defpred P[ Nat] means (( Partial_Sums F) . $1) = (a * ($1 + 1));

      (( Partial_Sums F) . 0 ) = (F . 0 ) by SERIES_1:def 1;

      then

       A2: P[ 0 ] by A1;

      

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

      proof

        let i be Nat;

        assume

         A4: P[i];

        reconsider i1 = (i + 1), One = 1 as Real;

        (( Partial_Sums F) . (i + 1)) = ((( Partial_Sums F) . i) + (F . (i + 1))) by SERIES_1:def 1;

        then (( Partial_Sums F) . (i + 1)) = ((a * (i + 1)) + a) by A1, A4;

        hence P[(i + 1)];

      end;

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

      hence thesis;

    end;

    theorem :: LIOUVIL1:13

    for n be Nat, a be Real holds (( Partial_Sums ( seq_const a)) . n) = (a * (n + 1))

    proof

      let n be Nat, a be Real;

      set f = ( seq_const a);

      for k be Nat holds (f . k) = a by SEQ_1: 57;

      hence thesis by Th14;

    end;

    registration

      let f be INT -valued Real_Sequence;

      cluster ( Partial_Sums f) -> INT -valued;

      coherence

      proof

        set g = ( Partial_Sums f);

        ( rng g) c= INT

        proof

          let y be object;

          assume y in ( rng g);

          then

          consider x be object such that

           A0: x in ( dom g) & y = (g . x) by FUNCT_1:def 3;

          reconsider n = x as Element of NAT by A0, FUNCT_2:def 1;

          defpred P[ Nat] means (g . $1) is integer;

          (g . 0 ) = (f . 0 ) by SERIES_1:def 1;

          then

           A1: P[ 0 ];

          

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

          proof

            let k be Nat;

            assume

             A3: P[k];

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

            (g . (k + 1)) = ((g . k) + (f . (k + 1))) by SERIES_1:def 1;

            hence thesis by A3;

          end;

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

          then (g . n) is integer;

          hence thesis by A0, INT_1:def 2;

        end;

        hence thesis by RELAT_1:def 19;

      end;

    end

    registration

      let f be NAT -valued Real_Sequence;

      cluster ( Partial_Sums f) -> NAT -valued;

      coherence

      proof

        set g = ( Partial_Sums f);

        ( rng g) c= NAT

        proof

          let y be object;

          assume y in ( rng g);

          then

          consider x be object such that

           A0: x in ( dom g) & y = (g . x) by FUNCT_1:def 3;

          reconsider n = x as Element of NAT by A0, FUNCT_2:def 1;

          defpred P[ Nat] means (g . $1) is Nat;

          (g . 0 ) = (f . 0 ) by SERIES_1:def 1;

          then

           A1: P[ 0 ];

          

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

          proof

            let k be Nat;

            assume

             A3: P[k];

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

            (g . (k + 1)) = ((g . k) + (f . (k + 1))) by SERIES_1:def 1;

            hence thesis by A3;

          end;

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

          then (g . n) is Nat;

          hence thesis by A0, ORDINAL1:def 12;

        end;

        hence thesis by RELAT_1:def 19;

      end;

    end

    theorem :: LIOUVIL1:14

    for f be Real_Sequence st ex n be Nat st (for k be Nat st k >= n holds (f . k) = 0 ) holds ex n be Nat st for k be Nat st k >= n holds (( Partial_Sums f) . k) = (( Partial_Sums f) . n)

    proof

      let f be Real_Sequence;

      given n be Nat such that

       A1: for k be Nat st k >= n holds (f . k) = 0 ;

      set p = ( Partial_Sums f);

      reconsider pk = (p . n) as Real;

      set r = ( seq_const pk);

      

       A2: for k be Nat st k >= n holds (p . k) = (r . k)

      proof

        let k be Nat;

        assume

         A3: k >= n;

        defpred P[ Nat] means (p . $1) = (r . $1);

        

         A4: P[n] by SEQ_1: 57;

        

         A5: for i be Nat st n <= i holds P[i] implies P[(i + 1)]

        proof

          let i be Nat;

          assume

           A6: n <= i;

          assume

           A7: P[i];

          (p . (i + 1)) = ((p . i) + (f . (i + 1))) by SERIES_1:def 1

          .= ((r . i) + 0 ) by A1, A6, A7, NAT_1: 12

          .= pk by SEQ_1: 57

          .= (r . (i + 1));

          hence thesis;

        end;

        for k be Nat st n <= k holds P[k] from NAT_1:sch 8( A4, A5);

        hence thesis by A3;

      end;

      take n;

      let k be Nat;

      assume k >= n;

      

      then (p . k) = (r . k) by A2

      .= (p . n) by SEQ_1: 57;

      hence thesis;

    end;

    theorem :: LIOUVIL1:15

    

     Th16: for f be INT -valued Real_Sequence st ex n be Nat st (for k be Nat st k >= n holds (f . k) = 0 ) holds ( Sum f) is Integer

    proof

      let f be INT -valued Real_Sequence;

      given n be Nat such that

       A1: for k be Nat st k >= n holds (f . k) = 0 ;

      set p = ( Partial_Sums f);

      reconsider pk = (p . n) as Real;

      set r = ( seq_const pk);

      for k be Nat st k >= n holds (p . k) = (r . k)

      proof

        let k be Nat;

        assume

         A2: k >= n;

        defpred P[ Nat] means (p . $1) = (r . $1);

        

         A3: P[n] by SEQ_1: 57;

        

         A4: for i be Nat st n <= i holds P[i] implies P[(i + 1)]

        proof

          let i be Nat;

          assume

           A5: n <= i;

          assume

           A6: P[i];

          (p . (i + 1)) = ((p . i) + (f . (i + 1))) by SERIES_1:def 1

          .= ((r . i) + 0 ) by A1, A5, A6, NAT_1: 12

          .= pk by SEQ_1: 57

          .= (r . (i + 1));

          hence thesis;

        end;

        for k be Nat st n <= k holds P[k] from NAT_1:sch 8( A3, A4);

        hence thesis by A2;

      end;

      then ( lim p) = ( lim r) by SEQ_4: 19;

      hence thesis;

    end;

    registration

      let f be nonnegative-yielding Real_Sequence;

      let n be Nat;

      cluster (f ^\ n) -> nonnegative-yielding;

      coherence

      proof

        ( rng (f ^\ n)) c= ( rng f) by NAT_1: 55;

        then for r be Real st r in ( rng (f ^\ n)) holds 0 <= r by PARTFUN3:def 4;

        hence thesis by PARTFUN3:def 4;

      end;

    end

    begin

    definition

      let f be Real_Sequence, X be Subset of NAT ;

      :: LIOUVIL1:def1

      func f |_ X -> Real_Sequence equals (( NAT --> 0 ) +* (f | X));

      coherence

      proof

        set g = (( NAT --> 0 ) +* (f | X));

        

         A0: ( dom g) = (( dom ( NAT --> 0 )) \/ ( dom (f | X))) by FUNCT_4:def 1

        .= ( NAT \/ ( dom (f | X)));

        ( dom f) = NAT by FUNCT_2:def 1;

        then ( dom (f | X)) = X by RELAT_1: 62;

        then

         A1: ( dom g) = NAT by XBOOLE_1: 12, A0;

        ( rng g) c= REAL ;

        hence thesis by A1, FUNCT_2: 2;

      end;

    end

    registration

      let f be Real_Sequence, X be Subset of NAT ;

      cluster (f | X) -> NAT -defined;

      coherence ;

    end

    registration

      let f be Real_Sequence, n be Nat;

      cluster (f |_ ( Seg n)) -> summable;

      coherence

      proof

        set seq = (f |_ ( Seg n));

        for k be Nat st k >= (n + 1) holds (seq . k) = 0

        proof

          let k be Nat;

          assume k >= (n + 1);

          then k > n by NAT_1: 16, XXREAL_0: 2;

          then not k in ( Seg n) by FINSEQ_1: 1;

          then not k in ( dom (f | ( Seg n))) by RELAT_1: 57;

          then (seq . k) = (( NAT --> 0 ) . k) by FUNCT_4: 11;

          hence thesis;

        end;

        hence thesis by Th12;

      end;

    end

    registration

      let f be INT -valued Real_Sequence, n be Nat;

      cluster (f |_ ( Seg n)) -> INT -valued;

      coherence ;

    end

    theorem :: LIOUVIL1:16

    for f be Real_Sequence holds (f |_ ( Seg 0 )) = ( seq_const 0 )

    proof

      let f be Real_Sequence;

      set ff = (f |_ ( Seg 0 ));

      set g = ( seq_const 0 );

      for x be Element of NAT holds (ff . x) = (g . x)

      proof

        let x be Element of NAT ;

         not x in ( dom (f | ( Seg 0 )));

        hence thesis by FUNCT_4: 11;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    definition

      let f be Real_Sequence, n be Nat;

      :: LIOUVIL1:def2

      func FinSeq (f,n) -> FinSequence of REAL equals (f | ( Seg n));

      coherence

      proof

        set g = (f | ( Seg n));

        

         A1: ( dom f) = NAT by FUNCT_2:def 1;

        ( dom g) = ( Seg n) by A1, RELAT_1: 62;

        then

         A2: g is FinSequence by FINSEQ_1:def 2;

        ( rng g) c= REAL ;

        hence thesis by A2, FINSEQ_1:def 4;

      end;

    end

    theorem :: LIOUVIL1:17

    

     Th17: for f be Real_Sequence, k,n be Nat st k in ( Seg n) holds ((f |_ ( Seg n)) . k) = (f . k)

    proof

      let f be Real_Sequence, k,n be Nat;

      assume

       A0: k in ( Seg n);

      

       A1: ( dom f) = NAT by FUNCT_2:def 1;

      ( dom (f | ( Seg n))) = ( Seg n) by A1, RELAT_1: 62;

      

      then ((f |_ ( Seg n)) . k) = ((f | ( Seg n)) . k) by A0, FUNCT_4: 13

      .= (f . k) by A0, FUNCT_1: 49;

      hence thesis;

    end;

    theorem :: LIOUVIL1:18

    

     Th18: for f be Real_Sequence, n be Nat st (f . 0 ) = 0 holds ( Sum ( FinSeq (f,n))) = ( Sum (f |_ ( Seg n)))

    proof

      let f be Real_Sequence, n be Nat;

      assume

       A0: (f . 0 ) = 0 ;

      set f1 = (f |_ ( Seg n));

      set g = ( FinSeq (f,n));

      reconsider f0 = (f . 0 ) as Element of REAL ;

      set h = ( <*f0*> ^ g);

      

       A1: ( dom f) = NAT by FUNCT_2:def 1;

      

       A2: ( dom g) = ( Seg n) by A1, RELAT_1: 62;

      then ( Seg ( len g)) = ( Seg n) by FINSEQ_1:def 3;

      then

       A3: ( len g) = n by FINSEQ_1: 6;

      ( len h) = (( len <*f0*>) + ( len g)) by FINSEQ_1: 22;

      then

       A4: ( len h) = (n + 1) by A3, FINSEQ_1: 39;

      reconsider g as FinSequence of REAL ;

      

       A5: ( len <*f0*>) = 1 by FINSEQ_1: 39;

      

       A6: for k be Nat st k < (n + 1) holds (f1 . k) = (h . (k + 1))

      proof

        let k be Nat;

        assume k < (n + 1);

        then

         A7: k <= n by NAT_1: 13;

        per cases by NAT_1: 14;

          suppose

           A8: 1 <= k;

          then

           A9: k in ( dom g) by FINSEQ_3: 25, A7, A3;

          

           A10: ((f | ( Seg n)) . k) = (f . k) by FUNCT_1: 49, A2, FINSEQ_3: 25, A7, A3, A8;

          ((f |_ ( Seg n)) . k) = (f . k) by A2, A8, Th17, FINSEQ_3: 25, A7, A3;

          hence thesis by FINSEQ_1:def 7, A5, A9, A10;

        end;

          suppose

           A11: k = 0 ;

          then not k in ( Seg n) by FINSEQ_1: 1;

          then not k in ( dom (f | ( Seg n))) by RELAT_1: 57;

          then (f1 . k) = (( NAT --> 0 ) . k) by FUNCT_4: 11;

          hence thesis by A0, A11;

        end;

      end;

      for k be Nat st k >= (n + 1) holds (f1 . k) = 0

      proof

        let k be Nat;

        assume k >= (n + 1);

        then k > n by XXREAL_0: 2, NAT_1: 16;

        then not k in ( Seg n) by FINSEQ_1: 1;

        then not k in ( dom (f | ( Seg n))) by RELAT_1: 57;

        

        then (f1 . k) = (( NAT --> 0 ) . k) by FUNCT_4: 11

        .= 0 ;

        hence thesis;

      end;

      then ( Sum f1) = ( Sum h) by IRRAT_1: 18, A6, A4;

      then ( Sum f1) = (f0 + ( Sum g)) by RVSUM_1: 76;

      hence thesis by A0;

    end;

    theorem :: LIOUVIL1:19

    

     Th19: for f be Real_Sequence, n be Nat holds ( dom ( FinSeq (f,n))) = ( Seg n)

    proof

      let f be Real_Sequence, n be Nat;

      ( dom f) = NAT by FUNCT_2:def 1;

      hence thesis by RELAT_1: 62;

    end;

    theorem :: LIOUVIL1:20

    

     Th20: for f be Real_Sequence, i be Nat holds (( FinSeq (f,i)) ^ <*(f . (i + 1))*>) = ( FinSeq (f,(i + 1)))

    proof

      let f be Real_Sequence, i be Nat;

      set f1 = ( FinSeq (f,i)), g = <*(f . (i + 1))*>, h = ( FinSeq (f,(i + 1)));

      ( dom f1) = ( Seg i) by Th19;

      then ( Seg ( len f1)) = ( Seg i) by FINSEQ_1:def 3;

      then

       A0: ( len f1) = i by FINSEQ_1: 6;

      

       A1: ( dom (f1 ^ g)) = ( Seg (( len f1) + ( len g))) by FINSEQ_1:def 7

      .= ( Seg (i + 1)) by FINSEQ_1: 39, A0

      .= ( dom h) by Th19;

      for k be Nat st k in ( dom (f1 ^ g)) holds ((f1 ^ g) . k) = (h . k)

      proof

        let k be Nat;

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

        then

         A2: ( Seg i) c= ( Seg (i + 1)) by FINSEQ_1: 5;

        assume k in ( dom (f1 ^ g));

        per cases by FINSEQ_1: 25;

          suppose

           A3: k in ( dom f1);

          then

           A4: k in ( Seg i) by Th19;

          ((f1 ^ g) . k) = (f1 . k) by FINSEQ_1:def 7, A3

          .= (f . k) by A4, FUNCT_1: 49

          .= (h . k) by A2, A4, FUNCT_1: 49;

          hence thesis;

        end;

          suppose ex n be Nat st n in ( dom g) & k = (( len f1) + n);

          then

          consider n be Nat such that

           A5: n in ( dom g) & k = (( len f1) + n);

          n in ( Seg 1) by A5, FINSEQ_1:def 8;

          then

           A6: n = 1 by TARSKI:def 1, FINSEQ_1: 2;

          1 <= (i + 1) by NAT_1: 12;

          hence thesis by FUNCT_1: 49, FINSEQ_1: 1, A0, A5, A6;

        end;

      end;

      hence thesis by A1, FINSEQ_1: 13;

    end;

    theorem :: LIOUVIL1:21

    

     Th21: for f be Real_Sequence, n be Nat st (f . 0 ) = 0 holds ( Sum ( FinSeq (f,n))) = (( Partial_Sums f) . n)

    proof

      let f be Real_Sequence, n be Nat;

      assume

       A0: (f . 0 ) = 0 ;

      defpred P[ Nat] means ( Sum ( FinSeq (f,$1))) = (( Partial_Sums f) . $1);

      ( Sum ( FinSeq (f, 0 ))) = 0

      .= (( Partial_Sums f) . 0 ) by A0, SERIES_1:def 1;

      then

       A1: P[ 0 ];

      

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

      proof

        let i be Nat;

        assume

         A3: P[i];

        

         A4: (( FinSeq (f,i)) ^ <*(f . (i + 1))*>) = ( FinSeq (f,(i + 1))) by Th20;

        (( Partial_Sums f) . (i + 1)) = ((( Partial_Sums f) . i) + (f . (i + 1))) by SERIES_1:def 1

        .= (( addreal "**" ( FinSeq (f,i))) + (f . (i + 1))) by RVSUM_1:def 12, A3

        .= ( addreal . (( addreal "**" ( FinSeq (f,i))),(f . (i + 1)))) by BINOP_2:def 9

        .= ( addreal "**" (( FinSeq (f,i)) ^ <*(f . (i + 1))*>)) by FINSOP_1: 4

        .= ( Sum ( FinSeq (f,(i + 1)))) by RVSUM_1:def 12, A4;

        hence thesis;

      end;

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

      hence thesis;

    end;

    theorem :: LIOUVIL1:22

    

     Th22: for f be Real_Sequence, n be Nat st (f . 0 ) = 0 holds ( Sum (f |_ ( Seg n))) = (( Partial_Sums f) . n)

    proof

      let f be Real_Sequence, n be Nat;

      assume

       A1: (f . 0 ) = 0 ;

      ( Sum ( FinSeq (f,n))) = (( Partial_Sums f) . n) by A1, Th21;

      hence thesis by A1, Th18;

    end;

    theorem :: LIOUVIL1:23

    for f be INT -valued Real_Sequence, n be Nat st (f . 0 ) = 0 holds ( Sum (f |_ ( Seg n))) is Integer

    proof

      let f be INT -valued Real_Sequence, n be Nat;

      assume

       A1: (f . 0 ) = 0 ;

      set ff = (f |_ ( Seg n));

      ( Sum ff) = (( Partial_Sums f) . n) by Th22, A1;

      hence thesis;

    end;

    theorem :: LIOUVIL1:24

    

     Th23: for f be Real_Sequence, n be Nat st f is summable & (f . 0 ) = 0 holds ( Sum f) = (( Sum ( FinSeq (f,n))) + ( Sum (f ^\ (n + 1))))

    proof

      let f be Real_Sequence, n be Nat;

      assume

       A1: f is summable & (f . 0 ) = 0 ;

      then ( Sum f) = ((( Partial_Sums f) . n) + ( Sum (f ^\ (n + 1)))) by SERIES_1: 15;

      hence thesis by A1, Th21;

    end;

    registration

      cluster positive-yielding NAT -valued for Real_Sequence;

      existence

      proof

        take ( seq_const 1);

        thus thesis;

      end;

    end

    begin

    definition

      let f be Real_Sequence;

      :: LIOUVIL1:def3

      attr f is eventually-non-zero means

      : ENZ: for n be Nat holds ex N be Nat st n <= N & (f . N) <> 0 ;

    end

    registration

      cluster eventually-nonzero -> eventually-non-zero for Real_Sequence;

      coherence

      proof

        let f be Real_Sequence;

        assume

         A1: f is eventually-nonzero;

        let n be Nat;

        consider N be Nat such that

         A2: for k be Nat st k >= N holds (f . k) <> 0 by A1;

        reconsider m = ( max (N,n)) as Nat;

        (f . m) <> 0 by A2, XXREAL_0: 25;

        hence thesis by XXREAL_0: 25;

      end;

    end

    registration

      cluster ( seq_id ( id NAT )) -> eventually-nonzero;

      coherence

      proof

        set f = ( seq_id ( id NAT ));

        

         A0: ( dom ( id NAT )) = NAT ;

        ( rng ( id NAT )) c= REAL ;

        then

         A1: ( id NAT ) is Function of NAT , REAL by A0, FUNCT_2: 2;

        take N = 1;

        let n be Nat;

        assume n >= N;

        hence thesis by FUNCT_1: 18, A1, ORDINAL1:def 12;

      end;

    end

    registration

      cluster eventually-non-zero for Real_Sequence;

      existence

      proof

        take f = ( seq_id ( id NAT ));

        thus thesis;

      end;

    end

    theorem :: LIOUVIL1:25

    

     Th24: for f be eventually-non-zero Real_Sequence holds for n be Nat holds (f ^\ n) is eventually-non-zero

    proof

      let f be eventually-non-zero Real_Sequence, n be Nat;

      set g = (f ^\ n);

      let k be Nat;

      consider N be Nat such that

       A1: (k + n) <= N & (f . N) <> 0 by ENZ;

      k <= (N - n) by A1, XREAL_1: 19;

      then (N - n) in NAT by INT_1: 3;

      then

      reconsider Nn = (N - n) as Nat;

      take Nn;

      (g . Nn) = (f . (Nn + n)) by NAT_1:def 3

      .= (f . N);

      hence thesis by A1, XREAL_1: 19;

    end;

    registration

      let f be eventually-non-zero Real_Sequence, n be Nat;

      cluster (f ^\ n) -> eventually-non-zero;

      coherence by Th24;

    end

    registration

      cluster non-zero constant -> eventually-non-zero for Real_Sequence;

      coherence

      proof

        let f be Real_Sequence;

        assume

         A0: f is non-zero constant;

        consider x be set such that

         A1: x in ( dom f) & ( the_value_of f) = (f . x) by FUNCT_1:def 12, A0;

        

         A2: ( the_value_of f) in ( rng f) by A1, FUNCT_1: 3;

        reconsider v = ( the_value_of f) as Real by A1;

        

         A3: ( dom f) = NAT by FUNCT_2:def 1;

        let n be Nat;

        take N = (n + 1);

        thus thesis by A0, A1, A2, A3, XREAL_1: 31, FUNCT_1:def 10;

      end;

    end

    definition

      let b be Nat;

      :: LIOUVIL1:def4

      func powerfact b -> Real_Sequence means

      : DefPower: for i be Nat holds (it . i) = (1 / (b to_power (i ! )));

      correctness

      proof

        deffunc F( Nat) = (1 / (b to_power ($1 ! )));

        thus (ex f be Real_Sequence st for n be Nat holds (f . n) = F(n)) & for f1,f2 be Real_Sequence st (for n be Nat holds (f1 . n) = F(n)) & (for n be Nat holds (f2 . n) = F(n)) holds f1 = f2 from IRRAT_1:sch 1;

      end;

    end

    theorem :: LIOUVIL1:26

    

     Th25: for b,i be Nat st b >= 1 holds (( powerfact b) . i) <= (((1 / b) GeoSeq ) . i)

    proof

      let b,i be Nat;

      assume

       A1: b >= 1;

      

       A3: (( powerfact b) . i) = (1 / (b to_power (i ! ))) by DefPower;

      

       A2: (((1 / b) GeoSeq ) . i) = ((1 / b) |^ i) by PREPOWER:def 1

      .= (1 / (b to_power i)) by PREPOWER: 7;

      (1 * (b to_power i)) <= (1 * (b to_power (i ! ))) by A1, PRE_FF: 8, NEWTON: 38;

      hence thesis by A2, A3, A1, XREAL_1: 102;

    end;

    theorem :: LIOUVIL1:27

    

     Th26: for b be Nat st b > 1 holds ( powerfact b) is summable & ( Sum ( powerfact b)) <= (b / (b - 1))

    proof

      let b be Nat;

      assume

       A1: b > 1;

      then |.(1 / b).| < (1 / 1) by XREAL_1: 76;

      then

       A3: ((1 / b) GeoSeq ) is summable by SERIES_1: 24;

      

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

      proof

        let i be Nat;

        (( powerfact b) . i) = (1 / (b to_power (i ! ))) by DefPower;

        hence thesis;

      end;

      

       A4: for i be Nat holds (( powerfact b) . i) <= (((1 / b) GeoSeq ) . i) by A1, Th25;

      then ( Sum ( powerfact b)) <= ( Sum ((1 / b) GeoSeq )) by A2, A3, SERIES_1: 20;

      hence thesis by Th13, A1, A2, A3, A4, SERIES_1: 20;

    end;

    registration

      let b be non trivial Nat;

      cluster ( powerfact b) -> summable;

      coherence

      proof

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

        then b > 1 by NAT_1: 13;

        hence thesis by Th26;

      end;

    end

    registration

      cluster nonnegative-yielding for Real_Sequence;

      existence

      proof

        take ( seq_const 1);

        thus thesis;

      end;

    end

    theorem :: LIOUVIL1:28

    

     Th27: for n,b be Nat st b > 1 & n >= 1 holds ( Sum ((b - 1) (#) (( powerfact b) ^\ (n + 1)))) < (1 / ((b to_power (n ! )) to_power n))

    proof

      let n,b be Nat;

      assume

       A0: b > 1 & n >= 1;

      then (( powerfact b) ^\ (n + 1)) is summable by Th26, SERIES_1: 12;

      then

       A2: ( Sum ((b - 1) (#) (( powerfact b) ^\ (n + 1)))) = ((b - 1) * ( Sum (( powerfact b) ^\ (n + 1)))) by SERIES_1: 10;

      1 < (b - 0 ) by A0;

      then

       A3: (b - 1) > 0 by XREAL_1: 12;

      set s1 = (( powerfact b) ^\ (n + 1));

      set s2 = (((1 / b) GeoSeq ) ^\ ((n + 1) ! ));

      

       A4: |.(1 / b).| < (1 / 1) by A0, XREAL_1: 76;

      then

       A5: ((1 / b) GeoSeq ) is summable by SERIES_1: 24;

      

       A6: for k be Nat holds 0 <= (s1 . k) & (s1 . k) <= (s2 . k)

      proof

        let k be Nat;

        

         A7: (s1 . k) = (( powerfact b) . (k + (n + 1))) by NAT_1:def 3

        .= (1 / (b to_power ((k + (n + 1)) ! ))) by DefPower;

        k = 0 or k >= (1 + 0 ) by NAT_1: 13;

        per cases ;

          suppose

           A8: k >= 1;

          

           A9: (s2 . k) = (((1 / b) GeoSeq ) . (k + ((n + 1) ! ))) by NAT_1:def 3

          .= ((1 / b) |^ (k + ((n + 1) ! ))) by PREPOWER:def 1

          .= (1 / (b |^ (k + ((n + 1) ! )))) by PREPOWER: 7;

          (n + 1) >= 1 by A0, NAT_1: 16;

          then (b to_power (k + ((n + 1) ! ))) <= (b to_power ((k + (n + 1)) ! )) by PRE_FF: 8, A0, Th8, A8;

          then ((b |^ (k + ((n + 1) ! ))) " ) >= ((b |^ ((k + (n + 1)) ! )) " ) by A0, XREAL_1: 85;

          then (1 / (b |^ (k + ((n + 1) ! )))) >= ((b |^ ((k + (n + 1)) ! )) " ) by XCMPLX_1: 215;

          hence thesis by A7, A9, XCMPLX_1: 215;

        end;

          suppose

           A10: k = 0 ;

          

          then

           A11: (s1 . k) = (( powerfact b) . ( 0 + (n + 1))) by NAT_1:def 3

          .= (1 / (b to_power ((n + 1) ! ))) by DefPower;

          hence (s1 . k) >= 0 ;

          (s2 . k) = (((1 / b) GeoSeq ) . ( 0 + ((n + 1) ! ))) by NAT_1:def 3, A10

          .= ((1 / b) |^ ( 0 + ((n + 1) ! ))) by PREPOWER:def 1

          .= (1 / (b |^ ( 0 + ((n + 1) ! )))) by PREPOWER: 7;

          hence thesis by A11;

        end;

      end;

      

       A12: s2 is summable by A4, SERIES_1: 12, SERIES_1: 24;

      ex k be Nat st 1 <= k & (s1 . k) < (s2 . k)

      proof

        take k = 2;

        

         A13: (s1 . k) = (( powerfact b) . (k + (n + 1))) by NAT_1:def 3

        .= (1 / (b to_power ((k + (n + 1)) ! ))) by DefPower;

        

         A14: (s2 . k) = (((1 / b) GeoSeq ) . (k + ((n + 1) ! ))) by NAT_1:def 3

        .= ((1 / b) |^ (k + ((n + 1) ! ))) by PREPOWER:def 1

        .= (1 / (b |^ (k + ((n + 1) ! )))) by PREPOWER: 7;

        (n + 1) > ( 0 + 1) by A0, XREAL_1: 8;

        then (b to_power (k + ((n + 1) ! ))) < (b to_power ((k + (n + 1)) ! )) by POWER: 39, A0, Th6;

        then ((b |^ (k + ((n + 1) ! ))) " ) > ((b |^ ((k + (n + 1)) ! )) " ) by A0, XREAL_1: 88;

        then (1 / (b |^ (k + ((n + 1) ! )))) > ((b |^ ((k + (n + 1)) ! )) " ) by XCMPLX_1: 215;

        hence thesis by A13, A14, XCMPLX_1: 215;

      end;

      then ( Sum s1) < ( Sum s2) by A6, A12, Th11;

      then

       A15: ((b - 1) * ( Sum (( powerfact b) ^\ (n + 1)))) < ((b - 1) * ( Sum (((1 / b) GeoSeq ) ^\ ((n + 1) ! )))) by XREAL_1: 68, A3;

      reconsider bn = (b |^ ((n + 1) ! )) as Nat;

      

       A16: (((1 / b) GeoSeq ) ^\ ((n + 1) ! )) = ((1 / bn) (#) ((1 / b) GeoSeq ))

      proof

        now

          let i be Element of NAT ;

          

          thus ((((1 / b) GeoSeq ) ^\ ((n + 1) ! )) . i) = (((1 / b) GeoSeq ) . (i + ((n + 1) ! ))) by NAT_1:def 3

          .= ((1 / b) |^ (i + ((n + 1) ! ))) by PREPOWER:def 1

          .= (((1 / b) |^ i) * ((1 / b) |^ ((n + 1) ! ))) by NEWTON: 8

          .= (((1 / b) |^ i) * (1 / (b |^ ((n + 1) ! )))) by PREPOWER: 7

          .= ((1 / (b |^ ((n + 1) ! ))) * (((1 / b) GeoSeq ) . i)) by PREPOWER:def 1

          .= (((1 / (b |^ ((n + 1) ! ))) (#) ((1 / b) GeoSeq )) . i) by VALUED_1: 6;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      ( Sum (((1 / b) GeoSeq ) ^\ ((n + 1) ! ))) = ((1 / (b |^ ((n + 1) ! ))) * ( Sum ((1 / b) GeoSeq ))) by A16, A5, SERIES_1: 10

      .= ((1 / (b |^ ((n + 1) ! ))) * (b / (b - 1))) by Th13, A0

      .= ((1 * b) / ((b |^ ((n + 1) ! )) * (b - 1))) by XCMPLX_1: 76

      .= (b / ((b |^ ((n + 1) ! )) * (b - 1)));

      

      then

       A17: ((b - 1) * ( Sum (((1 / b) GeoSeq ) ^\ ((n + 1) ! )))) = ((b - 1) * ((b / bn) / (b - 1))) by XCMPLX_1: 78

      .= (((b - 1) * (b / bn)) / (b - 1)) by XCMPLX_1: 74

      .= (b / (b |^ ((n + 1) ! ))) by A3, XCMPLX_1: 89;

      (n ! ) >= 1 by Th2;

      then

       A18: (b / (b |^ ((n + 1) ! ))) <= ((b |^ (n ! )) / (b |^ ((n + 1) ! ))) by XREAL_1: 72, A0, PREPOWER: 12;

      ((b |^ (n ! )) / (b |^ ((n + 1) ! ))) = ((b to_power (n ! )) / (b to_power ((n + 1) ! )))

      .= (b to_power ((n ! ) - ((n + 1) ! ))) by POWER: 29, A0

      .= (b to_power ( - (((n + 1) ! ) - (n ! ))))

      .= (b to_power ( - (n * (n ! )))) by Th3

      .= (1 / (b to_power (n * (n ! )))) by POWER: 28, A0

      .= (1 / ((b to_power (n ! )) to_power n)) by POWER: 33, A0;

      hence thesis by A2, A15, XXREAL_0: 2, A17, A18;

    end;

    begin

    ::$Notion-Name

    definition

      let x be Real;

      :: LIOUVIL1:def5

      attr x is liouville means for n be Nat holds ex p be Integer, q be Nat st q > 1 & 0 < |.(x - (p / q)).| < (1 / (q |^ n));

    end

    theorem :: LIOUVIL1:29

    

     Def2: for r be Real holds r is liouville iff for n be non zero Nat holds ex p be Integer, q be Nat st 1 < q & 0 < |.(r - (p / q)).| < (1 / (q |^ n))

    proof

      let r be Real;

      thus r is liouville implies for n be non zero Nat holds ex p be Integer, q be Nat st 1 < q & 0 < |.(r - (p / q)).| < (1 / (q |^ n));

      assume

       Z1: for n be non zero Nat holds ex p be Integer, q be Nat st 1 < q & 0 < |.(r - (p / q)).| < (1 / (q |^ n));

      let n be Nat;

      per cases ;

        suppose n is non zero;

        hence thesis by Z1;

      end;

        suppose

         A1: n is zero;

        consider p be Integer, q be Nat such that

         A2: 1 < q and

         A3: 0 < |.(r - (p / q)).| and

         A4: |.(r - (p / q)).| < (1 / (q |^ 1)) by Z1;

        take p, q;

        thus 1 < q & 0 < |.(r - (p / q)).| by A2, A3;

        

         A5: (q |^ 0 ) = 1 by NEWTON: 4;

        (1 / q) < (1 / 1) by A2, XREAL_1: 76;

        hence thesis by A1, A4, A5, XXREAL_0: 2;

      end;

    end;

    definition

      let a be Real_Sequence, b be Nat;

      :: LIOUVIL1:def6

      func Liouville_seq (a,b) -> Real_Sequence means

      : DefLio: (it . 0 ) = 0 & for k be non zero Nat holds (it . k) = ((a . k) / (b to_power (k ! )));

      existence

      proof

        deffunc G( Nat, Element of REAL ) = ( In (((a . ($1 + 1)) / (b to_power (($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

        .= ((a . (k + 1)) / (b to_power ((k + 1) ! )));

        hence thesis by A2;

      end;

      uniqueness

      proof

        let f1,f2 be Real_Sequence;

        assume that

         A1: (f1 . 0 ) = 0 & for n be non zero Nat holds (f1 . n) = ((a . n) / (b to_power (n ! ))) and

         A2: (f2 . 0 ) = 0 & for n be non zero Nat holds (f2 . n) = ((a . n) / (b to_power (n ! )));

        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 A1, A2;

          end;

            suppose

             A3: n <> 0 ;

            

            then (f1 . n) = ((a . n) / (b to_power (n ! ))) by A1

            .= (f2 . n) by A2, A3;

            hence thesis;

          end;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    ::$Notion-Name

    registration

      cluster liouville -> irrational for Real;

      coherence

      proof

        let x be Real;

        assume

         A0: x is liouville;

        assume x is rational;

        then

        consider c be Integer, d be Nat such that

         A1: d <> 0 & x = (c / d) by RAT_1: 8;

        consider n be non zero Nat such that

         ST: (2 to_power (n - 1)) > d by Th10;

        consider p be Integer, q be Nat such that

         B1: q > 1 & 0 < |.(x - (p / q)).| < (1 / (q |^ n)) by A0;

        

         SS: |.((c / d) - (p / q)).| = |.(((c * q) - (p * d)) / (d * q)).| by XCMPLX_1: 130, B1, A1

        .= ( |.((c * q) - (p * d)).| / |.(d * q).|) by COMPLEX1: 67

        .= ( |.((c * q) - (p * d)).| / (d * q));

        ((c * q) - (p * d)) <> 0

        proof

          assume ((c * q) - (p * d)) = 0 ;

          then (p / q) = (c / d) by XCMPLX_1: 94, B1, A1;

          hence thesis by B1, A1;

        end;

        then

         HR: |.(x - (p / q)).| >= (1 / (d * q)) by SS, A1, XREAL_1: 72, NAT_1: 14;

        (d * q) < ((2 to_power (n - 1)) * q) by B1, ST, XREAL_1: 68;

        then (1 / (d * q)) > (1 / ((2 to_power (n - 1)) * q)) by XREAL_1: 76, A1, B1;

        then

         HG: |.(x - (p / q)).| >= (1 / ((2 to_power (n - 1)) * q)) by HR, XXREAL_0: 2;

        

         FG: (2 to_power (n - 1)) > 0 by POWER: 34;

        (n - 0 ) >= 1 by NAT_1: 14;

        then

         FO: (n - 1) >= 0 by XREAL_1: 11;

        (1 + 1) <= q by B1, NAT_1: 13;

        then (2 to_power (n - 1)) <= (q to_power (n - 1)) by FO, HOLDER_1: 3;

        then ((2 to_power (n - 1)) * q) <= ((q to_power (n - 1)) * (q to_power 1)) by XREAL_1: 66, FG;

        then ((2 to_power (n - 1)) * q) <= (q to_power ((n - 1) + 1)) by B1, POWER: 27;

        then

         qa: ((2 to_power (n - 1)) * q) <= (q to_power n);

        (2 to_power (n - 1)) > 0 by POWER: 34;

        then (1 / ((2 to_power (n - 1)) * q)) >= (1 / (q |^ n)) by XREAL_1: 118, qa, B1;

        hence thesis by B1, XXREAL_0: 2, HG;

      end;

    end

    begin

    ::$Notion-Name

    definition

      let a be Real_Sequence, b be Nat;

      :: LIOUVIL1:def7

      func Liouville_constant (a,b) -> Real equals ( Sum ( Liouville_seq (a,b)));

      coherence ;

    end

    definition

      let b be Nat;

      :: LIOUVIL1:def8

      func BLiouville_seq b -> Real_Sequence means

      : LiuSeq: for n be Nat holds (it . n) = (b to_power (n ! ));

      correctness

      proof

        deffunc F( Nat) = (b to_power ($1 ! ));

        thus (ex f be Real_Sequence st for n be Nat holds (f . n) = F(n)) & for f1,f2 be Real_Sequence st (for n be Nat holds (f1 . n) = F(n)) & (for n be Nat holds (f2 . n) = F(n)) holds f1 = f2 from IRRAT_1:sch 1;

      end;

    end

    registration

      let b be Nat;

      cluster ( BLiouville_seq b) -> NAT -valued;

      coherence

      proof

        set f = ( BLiouville_seq b);

        let x be object;

        assume x in ( rng f);

        then

        consider n be object such that

         AB: n in ( dom f) & x = (f . n) by FUNCT_1:def 3;

        reconsider n as Nat by AB;

        (f . n) = (b to_power (n ! )) by LiuSeq;

        hence thesis by AB;

      end;

    end

    definition

      let a be Real_Sequence, b be Nat;

      :: LIOUVIL1:def9

      func ALiouville_seq (a,b) -> Real_Sequence means

      : ALiuDef: for n be Nat holds (it . n) = ((( BLiouville_seq b) . n) * ( Sum (( Liouville_seq (a,b)) |_ ( Seg n))));

      correctness

      proof

        deffunc F( Nat) = ((( BLiouville_seq b) . $1) * ( Sum (( Liouville_seq (a,b)) |_ ( Seg $1))));

        thus (ex f be Real_Sequence st for n be Nat holds (f . n) = F(n)) & for f1,f2 be Real_Sequence st (for n be Nat holds (f1 . n) = F(n)) & (for n be Nat holds (f2 . n) = F(n)) holds f1 = f2 from IRRAT_1:sch 1;

      end;

    end

    theorem :: LIOUVIL1:30

    

     Th28: for a be NAT -valued Real_Sequence, b,n,k be Nat st b > 0 & k <= n holds ((( Liouville_seq (a,b)) . k) * (( BLiouville_seq b) . n)) is Integer

    proof

      let a be NAT -valued Real_Sequence, b,n,k be Nat;

      assume

       A1: b > 0 & k <= n;

      then ( 0 + (k ! )) <= (n ! ) by SIN_COS: 39;

      then

       A2: ((n ! ) - (k ! )) in NAT by INT_1: 3, XREAL_1: 19;

      set bk = (b to_power (k ! )), bn = (b to_power (n ! ));

      

       A3: (bn / bk) = (b to_power ((n ! ) - (k ! ))) by A1, POWER: 29;

      per cases ;

        suppose k = 0 ;

        then (( Liouville_seq (a,b)) . k) = 0 by DefLio;

        hence thesis;

      end;

        suppose k is non zero;

        then (( Liouville_seq (a,b)) . k) = ((a . k) / (b to_power (k ! ))) by DefLio;

        

        then ((( Liouville_seq (a,b)) . k) * (( BLiouville_seq b) . n)) = (((a . k) / (b to_power (k ! ))) * ((b to_power (n ! )) / 1)) by LiuSeq

        .= (((a . k) * bn) / (bk * 1)) by XCMPLX_1: 76

        .= ((a . k) * (bn / bk)) by XCMPLX_1: 74;

        hence thesis by A2, A3;

      end;

    end;

    theorem :: LIOUVIL1:31

    

     Th29: for a be NAT -valued Real_Sequence, b,n be Nat st b > 0 holds (( ALiouville_seq (a,b)) . n) is Integer

    proof

      let a be NAT -valued Real_Sequence, b,n be Nat;

      set LS = ( Liouville_seq (a,b));

      set BS = ( BLiouville_seq b);

      set AS = ( ALiouville_seq (a,b));

      set ff = ((BS . n) (#) (LS |_ ( Seg n)));

      assume

       A0: b > 0 ;

      

       A1: (AS . n) = ((BS . n) * ( Sum (LS |_ ( Seg n)))) by ALiuDef;

      

       A2: ((BS . n) * ( Sum (LS |_ ( Seg n)))) = ( Sum ff) by SERIES_1: 10;

      ( rng ff) c= INT

      proof

        let y be object;

        assume y in ( rng ff);

        then

        consider x be object such that

         A3: x in ( dom ff) & y = (ff . x) by FUNCT_1:def 3;

        reconsider x as Nat by A3;

        

         A4: y = ((( BLiouville_seq b) . n) * ((( Liouville_seq (a,b)) |_ ( Seg n)) . x)) by A3, VALUED_1: 6;

        per cases ;

          suppose

           A5: x in ( Seg n);

          then

           A6: 1 <= x <= n by FINSEQ_1: 1;

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

          then x in ( dom (LS | ( Seg n))) by A5, RELAT_1: 62;

          

          then

           A8: ((( Liouville_seq (a,b)) |_ ( Seg n)) . x) = ((( Liouville_seq (a,b)) | ( Seg n)) . x) by FUNCT_4: 13

          .= (( Liouville_seq (a,b)) . x) by FUNCT_1: 49, A5;

          ((( Liouville_seq (a,b)) . x) * (( BLiouville_seq b) . n)) is Integer by A0, A6, Th28;

          hence thesis by INT_1:def 2, A4, A8;

        end;

          suppose not x in ( Seg n);

          then not x in ( dom (( Liouville_seq (a,b)) | ( Seg n))) by RELAT_1: 57;

          then ((( Liouville_seq (a,b)) |_ ( Seg n)) . x) = (( NAT --> 0 ) . x) by FUNCT_4: 11;

          hence thesis by INT_1:def 2, A4;

        end;

      end;

      then

      reconsider ff as INT -valued Real_Sequence by RELAT_1:def 19;

      set m = (n + 1);

      for k be Nat st k >= m holds (ff . k) = 0

      proof

        let k be Nat;

        assume k >= m;

        then k > n by NAT_1: 13;

        then not k in ( Seg n) by FINSEQ_1: 1;

        then

         A9: not k in ( dom (LS | ( Seg n))) by RELAT_1: 57;

        

         A10: (ff . k) = ((BS . n) * ((LS |_ ( Seg n)) . k)) by VALUED_1: 6;

        ((LS |_ ( Seg n)) . k) = (( NAT --> 0 ) . k) by FUNCT_4: 11, A9

        .= 0 ;

        hence thesis by A10;

      end;

      hence thesis by A1, A2, Th16;

    end;

    registration

      let a be NAT -valued Real_Sequence;

      let b be non zero Nat;

      cluster ( ALiouville_seq (a,b)) -> INT -valued;

      coherence

      proof

        set f = ( ALiouville_seq (a,b));

        ( rng f) c= INT

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A1: x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

          reconsider x as Nat by A1;

          y is Integer by Th29, A1;

          hence thesis by INT_1:def 2;

        end;

        hence thesis by RELAT_1:def 19;

      end;

    end

    theorem :: LIOUVIL1:32

    

     Th30: for n,b be non zero Nat st b > 1 holds (( BLiouville_seq b) . n) > 1

    proof

      let n,b be non zero Nat;

      assume

       A1: b > 1;

      (( BLiouville_seq b) . n) = (b to_power (n ! )) by LiuSeq;

      hence thesis by A1, POWER: 35;

    end;

    theorem :: LIOUVIL1:33

    

     Th31: for a be NAT -valued Real_Sequence, b be non zero Nat st b >= 2 & ( rng a) c= b holds ( Liouville_seq (a,b)) is summable

    proof

      let a be NAT -valued Real_Sequence, b be non zero Nat;

      assume

       A1: b >= 2 & ( rng a) c= b;

      

       A2: b > 1 by A1, XXREAL_0: 2;

      then

       A3: (b - 1) >= 0 by XREAL_1: 48;

      set f = ( Liouville_seq (a,b));

      

       A4: for i be Nat holds ((b - 1) / (b to_power (i ! ))) = (((b - 1) (#) ( powerfact b)) . i)

      proof

        let i be Nat;

        (((b - 1) (#) ( powerfact b)) . i) = ((b - 1) * (( powerfact b) . i)) by VALUED_1: 6

        .= ((b - 1) * (1 / (b to_power (i ! )))) by DefPower

        .= ((b - 1) / (b to_power (i ! ))) by XCMPLX_1: 99;

        hence thesis;

      end;

      

       A5: for i be Nat holds (f . i) >= 0 & (f . i) <= (((b - 1) (#) ( powerfact b)) . i)

      proof

        let i be Nat;

        reconsider b1 = (b - 1) as Element of NAT by INT_1: 3, XREAL_1: 48, A2;

        per cases ;

          suppose

           A6: i is zero;

          then

           A7: (f . i) = 0 by DefLio;

          

           A8: (b to_power (i ! )) = b by NEWTON: 12, A6;

          ((b - 1) / b) >= 0 by A3;

          hence thesis by A7, A4, A8;

        end;

          suppose

           A9: i is non zero;

          then

          reconsider ii = i as non zero Nat;

          

           A10: (f . i) = ((a . i) / (b to_power (i ! ))) by A9, DefLio;

          reconsider ai = (a . i) as Nat;

          (a . i) in ( rng a) by NAT_1: 51;

          then (a . i) in b by A1;

          then (a . i) in ( Segm b) by ORDINAL1:def 17;

          then ai < (b1 + 1) by NAT_1: 44;

          then ai <= b1 by NAT_1: 13;

          then (f . i) <= ((b - 1) / (b to_power (i ! ))) by A10, XREAL_1: 72;

          hence thesis by A4, A10;

        end;

      end;

      ( powerfact b) is summable by A2, Th26;

      then ((b - 1) (#) ( powerfact b)) is summable by SERIES_1: 10;

      hence thesis by A5, SERIES_1: 20;

    end;

    theorem :: LIOUVIL1:34

    

     Th32: for a be Real_Sequence, n be non zero Nat, b be non zero Nat st b > 1 holds ((( ALiouville_seq (a,b)) . n) / (( BLiouville_seq b) . n)) = ( Sum ( FinSeq (( Liouville_seq (a,b)),n)))

    proof

      let a be Real_Sequence, n,b be non zero Nat;

      assume b > 1;

      then

       A1: (( BLiouville_seq b) . n) <> 0 by Th30;

      

       A2: (( Liouville_seq (a,b)) . 0 ) = 0 by DefLio;

      

      thus ((( ALiouville_seq (a,b)) . n) / (( BLiouville_seq b) . n)) = (((( BLiouville_seq b) . n) * ( Sum (( Liouville_seq (a,b)) |_ ( Seg n)))) / (( BLiouville_seq b) . n)) by ALiuDef

      .= ( Sum (( Liouville_seq (a,b)) |_ ( Seg n))) by XCMPLX_1: 89, A1

      .= ( Sum ( FinSeq (( Liouville_seq (a,b)),n))) by Th18, A2;

    end;

    theorem :: LIOUVIL1:35

    

     Th33: for a be NAT -valued Real_Sequence, b be non trivial Nat, n be Nat holds (( Liouville_seq (a,b)) . n) >= 0

    proof

      let a be NAT -valued Real_Sequence, b be non trivial Nat, n be Nat;

      per cases ;

        suppose n = 0 ;

        hence thesis by DefLio;

      end;

        suppose n <> 0 ;

        then (( Liouville_seq (a,b)) . n) = ((a . n) / (b to_power (n ! ))) by DefLio;

        hence thesis;

      end;

    end;

    theorem :: LIOUVIL1:36

    for a be positive-yielding NAT -valued Real_Sequence, b be non trivial Nat, n be non zero Nat holds (( Liouville_seq (a,b)) . n) > 0

    proof

      let a be positive-yielding NAT -valued Real_Sequence, b be non trivial Nat, n be non zero Nat;

      

       A1: (( Liouville_seq (a,b)) . n) = ((a . n) / (b to_power (n ! ))) by DefLio;

      n in NAT by ORDINAL1:def 12;

      then n in ( dom a) by FUNCT_2:def 1;

      then (a . n) in ( rng a) by FUNCT_1: 3;

      then (a . n) > 0 by PARTFUN3:def 1;

      hence thesis by A1;

    end;

    registration

      let a be NAT -valued Real_Sequence, b be non trivial Nat;

      cluster ( Liouville_seq (a,b)) -> nonnegative-yielding;

      coherence

      proof

        let r be Real;

        assume r in ( rng ( Liouville_seq (a,b)));

        then

        consider n be object such that

         A1: n in ( dom ( Liouville_seq (a,b))) & r = (( Liouville_seq (a,b)) . n) by FUNCT_1:def 3;

        thus thesis by A1, Th33;

      end;

    end

    theorem :: LIOUVIL1:37

    

     Th34: for a be NAT -valued Real_Sequence, b,c be Nat st b >= 2 & c >= 1 & ( rng a) c= c & c <= b holds for i be Nat holds (( Liouville_seq (a,b)) . i) <= (((c - 1) (#) ( powerfact b)) . i)

    proof

      let a be NAT -valued Real_Sequence, b,c be Nat;

      assume

       A1: b >= 2 & c >= 1 & ( rng a) c= c & c <= b;

      set f = ( Liouville_seq (a,b));

      

       A2: for i be Nat holds ((c - 1) / (b to_power (i ! ))) = (((c - 1) (#) ( powerfact b)) . i)

      proof

        let i be Nat;

        (((c - 1) (#) ( powerfact b)) . i) = ((c - 1) * (( powerfact b) . i)) by VALUED_1: 6

        .= ((c - 1) * (1 / (b to_power (i ! )))) by DefPower

        .= ((c - 1) / (b to_power (i ! ))) by XCMPLX_1: 99;

        hence thesis;

      end;

      let i be Nat;

      

       A4: b >= 1 by A1, XXREAL_0: 2;

      reconsider b1 = (b - 1) as Element of NAT by A4, INT_1: 3, XREAL_1: 48;

      reconsider c1 = (c - 1) as Element of NAT by A1, INT_1: 3, XREAL_1: 48;

      per cases ;

        suppose

         A5: i is zero;

        then

         A6: (f . i) = 0 by DefLio;

        

         A7: (b to_power (i ! )) = b by NEWTON: 12, A5;

        c1 >= 0 ;

        then ((c - 1) / b) >= 0 ;

        hence thesis by A2, A6, A7;

      end;

        suppose

         A8: i is non zero;

        then

        reconsider ii = i as non zero Nat;

        

         A9: (f . i) = ((a . i) / (b to_power (i ! ))) by A8, DefLio;

        reconsider ai = (a . i) as Nat;

        (a . i) in ( rng a) by NAT_1: 51;

        then (a . i) in c by A1;

        then (a . i) in ( Segm c) by ORDINAL1:def 17;

        then ai < (c1 + 1) by NAT_1: 44;

        then ai <= c1 by NAT_1: 13;

        then (f . i) <= ((c - 1) / (b to_power (i ! ))) by A9, XREAL_1: 72;

        hence thesis by A2;

      end;

    end;

    theorem :: LIOUVIL1:38

    for a be NAT -valued Real_Sequence, b,c be Nat st b >= 2 & c >= 1 & ( rng a) c= c & c <= b holds ( Sum ( Liouville_seq (a,b))) <= ( Sum ((c - 1) (#) ( powerfact b)))

    proof

      let a be NAT -valued Real_Sequence, b,c be Nat;

      assume

       A0: b >= 2 & c >= 1 & ( rng a) c= c & c <= b;

      then b >= (1 + 1);

      then b > 1 by NAT_1: 13;

      then ( powerfact b) is summable by Th26;

      then

       A1: ((c - 1) (#) ( powerfact b)) is summable by SERIES_1: 10;

      b is 2 _or_greater by A0, EC_PF_2:def 1;

      then

       A2: for i be Nat holds 0 <= (( Liouville_seq (a,b)) . i) by Th33;

      for i be Nat holds (( Liouville_seq (a,b)) . i) <= (((c - 1) (#) ( powerfact b)) . i) by Th34, A0;

      hence thesis by SERIES_1: 20, A1, A2;

    end;

    theorem :: LIOUVIL1:39

    

     Th35: for a be NAT -valued Real_Sequence, b,c,n be Nat st b >= 2 & c >= 1 & ( rng a) c= c & c <= b holds ( Sum (( Liouville_seq (a,b)) ^\ (n + 1))) <= ( Sum ((c - 1) (#) (( powerfact b) ^\ (n + 1))))

    proof

      let a be NAT -valued Real_Sequence, b,c,n be Nat;

      set g = ((c - 1) (#) (( powerfact b) ^\ (n + 1)));

      assume

       A0: b >= 2 & c >= 1 & ( rng a) c= c & c <= b;

      then b >= (1 + 1);

      then b > 1 by NAT_1: 13;

      then (( powerfact b) ^\ (n + 1)) is summable by Th26, SERIES_1: 12;

      then

       A1: ((c - 1) (#) (( powerfact b) ^\ (n + 1))) is summable by SERIES_1: 10;

      set f = (( Liouville_seq (a,b)) ^\ (n + 1));

      

       A2: b is 2 _or_greater by A0, EC_PF_2:def 1;

      

       A3: for i be Nat holds 0 <= (f . i)

      proof

        let i be Nat;

        ( dom f) = NAT by FUNCT_2:def 1;

        then (f . i) in ( rng f) by FUNCT_1: 3, ORDINAL1:def 12;

        hence thesis by A2, PARTFUN3:def 4;

      end;

      for i be Nat holds (f . i) <= (g . i)

      proof

        let i be Nat;

        

         A4: (f . i) = (( Liouville_seq (a,b)) . ((n + 1) + i)) by NAT_1:def 3;

        (g . i) = ((c - 1) * ((( powerfact b) ^\ (n + 1)) . i)) by SEQ_1: 9

        .= ((c - 1) * (( powerfact b) . ((n + 1) + i))) by NAT_1:def 3

        .= (((c - 1) (#) ( powerfact b)) . ((n + 1) + i)) by SEQ_1: 9;

        hence thesis by A4, Th34, A0;

      end;

      hence thesis by SERIES_1: 20, A1, A3;

    end;

    theorem :: LIOUVIL1:40

    

     Th36: for a be NAT -valued Real_Sequence, b be non trivial Nat, n be Nat st a is eventually-non-zero & ( rng a) c= b holds ( Sum (( Liouville_seq (a,b)) ^\ (n + 1))) > 0

    proof

      let a be NAT -valued Real_Sequence, b be non trivial Nat, n be Nat;

      assume

       A1: a is eventually-non-zero & ( rng a) c= b;

      set LS = (( Liouville_seq (a,b)) ^\ (n + 1));

      

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

      proof

        let i be Nat;

        (LS . i) = (( Liouville_seq (a,b)) . ((n + 1) + i)) by NAT_1:def 3;

        hence thesis by Th33;

      end;

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

      proof

        consider j be Nat such that

         A3: (n + 1) <= j & (a . j) <> 0 by A1;

        (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;

        

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

        (LS . i) = (( Liouville_seq (a,b)) . j) by NAT_1:def 3, A4

        .= ((a . ((n + 1) + i)) / (b to_power (j ! ))) by DefLio;

        hence thesis by A5, A3, ORDINAL1:def 12;

      end;

      then

      consider k be Nat such that

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

      ( Liouville_seq (a,b)) is summable by Th31, A1, NAT_2: 29;

      then LS is summable by SERIES_1: 12;

      hence thesis by A6, RSSPACE2: 3, A2;

    end;

    theorem :: LIOUVIL1:41

    

     Th37: for a be NAT -valued Real_Sequence, b be non trivial Nat st ( rng a) c= b & a is eventually-non-zero holds for n be non zero Nat holds ex p be Integer, q be Nat st q > 1 & 0 < |.(( Liouville_constant (a,b)) - (p / q)).| < (1 / (q |^ n))

    proof

      let a be NAT -valued Real_Sequence, b be non trivial Nat;

      assume

       A1: ( rng a) c= b & a is eventually-non-zero;

      set x = ( Liouville_constant (a,b));

      

       A2: b >= (1 + 1) by NAT_2: 29;

      then

       A3: b > 1 by NAT_1: 13;

      set pn = ( ALiouville_seq (a,b));

      set qn = ( BLiouville_seq b);

      let n be non zero Nat;

      

       A4: n >= ( 0 + 1) by NAT_1: 13;

      reconsider p = (pn . n) as Integer;

      reconsider q = (qn . n) as Nat;

      take p, q;

      

       A5: q = (b to_power (n ! )) by LiuSeq;

      thus q > 1 by Th30, A3;

      set LS = ( Liouville_seq (a,b));

      

       A6: LS is summable by Th31, NAT_2: 29, A1;

      

       A7: ( Sum (( Liouville_seq (a,b)) ^\ (n + 1))) > 0 by Th36, A1;

      (LS . 0 ) = 0 by DefLio;

      then

       A8: ( Sum LS) = (( Sum ( FinSeq (LS,n))) + ( Sum (LS ^\ (n + 1)))) by Th23, A6;

      

       A9: |.(x - (p / q)).| = |.(( Sum ( Liouville_seq (a,b))) - ( Sum ( FinSeq (( Liouville_seq (a,b)),n)))).| by A3, Th32

      .= ( Sum (( Liouville_seq (a,b)) ^\ (n + 1))) by A7, A8, ABSVALUE:def 1;

      

       A10: ( Sum (( Liouville_seq (a,b)) ^\ (n + 1))) <= ( Sum ((b - 1) (#) (( powerfact b) ^\ (n + 1)))) by A1, A2, A3, Th35;

      ( Sum ((b - 1) (#) (( powerfact b) ^\ (n + 1)))) < (1 / ((b to_power (n ! )) to_power n)) by A3, A4, Th27;

      hence thesis by A1, A5, A9, A10, XXREAL_0: 2, Th36;

    end;

    definition

      :: LIOUVIL1:def10

      func Liouville_constant -> Real equals ( Liouville_constant (( seq_const 1),10));

      correctness ;

    end

    theorem :: LIOUVIL1:42

    

     Th38: for a be NAT -valued Real_Sequence, b be non trivial Nat st ( rng a) c= b & a is eventually-non-zero holds ( Liouville_constant (a,b)) is liouville

    proof

      let a be NAT -valued Real_Sequence, b be non trivial Nat;

      assume

       A1: ( rng a) c= b & a is eventually-non-zero;

      set x = ( Liouville_constant (a,b));

      for n be non zero Nat holds ex p be Integer, q be Nat st q > 1 & 0 < |.(x - (p / q)).| < (1 / (q |^ n)) by Th37, A1;

      hence thesis by Def2;

    end;

    registration

      cluster Liouville_constant -> liouville;

      coherence

      proof

        

         A0: ( rng ( seq_const 1)) = {1} by FUNCOP_1: 8;

        

         A1: 1 in 10 by ENUMSET1:def 8, CARD_1: 58;

        10 is non trivial by NAT_2: 28;

        hence thesis by A1, Th38, A0, ZFMISC_1: 31;

      end;

    end

    registration

      cluster liouville for Real;

      existence

      proof

        take Liouville_constant ;

        thus thesis;

      end;

    end

    definition

      mode Liouville is liouville Real;

    end

    theorem :: LIOUVIL1:43

    

     Th39: for m,n be non zero Nat holds (( Liouville_seq (( seq_const 1),m)) . n) = (m to_power ( - (n ! )))

    proof

      let m,n be non zero Nat;

      

      thus (( Liouville_seq (( seq_const 1),m)) . n) = ((( seq_const 1) . n) / (m to_power (n ! ))) by DefLio

      .= (1 / (m to_power (n ! ))) by SEQ_1: 57

      .= ((1 / m) to_power (n ! )) by PREPOWER: 7

      .= (m to_power ( - (n ! ))) by POWER: 32;

    end;

    

     TC1: for m,n be non zero Nat st 1 < m holds (( Liouville_seq (( seq_const 1),m)) . n) <= (1 / (2 to_power n))

    proof

      let m,n be non zero Nat;

      assume

       AS: 1 < m;

      then (1 + 1) <= m by INT_1: 7;

      then

       CCM2: 2 = m or 2 < m by XXREAL_0: 1;

      reconsider fn = (n ! ) as Real;

      

       TT1: (m to_power n) <= (m to_power fn) by PRE_FF: 8, ADDC1, AS;

      

       zz: (( Liouville_seq (( seq_const 1),m)) . n) = (m to_power ( - (n ! ))) by Th39

      .= (m to_power ( - fn))

      .= (1 / (m to_power fn)) by POWER: 28;

      then

       ZXC2: (( Liouville_seq (( seq_const 1),m)) . n) <= (1 / (m to_power n)) by TT1, XREAL_1: 118;

      per cases by POWER: 37, CCM2;

        suppose (2 to_power n) = (m to_power n);

        hence thesis by zz, TT1, XREAL_1: 118;

      end;

        suppose (2 to_power n) < (m to_power n);

        then (1 / (m to_power n)) < (1 / (2 to_power n)) by XREAL_1: 76;

        hence thesis by ZXC2, XXREAL_0: 2;

      end;

    end;

    

     TLLC: for m,n be Nat st 1 < m holds (( Liouville_seq (( seq_const 1),m)) . n) <= (1 / (2 to_power n))

    proof

      let m,n be Nat;

      assume

       AS: 1 < m;

      per cases ;

        suppose n = 0 ;

        hence thesis by DefLio;

      end;

        suppose n is non zero;

        hence thesis by TC1, AS;

      end;

    end;

    theorem :: LIOUVIL1:44

    for m be Nat st 1 < m holds ( Liouville_seq (( seq_const 1),m)) is negligible

    proof

      let m be Nat;

      assume

       AS: 1 < m;

      ex f be Function of NAT , REAL st for x be Nat holds (f . x) = (1 / (2 to_power x))

      proof

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

        (ex f be Real_Sequence st for n be Nat holds (f . n) = F(n)) & for f1,f2 be Real_Sequence st (for n be Nat holds (f1 . n) = F(n)) & (for n be Nat holds (f2 . n) = F(n)) holds f1 = f2 from IRRAT_1:sch 1;

        hence thesis;

      end;

      then

      consider f be Function of NAT , REAL such that

       ACF: for x be Nat holds (f . x) = (1 / (2 to_power x));

      set g = ( Liouville_seq (( seq_const 1),m));

      for x be Nat holds |.(g . x).| <= |.(f . x).|

      proof

        let x be Nat;

        

         m1: (f . x) = (1 / (2 to_power x)) by ACF;

        then

         M1: (g . x) <= (f . x) by TLLC, AS;

         0 <= (g . x)

        proof

          per cases ;

            suppose x = 0 ;

            hence thesis by DefLio;

          end;

            suppose x is non zero;

            then (g . x) = ((( seq_const 1) . x) / (m to_power (x ! ))) by DefLio;

            hence thesis;

          end;

        end;

        then ( - (f . x)) <= (g . x) by m1;

        then

         M3: |.(g . x).| <= (f . x) by M1, ABSVALUE: 5;

        (f . x) <= |.(f . x).| by ABSVALUE: 4;

        hence thesis by XXREAL_0: 2, M3;

      end;

      hence thesis by ACF, ASYMPT_3: 25, ASYMPT_3: 26;

    end;

    theorem :: LIOUVIL1:45

    (1 / 10) < Liouville_constant <= ((10 / 9) - (1 / 10))

    proof

      set x = Liouville_constant ;

      set a = ( seq_const 1);

      set b = 10;

      set c = 2;

      

       A0: ( rng a) = {1} by FUNCOP_1: 8;

      

       A1: 1 in 10 by ENUMSET1:def 8, CARD_1: 58;

      

       A2: 10 is non trivial by NAT_2: 28;

      reconsider n = 1 as non zero Nat;

      set f = ( Liouville_seq (a,b));

      set pb = ( powerfact b);

      

       A3: f is summable by Th31, A0, A1, ZFMISC_1: 31;

      for n be Nat holds 0 <= (f . n) by Th33, A2;

      then

       A4: (f . 1) <= ( Sum f) by RSSPACE2: 3, A3;

      

       A5: (f . 1) = (10 to_power ( - 1)) by NEWTON: 13, Th39

      .= ((1 / 10) to_power 1) by POWER: 32

      .= (1 / 10);

      set s1 = (f ^\ 2);

      set s2 = (pb ^\ 2);

      

       A6: (( powerfact b) . 0 ) = (1 / (b to_power ( 0 ! ))) by DefPower

      .= (1 / b) by NEWTON: 12;

      

       A7: (( powerfact b) . 1) = (1 / (b to_power (1 ! ))) by DefPower

      .= (1 / b) by NEWTON: 13;

      

       A8: (( Partial_Sums pb) . ( 0 + 1)) = ((( Partial_Sums pb) . 0 ) + (pb . ( 0 + 1))) by SERIES_1:def 1

      .= ((pb . 0 ) + (pb . ( 0 + 1))) by SERIES_1:def 1;

      ( Sum pb) = ((( Partial_Sums pb) . 1) + ( Sum (pb ^\ (1 + 1)))) by Th26, SERIES_1: 15

      .= ((2 / b) + ( Sum s2)) by A6, A7, A8;

      then

       A9: ( Sum s2) = (( Sum pb) - (2 / b));

      ( Sum pb) <= (b / (b - 1)) by Th26;

      then

       A10: ( Sum s2) <= ((b / (b - 1)) - (2 / b)) by A9, XREAL_1: 9;

      

       A11: s2 is summable by Th26, SERIES_1: 12;

      for n be Nat holds 0 <= (s1 . n) & (s1 . n) <= (s2 . n)

      proof

        let n be Nat;

        

         A12: (s1 . n) = (f . (n + 2)) by NAT_1:def 3;

        (f . (n + 2)) <= (((c - 1) (#) ( powerfact b)) . (n + 2)) by Th34, A0, ZFMISC_1: 7, CARD_1: 50;

        then (f . (n + 2)) <= ((c - 1) * (( powerfact b) . (n + 2))) by VALUED_1: 6;

        hence thesis by Th33, A2, A12, NAT_1:def 3;

      end;

      then

       A13: ( Sum s1) <= ( Sum s2) by SERIES_1: 20, A11;

      

       A14: ( Sum f) = ((( Partial_Sums f) . 1) + ( Sum (f ^\ (1 + 1)))) by A3, SERIES_1: 15

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

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

      .= (( 0 + (f . 1)) + ( Sum (f ^\ (1 + 1)))) by DefLio

      .= ((1 / 10) + ( Sum (f ^\ 2))) by A5;

      ( Sum s1) <= ((10 / (10 - 1)) - (2 / 10)) by A13, A10, XXREAL_0: 2;

      then ((1 / 10) + ( Sum (f ^\ 2))) <= ((1 / 10) + ((10 / (10 - 1)) - (2 / 10))) by XREAL_1: 7;

      hence thesis by A4, A5, A14, XXREAL_0: 1;

    end;

    theorem :: LIOUVIL1:46

    

     Th40: for nl be Liouville, z be Integer holds (z + nl) is liouville

    proof

      let nl be Liouville, z be Integer;

      set zl = (z + nl);

      for n be non zero Nat holds ex p be Integer, q be Nat st q > 1 & 0 < |.(zl - (p / q)).| < (1 / (q |^ n))

      proof

        let n be non zero Nat;

        nl is liouville;

        then

        consider p1 be Integer, q1 be Nat such that

         A1: q1 > 1 & 0 < |.(nl - (p1 / q1)).| < (1 / (q1 |^ n));

        set p2 = ((z * q1) + p1);

        take p2, q2 = q1;

        thus q2 > 1 by A1;

        (p2 / q2) = (((z * q1) / q1) + (p1 / q1)) by XCMPLX_1: 62

        .= (z + (p1 / q1)) by A1, XCMPLX_1: 89;

        hence thesis by A1;

      end;

      hence thesis by Def2;

    end;

    registration

      let nl be Liouville, z be Integer;

      cluster (nl + z) -> liouville;

      coherence by Th40;

    end

    definition

      :: LIOUVIL1:def11

      func LiouvilleNumbers -> Subset of REAL equals the set of all nl where nl be Liouville;

      coherence

      proof

         the set of all nl where nl be Liouville c= REAL

        proof

          let x be object;

          assume x in the set of all nl where nl be Liouville;

          then ex nl be Liouville st x = nl;

          hence thesis by XREAL_0:def 1;

        end;

        hence thesis;

      end;

    end

    registration

      cluster LiouvilleNumbers -> non empty;

      coherence

      proof

         Liouville_constant in the set of all r where r be Liouville;

        hence thesis;

      end;

    end

    registration

      cluster LiouvilleNumbers -> infinite;

      coherence

      proof

        deffunc F( Element of INT ) = ( In (($1 + Liouville_constant ), LiouvilleNumbers ));

        consider f be Function of INT , LiouvilleNumbers such that

         A1: for i be Element of INT holds (f . i) = F(i) from FUNCT_2:sch 4;

        

         A2: ( dom f) = INT by FUNCT_2:def 1;

        

         A3: ( rng f) c= LiouvilleNumbers by RELAT_1:def 19;

        for x1,x2 be object st x1 in INT & x2 in INT & (f . x1) = (f . x2) holds x1 = x2

        proof

          let x1,x2 be object;

          assume x1 in INT & x2 in INT ;

          then

          reconsider xx1 = x1, xx2 = x2 as Element of INT ;

          assume

           A4: (f . x1) = (f . x2);

          

           A5: (xx1 + Liouville_constant ) in LiouvilleNumbers & (xx2 + Liouville_constant ) in LiouvilleNumbers ;

          

           A6: (f . x1) = ( In ((xx1 + Liouville_constant ), LiouvilleNumbers )) by A1

          .= (xx1 + Liouville_constant ) by A5, SUBSET_1:def 8;

          (f . x2) = ( In ((xx2 + Liouville_constant ), LiouvilleNumbers )) by A1

          .= (xx2 + Liouville_constant ) by A5, SUBSET_1:def 8;

          hence thesis by A4, A6;

        end;

        then f is one-to-one by FUNCT_2: 19;

        then omega c= ( card LiouvilleNumbers ) by TOPGEN_3: 16, A2, A3, CARD_1: 10;

        hence thesis by FINSET_1: 1;

      end;

    end