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