:: Formal Proof of Transcendence of the Number $e$. {P}art {II}
:: by Yasushige Watase
::
:: Received November 17, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users


Lm26: for n being Nat
for a being Real holds n * a = n * (In (a,F_Real))

proof end;

Lm30: for n being Nat
for z being Element of INT.Ring
for r being Integer st z = r holds
n * z = n * r

proof end;

Lm1: for n being Nat
for z being Element of INT.Ring holds n * z = (In (n,INT.Ring)) * z

proof end;

Lm2: for a being Integer
for n being Nat holds (In (a,INT)) |^ n = (In (a,INT.Ring)) |^ n

proof end;

Lm3: for n being Nat
for z being Element of INT.Ring
for r being Real st z = r holds
n * z = n * r

proof end;

theorem Th3: :: E_TRANS2:1
for i being Nat
for r being Element of F_Real holds Sum (i |-> r) = i * r
proof end;

Lm14: for z being Element of F_Real st z <> 0. F_Real holds
for n being Nat holds |.(power (z,n)).| = |.z.| to_power n

proof end;

Lm15: for m being positive Nat
for j being Nat
for ks being Real st j in Seg m & 0 <= ks & ks <= m holds
|.(j - ks).| <= m

proof end;

Lm5: for k being Nat holds eta (k,k) = k !
proof end;

theorem Th14: :: E_TRANS2:2
for p1, q1 being sequence of INT.Ring holds (p1 *' q1) . 0 = (p1 . 0) * (q1 . 0)
proof end;

theorem Th4: :: E_TRANS2:3
for f being Element of the carrier of (Polynom-Ring INT.Ring)
for n being Nat holds ^ (f |^ n) = (^ f) |^ n
proof end;

theorem Th5: :: E_TRANS2:4
for R being domRing
for f being Element of the carrier of (Polynom-Ring R)
for n being Nat holds ~ (f |^ n) = (~ f) `^ n
proof end;

theorem Th6: :: E_TRANS2:5
for n being Nat
for f being Element of the carrier of (Polynom-Ring INT.Ring) holds n * f = (In (n,INT.Ring)) * f
proof end;

Lm16: for m being positive Nat
for n being Nat
for m0 being Element of F_Real st m = m0 holds
m |^ n = m0 |^ n

proof end;

theorem Th41: :: E_TRANS2:6
for M being Element of F_Real
for F being FinSequence of F_Real st ( for i being Nat st i in dom F holds
|.(F . i).| <= M ) holds
|.(Product F).| <= M |^ (len F)
proof end;

definition
let p be Polynomial of INT.Ring;
A1: dom |.p.| = dom p by VALUED_1:def 11
.= NAT by FUNCT_2:def 1 ;
:: original: |.
redefine func |.p.| -> sequence of INT.Ring means :Def9: :: E_TRANS2:def 1
for n being Nat holds it . n = |.(p . n).|;
coherence
|.p.| is sequence of INT.Ring
proof end;
compatibility
for b1 being sequence of INT.Ring holds
( b1 = |.p.| iff for n being Nat holds b1 . n = |.(p . n).| )
proof end;
end;

:: deftheorem Def9 defines |. E_TRANS2:def 1 :
for p being Polynomial of INT.Ring
for b2 being sequence of INT.Ring holds
( b2 = |.p.| iff for n being Nat holds b2 . n = |.(p . n).| );

Lm18: for n being set
for p being finite-Support sequence of INT.Ring holds Support p = Support |.p.|

proof end;

registration
let p be Polynomial of INT.Ring;
cluster |.p.| -> the carrier of INT.Ring -valued finite-Support for the carrier of INT.Ring -valued Function;
coherence
for b1 being the carrier of INT.Ring -valued Function st b1 = |.p.| holds
b1 is finite-Support
proof end;
end;

Lm19: for n being Nat
for x being Element of F_Real st x > 0 holds
(power F_Real) . (x,n) = x to_power n

proof end;

Lm22: for m being positive Nat
for x0 being Element of F_Real
for s, z0 being Real st 0 < x0 & x0 <= m & 0 < s & s < 1 & 1 < z0 holds
|.(- (x0 * (z0 to_power (x0 * (1 - s))))).| <= m * (z0 to_power m)

proof end;

Lm23: for g being non zero Polynomial of INT.Ring holds rng |.g.| is finite
proof end;

registration
let g be non zero Polynomial of INT.Ring;
cluster rng |.g.| -> finite ;
coherence
rng |.g.| is finite
by Lm23;
end;

theorem Th43: :: E_TRANS2:7
for g being non zero Polynomial of INT.Ring ex M being Nat st
for i being Nat holds |.(g . i).| <= M
proof end;

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: construct Polynomial
:: f(p,m) = x^{p-1}(1-x)^{p}(2-x)^{p}\cdots (n-x)^{p}
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let i be Nat;
func tau i -> Element of the carrier of (Polynom-Ring INT.Ring) equals :: E_TRANS2:def 2
<%(In ((- i),INT.Ring)),(1. INT.Ring)%>;
coherence
<%(In ((- i),INT.Ring)),(1. INT.Ring)%> is Element of the carrier of (Polynom-Ring INT.Ring)
by POLYNOM3:def 10;
end;

:: deftheorem defines tau E_TRANS2:def 2 :
for i being Nat holds tau i = <%(In ((- i),INT.Ring)),(1. INT.Ring)%>;

definition
let p be non zero Nat;
let m be Nat;
func x. (m,p) -> FinSequence of the carrier of (Polynom-Ring INT.Ring) means :Def2: :: E_TRANS2:def 3
( len it = m & ( for i being Nat st i in dom it holds
it . i = (tau i) |^ p ) );
existence
ex b1 being FinSequence of the carrier of (Polynom-Ring INT.Ring) st
( len b1 = m & ( for i being Nat st i in dom b1 holds
b1 . i = (tau i) |^ p ) )
proof end;
uniqueness
for b1, b2 being FinSequence of the carrier of (Polynom-Ring INT.Ring) st len b1 = m & ( for i being Nat st i in dom b1 holds
b1 . i = (tau i) |^ p ) & len b2 = m & ( for i being Nat st i in dom b2 holds
b2 . i = (tau i) |^ p ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines x. E_TRANS2:def 3 :
for p being non zero Nat
for m being Nat
for b3 being FinSequence of the carrier of (Polynom-Ring INT.Ring) holds
( b3 = x. (m,p) iff ( len b3 = m & ( for i being Nat st i in dom b3 holds
b3 . i = (tau i) |^ p ) ) );

definition
let p be prime odd Nat;
let m be positive Nat;
func ff_0 (m,p) -> FinSequence of the carrier of (Polynom-Ring INT.Ring) equals :: E_TRANS2:def 4
(x. (m,p)) ^ <*((tau 0) |^ (p -' 1))*>;
coherence
(x. (m,p)) ^ <*((tau 0) |^ (p -' 1))*> is FinSequence of the carrier of (Polynom-Ring INT.Ring)
;
end;

:: deftheorem defines ff_0 E_TRANS2:def 4 :
for p being prime odd Nat
for m being positive Nat holds ff_0 (m,p) = (x. (m,p)) ^ <*((tau 0) |^ (p -' 1))*>;

definition
let p be prime odd Nat;
let m be positive Nat;
func f_0 (m,p) -> Element of the carrier of (Polynom-Ring INT.Ring) equals :: E_TRANS2:def 5
Product (ff_0 (m,p));
coherence
Product (ff_0 (m,p)) is Element of the carrier of (Polynom-Ring INT.Ring)
;
end;

:: deftheorem defines f_0 E_TRANS2:def 5 :
for p being prime odd Nat
for m being positive Nat holds f_0 (m,p) = Product (ff_0 (m,p));

theorem Th8: :: E_TRANS2:8
for i, n being Nat holds len (~ ((tau i) |^ n)) = n + 1
proof end;

theorem Th9: :: E_TRANS2:9
for f, g being Element of the carrier of (Polynom-Ring INT.Ring) st (len (~ f)) * (len (~ g)) <> 0 holds
len (~ (f * g)) = ((len (~ f)) + (len (~ g))) - 1
proof end;

theorem Th10: :: E_TRANS2:10
for k being non zero Nat
for p being prime odd Nat holds
( (x. (k,p)) ^ <*((tau (k + 1)) |^ p)*> = x. ((k + 1),p) & Product (x. ((k + 1),p)) = (Product (x. (k,p))) * ((tau (k + 1)) |^ p) )
proof end;

theorem Th11: :: E_TRANS2:11
for p being prime odd Nat
for m being positive Nat holds len (~ (Product (x. (m,p)))) = (m * p) + 1
proof end;

theorem Th12: :: E_TRANS2:12
for p being prime odd Nat
for m being positive Nat holds len (~ (f_0 (m,p))) = (m * p) + p
proof end;

Lm4: for i being Nat holds Roots (tau i) = {(In (i,INT.Ring))}
proof end;

theorem Th13: :: E_TRANS2:13
for i being Nat holds (Der1 INT.Ring) . (tau i) = 1. (Polynom-Ring INT.Ring)
proof end;

theorem Th15: :: E_TRANS2:14
for f being Element of the carrier of (Polynom-Ring INT.Ring)
for i being Nat holds
( ((tau 0) *' f) . (i + 1) = f . i & ((tau 0) *' f) . 0 = 0. INT.Ring )
proof end;

Lm6: for f being Element of the carrier of (Polynom-Ring INT.Ring)
for n being non zero Nat
for i being Element of NAT holds
( ((~ ((tau 0) |^ n)) *' f) . (i + n) = f . i & ((~ ((tau 0) |^ n)) *' f) | (Segm n) = (Segm n) --> (0. INT.Ring) )

proof end;

theorem Th16: :: E_TRANS2:15
for p being prime odd Nat
for m being positive Nat holds
( len (x. (m,p)) = m & len (ff_0 (m,p)) = m + 1 & (ff_0 (m,p)) . ((len (x. (m,p))) + 1) = (tau 0) |^ (p -' 1) )
proof end;

Lm7: for p being prime odd Nat
for m being positive Nat
for i being Nat st i in Seg m holds
( (ff_0 (m,p)) /. i = (tau i) |^ p & (ff_0 (m,p)) . i = (tau i) |^ p & i in dom (ff_0 (m,p)) )

proof end;

Lm8: for i being Nat
for k being non zero Nat holds tau i divides (tau i) |^ k

proof end;

Lm9: for p being prime odd Nat
for m being positive Nat
for j being Nat st j in Seg m holds
Product (ff_0 (m,p)) = ((tau j) |^ p) * (Product (Del ((ff_0 (m,p)),j)))

proof end;

theorem Th18: :: E_TRANS2:16
for p being prime odd Nat
for m being positive Nat
for k being Nat st 0 <= k & k <= p - 1 holds
for i, j being Nat st i in Seg (k + 1) holds
tau j divides (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i
proof end;

Lm10: for n, i being Nat holds (~ ((tau i) |^ n)) . 0 = (In ((- i),INT.Ring)) |^ n
proof end;

theorem Th20: :: E_TRANS2:17
for p being prime odd Nat
for m being positive Nat holds (~ (Product (x. (m,p)))) . 0 = (((- 1) |^ m) * (m !)) |^ p
proof end;

theorem Th21: :: E_TRANS2:18
for p being prime odd Nat
for m being positive Nat
for k being Nat st 0 <= k & k <= p -' 2 holds
(((Der1 INT.Ring) |^ k) . (f_0 (m,p))) . 0 = 0. INT.Ring
proof end;

theorem Th22: :: E_TRANS2:19
for p being prime odd Nat
for m being positive Nat
for k being Nat st 0 <= k & k <= p -' 2 holds
eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(0. INT.Ring)) = 0. INT.Ring
proof end;

theorem Th23: :: E_TRANS2:20
for p being prime odd Nat
for m being positive Nat holds eval ((~ (((Der1 INT.Ring) |^ (p -' 1)) . (f_0 (m,p)))),(0. INT.Ring)) = ((p -' 1) !) * (In (((((- 1) |^ m) * (m !)) |^ p),INT.Ring))
proof end;

theorem Th24: :: E_TRANS2:21
for p being prime odd Nat
for m being positive Nat
for k being non zero Nat st p <= k holds
eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(0. INT.Ring)) = (k !) * ((~ (Product (x. (m,p)))) . (k -' (p -' 1)))
proof end;

theorem Th25: :: E_TRANS2:22
for j being Nat
for u being Element of the carrier of (Polynom-Ring INT.Ring) holds eval ((~ ((tau j) * u)),(In (j,INT.Ring))) = 0. INT.Ring
proof end;

theorem Th26: :: E_TRANS2:23
for p being prime odd Nat
for m being positive Nat
for k, j being Nat st k < p & j in Seg m holds
eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(In (j,INT.Ring))) = 0. INT.Ring
proof end;

theorem Th27: :: E_TRANS2:24
for i being Nat holds (Der1 INT.Ring) . (tau i) = 1. (Polynom-Ring INT.Ring)
proof end;

Lm11: for R being domRing
for k being Nat
for f being Element of the carrier of (Polynom-Ring R) holds ((Der1 R) |^ 0) . (f |^ k) = f |^ k

proof end;

theorem Th28: :: E_TRANS2:25
for p being prime odd Nat
for m being positive Nat
for j, k being Nat st j in Seg m & p <= k holds
for i being Nat st i in Seg p holds
tau j divides (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i
proof end;

theorem Th29: :: E_TRANS2:26
for p being prime odd Nat
for m being positive Nat
for k, j, i being Nat st p + 1 < i & i in dom (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) holds
(LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i = 0. (Polynom-Ring INT.Ring)
proof end;

theorem Th30: :: E_TRANS2:27
for p being prime odd Nat
for m being positive Nat
for k, j being Nat st j in Seg m & p <= k holds
ex u, v being Element of the carrier of (Polynom-Ring INT.Ring) st ((Der1 INT.Ring) |^ k) . (f_0 (m,p)) = ((tau j) * u) + ((p !) * v)
proof end;

theorem Th31: :: E_TRANS2:28
for u being Element of the carrier of (Polynom-Ring INT.Ring)
for a, b being Element of INT.Ring holds eval ((a * (~ u)),b) in {a} -Ideal
proof end;

theorem Th32: :: E_TRANS2:29
for p being prime odd Nat
for m being positive Nat
for k, j being Nat st j in Seg m & p <= k holds
eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(In (j,INT.Ring))) in {(In ((p !),INT.Ring))} -Ideal
proof end;

:: WP: Now we apply the polynomial transformation 'F' to f_0.
theorem Th33: :: E_TRANS2:30
for p being prime odd Nat
for m being positive Nat ex u being Element of INT.Ring st ('F' (f_0 (m,p))) . 0 = (((p -' 1) !) * (In (((((- 1) |^ m) * (m !)) |^ p),INT.Ring))) + ((In ((p !),INT.Ring)) * u)
proof end;

theorem Th34: :: E_TRANS2:31
for p being prime odd Nat
for m being positive Nat
for j being Nat st j in Seg m holds
('F' (f_0 (m,p))) . (In (j,F_Real)) in {(In ((p !),INT.Ring))} -Ideal
proof end;

::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::: Formalize "die Gleichumgen (4)"
::: F(i) - e^{i}F(0) = \varepsilon_{i} (i=1,...,n=deg g)
:: delta_1.i corresponds to F(i)
:: delta_2.i corresponds to -e^i*F(0)
:: delta = epsilon_i = delta_1 + delta_2 however slightly modified to
:: multiply g.i where g is deg g = n polynomial, also not yet apply
:: the denominator 1/(p-1)! for faciltating later culuculation
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem Th35: :: E_TRANS2:32
for p being prime odd Nat
for m being positive Nat
for x being Element of F_Real holds (Eval (~ (^ (f_0 (m,p))))) . x = (eval ((~ (^ (Product (x. (m,p))))),x)) * (eval ((~ (^ ((tau 0) |^ (p -' 1)))),x))
proof end;

definition
let m be positive Nat;
let p be prime odd Nat;
let g be non zero Polynomial of INT.Ring;
func delta_1 (m,p,g) -> FinSequence of F_Real means :Def5: :: E_TRANS2:def 6
( len it = m & ( for i being Nat st i in dom it holds
it . i = (g . i) * (('F' (f_0 (m,p))) . (In (i,F_Real))) ) );
existence
ex b1 being FinSequence of F_Real st
( len b1 = m & ( for i being Nat st i in dom b1 holds
b1 . i = (g . i) * (('F' (f_0 (m,p))) . (In (i,F_Real))) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of F_Real st len b1 = m & ( for i being Nat st i in dom b1 holds
b1 . i = (g . i) * (('F' (f_0 (m,p))) . (In (i,F_Real))) ) & len b2 = m & ( for i being Nat st i in dom b2 holds
b2 . i = (g . i) * (('F' (f_0 (m,p))) . (In (i,F_Real))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines delta_1 E_TRANS2:def 6 :
for m being positive Nat
for p being prime odd Nat
for g being non zero Polynomial of INT.Ring
for b4 being FinSequence of F_Real holds
( b4 = delta_1 (m,p,g) iff ( len b4 = m & ( for i being Nat st i in dom b4 holds
b4 . i = (g . i) * (('F' (f_0 (m,p))) . (In (i,F_Real))) ) ) );

definition
let m be positive Nat;
let p be prime odd Nat;
let g be non zero Polynomial of INT.Ring;
let z0 be non zero Element of F_Real;
func delta_2 (m,p,g,z0) -> FinSequence of F_Real means :Def6: :: E_TRANS2:def 7
( len it = m & ( for i being Nat st i in dom it holds
it . i = - ((g . i) * (((power F_Real) . (z0,i)) * (('F' (f_0 (m,p))) . 0))) ) );
existence
ex b1 being FinSequence of F_Real st
( len b1 = m & ( for i being Nat st i in dom b1 holds
b1 . i = - ((g . i) * (((power F_Real) . (z0,i)) * (('F' (f_0 (m,p))) . 0))) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of F_Real st len b1 = m & ( for i being Nat st i in dom b1 holds
b1 . i = - ((g . i) * (((power F_Real) . (z0,i)) * (('F' (f_0 (m,p))) . 0))) ) & len b2 = m & ( for i being Nat st i in dom b2 holds
b2 . i = - ((g . i) * (((power F_Real) . (z0,i)) * (('F' (f_0 (m,p))) . 0))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines delta_2 E_TRANS2:def 7 :
for m being positive Nat
for p being prime odd Nat
for g being non zero Polynomial of INT.Ring
for z0 being non zero Element of F_Real
for b5 being FinSequence of F_Real holds
( b5 = delta_2 (m,p,g,z0) iff ( len b5 = m & ( for i being Nat st i in dom b5 holds
b5 . i = - ((g . i) * (((power F_Real) . (z0,i)) * (('F' (f_0 (m,p))) . 0))) ) ) );

definition
let m be positive Nat;
let p be prime odd Nat;
let g be non zero Polynomial of INT.Ring;
let z0 be non zero Element of F_Real;
func delta (m,p,g,z0) -> FinSequence of F_Real equals :: E_TRANS2:def 8
(delta_1 (m,p,g)) + (delta_2 (m,p,g,z0));
coherence
(delta_1 (m,p,g)) + (delta_2 (m,p,g,z0)) is FinSequence of F_Real
;
end;

:: deftheorem defines delta E_TRANS2:def 8 :
for m being positive Nat
for p being prime odd Nat
for g being non zero Polynomial of INT.Ring
for z0 being non zero Element of F_Real holds delta (m,p,g,z0) = (delta_1 (m,p,g)) + (delta_2 (m,p,g,z0));

Lm12: for p being prime odd Nat
for m being positive Nat
for g being non zero Polynomial of INT.Ring holds delta_1 (m,p,g) is FinSequence of INT.Ring

proof end;

definition
let m be positive Nat;
let p be prime odd Nat;
let g be non zero Polynomial of INT.Ring;
func ^delta (m,p,g) -> FinSequence of INT.Ring equals :: E_TRANS2:def 9
delta_1 (m,p,g);
coherence
delta_1 (m,p,g) is FinSequence of INT.Ring
by Lm12;
end;

:: deftheorem defines ^delta E_TRANS2:def 9 :
for m being positive Nat
for p being prime odd Nat
for g being non zero Polynomial of INT.Ring holds ^delta (m,p,g) = delta_1 (m,p,g);

theorem Th36: :: E_TRANS2:33
for p being prime odd Nat
for m being positive Nat
for g being non zero Polynomial of INT.Ring holds Sum (delta_1 (m,p,g)) in INT.Ring
proof end;

Lm13: for i being Nat holds exp_R . i = (power F_Real) . ((In (number_e,F_Real)),i)
proof end;

theorem Th37: :: E_TRANS2:34
for p being prime odd Nat
for m being positive Nat
for g being non zero Polynomial of INT.Ring st deg g = m holds
for x being non zero Element of F_Real holds Sum (delta_2 (m,p,g,x)) = ((g . 0) * (('F' (f_0 (m,p))) . 0)) - ((Ext_eval (g,x)) * (('F' (f_0 (m,p))) . 0))
proof end;

theorem Th38: :: E_TRANS2:35
for p being prime odd Nat
for m being positive Nat
for g being non zero Polynomial of INT.Ring holds Sum (delta_1 (m,p,g)) in {(In ((p !),INT.Ring))} -Ideal
proof end;

theorem Th39: :: E_TRANS2:36
for p being prime odd Nat
for m being positive Nat
for x being Element of F_Real st 0 < x & x <= m holds
for i being Nat st i in Seg m holds
|.(eval ((~ (^ ((x. (m,p)) /. i))),x)).| <= m |^ p
proof end;

theorem Th40: :: E_TRANS2:37
for p being prime odd Nat
for x being Element of F_Real holds eval ((~ (^ ((tau 0) |^ (p -' 1)))),x) = x |^ (p -' 1)
proof end;

Lm17: for p being prime odd Nat
for m being positive Nat
for x being Element of F_Real st 0 < x & x <= m holds
|.(eval ((~ (^ (Product (x. (m,p))))),x)).| <= m |^ (p * m)

proof end;

Lm20: for p being prime odd Nat
for m being positive Nat
for j being Element of F_Real st 0 < j & j <= m holds
eval ((~ (^ ((tau 0) |^ (p -' 1)))),j) <= m |^ (p -' 1)

proof end;

Lm21: for p being prime odd Nat
for m being positive Nat
for k being Element of F_Real st 0 < k & k <= m holds
|.((Eval (~ (^ (f_0 (m,p))))) . k).| <= m |^ ((p * m) + (p -' 1))

proof end;

Lm24: for p being prime odd Nat
for m being positive Nat
for g being non zero Polynomial of INT.Ring
for z0 being non zero Element of F_Real
for k being Nat st k in Seg m holds
( (delta (m,p,g,z0)) . k = (delta (m,p,g,z0)) /. k & (delta (m,p,g,z0)) . k = ((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k) )

proof end;

Lm25: for p being prime odd Nat
for m being positive Nat
for g being non zero Polynomial of INT.Ring
for z0 being non zero Element of F_Real
for M being Nat st z0 = number_e & ( for i being Nat holds |.(g . i).| <= M ) holds
for k being Nat st k in Seg m holds
|.(((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k)).| <= M * ((z0 to_power m) * (m |^ (p * (m + 1))))

proof end;

Lm27: for p being prime odd Nat
for m being positive Nat
for g being non zero Polynomial of INT.Ring
for z0 being non zero Element of F_Real
for M being Nat st z0 = number_e & ( for i being Nat holds |.(g . i).| <= M ) & ( for k being Nat st k in Seg m holds
|.(((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k)).| <= M * ((z0 to_power m) * (m |^ (p * (m + 1)))) ) holds
Sum (delta (m,p,g,z0)) <= ((m * M) * (z0 to_power m)) * (m |^ (p * (m + 1)))

proof end;

Lm28: for p being prime odd Nat
for m being positive Nat
for g being non zero Polynomial of INT.Ring
for z0 being non zero Element of F_Real
for M being Nat st z0 = number_e & ( for i being Nat holds |.(g . i).| <= M ) & ( for k being Nat st k in Seg m holds
|.(((delta_1 (m,p,g)) . k) + ((delta_2 (m,p,g,z0)) . k)).| <= M * ((z0 to_power m) * (m |^ (p * (m + 1)))) ) holds
- (((m * M) * (z0 to_power m)) * (m |^ (p * (m + 1)))) <= Sum (delta (m,p,g,z0))

proof end;

theorem Th44: :: E_TRANS2:38
for m being positive Nat holds
( (m |^ (m + 1)) rExpSeq is convergent & lim ((m |^ (m + 1)) rExpSeq) = 0 )
proof end;

theorem Th45: :: E_TRANS2:39
for m being positive Nat
for M being non zero Nat
for z0 being non zero Element of F_Real st z0 = number_e holds
ex n1 being Nat st
for n being Nat st n1 <= n holds
|.((((m |^ (m + 1)) |^ n) / (n !)) - 0).| < 1 / (2 * (M * (z0 to_power m)))
proof end;

theorem Th46: :: E_TRANS2:40
for f being INT -valued Polynomial of F_Rat holds f is Polynomial of INT.Ring
proof end;

Lm8a: for n being Nat
for f being Element of the carrier of (Polynom-Ring F_Rat) holds n * f = ((In (n,F_Rat)) | F_Rat) *' (~ f)

proof end;

::$INSERT The following theorem corresponds to the equation (3) in \cite{HURWITZ1}.
theorem LMM: :: E_TRANS2:41
( number_e is algebraic implies ex g being INT -valued Polynomial of F_Rat st
( @ g is irreducible & Ext_eval (g,(In (number_e,F_Real))) = 0 & deg g >= 2 & g . 0 <> 0. F_Rat ) )
proof end;

::$MR The Main Theorem
theorem :: E_TRANS2:42
number_e is transcendental
proof end;