irrat_1.miz



    begin

    reserve k,m,n,p,K,N for Nat;

    reserve i for Integer;

    reserve x,y,eps for Real;

    reserve seq,seq1,seq2 for Real_Sequence;

    reserve sq for FinSequence of REAL ;

    notation

      let x be Real;

      antonym x is irrational for x is rational;

    end

    notation

      let x,y be Real;

      synonym x ^ y for x to_power y;

    end

    ::$Notion-Name

    theorem :: IRRAT_1:1

    

     Th1: p is prime implies ( sqrt p) is irrational

    proof

      assume

       A1: p is prime;

      then

       A2: p > 1 by INT_2:def 4;

      assume ( sqrt p) is rational;

      then

      consider i, n such that

       A3: n <> 0 and

       A4: ( sqrt p) = (i / n) and

       A5: for i1 be Integer, n1 be Nat st n1 <> 0 & ( sqrt p) = (i1 / n1) holds n <= n1 by RAT_1: 9;

      

       A6: i = (( sqrt p) * n) by A3, A4, XCMPLX_1: 87;

      ( sqrt p) >= 0 by SQUARE_1:def 2;

      then

      reconsider m = i as Element of NAT by A6, INT_1: 3;

      

       A7: (m ^2 ) = ((( sqrt p) ^2 ) * (n ^2 )) by A6

      .= (p * (n ^2 )) by SQUARE_1:def 2;

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

      then p divides m by A1, NEWTON: 80;

      then

      consider m1 be Nat such that

       A8: m = (p * m1) by NAT_D:def 3;

      (n ^2 ) = ((p * (p * (m1 ^2 ))) / p) by A2, A7, A8, XCMPLX_1: 89

      .= (p * (m1 ^2 )) by A2, XCMPLX_1: 89;

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

      then p divides n by A1, NEWTON: 80;

      then

      consider n1 be Nat such that

       A9: n = (p * n1) by NAT_D:def 3;

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

      

       A10: (m1 / n1) = ( sqrt p) by A2, A4, A8, A9, XCMPLX_1: 91;

      

       A11: n1 <> 0 by A3, A9;

      then (p * n1) > (1 * n1) by A2, XREAL_1: 98;

      hence contradiction by A5, A9, A11, A10;

    end;

    theorem :: IRRAT_1:2

    ex x, y st x is irrational & y is irrational & (x ^ y) is rational

    proof

      set w = ( sqrt 2);

      

       A1: ((w ^ w) ^ w) = (w ^ (w ^2 )) by POWER: 33, SQUARE_1: 19

      .= (w ^ 2) by SQUARE_1:def 2

      .= (w ^2 ) by POWER: 46

      .= 2 by SQUARE_1:def 2;

      reconsider dwa = 2 as Real;

      per cases ;

        suppose

         A2: (w ^ w) is rational;

        take w, w;

        thus thesis by A2, Th1, INT_2: 28;

      end;

        suppose

         A3: (w ^ w) is irrational;

        take (w ^ w), w;

        thus thesis by A1, A3, Th1, INT_2: 28;

      end;

    end;

    begin

    scheme :: IRRAT_1:sch1

    LambdaRealSeq { F( set) -> Real } :

(ex seq st for n holds (seq . n) = F(n)) & for seq1, seq2 st (for n holds (seq1 . n) = F(n)) & (for n holds (seq2 . n) = F(n)) holds seq1 = seq2;

      thus ex seq st for n holds (seq . n) = F(n) from SEQ_1:sch 1;

      let seq1, seq2;

      assume

       A1: for n holds (seq1 . n) = F(n);

      assume

       A2: for n holds (seq2 . n) = F(n);

      now

        let n be Element of NAT ;

        

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

        .= (seq2 . n) by A2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    definition

      let k be Nat;

      :: IRRAT_1:def1

      func aseq (k) -> Real_Sequence means

      : Def1: for n holds (it . n) = ((n - k) / n);

      correctness

      proof

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

        thus (ex seq be Real_Sequence st for n be Nat holds (seq . n) = F(n)) & for seq1,seq2 be Real_Sequence st (for n be Nat holds (seq1 . n) = F(n)) & (for n be Nat holds (seq2 . n) = F(n)) holds seq1 = seq2 from LambdaRealSeq;

      end;

      :: IRRAT_1:def2

      func bseq (k) -> Real_Sequence means

      : Def2: for n holds (it . n) = ((n choose k) * (n ^ ( - k)));

      correctness

      proof

        deffunc F( Nat) = (($1 choose k) * ($1 ^ ( - k)));

        thus (ex seq be Real_Sequence st for n be Nat holds (seq . n) = F(n)) & for seq1,seq2 be Real_Sequence st (for n be Nat holds (seq1 . n) = F(n)) & (for n be Nat holds (seq2 . n) = F(n)) holds seq1 = seq2 from LambdaRealSeq;

      end;

    end

    definition

      let n be Nat;

      :: IRRAT_1:def3

      func cseq (n) -> Real_Sequence means

      : Def3: for k holds (it . k) = ((n choose k) * (n ^ ( - k)));

      correctness

      proof

        deffunc F( Nat) = ((n choose $1) * (n ^ ( - $1)));

        thus (ex seq be Real_Sequence st for n be Nat holds (seq . n) = F(n)) & for seq1,seq2 be Real_Sequence st (for n be Nat holds (seq1 . n) = F(n)) & (for n be Nat holds (seq2 . n) = F(n)) holds seq1 = seq2 from LambdaRealSeq;

      end;

    end

    theorem :: IRRAT_1:3

    

     Th3: (( cseq n) . k) = (( bseq k) . n)

    proof

      

      thus (( cseq n) . k) = ((n choose k) * (n ^ ( - k))) by Def3

      .= (( bseq k) . n) by Def2;

    end;

    definition

      :: IRRAT_1:def4

      func dseq -> Real_Sequence means

      : Def4: for n holds (it . n) = ((1 + (1 / n)) ^ n);

      correctness

      proof

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

        thus (ex seq be Real_Sequence st for n be Nat holds (seq . n) = F(n)) & for seq1,seq2 be Real_Sequence st (for n be Nat holds (seq1 . n) = F(n)) & (for n be Nat holds (seq2 . n) = F(n)) holds seq1 = seq2 from LambdaRealSeq;

      end;

    end

    definition

      :: IRRAT_1:def5

      func eseq -> Real_Sequence means

      : Def5: for k holds (it . k) = (1 / (k ! ));

      correctness

      proof

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

        thus (ex seq be Real_Sequence st for n be Nat holds (seq . n) = F(n)) & for seq1,seq2 be Real_Sequence st (for n be Nat holds (seq1 . n) = F(n)) & (for n be Nat holds (seq2 . n) = F(n)) holds seq1 = seq2 from LambdaRealSeq;

      end;

    end

    theorem :: IRRAT_1:4

    

     Th4: n > 0 implies (n ^ ( - (k + 1))) = ((n ^ ( - k)) / n)

    proof

      assume

       A1: n > 0 ;

      

      thus (n ^ ( - (k + 1))) = (n ^ (( - k) - 1))

      .= ((n ^ ( - k)) / (n ^ 1)) by A1, POWER: 29

      .= ((n ^ ( - k)) / n);

    end;

    theorem :: IRRAT_1:5

    

     Th5: (n choose (k + 1)) = (((n - k) / (k + 1)) * (n choose k))

    proof

      per cases ;

        suppose

         A1: (k + 1) <= n;

        then

        reconsider l = (n - (k + 1)) as Element of NAT by INT_1: 5;

        (l + 1) = (n - k);

        then

        reconsider l1 = (n - k) as Element of NAT ;

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

        then

         A2: k <= n by A1, XXREAL_0: 2;

        

        thus (n choose (k + 1)) = ((n ! ) / (((k + 1) ! ) * (l ! ))) by A1, NEWTON:def 3

        .= ((n ! ) / (((k ! ) * (k + 1)) * (l ! ))) by NEWTON: 15

        .= ((n ! ) / (((k ! ) * (k + 1)) * (((l ! ) * (l + 1)) / (l + 1)))) by XCMPLX_1: 89

        .= ((n ! ) / (((k ! ) * (k + 1)) * (((l + 1) ! ) / (l + 1)))) by NEWTON: 15

        .= ((l1 / (k + 1)) * ((n ! ) / ((k ! ) * (l1 ! )))) by XCMPLX_1: 233

        .= (((n - k) / (k + 1)) * (n choose k)) by A2, NEWTON:def 3;

      end;

        suppose

         A3: (k + 1) > n & k <= n;

        then k >= n by NAT_1: 13;

        then k = n by A3, XXREAL_0: 1;

        hence thesis by A3, NEWTON:def 3;

      end;

        suppose

         A4: (k + 1) > n & k > n;

        

        hence (n choose (k + 1)) = (((n - k) / (k + 1)) * 0 ) by NEWTON:def 3

        .= (((n - k) / (k + 1)) * (n choose k)) by A4, NEWTON:def 3;

      end;

    end;

    theorem :: IRRAT_1:6

    

     Th6: n > 0 implies (( bseq (k + 1)) . n) = (((1 / (k + 1)) * (( bseq k) . n)) * (( aseq k) . n))

    proof

      assume

       A1: n > 0 ;

      

      thus (( bseq (k + 1)) . n) = ((n choose (k + 1)) * (n ^ ( - (k + 1)))) by Def2

      .= ((((n - k) / (k + 1)) * (n choose k)) * (n ^ ( - (k + 1)))) by Th5

      .= ((((n - k) / (k + 1)) * (n choose k)) * ((n ^ ( - k)) / n)) by A1, Th4

      .= ((((n - k) * ((k + 1) " )) * (n choose k)) * ((n ^ ( - k)) / n))

      .= ((((n - k) * ((k + 1) " )) * (n choose k)) * ((n ^ ( - k)) * (n " )))

      .= ((((k + 1) " ) * ((n choose k) * (n ^ ( - k)))) * ((n - k) * (n " )))

      .= (((1 / (k + 1)) * ((n choose k) * (n ^ ( - k)))) * ((n - k) * (n " )))

      .= (((1 / (k + 1)) * ((n choose k) * (n ^ ( - k)))) * ((n - k) / n))

      .= (((1 / (k + 1)) * (( bseq k) . n)) * ((n - k) / n)) by Def2

      .= (((1 / (k + 1)) * (( bseq k) . n)) * (( aseq k) . n)) by Def1;

    end;

    theorem :: IRRAT_1:7

    

     Th7: n > 0 implies (( aseq k) . n) = (1 - (k / n))

    proof

      assume

       A1: n > 0 ;

      

      thus (( aseq k) . n) = ((n - k) / n) by Def1

      .= ((n / n) - (k / n))

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

    end;

    theorem :: IRRAT_1:8

    

     Th8: ( aseq k) is convergent & ( lim ( aseq k)) = 1

    proof

      

       A1: for eps be Real st 0 < eps holds ex N st for n st N <= n holds |.((( aseq k) . n) - 1).| < eps

      proof

        let eps be Real;

        assume

         A2: eps > 0 ;

        consider N such that

         A3: N > (k / eps) by SEQ_4: 3;

        take N;

        let n;

        assume

         A4: n >= N;

        then n > (k / eps) by A3, XXREAL_0: 2;

        then ((k / eps) * eps) < (n * eps) by A2, XREAL_1: 68;

        then

         A5: k < (n * eps) by A2, XCMPLX_1: 87;

        

         A6: n > 0 by A2, A3, A4;

        

        then |.((( aseq k) . n) - 1).| = |.((1 - (k / n)) - 1).| by Th7

        .= |.( - (k / n)).|

        .= |.(k / n).| by COMPLEX1: 52

        .= (k / n) by ABSVALUE:def 1;

        hence thesis by A6, A5, XREAL_1: 83;

      end;

      thus ( aseq k) is convergent by A1;

      hence thesis by A1, SEQ_2:def 7;

    end;

    theorem :: IRRAT_1:9

    

     Th9: for seq st for n be Nat holds (seq . n) = x holds seq is convergent & ( lim seq) = x

    proof

      let seq;

      assume

       A1: for n be Nat holds (seq . n) = x;

      x in REAL by XREAL_0:def 1;

      then

       A2: seq is constant by A1, VALUED_0:def 18;

      hence seq is convergent;

      

      thus ( lim seq) = (seq . 0 ) by A2, SEQ_4: 26

      .= x by A1;

    end;

    theorem :: IRRAT_1:10

    

     Th10: for n holds (( bseq 0 ) . n) = 1

    proof

      let n;

      

      thus (( bseq 0 ) . n) = ((n choose 0 ) * (n ^ ( - 0 ))) by Def2

      .= (1 * (n ^ ( - 0 ))) by NEWTON: 19

      .= 1 by POWER: 24;

    end;

    theorem :: IRRAT_1:11

    

     Th11: ((1 / (k + 1)) * (1 / (k ! ))) = (1 / ((k + 1) ! ))

    proof

      

      thus ((1 / (k + 1)) * (1 / (k ! ))) = (1 / ((k + 1) * (k ! ))) by XCMPLX_1: 102

      .= (1 / ((k + 1) ! )) by NEWTON: 15;

    end;

    theorem :: IRRAT_1:12

    

     Th12: ( bseq k) is convergent & ( lim ( bseq k)) = (1 / (k ! )) & ( lim ( bseq k)) = ( eseq . k)

    proof

      defpred P[ Nat] means ( bseq $1) is convergent & ( lim ( bseq $1)) = (1 / ($1 ! ));

       A1:

      now

        let k;

        assume

         A2: P[k];

        thus P[(k + 1)]

        proof

          deffunc F( Nat) = ((1 / (k + 1)) * (( bseq k) . $1));

          consider seq such that

           A3: for n holds (seq . n) = F(n) from SEQ_1:sch 1;

          deffunc G( Nat) = ((seq . $1) * (( aseq k) . $1));

          consider seq1 such that

           A4: for n holds (seq1 . n) = G(n) from SEQ_1:sch 1;

          

           A5: for n st n >= 1 holds (( bseq (k + 1)) . n) = (seq1 . n)

          proof

            let n;

            assume n >= 1;

            

            hence (( bseq (k + 1)) . n) = (((1 / (k + 1)) * (( bseq k) . n)) * (( aseq k) . n)) by Th6

            .= ((seq . n) * (( aseq k) . n)) by A3

            .= (seq1 . n) by A4;

          end;

          

           A6: seq = ((1 / (k + 1)) (#) ( bseq k)) by A3, SEQ_1: 9;

          then

           A7: seq is convergent by A2;

          

           A8: ( lim seq) = ((1 / (k + 1)) * (1 / (k ! ))) by A2, A6, SEQ_2: 8

          .= (1 / ((k + 1) ! )) by Th11;

          

           A9: ( aseq k) is convergent by Th8;

          

           A10: seq1 = (seq (#) ( aseq k)) by A4, SEQ_1: 8;

          then

           A11: seq1 is convergent by A7, A9;

          hence ( bseq (k + 1)) is convergent by A5, SEQ_4: 18;

          ( lim seq1) = (( lim seq) * ( lim ( aseq k))) by A7, A10, A9, SEQ_2: 15

          .= (1 / ((k + 1) ! )) by A8, Th8;

          hence thesis by A11, A5, SEQ_4: 19;

        end;

      end;

      

       A12: P[ 0 ]

      proof

        reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

        set bseq0 = ( seq_const 1);

        

         A13: for n be Nat holds (bseq0 . n) = 1 by SEQ_1: 57;

        

         A14: for n st n >= 1 holds (( bseq 0 ) . n) = (bseq0 . n)

        proof

          let n;

          assume n >= 1;

          

          thus (( bseq 0 ) . n) = 1 by Th10

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

        end;

        hence ( bseq 0 ) is convergent by SEQ_4: 18;

        ( lim bseq0) = 1 by A13, Th9;

        hence thesis by A14, NEWTON: 12, SEQ_4: 19;

      end;

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

      hence ( bseq k) is convergent & ( lim ( bseq k)) = (1 / (k ! ));

      hence thesis by Def5;

    end;

    theorem :: IRRAT_1:13

    

     Th13: k < n implies 0 < (( aseq k) . n) & (( aseq k) . n) <= 1

    proof

      

       A1: (( aseq k) . n) = ((n - k) / n) by Def1;

      assume

       A2: k < n;

      then (n - k) > 0 by XREAL_1: 50;

      hence (( aseq k) . n) > 0 by A2, A1, XREAL_1: 139;

      (1 - (k / n)) <= (1 - 0 ) by XREAL_1: 6;

      hence thesis by A2, Th7;

    end;

    theorem :: IRRAT_1:14

    

     Th14: n > 0 implies 0 <= (( bseq k) . n) & (( bseq k) . n) <= (1 / (k ! )) & (( bseq k) . n) <= ( eseq . k) & 0 <= (( cseq n) . k) & (( cseq n) . k) <= (1 / (k ! )) & (( cseq n) . k) <= ( eseq . k)

    proof

      defpred P[ Nat] means (( bseq $1) . n) <= (1 / ($1 ! ));

      assume

       A1: n > 0 ;

      then

       A2: (n ^ ( - k)) > 0 by POWER: 34;

       A3:

      now

        let k;

        assume

         A4: P[k];

        thus P[(k + 1)]

        proof

          per cases ;

            suppose

             A5: k < n;

            ((1 / (k + 1)) * (( bseq k) . n)) <= ((1 / (k + 1)) * (1 / (k ! ))) by A4, XREAL_1: 64;

            then

             A6: ((1 / (k + 1)) * (( bseq k) . n)) <= (1 / ((k + 1) ! )) by Th11;

            (( aseq k) . n) >= 0 by A5, Th13;

            then

             A7: (((1 / (k + 1)) * (( bseq k) . n)) * (( aseq k) . n)) <= ((1 / ((k + 1) ! )) * (( aseq k) . n)) by A6, XREAL_1: 64;

            (( aseq k) . n) <= 1 by A5, Th13;

            then

             A8: ((1 / ((k + 1) ! )) * (( aseq k) . n)) <= (1 / ((k + 1) ! )) by XREAL_1: 153;

            (( bseq (k + 1)) . n) = (((1 / (k + 1)) * (( bseq k) . n)) * (( aseq k) . n)) by A1, Th6;

            hence thesis by A7, A8, XXREAL_0: 2;

          end;

            suppose k >= n;

            then

             A9: (k + 1) > n by NAT_1: 13;

            (( bseq (k + 1)) . n) = ((n choose (k + 1)) * (n ^ ( - (k + 1)))) by Def2

            .= ( 0 * (n ^ ( - (k + 1)))) by A9, NEWTON:def 3

            .= 0 ;

            hence thesis;

          end;

        end;

      end;

      

       A10: (( bseq k) . n) = ((n choose k) * (n ^ ( - k))) by Def2;

      hence 0 <= (( bseq k) . n) by A2;

      

       A11: P[ 0 ] by Th10, NEWTON: 12;

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

      hence

       A12: (( bseq k) . n) <= (1 / (k ! ));

      hence (( bseq k) . n) <= ( eseq . k) by Def5;

      hence thesis by A10, A2, A12, Th3;

    end;

    theorem :: IRRAT_1:15

    

     Th15: for seq st (seq ^\ 1) is summable holds seq is summable & ( Sum seq) = ((seq . 0 ) + ( Sum (seq ^\ 1)))

    proof

      let seq;

      assume

       A1: (seq ^\ 1) is summable;

      hence seq is summable by SERIES_1: 13;

      

      thus ( Sum seq) = ((( Partial_Sums seq) . 0 ) + ( Sum (seq ^\ (1 + 0 )))) by A1, SERIES_1: 13, SERIES_1: 15

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

    end;

    theorem :: IRRAT_1:16

    

     Th16: for D be non empty set, sq be FinSequence of D st 1 <= k & k < ( len sq) holds ((sq /^ 1) . k) = (sq . (k + 1))

    proof

      let D be non empty set, sq be FinSequence of D;

      assume that

       A1: 1 <= k and

       A2: k < ( len sq);

      

       A3: ( len sq) = ((( len sq) - 1) + 1);

      (k + 1) <= ( len sq) by A2, NAT_1: 13;

      then

       A4: k <= (( len sq) - 1) by A3, XREAL_1: 6;

      

       A5: ( len sq) >= 1 by A1, A2, XXREAL_0: 2;

      then ( len (sq /^ 1)) = (( len sq) - 1) by RFINSEQ:def 1;

      then k in ( dom (sq /^ 1)) by A1, A4, FINSEQ_3: 25;

      hence thesis by A5, RFINSEQ:def 1;

    end;

    theorem :: IRRAT_1:17

    

     Th17: for sq st ( len sq) > 0 holds ( Sum sq) = ((sq . 1) + ( Sum (sq /^ 1)))

    proof

      let sq;

      assume

       A1: ( len sq) > 0 ;

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

      then

       A2: 1 in ( dom sq) by FINSEQ_3: 25;

      

      thus ( Sum sq) = ( Sum ( <*(sq /. 1)*> ^ (sq /^ 1))) by A1, CARD_1: 27, FINSEQ_5: 29

      .= ( Sum ( <*(sq . 1)*> ^ (sq /^ 1))) by A2, PARTFUN1:def 6

      .= ((sq . 1) + ( Sum (sq /^ 1))) by RVSUM_1: 76;

    end;

    theorem :: IRRAT_1:18

    

     Th18: for n holds for seq, sq st ( len sq) = n & (for k st k < n holds (seq . k) = (sq . (k + 1))) & (for k st k >= n holds (seq . k) = 0 ) holds seq is summable & ( Sum seq) = ( Sum sq)

    proof

      defpred P[ Nat] means for seq, sq st ( len sq) = $1 & (for k st k < $1 holds (seq . k) = (sq . (k + 1))) & (for k st k >= $1 holds (seq . k) = 0 ) holds seq is summable & ( Sum seq) = ( Sum sq);

      now

        let n;

        assume

         A1: for seq, sq st ( len sq) = n & (for k st k < n holds (seq . k) = (sq . (k + 1))) & (for k st k >= n holds (seq . k) = 0 ) holds seq is summable & ( Sum seq) = ( Sum sq);

        let seq, sq;

        assume that

         A2: ( len sq) = (n + 1) and

         A3: for k st k < (n + 1) holds (seq . k) = (sq . (k + 1)) and

         A4: for k st k >= (n + 1) holds (seq . k) = 0 ;

         A5:

        now

          let k;

          

           A6: (k + 1) >= ( 0 + 1) by XREAL_1: 6;

          assume k < n;

          then

           A7: (k + 1) < (n + 1) by XREAL_1: 6;

          

          thus ((seq ^\ 1) . k) = (seq . (k + 1)) by NAT_1:def 3

          .= (sq . ((k + 1) + 1)) by A3, A7

          .= ((sq /^ 1) . (k + 1)) by A2, A7, A6, Th16;

        end;

         A8:

        now

          let k;

          assume k >= n;

          then

           A9: (k + 1) >= (n + 1) by XREAL_1: 6;

          

          thus ((seq ^\ 1) . k) = (seq . (k + 1)) by NAT_1:def 3

          .= 0 by A4, A9;

        end;

        (n + 1) >= ( 0 + 1) by XREAL_1: 6;

        

        then

         A10: ( len (sq /^ 1)) = (( len sq) - 1) by A2, RFINSEQ:def 1

        .= n by A2;

        then

         A11: ( Sum (seq ^\ 1)) = ( Sum (sq /^ 1)) by A1, A5, A8;

        

         A12: (seq ^\ 1) is summable by A1, A10, A5, A8;

        hence seq is summable by Th15;

        

        thus ( Sum seq) = ((seq . 0 ) + ( Sum (seq ^\ 1))) by A12, Th15

        .= ((sq . ( 0 + 1)) + ( Sum (seq ^\ 1))) by A3

        .= ( Sum sq) by A2, A11, Th17;

      end;

      then

       A13: P[k] implies P[(k + 1)];

      now

        let seq, sq;

        assume that

         A14: ( len sq) = 0 and for k st k < 0 holds (seq . k) = (sq . (k + 1)) and

         A15: for k st k >= 0 holds (seq . k) = 0 ;

        sq is Element of ( 0 -tuples_on REAL ) by A14, FINSEQ_2: 92;

        then

         A16: ( Sum sq) = 0 by RVSUM_1: 79;

        defpred P[ Nat] means (( Partial_Sums seq) . $1) = 0 ;

         A17:

        now

          let k be Nat;

          

           A18: (( Partial_Sums seq) . (k + 1)) = ((( Partial_Sums seq) . k) + (seq . (k + 1))) by SERIES_1:def 1;

          assume P[k];

          hence P[(k + 1)] by A15, A18;

        end;

        (seq . 0 ) = 0 by A15;

        then

         A19: P[ 0 ] by SERIES_1:def 1;

        

         A20: for k be Nat holds P[k] from NAT_1:sch 2( A19, A17);

        then ( Partial_Sums seq) is convergent by Th9;

        hence seq is summable by SERIES_1:def 2;

        ( lim ( Partial_Sums seq)) = 0 by A20, Th9;

        hence ( Sum seq) = ( Sum sq) by A16, SERIES_1:def 3;

      end;

      then

       A21: P[ 0 ];

      thus P[n] from NAT_1:sch 2( A21, A13);

    end;

    theorem :: IRRAT_1:19

    

     Th19: k <= n implies (((x,y) In_Power n) . (k + 1)) = (((n choose k) * (x ^ (n - k))) * (y ^ k))

    proof

      reconsider i1 = ((k + 1) - 1) as Element of NAT by ORDINAL1:def 12;

      

       A1: (k + 1) >= ( 0 + 1) & ( len ((x,y) In_Power n)) = (n + 1) by NEWTON:def 4, XREAL_1: 6;

      assume

       A2: k <= n;

      then

      reconsider l = (n - i1) as Element of NAT by INT_1: 5;

      (k + 1) <= (n + 1) by A2, XREAL_1: 6;

      then (k + 1) in ( dom ((x,y) In_Power n)) by A1, FINSEQ_3: 25;

      

      hence (((x,y) In_Power n) . (k + 1)) = (((n choose i1) * (x ^ l)) * (y |^ i1)) by NEWTON:def 4

      .= (((n choose k) * (x ^ (n - k))) * (y ^ k));

    end;

    theorem :: IRRAT_1:20

    

     Th20: n > 0 & k <= n implies (( cseq n) . k) = (((1,(1 / n)) In_Power n) . (k + 1))

    proof

      assume that

       A1: n > 0 and

       A2: k <= n;

      

      thus (((1,(1 / n)) In_Power n) . (k + 1)) = (((n choose k) * (1 ^ (n - k))) * ((1 / n) ^ k)) by A2, Th19

      .= (((n choose k) * 1) * ((1 / n) ^ k)) by POWER: 26

      .= ((n choose k) * (n ^ ( - k))) by A1, POWER: 32

      .= (( cseq n) . k) by Def3;

    end;

    theorem :: IRRAT_1:21

    

     Th21: n > 0 implies ( cseq n) is summable & ( Sum ( cseq n)) = ((1 + (1 / n)) ^ n) & ( Sum ( cseq n)) = ( dseq . n)

    proof

       A1:

      now

        let k;

        assume k >= (n + 1);

        then

         A2: k > n by NAT_1: 13;

        

        thus (( cseq n) . k) = ((n choose k) * (n ^ ( - k))) by Def3

        .= ( 0 * (n ^ ( - k))) by A2, NEWTON:def 3

        .= 0 ;

      end;

      assume

       A3: n > 0 ;

       A4:

      now

        let k;

        assume k < (n + 1);

        then k <= n by NAT_1: 13;

        hence (( cseq n) . k) = (((1,(1 / n)) In_Power n) . (k + 1)) by A3, Th20;

      end;

      

       A5: ( len ((1,(1 / n)) In_Power n)) = (n + 1) by NEWTON:def 4;

      hence ( cseq n) is summable by A4, A1, Th18;

      

      thus ((1 + (1 / n)) ^ n) = ( Sum ((1,(1 / n)) In_Power n)) by NEWTON: 30

      .= ( Sum ( cseq n)) by A5, A4, A1, Th18;

      hence thesis by Def4;

    end;

    theorem :: IRRAT_1:22

    

     Th22: dseq is convergent & ( lim dseq ) = number_e

    proof

       A1:

      now

        let n be Nat;

        

        thus (( dseq ^\ 1) . n) = ( dseq . (n + 1)) by NAT_1:def 3

        .= ((1 + (1 / (n + 1))) ^ (n + 1)) by Def4;

      end;

      then

       A2: ( dseq ^\ 1) is convergent by POWER: 59;

      hence dseq is convergent by SEQ_4: 21;

      for n be Nat holds (( dseq ^\ 1) . n) = ((1 + (1 / (n + 1))) ^ (n + 1)) by A1;

      then number_e = ( lim ( dseq ^\ 1)) by POWER:def 4;

      hence thesis by A2, SEQ_4: 22;

    end;

    theorem :: IRRAT_1:23

    

     Th23: eseq is summable & ( Sum eseq ) = ( exp_R 1)

    proof

      now

        let k be Element of NAT ;

        

        thus ( eseq . k) = (1 / (k ! )) by Def5

        .= ((1 |^ k) / (k ! ))

        .= ((1 rExpSeq ) . k) by SIN_COS:def 5;

      end;

      then

       A1: eseq = (1 rExpSeq ) by FUNCT_2: 63;

      hence eseq is summable by SIN_COS: 45;

      

      thus ( exp_R 1) = ( exp_R . 1) by SIN_COS:def 23

      .= ( Sum eseq ) by A1, SIN_COS:def 22;

    end;

    theorem :: IRRAT_1:24

    

     Th24: for K holds for dseqK be Real_Sequence st for n holds (dseqK . n) = (( Partial_Sums ( cseq n)) . K) holds dseqK is convergent & ( lim dseqK) = (( Partial_Sums eseq ) . K)

    proof

      defpred P[ Nat] means for dseqK be Real_Sequence st for n holds (dseqK . n) = (( Partial_Sums ( cseq n)) . $1) holds dseqK is convergent & ( lim dseqK) = (( Partial_Sums eseq ) . $1);

      now

        let K;

        deffunc F( Nat) = (( Partial_Sums ( cseq $1)) . K);

        consider dseqK be Real_Sequence such that

         A1: for n holds (dseqK . n) = F(n) from SEQ_1:sch 1;

        assume

         A2: for dseqK be Real_Sequence st for n holds (dseqK . n) = (( Partial_Sums ( cseq n)) . K) holds dseqK is convergent & ( lim dseqK) = (( Partial_Sums eseq ) . K);

        then

         A3: dseqK is convergent by A1;

        let dseqK1 be Real_Sequence;

        assume

         A4: for n holds (dseqK1 . n) = (( Partial_Sums ( cseq n)) . (K + 1));

        now

          let n be Element of NAT ;

          

          thus (dseqK1 . n) = (( Partial_Sums ( cseq n)) . (K + 1)) by A4

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

          .= ((dseqK . n) + (( cseq n) . (K + 1))) by A1

          .= ((dseqK . n) + (( bseq (K + 1)) . n)) by Th3

          .= ((dseqK + ( bseq (K + 1))) . n) by SEQ_1: 7;

        end;

        then

         A5: dseqK1 = (dseqK + ( bseq (K + 1))) by FUNCT_2: 63;

        

         A6: ( lim dseqK) = (( Partial_Sums eseq ) . K) by A2, A1;

        

         A7: ( bseq (K + 1)) is convergent by Th12;

        hence dseqK1 is convergent by A3, A5;

        

        thus ( lim dseqK1) = (( lim dseqK) + ( lim ( bseq (K + 1)))) by A3, A5, A7, SEQ_2: 6

        .= ((( Partial_Sums eseq ) . K) + ( eseq . (K + 1))) by A6, Th12

        .= (( Partial_Sums eseq ) . (K + 1)) by SERIES_1:def 1;

      end;

      then

       A8: P[n] implies P[(n + 1)];

      now

        let dseq0 be Real_Sequence;

        assume

         A9: for n holds (dseq0 . n) = (( Partial_Sums ( cseq n)) . 0 );

        now

          let n be Element of NAT ;

          

          thus (dseq0 . n) = (( Partial_Sums ( cseq n)) . 0 ) by A9

          .= (( cseq n) . 0 ) by SERIES_1:def 1

          .= (( bseq 0 ) . n) by Th3;

        end;

        then

         A10: dseq0 = ( bseq 0 ) by FUNCT_2: 63;

        hence dseq0 is convergent by Th12;

        

        thus ( lim dseq0) = ( eseq . 0 ) by A10, Th12

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

      end;

      then

       A11: P[ 0 ];

      thus P[n] from NAT_1:sch 2( A11, A8);

    end;

    theorem :: IRRAT_1:25

    

     Th25: seq is convergent & ( lim seq) = x implies for eps st eps > 0 holds ex N st for n st n >= N holds (seq . n) > (x - eps)

    proof

      assume

       A1: seq is convergent & ( lim seq) = x;

      let eps;

      assume eps > 0 ;

      then

      consider N such that

       A2: for n st n >= N holds |.((seq . n) - x).| < eps by A1, SEQ_2:def 7;

      take N;

      let n;

      assume n >= N;

      then |.((seq . n) - x).| < eps by A2;

      then ((seq . n) - x) > ( - eps) by SEQ_2: 1;

      then (((seq . n) - x) + x) > (( - eps) + x) by XREAL_1: 6;

      hence thesis;

    end;

    theorem :: IRRAT_1:26

    

     Th26: (for eps st eps > 0 holds ex N st for n st n >= N holds (seq . n) > (x - eps)) & (ex N st for n st n >= N holds (seq . n) <= x) implies seq is convergent & ( lim seq) = x

    proof

      assume that

       A1: for eps st eps > 0 holds ex N st for n st n >= N holds (seq . n) > (x - eps) and

       A2: ex N st for n st n >= N holds (seq . n) <= x;

      

       A3: for eps be Real st eps > 0 holds ex N st for n st n >= N holds |.((seq . n) - x).| < eps

      proof

        let eps be Real;

        assume

         A4: eps > 0 ;

        then

         A5: (x + eps) > (x + 0 ) by XREAL_1: 6;

        consider N2 be Nat such that

         A6: for n st n >= N2 holds (seq . n) <= x by A2;

        consider N1 be Nat such that

         A7: for n st n >= N1 holds (seq . n) > (x - eps) by A1, A4;

        reconsider N = ( max (N1,N2)) as Nat by TARSKI: 1;

        take N;

        let n;

        assume

         A8: n >= N;

        then n >= N1 by XXREAL_0: 30;

        then (seq . n) > (x - eps) by A7;

        then

         A9: ((seq . n) - x) > ((x - eps) - x) by XREAL_1: 9;

        (seq . n) <= x by A6, A8, XXREAL_0: 30;

        then (seq . n) < (x + eps) by A5, XXREAL_0: 2;

        then ((seq . n) - x) < eps by XREAL_1: 19;

        hence thesis by A9, SEQ_2: 1;

      end;

      hence seq is convergent;

      hence thesis by A3, SEQ_2:def 7;

    end;

    theorem :: IRRAT_1:27

    

     Th27: seq is summable implies for eps st eps > 0 holds ex K st (( Partial_Sums seq) . K) > (( Sum seq) - eps)

    proof

      assume seq is summable;

      then

       A1: ( Partial_Sums seq) is convergent by SERIES_1:def 2;

      let eps;

      assume eps > 0 ;

      then

      consider K such that

       A2: for k st k >= K holds (( Partial_Sums seq) . k) > (( lim ( Partial_Sums seq)) - eps) by A1, Th25;

      take K;

      ( Sum seq) = ( lim ( Partial_Sums seq)) by SERIES_1:def 3;

      hence thesis by A2;

    end;

    theorem :: IRRAT_1:28

    

     Th28: n >= 1 implies ( dseq . n) <= ( Sum eseq )

    proof

      assume

       A1: n >= 1;

      then for k holds 0 <= (( cseq n) . k) & (( cseq n) . k) <= ( eseq . k) by Th14;

      then ( Sum ( cseq n)) <= ( Sum eseq ) by Th23, SERIES_1: 20;

      hence thesis by A1, Th21;

    end;

    theorem :: IRRAT_1:29

    

     Th29: seq is summable & (for k holds (seq . k) >= 0 ) implies ( Sum seq) >= (( Partial_Sums seq) . K)

    proof

      assume that

       A1: seq is summable and

       A2: for k holds (seq . k) >= 0 ;

       A3:

      now

        let k;

        ((seq ^\ (K + 1)) . k) = (seq . ((K + 1) + k)) by NAT_1:def 3;

        hence ((seq ^\ (K + 1)) . k) >= 0 by A2;

      end;

      (seq ^\ (K + 1)) is summable by A1, SERIES_1: 12;

      then ( Sum (seq ^\ (K + 1))) >= 0 by A3, SERIES_1: 18;

      then ((( Partial_Sums seq) . K) + ( Sum (seq ^\ (K + 1)))) >= ((( Partial_Sums seq) . K) + 0 ) by XREAL_1: 6;

      hence thesis by A1, SERIES_1: 15;

    end;

    theorem :: IRRAT_1:30

    

     Th30: dseq is convergent & ( lim dseq ) = ( Sum eseq )

    proof

      for eps st eps > 0 holds ex N st for n st n >= N holds ( dseq . n) > (( Sum eseq ) - eps)

      proof

        let eps;

        assume

         A1: eps > 0 ;

        then

        consider K such that

         A2: (( Partial_Sums eseq ) . K) > (( Sum eseq ) - (eps / 2)) by Th23, Th27, XREAL_1: 139;

        

         A3: ((( Partial_Sums eseq ) . K) - (eps / 2)) > ((( Sum eseq ) - (eps / 2)) - (eps / 2)) by A2, XREAL_1: 9;

        deffunc F( Nat) = (( Partial_Sums ( cseq $1)) . K);

        consider dseqK be Real_Sequence such that

         A4: for n holds (dseqK . n) = F(n) from SEQ_1:sch 1;

        dseqK is convergent & ( lim dseqK) = (( Partial_Sums eseq ) . K) by A4, Th24;

        then

        consider N such that

         A5: for n st n >= N holds (dseqK . n) > ((( Partial_Sums eseq ) . K) - (eps / 2)) by A1, Th25, XREAL_1: 139;

        take N1 = (N + 1);

        let n;

        assume

         A6: n >= N1;

        then (for k holds (( cseq n) . k) >= 0 ) & ( cseq n) is summable by Th14, Th21;

        then ( Sum ( cseq n)) >= (( Partial_Sums ( cseq n)) . K) by Th29;

        then ( dseq . n) >= (( Partial_Sums ( cseq n)) . K) by A6, Th21;

        then

         A7: ( dseq . n) >= (dseqK . n) by A4;

        (N + 1) >= (N + 0 ) by XREAL_1: 6;

        then n >= N by A6, XXREAL_0: 2;

        then (dseqK . n) > ((( Partial_Sums eseq ) . K) - (eps / 2)) by A5;

        then ( dseq . n) > ((( Partial_Sums eseq ) . K) - (eps / 2)) by A7, XXREAL_0: 2;

        hence thesis by A3, XXREAL_0: 2;

      end;

      hence thesis by Th26, Th28;

    end;

    definition

      :: original: number_e

      redefine

      :: IRRAT_1:def6

      func number_e equals ( Sum eseq );

      compatibility by Th22, Th30;

    end

    definition

      :: original: number_e

      redefine

      :: IRRAT_1:def7

      func number_e equals ( exp_R 1);

      compatibility by Th23;

    end

    begin

    theorem :: IRRAT_1:31

    

     Th31: x is rational implies ex n st n >= 2 & ((n ! ) * x) is integer

    proof

      assume x is rational;

      then

      consider i, n such that

       A1: n <> 0 and

       A2: x = (i / n) by RAT_1: 8;

      per cases ;

        suppose

         A3: n < (1 + 1);

        

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

        n <= 1 by A3, NAT_1: 13;

        then n = 1 by A4, XXREAL_0: 1;

        then

        reconsider x1 = x as Integer by A2;

        take n = 2;

        ((n ! ) * x1) is integer;

        hence thesis;

      end;

        suppose

         A5: n >= 2;

        take n;

        thus n >= 2 by A5;

        reconsider m = (n - 1) as Element of NAT by A5, INT_1: 5, XXREAL_0: 2;

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

        .= ((n * x) * (m ! ))

        .= (i * (m ! )) by A1, A2, XCMPLX_1: 87;

        hence thesis;

      end;

    end;

    theorem :: IRRAT_1:32

    

     Th32: ((n ! ) * ( eseq . k)) = ((n ! ) / (k ! ))

    proof

      

      thus ((n ! ) * ( eseq . k)) = ((n ! ) * (1 / (k ! ))) by Def5

      .= ((n ! ) / (k ! ));

    end;

    theorem :: IRRAT_1:33

    ((n ! ) / (k ! )) > 0 by XREAL_1: 139;

    theorem :: IRRAT_1:34

    

     Th34: seq is summable & (for n holds (seq . n) > 0 ) implies ( Sum seq) > 0

    proof

      assume that

       A1: seq is summable and

       A2: for n holds (seq . n) > 0 ;

      

       A3: ( Sum seq) = ((( Partial_Sums seq) . 0 ) + ( Sum (seq ^\ ( 0 + 1)))) by A1, SERIES_1: 15

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

       A4:

      now

        let n;

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

        hence ((seq ^\ 1) . n) >= 0 by A2;

      end;

      (seq ^\ 1) is summable by A1, SERIES_1: 12;

      then ( Sum (seq ^\ 1)) >= 0 by A4, SERIES_1: 18;

      then ( Sum seq) > ( 0 + 0 ) by A2, A3, XREAL_1: 8;

      hence thesis;

    end;

    theorem :: IRRAT_1:35

    

     Th35: ((n ! ) * ( Sum ( eseq ^\ (n + 1)))) > 0

    proof

       A1:

      now

        let k;

        (( eseq ^\ (n + 1)) . k) = ( eseq . ((n + 1) + k)) by NAT_1:def 3

        .= (1 / (((n + 1) + k) ! )) by Def5;

        hence (( eseq ^\ (n + 1)) . k) > 0 ;

      end;

      ( eseq ^\ (n + 1)) is summable by Th23, SERIES_1: 12;

      then (n ! ) > 0 & ( Sum ( eseq ^\ (n + 1))) > 0 by A1, Th34;

      hence thesis by XREAL_1: 129;

    end;

    theorem :: IRRAT_1:36

    

     Th36: k <= n implies ((n ! ) / (k ! )) is integer

    proof

      defpred P[ Nat] means ((($1 + k) ! ) / (k ! )) is integer;

      assume k <= n;

      then

      reconsider m = (n - k) as Element of NAT by INT_1: 5;

      

       A1: n = (m + k);

      now

        let m;

        

         A2: ((((m + 1) + k) ! ) / (k ! )) = ((((m + k) + 1) * ((m + k) ! )) * ((k ! ) " )) by NEWTON: 15

        .= (((m + k) + 1) * (((m + k) ! ) * ((k ! ) " )))

        .= (((m + k) + 1) * (((m + k) ! ) / (k ! )));

        assume (((m + k) ! ) / (k ! )) is integer;

        then

        reconsider i = (((m + k) ! ) / (k ! )) as Integer;

        (((m + k) + 1) * i) is Integer;

        hence ((((m + 1) + k) ! ) / (k ! )) is integer by A2;

      end;

      then

       A3: for n be Nat holds P[n] implies P[(n + 1)];

      

       A4: P[ 0 ] by XCMPLX_1: 60;

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

      hence thesis by A1;

    end;

    theorem :: IRRAT_1:37

    

     Th37: ((n ! ) * (( Partial_Sums eseq ) . n)) is integer

    proof

      defpred P[ Nat] means $1 <= n implies ((n ! ) * (( Partial_Sums eseq ) . $1)) is integer;

      now

        let k;

        assume

         A1: k <= n implies ((n ! ) * (( Partial_Sums eseq ) . k)) is integer;

        assume

         A2: (k + 1) <= n;

        (k + 0 ) <= (k + 1) by XREAL_1: 6;

        then

        reconsider i = ((n ! ) * (( Partial_Sums eseq ) . k)) as Integer by A1, A2, XXREAL_0: 2;

        ((n ! ) * ( eseq . (k + 1))) = ((n ! ) / ((k + 1) ! )) by Th32;

        then

        reconsider j = ((n ! ) * ( eseq . (k + 1))) as Integer by A2, Th36;

        

         A3: (i + j) is Integer;

        ((n ! ) * (( Partial_Sums eseq ) . (k + 1))) = ((n ! ) * ((( Partial_Sums eseq ) . k) + ( eseq . (k + 1)))) by SERIES_1:def 1

        .= (((n ! ) * (( Partial_Sums eseq ) . k)) + ((n ! ) * ( eseq . (k + 1))));

        hence ((n ! ) * (( Partial_Sums eseq ) . (k + 1))) is integer by A3;

      end;

      then

       A4: P[k] implies P[(k + 1)];

      now

        assume 0 <= n;

        ((n ! ) * (( Partial_Sums eseq ) . 0 )) = ((n ! ) * ( eseq . 0 )) by SERIES_1:def 1

        .= ((n ! ) / ( 0 ! )) by Th32;

        hence ((n ! ) * (( Partial_Sums eseq ) . 0 )) is integer by Th36;

      end;

      then

       A5: P[ 0 ];

      for k holds P[k] from NAT_1:sch 2( A5, A4);

      hence thesis;

    end;

    theorem :: IRRAT_1:38

    

     Th38: x = (1 / (n + 1)) implies ((n ! ) / (((n + k) + 1) ! )) <= (x ^ (k + 1))

    proof

      defpred P[ Nat] means ((n ! ) / (((n + $1) + 1) ! )) <= (x ^ ($1 + 1));

      assume

       A1: x = (1 / (n + 1));

       A2:

      now

        let k;

        assume

         A3: P[k];

        

         A4: ((n ! ) / (((n + (k + 1)) + 1) ! )) = ((n ! ) * ((((n + (k + 1)) + 1) ! ) " ))

        .= ((n ! ) * ((((n + (k + 1)) + 1) * (((n + k) + 1) ! )) " )) by NEWTON: 15

        .= ((n ! ) * ((((n + (k + 1)) + 1) " ) * ((((n + k) + 1) ! ) " ))) by XCMPLX_1: 204

        .= (((n ! ) * ((((n + k) + 1) ! ) " )) * (((n + (k + 1)) + 1) " ))

        .= (((n ! ) / (((n + k) + 1) ! )) * (((n + (k + 1)) + 1) " ));

        (n + (k + 1)) >= (n + 0 ) by XREAL_1: 6;

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

        then

         A5: (((n + (k + 1)) + 1) " ) <= (1 / (n + 1)) by XREAL_1: 85;

        ((x ^ (k + 1)) * x) = ((x ^ (k + 1)) * (x ^ 1))

        .= (x ^ ((k + 1) + 1)) by A1, POWER: 27;

        hence P[(k + 1)] by A1, A3, A5, A4, XREAL_1: 66;

      end;

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

      .= ((n ! ) * (((n + 1) * (n ! )) " ))

      .= ((n ! ) * (((n + 1) " ) * ((n ! ) " ))) by XCMPLX_1: 204

      .= (((n ! ) * ((n ! ) " )) * ((n + 1) " ))

      .= (1 * ((n + 1) " )) by XCMPLX_0:def 7

      .= x by A1;

      then

       A6: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: IRRAT_1:39

    

     Th39: n > 0 & x = (1 / (n + 1)) implies ((n ! ) * ( Sum ( eseq ^\ (n + 1)))) <= (x / (1 - x))

    proof

      assume that

       A1: n > 0 and

       A2: x = (1 / (n + 1));

      deffunc F( Nat) = (x ^ ($1 + 1));

      consider seq be Real_Sequence such that

       A3: for k holds (seq . k) = F(k) from SEQ_1:sch 1;

       A4:

      now

        let k;

        

         A5: (((n ! ) (#) ( eseq ^\ (n + 1))) . k) = ((n ! ) * (( eseq ^\ (n + 1)) . k)) by SEQ_1: 9

        .= ((n ! ) * ( eseq . ((n + 1) + k))) by NAT_1:def 3

        .= ((n ! ) * (1 / (((n + k) + 1) ! ))) by Def5

        .= ((n ! ) / (((n + k) + 1) ! ));

        hence (((n ! ) (#) ( eseq ^\ (n + 1))) . k) >= 0 ;

        (seq . k) = (x ^ (k + 1)) by A3;

        hence (((n ! ) (#) ( eseq ^\ (n + 1))) . k) <= (seq . k) by A2, A5, Th38;

      end;

      

       A6: (seq . 0 ) = (x ^ ( 0 + 1)) by A3

      .= x;

      

       A7: ( eseq ^\ (n + 1)) is summable by Th23, SERIES_1: 12;

      (n + 1) > ( 0 + 1) by A1, XREAL_1: 6;

      then

       A8: x < 1 by A2, XREAL_1: 212;

       A9:

      now

        let k;

        

        thus (seq . (k + 1)) = (x ^ ((k + 1) + 1)) by A3

        .= ((x ^ 1) * (x ^ (k + 1))) by A2, POWER: 27

        .= (x * (x ^ (k + 1)))

        .= (x * (seq . k)) by A3;

      end;

       |.x.| = x by A2, ABSVALUE:def 1;

      then seq is summable by A8, A9, SERIES_1: 25;

      then

       A10: ( Sum ((n ! ) (#) ( eseq ^\ (n + 1)))) <= ( Sum seq) by A4, SERIES_1: 20;

       |.x.| < 1 by A2, A8, ABSVALUE:def 1;

      then ( Sum seq) = (x / (1 - x)) by A6, A9, SERIES_1: 25;

      hence thesis by A7, A10, SERIES_1: 10;

    end;

    theorem :: IRRAT_1:40

    

     Th40: for n be Real st n >= 2 & x = (1 / (n + 1)) holds (x / (1 - x)) < 1

    proof

      let n be Real;

      assume that

       A1: n >= 2 and

       A2: x = (1 / (n + 1));

      (n + 1) > n by XREAL_1: 29;

      then 2 < (n + 1) by A1, XXREAL_0: 2;

      then (2 / (n + 1)) < 1 by XREAL_1: 189;

      then (x + x) < 1 by A2;

      then x < (1 - x) by XREAL_1: 20;

      hence thesis by A1, A2, XREAL_1: 189;

    end;

    ::$Notion-Name

    theorem :: IRRAT_1:41

     number_e is irrational

    proof

      assume number_e is rational;

      then

      consider n such that

       A1: n >= 2 and

       A2: ((n ! ) * number_e ) is integer by Th31;

      reconsider ne = ((n ! ) * number_e ) as Integer by A2;

      set x = (1 / (n + 1));

      reconsider ne1 = ((n ! ) * (( Partial_Sums eseq ) . n)) as Integer by Th37;

      ((n ! ) * number_e ) = ((n ! ) * ((( Partial_Sums eseq ) . n) + ( Sum ( eseq ^\ (n + 1))))) by Th23, SERIES_1: 15

      .= (((n ! ) * (( Partial_Sums eseq ) . n)) + ((n ! ) * ( Sum ( eseq ^\ (n + 1)))));

      then

       A3: ((n ! ) * ( Sum ( eseq ^\ (n + 1)))) = (ne - ne1);

      (x / (1 - x)) < 1 & ((n ! ) * ( Sum ( eseq ^\ (n + 1)))) <= (x / (1 - x)) by A1, Th39, Th40;

      then ((n ! ) * ( Sum ( eseq ^\ (n + 1)))) < ( 0 + 1) by XXREAL_0: 2;

      hence contradiction by A3, Th35, INT_1: 7;

    end;