assume not number_e is irrational ; :: thesis: contradiction
then consider n being Element of NAT such that
A1: n >= 2 and
A2: (n ! ) * number_e is integer by Th32;
reconsider ne = (n ! ) * number_e as Integer by A2;
set x = 1 / (n + 1);
reconsider ne1 = (n ! ) * ((Partial_Sums eseq ) . n) as Integer by Th38;
(n ! ) * number_e = (n ! ) * (((Partial_Sums eseq ) . n) + (Sum (eseq ^\ (n + 1)))) by Th24, SERIES_1:18
.= ((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, Th40, Th41;
then (n ! ) * (Sum (eseq ^\ (n + 1))) < 0 + 1 by XXREAL_0:2;
hence contradiction by A3, Th36, INT_1:20; :: thesis: verum