assume
number_e is rational
; :: thesis: contradiction

then consider n being Nat 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 ;

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

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

hence contradiction by A3, Th35, INT_1:7; :: thesis: verum

then consider n being Nat 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 ;

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

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

hence contradiction by A3, Th35, INT_1:7; :: thesis: verum