environ

 vocabulary IRRAT_1, SEQ1, NEWTON, FUNC, QC_LANG, SEQ2, REAL_1, METRIC_6,
  POWER, POWER1, ANAL, F_DIFF, FINSEQ, SIGMA, LEB, TUPLES, SERIES, SEQM,
  RFINSEQ, FUNC_REL, PI, ONOP_1, SIN_COS, RAT_1, SQUARE, INT_1, NAT_1,
  NT_LAT;
 notation ARYTM, INT_1, NAT_1, NEWTON, FUNCT_1, REAL_1, SEQ_1, SEQ_2,
  PREPOWER, POWER, ANAL_1, SEQM_3, FINSEQ_1, RVSUM_1, SERIES_1, FINSEQ_2,
  RFINSEQ, FINSEQ_4, SIN_COS, COMPLEX1, COMSEQ_3, RAT_1, SQUARE_1, LIMFUNC1,
  NAT_LAT, INT_2, PEPIN;
 constructors ARYTM, NAT_1, NEWTON, FUNCT_1, REAL_1, SEQ_1, SEQ_2, FUNCT_2,
  PARTFUN1, RELSET_1, RELAT_1, PREPOWER, POWER, ANAL_1, SEQM_3, FINSEQ_1,
  RVSUM_1, SERIES_1, FINSEQ_2, RFINSEQ, FINSEQ_4, SIN_COS, COMPLEX1,
  COMSEQ_3, RAT_1, SQUARE_1, LIMFUNC1, INT_1, NAT_LAT, INT_2, PEPIN;
 theorems SEQ_1, REAL_2, PREPOWER, POWER, NEWTON, REAL_1, AXIOMS, NAT_1,
  SEQ_2, SEQ_4, ANAL_1, SEQM_3, RVSUM_1, FINSEQ_2, SERIES_1, RFINSEQ,
  FINSEQ_3, FINSEQ_4, FINSEQ_5, FINSEQ_1, SIN_COS, SQUARE_1, INT_1, RAT_1,
  INT_2, NAT_LAT;
 definitions SEQ_2;
 clusters RELSET_1, ARYTM, SEQ_1, INT_1;
 schemes SEQ_1, NAT_1;
 requirements ARYTM;


begin :: square roots of primes are irrational

 reserve k, m, n, p, K, N for Nat;
 reserve i, j for Integer;
 reserve x, y, eps for Real;
 reserve seq, seq1, seq2 for Real_Sequence;
 reserve sq for FinSequence of REAL;

definition
 let x;
 redefine attr x is rational;
 antonym x is irrational;
end;

definition
 let x, y;
 redefine func x to_power y;
 synonym x.^.y;
end;

theorem T1:
 p is prime implies ûp is irrational
proof
 assume H1: p is prime;
 then H2: p>1 by INT_2:def 5;
 then H3: p>0 by AXIOMS:22;
 assume ûp is rational;
 then consider i, n such that H4: n<>0 & ûp=i/n &
   for i1 being Integer, n1 being Nat st n1<>0 & ûp=i1/n1 holds nón1
  by RAT_1:25;
 H5: i=ûpùn by REAL_2:73,H4;
 ûpò0 & nò0 by SQUARE_1:87,NAT_1:18,H3;
 then iò0 by REAL_2:121,H5;
 then reconsider m = i as Nat by INT_1:16;
 H6: mý = (ûpùn)ý by H5
  .= (ûp)ýùný by SQUARE_1:68
  .= pùný by SQUARE_1:88,H3;
 then p³mý by NAT_1:def 3;
 then p³mùm by SQUARE_1:58;
 then p³m by NAT_LAT:95,H1;
 then consider m1 being Nat such that H7: m=pùm1 by NAT_1:def 3;
 ný = mý/p by REAL_2:72,H3,H6
  .= (pùm1)ý/p by H7
  .= pýùm1ý/p by SQUARE_1:68
  .= pùpùm1ý/p by SQUARE_1:58
  .= pù(pùm1ý)/p by AXIOMS:16
  .= pùm1ý by REAL_2:62,H3;
 then p³ný by NAT_1:def 3;
 then p³nùn by SQUARE_1:58;
 then p³n by NAT_LAT:95,H1;
 then consider n1 being Nat such that H8: n=pùn1 by NAT_1:def 3;
 n1<>0 by H4,H8;
 then H9: n1>0 by NAT_1:19;
 then m1/n1 = (pùm1)/(pùn1) by REAL_2:55,H3
  .= m/n by H7,H8
  .= ûp by H4;
 then H10: nón1 by H4,H9;
 pùn1>1ùn1 by REAL_2:199,H2,H9;
 then n>n1 by H8;
 hence contradiction by H10;
end;

theorem T2:
 ex x, y st x is irrational & y is irrational & x.^.y is rational
proof
 set w = û2;
 H1: w is irrational by INT_2:44,T1;
 w>0 by AXIOMS:22,SQUARE_1:84;
 then (w.^.w).^.w = w.^.(wùw) by POWER:38
  .= w.^.(wý) by SQUARE_1:58
  .= w.^.2 by SQUARE_1:88
  .= wý by POWER:53
  .= 2 by SQUARE_1:88;
 then H2: (w.^.w).^.w is rational by RAT_1:8;
 per cases;
 suppose H3: w.^.w is rational;
  take w, w;
  thus thesis by H1,H3;
 suppose H4: w.^.w is irrational;
  take w.^.w, w;
  thus thesis by H1,H2,H4;
end;


begin :: a proof that e = e

scheme LambdaRealSeq{F(Nat)->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)
proof
 thus ex seq st for n holds seq.n=F(n) from ExRealSeq;
 let seq1, seq2;
 assume H1: for n holds seq1.n=F(n);
 assume H2: for n holds seq2.n=F(n);
 now let n;
  thus seq1.n = F(n) by H1
   .= seq2.n by H2;
 end;
 hence seq1 = seq2 by SEQ_1:9;
end;

definition
 let k;
 func aseq(k) -> Real_Sequence means
  :Daseq: for n holds it.n=(n-k)/n;
 correctness from LambdaRealSeq;
end;

definition
 let k;
 func bseq(k) -> Real_Sequence means
  :Dbseq: for n holds it.n=(n choose k)ù(n.^.(-k));
 correctness from LambdaRealSeq;
end;

definition
 let n;
 func cseq(n) -> Real_Sequence means
  :Dcseq: for k holds it.k=(n choose k)ù(n.^.(-k));
 correctness from LambdaRealSeq;
end;

theorem T3:
 cseq(n).k=bseq(k).n
proof
 thus cseq(n).k = (n choose k)ù(n.^.(-k)) by Dcseq
  .= bseq(k).n by Dbseq;
end;

definition
 func dseq -> Real_Sequence means
  :Ddseq: for n holds it.n=(1+(1/n)).^.n;
 correctness from LambdaRealSeq;
end;

definition
 func eseq -> Real_Sequence means
  :Deseq: for k holds it.k=1/(k!);
 correctness from LambdaRealSeq;
end;

:: lim(\n:(n choose k)ù(n.^.(-k))) = 1/(k!)

theorem T4:
 n>0 implies (n.^.(-(k+1)))=(n.^.(-k))/n
proof
 assume H: n>0;
 thus (n.^.(-(k+1))) = (n.^.((-k)-1)) by REAL_2:6
  .= (n.^.(-k))/(n.^.1) by POWER:34,H
  .= (n.^.(-k))/n by POWER:30;
end;

theorem T5:
 for x, y, z, v, w being Real st y<>0 & z<>0 & v<>0 & w<>0 holds
  x/(yùzù(v/w))=(w/z)ù(x/(yùv))
proof
 let x, y, z, v, w be Real;
 assume H1: y<>0 & z<>0 & v<>0 & w<>0;
 H2: yùv<>0 by REAL_1:23,H1;
 H3: w/z<>0 by REAL_2:50,H1;
 thus x/(yùzù(v/w)) = x/(yùzù(vùw")) by REAL_1:16
  .= x/(zù(yù(vùw"))) by AXIOMS:16
  .= x/(zù(yùvùw")) by AXIOMS:16
  .= x/(zù((yùv)/w)) by REAL_1:16
  .= x/((yùv)/(w/z)) by REAL_2:61,H1
  .= (w/z)ù(x/(yùv)) by REAL_2:61,H2,H3;
end;

theorem T6:
 (n choose (k+1))=((n-k)/(k+1))ù(n choose k)
proof
 per cases;
 suppose H1: k+1ón;
  reconsider l = n-(k+1) as Nat by NEWTON:2,H1;
  H2: l+1 = n-(k+1-1) by REAL_1:28
   .= n-k by REAL_2:17;
  reconsider l1 = n-k as Nat by H2;
  H3: l1 = l+1 by H2;
  k ó k+1 by NAT_1:29; then H4: k ó n by AXIOMS:22,H1;
  H5: k+1<>0 & l+1<>0 & l1<>0 & k!<>0 & l1!<>0 by NAT_1:21,NEWTON:23,H3;
  thus (n choose (k+1)) = n!/((k+1)!ù(l!)) by NEWTON:def 3,H1
   .= n!/((k!ù(k+1))ù(l!)) by NEWTON:21
   .= n!/((k!ù(k+1))ù((l!)ù(l+1)/(l+1))) by REAL_2:72,H5
   .= n!/((k!ù(k+1))ù((l+1)!/(l+1))) by NEWTON:21
   .= n!/((k!ù(k+1))ù(l1!/(l+1))) by H3
   .= n!/((k!ù(k+1))ù(l1!/l1)) by H3
   .= (l1/(k+1))ù(n!/((k!)ù(l1!))) by T5,H5
   .= ((n-k)/(k+1))ù(n choose k) by NEWTON:def 3,H4;
 suppose H6: k+1>n & kón;
  then kòn & kón by NAT_1:38;
  then k=n by AXIOMS:21;
  then H7: n-k=0 by REAL_1:36;
  thus (n choose (k+1)) = 0 by NEWTON:def 3,H6
   .= 0ù(n choose k)
   .= (0ù(k+1)")ù(n choose k)
   .= (0/(k+1))ù(n choose k) by REAL_1:16
   .= ((n-k)/(k+1))ù(n choose k) by H7;
 suppose H8: k+1>n & k>n;
  thus (n choose (k+1)) = 0 by NEWTON:def 3,H8
   .= ((n-k)/(k+1))ù0
   .= ((n-k)/(k+1))ù(n choose k) by NEWTON:def 3,H8;
end;

theorem T7:
 n>0 implies bseq(k+1).n=(1/(k+1))ù(bseq(k).n)ù(aseq(k).n)
proof
 assume H: n>0;
 thus bseq(k+1).n = (n choose (k+1))ù(n.^.(-(k+1))) by Dbseq
  .= ((n-k)/(k+1))ù(n choose k)ù(n.^.(-(k+1))) by T6
  .= ((n-k)/(k+1))ù(n choose k)ù((n.^.(-k))/n) by T4,H
  .= (n-k)ù(k+1)"ù(n choose k)ù((n.^.(-k))/n) by REAL_1:16
  .= (n-k)ù(k+1)"ù(n choose k)ù((n.^.(-k))ùn") by REAL_1:16
  .= (n-k)ù(k+1)"ù(n choose k)ù(n.^.(-k))ùn" by AXIOMS:16
  .= (k+1)"ù(n choose k)ù(n-k)ù(n.^.(-k))ùn" by AXIOMS:16
  .= (k+1)"ù(n choose k)ù(n.^.(-k))ù(n-k)ùn" by AXIOMS:16
  .= (k+1)"ù((n choose k)ù(n.^.(-k)))ù(n-k)ùn" by AXIOMS:16
  .= (k+1)"ù((n choose k)ù(n.^.(-k)))ù((n-k)ùn") by AXIOMS:16
  .= (1/(k+1))ù((n choose k)ù(n.^.(-k)))ù((n-k)ùn") by REAL_1:33
  .= (1/(k+1))ù((n choose k)ù(n.^.(-k)))ù((n-k)/n) by REAL_1:16
  .= (1/(k+1))ù(bseq(k).n)ù((n-k)/n) by Dbseq
  .= (1/(k+1))ù(bseq(k).n)ù(aseq(k).n) by Daseq;
end;

theorem T8:
 n>0 implies aseq(k).n=1-(k/n)
proof
 assume H: n>0;
 thus aseq(k).n = (n-k)/n by Daseq
  .= (n/n)-(k/n) by REAL_1:40,H
  .= 1-(k/n) by REAL_1:37,H;
end;

theorem T9:
 aseq(k) is convergent & lim(aseq(k))=1
proof
 H1: for eps st 0<eps
  ex N st for n st Nón holds ³.aseq(k).n-1.³<eps
 proof
  let eps;
  assume H2: eps>0;
  consider N such that H3: N>k/eps by SEQ_4:10;
  kò0ùeps by NAT_1:18;
  then k/epsò0 by REAL_2:177,H2;
  then H4: N>0 by AXIOMS:22,H3;
  take N;
  let n;
  assume H5: nòN;
  then H6: n>0 by AXIOMS:22,H4;
  kò0ùn by NAT_1:18;
  then H7: k/nò0 by REAL_2:177,H6;
  H8: ³.aseq(k).n-1.³ = ³.(1-(k/n))-1.³ by T8,H6
   .= ³.(1+-(k/n))-1.³ by REAL_1:14
   .= ³.-(k/n).³ by REAL_2:17
   .= ³.k/n.³ by ANAL_1:17
   .= k/n by ANAL_1:1,H7;
  n>(k/eps) by AXIOMS:22,H3,H5;
  then (k/eps)ùeps<nùeps by REAL_1:70,H2;
  then k<nùeps by REAL_1:43,H2;
  then (k/n)<eps by REAL_2:178,H6;
  hence thesis by H8;
 end;
 thus aseq(k) is convergent
 proof
  take 1;
  thus thesis by H1;
 end;
 hence lim(aseq(k))=1 by SEQ_2:def 5,H1;
end;

theorem T10:
 for seq st for n holds seq.n=x holds seq is convergent & lim(seq)=x
proof
 let seq;
 assume H1: for n holds seq.n=x;
 then H2: seq is constant by SEQM_3:def 6;
 hence seq is convergent by SEQ_4:39;
 thus lim(seq) = seq.0 by SEQ_4:41,H2
  .= x by H1;
end;

theorem T11:
 for n st n>0 holds bseq(0).n=1
proof
 let n;
 assume H: n>0;
 thus bseq(0).n = (n choose 0)ù(n.^.(-0)) by Dbseq
  .= 1ù(n.^.(-0)) by NEWTON:29
  .= 1ù(n.^.0) by REAL_1:26
  .= 1 by POWER:29,H;
end;

theorem T12:
 (1/(k+1))ù(1/(k!))=1/((k+1)!)
proof
 k+1<>0 & k!<>0 by NAT_1:21,NEWTON:23;
 hence (1/(k+1))ù(1/(k!)) = 1/((k+1)ù(k!)) by REAL_2:51
  .= 1/((k+1)!) by NEWTON:21;
end;

theorem T13:
 bseq(k) is convergent & lim(bseq(k))=1/(k!) & lim(bseq(k))=eseq.k
proof
 H1: bseq(0) is convergent & lim(bseq(0))=1/(0!)
 proof
  consider bseq0 being Real_Sequence such that
   H2: for n holds bseq0.n=1 from ExRealSeq;
  H3: bseq0 is convergent & lim(bseq0)=1 by T10,H2;
  for n st nò1 holds bseq(0).n=bseq0.n
  proof
   let n;
   assume nò1;
   then nò0+1;
   then n>0 by NAT_1:38;
   hence bseq(0).n = 1 by T11
    .= bseq0.n by H2;
  end;
  then H4: ex N st for n st nòN holds bseq(0).n=bseq0.n;
  hence bseq(0) is convergent by SEQ_4:31,H3;
  thus lim(bseq(0)) = lim(bseq0) by SEQ_4:32,H3,H4
   .= 1 by H3
   .= 1/1 by REAL_2:43
   .= 1/(0!) by NEWTON:18;
 end;
 H5: now let k;
  assume H6: bseq(k) is convergent & lim(bseq(k))=1/(k!);
  thus bseq(k+1) is convergent & lim(bseq(k+1))=1/((k+1)!)
  proof
   consider seq such that
    H7: for n holds seq.n = (1/(k+1))ù(bseq(k).n) from ExRealSeq;
   H8: seq = (1/(k+1))þ(bseq(k)) by SEQ_1:13,H7;
   H9: seq is convergent & lim(seq)=1/((k+1)!)
   proof
    thus seq is convergent by SEQ_2:21,H6,H8;
    thus lim(seq) = (1/(k+1))ù(1/(k!)) by SEQ_2:22,H6,H8
     .= 1/((k+1)!) by T12;
   end;
   consider seq1 such that
    H10: for n holds seq1.n=seq.nù(aseq(k).n) from ExRealSeq;
   H11: seq1=seqþ(aseq(k)) by SEQ_1:12,H10;
   H12: seq1 is convergent & lim(seq1)=1/((k+1)!)
   proof
    H13: aseq(k) is convergent & lim(aseq(k))=1 by T9;
    then seqþ(aseq(k)) is convergent by SEQ_2:28,H9;
    hence seq1 is convergent by H11;
    thus lim(seq1) = lim(seqþ(aseq(k))) by H11
     .= lim(seq)ùlim(aseq(k)) by SEQ_2:29,H9,H13
     .= (1/((k+1)!))ùlim(aseq(k)) by H9
     .= (1/((k+1)!))ù1 by H13
     .= 1/((k+1)!);
   end;
   for n st nò1 holds bseq(k+1).n=seq1.n
   proof
    let n;
    assume nò1;
    then nò0+1;
    then n>0 by NAT_1:38;
    hence bseq(k+1).n = (1/(k+1))ù(bseq(k).n)ù(aseq(k).n) by T7
     .= (seq.n)ù(aseq(k).n) by H7
     .= seq1.n by H10;
   end;
   then H14: ex N st for n st nòN holds bseq(k+1).n=seq1.n;
   hence bseq(k+1) is convergent by SEQ_4:31,H12;
   thus lim(bseq(k+1)) = lim(seq1) by SEQ_4:32,H12,H14
    .= 1/((k+1)!) by H12;
  end;
 end;
 for k holds bseq(k) is convergent & lim(bseq(k))=1/(k!) from Ind(H1,H5);
 hence bseq(k) is convergent & lim(bseq(k))=1/(k!);
 hence lim(bseq(k))=eseq.k by Deseq;
end;

:: 0 ó (n choose k)ù(n.^.(-k))) ó 1/(k!)

theorem T14:
 k<n implies 0<aseq(k).n & aseq(k).nó1
proof
 assume H1: k<n;
 H2: 0ók by NAT_1:18;
 then H3: n>0 by AXIOMS:22,H1;
 H4: aseq(k).n=(n-k)/n by Daseq;
 H5: aseq(k).n=1-(k/n) by T8,H3;
 n-k>0 by REAL_2:108,H1;
 then (n-k)/n>0 by REAL_2:127,H3;
 hence aseq(k).n>0 by H4;
 k/nò0 by REAL_2:125,H2,H3;
 then 1-(k/n)ó1-0 by REAL_2:107;
 then 1-(k/n)ó1 by REAL_1:25;
 hence aseq(k).nó1 by H5;
end;

theorem T15:
 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
 assume H1: n>0;
 H2: bseq(k).n=(n choose k)ù(n.^.(-k)) by Dbseq;
 (n choose k) is Nat by NEWTON:35;
 then H3: (n choose k)ò0 by NAT_1:18;
 n.^.(-k)>0 by POWER:39,H1;
 then (n choose k)ù(n.^.(-k))ò0 by REAL_2:121,H3;
 hence H4: 0óbseq(k).n by H2;
 H5: bseq(0).nó1/(0!)
 proof
  H6: bseq(0).n=1 by T11,H1;
  1 = 1/1 by REAL_2:43
   .= 1/(0!) by NEWTON:18;
  then 1ó1/(0!);
  hence bseq(0).nó1/(0!) by H6;
 end;
 H7: now let k;
  assume H8: bseq(k).nó1/(k!);
  thus bseq(k+1).nó1/((k+1)!)
  proof
   (k+1)!>0 by NEWTON:23;
   then H9: 1/((k+1)!)>0 by REAL_2:149;
   per cases;
   suppose H10: k<n;
    H11: bseq(k+1).n=(1/(k+1))ù(bseq(k).n)ù(aseq(k).n) by T7,H1;
    k+1<>0 by NAT_1:21;
    then k+1>0 by NAT_1:19;
    then 1/(k+1)>0 by REAL_2:149;
    then 1/(k+1)ò0;
    then (1/(k+1))ù(bseq(k).n)ó(1/(k+1))ù(1/(k!)) by AXIOMS:25,H8;
    then H12: (1/(k+1))ù(bseq(k).n)ó1/((k+1)!) by T12;
    aseq(k).nò0 by T14,H10;
    then (1/(k+1))ù(bseq(k).n)ù(aseq(k).n)ó(1/((k+1)!))ù(aseq(k).n)
      by AXIOMS:25,H12;
    then H13: bseq(k+1).nó(1/((k+1)!))ù(aseq(k).n) by H11;
    aseq(k).nó1 by T14,H10;
    then 1/((k+1)!)ù(aseq(k).n)ó1/((k+1)!) by REAL_2:147,H9;
    hence thesis by AXIOMS:22,H13;
   suppose kòn;
    then H14: k+1>n by NAT_1:38;
    bseq(k+1).n = (n choose (k+1))ù(n.^.(-(k+1))) by Dbseq
     .= 0ù(n.^.(-(k+1))) by NEWTON:def 3,H14
     .= 0;
    hence thesis by H9;
  end;
 end;
 for k holds bseq(k).nó1/(k!) from Ind(H5,H7);
 hence H15: bseq(k).nó1/(k!);
 eseq.k=1/(k!) by Deseq;
 hence H16: bseq(k).nóeseq.k by H15;
 bseq(k).n=cseq(n).k by T3;
 hence 0ócseq(n).k & cseq(n).kó1/(k!) & cseq(n).kóeseq.k by H4,H15,H16;
end;

:: n>0 implies (1+(1/n)).^.n = ä(\k:(n choose k)ù(n.^.(-k)))

theorem T16:
 for seq st seq^\1 is summable holds
  seq is summable & ä(seq)=(seq.0)+ä(seq^\1)
proof
 let seq;
 assume seq^\1 is summable;
 hence seq is summable by SERIES_1:16;
 hence ä(seq) = Partial_Sums(seq).0+ä(seq^\(1+0)) by SERIES_1:18
  .= (seq.0)+ä(seq^\1) by SERIES_1:def 1;
end;

theorem T17:
 for sq st len(sq)=n & 1ók & k<n holds (sq/^1).k=sq.(k+1)
proof
 let sq;
 assume H1: len(sq)=n & 1ók & k<n;
 H2: len(sq)ò1 by AXIOMS:22,H1;
 len(sq/^1)=len(sq)-1 by RFINSEQ:def 2,H2;
 then H3: len(sq/^1)=n-1 by H1;
 H4: k+1ón by NAT_1:38,H1;
 n=(n-1)+1 by REAL_2:12;
 then k+1ó(n-1)+1 by H4;
 then kón-1 by REAL_1:53;
 then 1ók & kón-1 by H1;
 then 1ók & kólen(sq/^1) by H3;
 then kîdom(sq/^1) by FINSEQ_3:27;
 hence (sq/^1).k=sq.(k+1) by RFINSEQ:def 2,H2;
end;

theorem T18:
 for sq st len(sq)>0 holds
  ä(sq)=(sq.1)+ä(sq/^1)
proof
 let sq;
 assume H1: len(sq)>0;
 then 1ó1 & 0+1ólen(sq) by NAT_1:38;
 then H2: 1îdom(sq) by FINSEQ_3:27;
 sq is non empty by FINSEQ_1:25,H1;
 hence ä(sq) = ä(<*ã(sq,1)*>^(sq/^1)) by FINSEQ_5:32
  .= ä(<*sq.1*>^(sq/^1)) by FINSEQ_4:22,H2
  .= (sq.1)+ä(sq/^1) by RVSUM_1:106;
end;

theorem T19:
 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 & ä(seq)=ä(sq)
proof
 H1: now
  let seq, sq;
  assume H2: len(sq)=0 &
   (for k st k<0 holds seq.k=sq.(k+1)) &
   (for k st kò0 holds seq.k=0);
  sq is Element of 0-tuples_on REAL by FINSEQ_2:110,H2;
  then H3: ä(sq)=0 by RVSUM_1:109;
  H4: now let k;
   kò0 by NAT_1:18;
   hence seq.k = 0 by H2;
  end;
  seq.0=0 by H4;
  then H5: Partial_Sums(seq).0=0 by SERIES_1:def 1;
  H6: now let k;
   assume H7: Partial_Sums(seq).k=0;
   thus Partial_Sums(seq).(k+1)
    = (Partial_Sums(seq).k)+(seq.(k+1)) by SERIES_1:def 1
    .= 0+(seq.(k+1)) by H7
    .= 0 by H4;
  end;
  for k holds Partial_Sums(seq).k=0 from Ind(H5,H6);
  then H8:
   Partial_Sums(seq) is convergent & lim(Partial_Sums(seq))=0 by T10;
  hence seq is summable by SERIES_1:def 2;
  thus ä(seq) = 0 by SERIES_1:def 3,H8
   .= ä(sq) by H3;
 end;
 H9: now let n;
  assume H10:
   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 & ä(seq)=ä(sq);
  let seq, sq;
  assume H11: len(sq)=n+1 &
   (for k st k<n+1 holds seq.k=sq.(k+1)) &
   (for k st kòn+1 holds seq.k=0);
  H12: nò0 by NAT_1:18;
  then H13: n+1>0 by NAT_1:38;
  then H14: len(sq)>0 by H11;
  n+1ò0+1 by AXIOMS:24,H12;
  then n+1ò1;
  then len(sq)ò1 by H11;
  then H15: len(sq/^1) = len(sq)-1 by RFINSEQ:def 2
   .= (n+1)-1 by H11
   .= n by REAL_2:17;
  H16: now let k;
   assume k<n;
   then H17: k+1<n+1 by REAL_1:59;
   kò0 by NAT_1:18;
   then k+1ò0+1 by AXIOMS:24;
   then H18: k+1ò1;
   thus (seq^\1).k = seq.(k+1) by SEQM_3:def 9
    .= sq.((k+1)+1) by H11,H17
    .= (sq/^1).(k+1) by T17,H11,H17,H18;
  end;
  H19: now let k;
   assume kòn;
   then H20: k+1òn+1 by AXIOMS:24;
   thus (seq^\1).k = seq.(k+1) by SEQM_3:def 9
    .= 0 by H11,H20;
  end;
  H21: seq^\1 is summable & ä(seq^\1)=ä(sq/^1) by H10,H15,H16,H19;
  hence seq is summable by T16;
  thus ä(seq) = (seq.0)+ä(seq^\1) by T16,H21
   .= (sq.(0+1))+ä(seq^\1) by H11,H13
   .= (sq.1)+ä(seq^\1)
   .= (sq.1)+ä(sq/^1) by H21
   .= ä(sq) by T18,H14;
 end;
 thus thesis from Ind(H1,H9);
end;

theorem T20:
 x<>0 & y<>0 & kón implies
  ((x,y) In_Power n).(k+1)=(n choose k)ù(x.^.(n-k))ù(y.^.k)
proof
 assume H1: x<>0 & y<>0 & kón;
 kò0 by NAT_1:18;
 then H2: k+1ò0+1 by AXIOMS:24;
 then reconsider i1 = (k+1)-1 as Nat by NEWTON:2;
 H3: i1=k by REAL_2:17;
 then i1ón by H1;
 then reconsider l = n-i1 as Nat by NEWTON:2;
 H4: l=n-k by H3;
 H5: len((x,y) In_Power n)=n+1 by NEWTON:def 4;
 1ók+1 & k+1ón+1 by AXIOMS:24,H1,H2;
 then 1ók+1 & k+1ólen((x,y) In_Power n) by H5;
 then k+1îdom((x,y) In_Power n) by FINSEQ_3:27;
 hence ((x,y) In_Power n).(k+1)
  = (n choose i1)ù(x|^l)ù(y|^i1) by NEWTON:def 4
  .= (n choose i1)ù(x.^.l)ù(y|^i1) by POWER:48,H1
  .= (n choose i1)ù(x.^.l)ù(y.^.i1) by POWER:48,H1
  .= (n choose k)ù(x.^.l)ù(y.^.i1) by H3
  .= (n choose k)ù(x.^.(n-k))ù(y.^.i1) by H4
  .= (n choose k)ù(x.^.(n-k))ù(y.^.k) by H3;
end;

theorem T21:
 n>0 & kón implies cseq(n).k=((1,1/n) In_Power n).(k+1)
proof
 assume H1: n>0 & kón;
 then H2: 1/n>0 by REAL_2:149;
 H3: 1<>0;
 thus ((1,1/n) In_Power n).(k+1)
  = (n choose k)ù(1.^.(n-k))ù((1/n).^.k) by T20,H1,H2,H3
  .= (n choose k)ù1ù((1/n).^.k) by POWER:31
  .= (n choose k)ù((1/n).^.k)
  .= (n choose k)ù(n.^.(-k)) by POWER:37,H1
  .= cseq(n).k by Dcseq;
end;

theorem T22:
 n>0 implies
  cseq(n) is summable & ä(cseq(n))=(1+(1/n)).^.n & ä(cseq(n))=dseq.n
proof
 assume H1: n>0;
 then 1/n>0 by REAL_2:149;
 then H2: 1+(1/n)>1+0 by REAL_1:59;
 H3: 1+(1/n)>0 by AXIOMS:22,H2;
 H4: len((1,1/n) In_Power n)=n+1 by NEWTON:def 4;
 H5: now let k;
  assume k<n+1;
  then kón by NAT_1:38;
  hence cseq(n).k=((1,1/n) In_Power n).(k+1) by T21,H1;
 end;
 H6: now let k;
  assume kòn+1;
  then H7: k>n by NAT_1:38;
  thus cseq(n).k = (n choose k)ù(n.^.(-k)) by Dcseq
   .= 0ù(n.^.(-k)) by NEWTON:def 3,H7
   .= 0;
 end;
 thus cseq(n) is summable by T19,H4,H5,H6;
 thus H8: (1+(1/n)).^.n = (1+(1/n))|^n by POWER:48,H3
  .= ä((1,1/n) In_Power n) by NEWTON:41
  .= ä(cseq(n)) by T19,H4,H5,H6;
 thus dseq.n = (1+(1/n)).^.n by Ddseq
  .= ä(cseq(n)) by H8;
end;

:: number_e = lim(\n:(1+(1/n)).^.n)

theorem T23:
 dseq is convergent & lim(dseq)=number_e
proof
 H1: now let n;
  thus (dseq^\1).n = dseq.(n+1) by SEQM_3:def 9
   .= (1+1/(n+1)).^.(n+1) by Ddseq;
 end;
 then H2: dseq^\1 is convergent by POWER:67;
 hence dseq is convergent by SEQ_4:35;
 number_e=lim(dseq^\1) by POWER:def 4,H1;
 hence number_e=lim(dseq) by SEQ_4:36,H2;
end;

:: exp(1) = ä(\k:1/(k!))

theorem T24:
 eseq is summable & ä(eseq)=exp(1)
proof
 now let k;
  thus eseq.k = 1/(k!) by Deseq
   .= (1 #N k)/(k!) by PREPOWER:8
   .= (1 ExpSeq).k by SIN_COS:def 9;
 end;
 then H: eseq=(1 ExpSeq) by SEQ_1:9;
 1 ExpSeq is summable by SIN_COS:49;
 hence eseq is summable by H;
 thus exp(1) = exp.1 by SIN_COS:def 27
  .= ä(1 ExpSeq) by SIN_COS:def 26
  .= ä(eseq) by H;
end;

:: lim(\n:(1+(1/n)).^.n) = ä(\k:1/(k!))

theorem T25:
 for K holds
  for dseqK being Real_Sequence st
   for n holds dseqK.n=Partial_Sums(cseq(n)).K holds
    dseqK is convergent & lim(dseqK)=Partial_Sums(eseq).K
proof
 H1: now let dseq0 be Real_Sequence;
  assume H2: for n holds dseq0.n=Partial_Sums(cseq(n)).0;
  now let n;
   thus dseq0.n = Partial_Sums(cseq(n)).0 by H2
    .= cseq(n).0 by SERIES_1:def 1
    .= bseq(0).n by T3;
  end;
  then H3: dseq0 = bseq(0) by SEQ_1:9;
  hence dseq0 is convergent by T13;
  thus lim(dseq0) = lim(bseq(0)) by H3
   .= eseq.0 by T13
   .= Partial_Sums(eseq).0 by SERIES_1:def 1;
 end;
 H4: now let K;
  assume
   H5: for dseqK being Real_Sequence st
    for n holds dseqK.n=Partial_Sums(cseq(n)).K holds
     dseqK is convergent & lim(dseqK)=Partial_Sums(eseq).K;
  consider dseqK being Real_Sequence such that
   H6: for n holds dseqK.n=Partial_Sums(cseq(n)).K from ExRealSeq;
  H7: dseqK is convergent & lim(dseqK)=Partial_Sums(eseq).K by H5,H6;
  let dseqK1 being Real_Sequence;
  assume H8: for n holds dseqK1.n=Partial_Sums(cseq(n)).(K+1);
  now let n;
   thus dseqK1.n = Partial_Sums(cseq(n)).(K+1) by H8
    .= Partial_Sums(cseq(n)).K+cseq(n).(K+1) by SERIES_1:def 1
    .= dseqK.n+cseq(n).(K+1) by H6
    .= dseqK.n+bseq(K+1).n by T3
    .= (dseqK+bseq(K+1)).n by SEQ_1:11;
  end;
  then H9: dseqK1=dseqK+bseq(K+1) by SEQ_1:9;
  H10: bseq(K+1) is convergent by T13;
  hence dseqK1 is convergent by SEQ_2:19,H7,H9;
  thus lim(dseqK1) = lim(dseqK+bseq(K+1)) by H9
   .= lim(dseqK)+lim(bseq(K+1)) by SEQ_2:20,H7,H10
   .= Partial_Sums(eseq).K+lim(bseq(K+1)) by H7
   .= Partial_Sums(eseq).K+eseq.(K+1) by T13
   .= Partial_Sums(eseq).(K+1) by SERIES_1:def 1;
 end;
 thus thesis from Ind(H1,H4);
end;

theorem T26:
 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 seq is convergent & lim(seq)=x;
 then H1: for eps st eps>0 ex N st for n st nòN holds ³.seq.n-x.³<eps
  by SEQ_2:def 5;
 let eps;
 assume eps>0;
 then consider N such that H2: for n st nòN holds ³.seq.n-x.³<eps by H1;
 take N;
 let n;
 assume nòN;
 then ³.seq.n-x.³<eps by H2;
 then seq.n-x>-eps by SEQ_2:9;
 then H3: (seq.n-x)+x>-eps+x by REAL_1:59;
 (seq.n-x)+x=seq.n by REAL_2:12;
 then H4: seq.n>-eps+x by H3;
 -eps+x=x-eps by REAL_1:def 3;
 hence seq.n>x-eps by H4;
end;

theorem T27:
 (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 H1:
  (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);
 H2: for eps st eps>0 holds ex N st for n st nòN holds ³.seq.n-x.³<eps
 proof
  let eps;
  assume H3: eps>0;
  then consider N1 being Nat such that
   H4: for n st nòN1 holds seq.n>x-eps by H1;
  consider N2 being Nat such that
   H5: for n st nòN2 holds seq.nóx by H1;
  take N = max(N1,N2);
  let n;
  assume nòN;
  then nòN1 & nòN2 by SQUARE_1:50;
  then H6: seq.n>x-eps & seq.nóx by H4,H5;
  then H7: seq.n-x>(x-eps)-x by REAL_1:59;
  (x-eps)-x = (x+-eps)-x by REAL_1:def 3
   .= -eps by REAL_2:17;
  then H8: seq.n-x>-eps by H7;
  x+eps>x+0 by REAL_1:59,H3;
  then seq.n<x+eps by AXIOMS:22,H6;
  then seq.n-x<eps by REAL_1:85;
  hence ³.seq.n-x.³<eps by SEQ_2:9,H8;
 end;
 hence seq is convergent by SEQ_2:def 4;
 hence lim(seq)=x by SEQ_2:def 5,H2;
end;

theorem T28:
 seq is summable implies
  for eps st eps>0 holds ex K st Partial_Sums(seq).K>ä(seq)-eps
proof
 assume H1: seq is summable;
 let eps;
 assume H2: eps>0;
 Partial_Sums(seq) is convergent by SERIES_1:def 2,H1;
 then consider K such that
  H3: for k st kòK holds
   Partial_Sums(seq).k>lim(Partial_Sums(seq))-eps by T26,H2;
 take K;
 ä(seq)=lim(Partial_Sums(seq)) by SERIES_1:def 3;
 then H4: for k st kòK holds Partial_Sums(seq).k>ä(seq)-eps by H3;
 thus Partial_Sums(seq).K>ä(seq)-eps by H4;
end;

theorem T29:
 nò1 implies dseq.nóä(eseq)
proof
 assume nò1;
 then nò0+1;
 then H: n>0 by NAT_1:38;
 for k holds 0ócseq(n).k & cseq(n).kóeseq.k by T15,H;
 then ä(cseq(n))óä(eseq) by SERIES_1:24,T24;
 hence dseq.nóä(eseq) by T22,H;
end;

theorem T30:
 seq is summable & (for k holds seq.kò0) implies
  ä(seq)òPartial_Sums(seq).K
proof
 assume H1: seq is summable & (for k holds seq.kò0);
 then H2: seq^\(K+1) is summable by SERIES_1:15;
 now let k;
  (seq^\(K+1)).k = seq.(K+1+k) by SEQM_3:def 9;
  hence (seq^\(K+1)).kò0 by H1;
 end;
 then ä(seq^\(K+1))ò0 by SERIES_1:21,H2;
 then Partial_Sums(seq).K+ä(seq^\(K+1))òPartial_Sums(seq).K+0 by AXIOMS:24;
 hence ä(seq)òPartial_Sums(seq).K by SERIES_1:18,H1;
end;

theorem T31:
 dseq is convergent & lim(dseq)=ä(eseq)
proof
 for eps st eps>0 holds ex N st for n st nòN holds dseq.n>ä(eseq)-eps
 proof
  let eps;
  assume eps>0;
  then H1: eps/2>0 by REAL_2:127;
  consider K such that
   H2: Partial_Sums(eseq).K>ä(eseq)-eps/2 by T28,T24,H1;
  consider dseqK being Real_Sequence such that
   H3: for n holds dseqK.n=Partial_Sums(cseq(n)).K from ExRealSeq;
  H4: dseqK is convergent & lim(dseqK)=Partial_Sums(eseq).K by T25,H3;
  consider N such that
   H5: for n st nòN holds dseqK.n>Partial_Sums(eseq).K-eps/2 by T26,H1,H4;
  take N1 = N+1;
  let n;
  assume H6: nòN1;
  N+1òN+0 by AXIOMS:24;
  then H7: nòN by AXIOMS:22,H6;
  Nò0 by NAT_1:18;
  then N1>0 by NAT_1:38;
  then H8: n>0 by AXIOMS:22,H6;
  H9: for k holds cseq(n).kò0 by T15,H8;
  cseq(n) is summable by T22,H8;
  then ä(cseq(n))òPartial_Sums(cseq(n)).K by T30,H9;
  then dseq.nòPartial_Sums(cseq(n)).K by T22,H8;
  then H10: dseq.nòdseqK.n by H3;
  dseqK.n>Partial_Sums(eseq).K-eps/2 by H5,H7;
  then H11: dseq.n>Partial_Sums(eseq).K-eps/2 by AXIOMS:22,H10;
  H12: ä(eseq)-eps/2-eps/2 = ä(eseq)-(eps/2+eps/2) by REAL_1:27
   .= ä(eseq)-eps by REAL_2:90;
  Partial_Sums(eseq).K-eps/2>ä(eseq)-eps/2-eps/2 by REAL_1:59,H2;
  then Partial_Sums(eseq).K-eps/2>ä(eseq)-eps by H12;
  hence dseq.n>ä(eseq)-eps by AXIOMS:22,H11;
 end;
 hence dseq is convergent & lim(dseq)=ä(eseq) by T27,T29;
end;

:: number_e = exp(1)

definition
 redefine func number_e equals
  :Dnumber_e: ä(eseq);
 compatibility
 proof
  number_e = lim(dseq) by T23
   .= ä(eseq) by T31;
  hence thesis;
 end;
end;

definition
 redefine func number_e equals
  exp(1);
 compatibility
 proof
  number_e = ä(eseq) by Dnumber_e
   .= exp(1) by T24;
  hence thesis;
 end;
end;


begin :: number_e is irrational

theorem T32:
 x is rational implies ex n st nò2 & n!ùx is integer
proof
 assume H1: x is rational;
 consider i, n such that H2: n<>0 & x=i/n by RAT_1:24,H1;
 per cases;
 suppose n<1+1;
  then H3: nó1 by NAT_1:38;
  n>0 by NAT_1:19,H2;
  then nò0+1 by NAT_1:38;
  then H4: n=1 by AXIOMS:21,H3;
  x = i/n by H2
   .= i/1 by H4
   .= i by REAL_2:44;
  then reconsider x1 = x as Integer;
  take n = 2;
  n!ùx1 is integer;
  hence nò2 & n!ùx is integer;
 suppose H5: nò2;
  take n;
  thus nò2 by H5;
  then nò1 by AXIOMS:22;
  then reconsider m = n-1 as Nat by INT_1:18;
  H6: n=m+1 by REAL_2:12;
  then n!ùx = (m+1)!ùx
   .= (m+1)ù(m!)ùx by NEWTON:21
   .= (nù(m!))ùx by H6
   .= nù(xù(m!)) by AXIOMS:16
   .= (nùx)ù(m!) by AXIOMS:16
   .= (nù(i/n))ù(m!) by H2
   .= iù(m!) by REAL_1:43,H2;
  hence n!ùx is integer;
end;

theorem T33:
 n!ùeseq.k = (n!)/(k!)
proof
 H: k!<>0 by NEWTON:23;
 thus n!ùeseq.k = n!ù(1/(k!)) by Deseq
  .= (n!)/(k!) by REAL_2:56,H;
end;

theorem T34:
 (n!)/(k!)>0
proof
 n!>0 & k!>0 by NEWTON:23;
 hence (n!)/(k!)>0 by REAL_2:127;
end;

theorem T35:
 seq is summable & (for n holds seq.n>0) implies ä(seq)>0
proof
 assume H1: seq is summable & (for n holds seq.n>0);
 H2: ä(seq)=(Partial_Sums(seq).0)+ä(seq^\(0+1)) by SERIES_1:18,H1
  .= seq.0+ä(seq^\1) by SERIES_1:def 1;
 H3: seq.0>0 by H1;
 H4: seq^\1 is summable by SERIES_1:15,H1;
 now let n;
  (seq^\1).n = seq.(1+n) by SEQM_3:def 9;
  hence (seq^\1).nò0 by H1;
 end;
 then ä(seq^\1)ò0 by SERIES_1:21,H4;
 then ä(seq)>0+0 by REAL_1:67,H2,H3;
 hence ä(seq)>0;
end;

theorem T36:
 n!ùä(eseq^\(n+1))>0
proof
 H1: n!>0 by NEWTON:23;
 H2: eseq^\(n+1) is summable by SERIES_1:15,T24;
 now let k;
  H3: (eseq^\(n+1)).k = eseq.(n+1+k) by SEQM_3:def 9
   .= 1/((n+1+k)!) by Deseq;
  (n+1+k)!>0 by NEWTON:23;
  hence (eseq^\(n+1)).k>0 by REAL_2:149,H3;
 end;
 then ä(eseq^\(n+1))>0 by T35,H2;
 hence thesis by REAL_2:122,H1;
end;

theorem T37:
 kón implies (n!)/(k!) is integer
proof
 assume kón;
 then reconsider m = n-k as Nat by INT_1:18;
 H1: n=m+k by REAL_2:12;
 for m holds ((m+k)!)/(k!) is integer
 proof
  k!<>0 by NEWTON:23;
  then ((0+k)!)/(k!) = 1 by REAL_1:37;
  then H2: ((0+k)!)/(k!) is integer;
  H3: now let m;
   assume ((m+k)!)/(k!) is integer;
   then reconsider i = ((m+k)!)/(k!) as Integer;
   H4: (m+k+1)ùi is Integer;
   ((m+1)+k)! = (m+k+1)! by AXIOMS:13
    .= (m+k+1)ù((m+k)!) by NEWTON:21;
   then (((m+1)+k)!)/(k!) = (m+k+1)ù((m+k)!)/(k!)
    .= (m+k+1)ù((m+k)!)ù(k!)" by REAL_1:16
    .= (m+k+1)ù(((m+k)!)ù(k!)") by AXIOMS:16
    .= (m+k+1)ù(((m+k)!)/(k!)) by REAL_1:16;
   hence (((m+1)+k)!)/(k!) is integer by H4;
  end;
  thus thesis from Ind(H2,H3);
 end;
 then ((m+k)!)/(k!) is integer;
 hence (n!)/(k!) is integer by H1;
end;

theorem T38:
 n!ùPartial_Sums(eseq).n is integer
proof
 for k st kón holds n!ùPartial_Sums(eseq).k is integer
 proof
  H1: now assume H2: 0ón;
   n!ùPartial_Sums(eseq).0 = n!ùeseq.0 by SERIES_1:def 1
    .= (n!)/(0!) by T33;
   hence n!ùPartial_Sums(eseq).0 is integer by T37,H2;
  end;
  H3: now let k;
   assume H4: kón implies n!ùPartial_Sums(eseq).k is integer;
   assume H5: k+1ón;
   k+0ók+1 by AXIOMS:24;
   then kón by AXIOMS:22,H5;
   then reconsider i = n!ùPartial_Sums(eseq).k as Integer by H4;
   n!ùeseq.(k+1) = (n!)/((k+1)!) by T33;
   then reconsider j = n!ùeseq.(k+1) as Integer by T37,H5;
   H6: 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) by AXIOMS:18;
   i+j is Integer;
   hence n!ùPartial_Sums(eseq).(k+1) is integer by H6;
  end;
  thus thesis from Ind(H1,H3);
 end;
 hence thesis;
end;

theorem T39:
 x=1/(n+1) implies (n!)/((n+k+1)!)óx.^.(k+1)
proof
 assume H1: x=1/(n+1);
 for k holds (n!)/((n+k+1)!)óx.^.(k+1)
 proof
  H2: now
   H3: n+1<>0 & n!<>0 by NAT_1:21,NEWTON:23;
   H4: (n!)/((n+1)!) = (n!)/((n+1)ù(n!)) by NEWTON:21
    .= (n!)ù((n+1)ù(n!))" by REAL_1:16
    .= (n!)ù((n+1)"ù(n!)") by REAL_1:24,H3
    .= (n!)ù(n!)"ù(n+1)" by AXIOMS:16
    .= 1ù(n+1)" by REAL_1:def 2,H3
    .= 1/(n+1) by REAL_1:33
    .= x by H1;
   H5: x = x.^.(0+1) by POWER:30;
   thus (n!)/((n+0+1)!)óx.^.(0+1) by H4,H5;
  end;
  H6: now let k;
   assume H7: (n!)/((n+k+1)!)óx.^.(k+1);
   nò0 & n+(k+1)ò0 by NAT_1:18;
   then H8: n+1>0 & n+(k+1)+1>0 & (n+k+1)!<>0 & (n+k)!<>0
    by NAT_1:38,NEWTON:23;
   then 1/(n+1)>0 by REAL_2:149;
   then H9: x>0 by H1;
   k+1ò0 by NAT_1:18;
   then n+(k+1)òn+0 by AXIOMS:24;
   then n+(k+1)+1òn+1 by AXIOMS:24;
   then 1/(n+(k+1)+1)ó1/(n+1) by REAL_2:152,H8;
   then (n+(k+1)+1)"ó1/(n+1) by REAL_1:33;
   then H10: (n+(k+1)+1)"óx by H1;
   H11: (n!)/((n+k+1)!)>0 by T34;
   (n+(k+1)+1)">0 by REAL_1:72,H8;
   then H12: (n!)/((n+k+1)!)ù(n+(k+1)+1)"óx.^.(k+1)ùx
    by REAL_2:197,H7,H10,H11;
   x.^.(k+1)ùx = x.^.(k+1)ùx.^.1 by POWER:30
    .= x.^.((k+1)+1) by POWER:32,H9;
   then H13: (n!)/((n+k+1)!)ù(n+(k+1)+1)"óx.^.((k+1)+1) by H12;
   (n!)/((n+(k+1)+1)!) = (n!)ù((n+(k+1)+1)!)" by REAL_1:16
    .= (n!)ù((n+(k+1)+1)ù((n+(k+1))!))" by NEWTON:21
    .= (n!)ù((n+(k+1)+1)ù((n+k+1)!))" by AXIOMS:13
    .= (n!)ù((n+(k+1)+1)"ù((n+k+1)!)") by REAL_1:24,H8
    .= (n!)ù((n+k+1)!)"ù(n+(k+1)+1)" by AXIOMS:16
    .= (n!)/((n+k+1)!)ù(n+(k+1)+1)" by REAL_1:16;
   hence (n!)/((n+(k+1)+1)!)óx.^.((k+1)+1) by H13;
  end;
  thus thesis from Ind(H2,H6);
 end;
 hence thesis;
end;

theorem T40:
 n>0 & x=1/(n+1) implies n!ùä(eseq^\(n+1))óx/(1-x)
proof
 assume H1: n>0 & x=1/(n+1);
 n+1>0+1 by REAL_1:59,H1;
 then 0<1/(n+1) & 1/(n+1)<1 by REAL_2:163;
 then H2: 0<x & x<1 by H1;
 consider seq being Real_Sequence such that
  H3: for k holds seq.k=x.^.(k+1) from ExRealSeq;
 H4: seq.0 = x.^.(0+1) by H3
  .= x by POWER:30;
 ³.x.³=x by ANAL_1:2,H2;
 then H5: ³.x.³<1 by H2;
 now let k;
  thus seq.(k+1) = x.^.(k+1+1) by H3
   .= x.^.1ùx.^.(k+1) by POWER:32,H2
   .= xùx.^.(k+1) by POWER:30
   .= xùseq.k by H3;
 end;
 then H6: seq is summable & ä(seq)=seq.0/(1-x) by SERIES_1:29,H5;
 then H7: ä(seq)=x/(1-x) by H4;
 H8: eseq^\(n+1) is summable by SERIES_1:15,T24;
 now let k;
  H9: (n+k+1)!<>0 by NEWTON:23;
  H10: (n!þ(eseq^\(n+1))).k = n!ù((eseq^\(n+1)).k) by SEQ_1:13
   .= n!ùeseq.(n+1+k) by SEQM_3:def 9
   .= n!ùeseq.(n+k+1) by AXIOMS:13
   .= n!ù(1/((n+k+1)!)) by Deseq
   .= n!/((n+k+1)!) by REAL_2:56,H9;
  hence (n!þ(eseq^\(n+1))).kò0 by T34;
  seq.k=x.^.(k+1) by H3;
  hence (n!þ(eseq^\(n+1))).kóseq.k by T39,H1,H10;
 end;
 then ä(n!þ(eseq^\(n+1)))óä(seq) by SERIES_1:24,H6;
 then ä(n!þ(eseq^\(n+1)))óx/(1-x) by H7;
 hence n!ùä(eseq^\(n+1))óx/(1-x) by SERIES_1:13,H8;
end;

theorem T41:
 nò2 & x=1/(n+1) implies x/(1-x)<1
proof
 assume H1: nò2 & x=1/(n+1);
 nò0 by NAT_1:18;
 then H2: n+1>0 by NAT_1:38;
 then H3: x>0 by REAL_2:149,H1;
 2<n+1 by NAT_1:38,H1;
 then 2/(n+1)<1 by REAL_2:142;
 then 2ùx<1 by REAL_2:56,H1,H2;
 then x+x<1 by SQUARE_1:5;
 then x<1-x by REAL_1:86;
 hence x/(1-x)<1 by REAL_2:142,H3;
end;

theorem T42:
 number_e is irrational
proof
 assume number_e is rational;
 then consider n such that H1: nò2 & n!ùnumber_e is integer by T32;
 H2: n!ùnumber_e = n!ùä(eseq) by Dnumber_e
  .= n!ù((Partial_Sums(eseq).n)+ä(eseq^\(n+1))) by SERIES_1:18,T24
  .= n!ù(Partial_Sums(eseq).n)+n!ùä(eseq^\(n+1)) by AXIOMS:18;
 reconsider ne = n!ùnumber_e as Integer by H1;
 reconsider ne1 = n!ùPartial_Sums(eseq).n as Integer by T38;
 n!ùä(eseq^\(n+1))=ne-ne1 by REAL_1:30,H2;
 then H3: n!ùä(eseq^\(n+1)) is integer;
 set x = 1/(n+1);
 H4: x/(1-x)<1 by T41,H1;
 n>0 by AXIOMS:22,H1;
 then n!ùä(eseq^\(n+1))óx/(1-x) by T40;
 then n!ùä(eseq^\(n+1))<0+1 by AXIOMS:22,H4;
 then H5: n!ùä(eseq^\(n+1))ó0 by INT_1:20,H3;
 n!ùä(eseq^\(n+1))>0 by T36;
 hence contradiction by H5;
end;