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

Lm23A: ( dom (exp_R ^) = REAL & exp_R " {0} = {} )

proof end;

definition

func exp_R1 -> Function of REAL,REAL equals :: E_TRANS1:def 1
exp_R ^ ;

coherence
exp_R ^ is Function of REAL,REAL by Lm23A, FUNCT_2:def 1;

end;

:: deftheorem defines exp_R1 E_TRANS1:def 1 :
exp_R1 = exp_R ^ ;

Lm24: ( exp_R ^ is_differentiable_on REAL & exp_R ^ is differentiable Function of REAL,REAL & exp_R is differentiable )

proof end;

registration

cluster exp_R1 -> differentiable for Function of REAL,REAL;

coherence
for b₁ being Function of REAL,REAL st b₁ = exp_R1 holds
b₁ is differentiable by Lm24;

end;

registration

cluster exp_R -> differentiable for Function of REAL,REAL;

coherence
for b₁ being Function of REAL,REAL st b₁ = exp_R holds
b₁ is differentiable by Lm24;

end;

Lm26: exp_R / exp_R = REAL --> 1

proof end;

Lm27: for f being Function of REAL,REAL holds f - f = REAL --> 0

proof end;

Lm28: exp_R1 `| = - exp_R1

proof end;

Lm29: for x0 being positive Real holds (exp_R ^) | [.0,x0.] is continuous

proof end;

Lm31: for x0 being positive Real holds exp_R ^ is_differentiable_on ].0,x0.[

proof end;

Lm35: for f being Function of REAL,REAL holds 0 (#) f = REAL --> 0

proof end;

theorem Lm11: :: E_TRANS1:1

for R being domRing
for n, m being Nat
for b being Element of R holds (n * m) * b = n * (m * b)

proof end;

Lm20: for n being Nat
for z being Real
for e being Element of F_Real st z = e holds
n * z = n * e

proof end;

theorem :: E_TRANS1:2

for F, G being FinSequence of F_Real st len F = len G & ( for i being Nat st i in dom F holds
F . i <= G . i ) holds
Sum F <= Sum G

proof end;

:: Generalization of ZMATRLIN:42 ::: TODO

theorem Th13: :: E_TRANS1:3

for L being comRing
for I being Ideal of L
for F being FinSequence of L st ( for i being Nat st i in dom F holds
F . i in I ) holds
Sum F in I

proof end;

theorem :: E_TRANS1:4

for L being comRing
for a being Element of L
for p being non empty FinSequence of the carrier of L st ( for j being Nat st j in dom p holds
a divides p /. j ) holds
a divides Sum p

proof end;

definition

let k, j be Nat;

func eta (k,j) -> Element of NAT equals :: E_TRANS1:def 2
(k !) / ((k -' j) !);

coherence
(k !) / ((k -' j) !) is Element of NAT

proof end;

end;

:: deftheorem defines eta E_TRANS1:def 2 :
for k, j being Nat holds eta (k,j) = (k !) / ((k -' j) !);

theorem Th17: :: E_TRANS1:5

for k, j being Nat st j <= k holds
(j !) * (k choose j) = eta (k,j)

proof end;

Lm13: for i, n being Nat holds (i + 1) * (eta (((i + 1) + n),n)) = eta ((i + (n + 1)),(n + 1))

proof end;

registration

let R be INT.Ring -extending comRing;
let i be Integer;

reduce In (i,R) to i;

reducibility
In (i,R) = i

proof end;

end;

theorem Lm1: :: E_TRANS1:6

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

proof end;

theorem Lm2: :: E_TRANS1:7

for L being comRing
for n being Nat
for f, g being Element of L st f divides g holds
f divides n * g

proof end;

registration

cluster Relation-like NAT -defined INT -valued the carrier of F_Rat -valued Function-like finite FinSequence-like FinSubsequence-like for FinSequence of the carrier of F_Rat;

existence
ex b₁ being FinSequence of F_Rat st b₁ is INT -valued

proof end;

end;

registration

cluster 0_. F_Rat -> INT -valued ;

coherence
0_. F_Rat is INT -valued by GAUSSINT:def 14;

end;

registration

cluster 1_. F_Rat -> INT -valued ;

coherence
1_. F_Rat is INT -valued

proof end;

end;

registration

cluster non empty Relation-like NAT -defined INT -valued the carrier of F_Rat -valued Function-like total quasi_total finite-Support monic for Element of K10(K11(NAT, the carrier of F_Rat));

existence
ex b₁ being Polynomial of F_Rat st
( b₁ is monic & b₁ is INT -valued )

proof end;

end;

theorem Th3: :: E_TRANS1:8

for R being domRing
for f being Element of the carrier of (Polynom-Ring R) holds rng f = (f .: (Support f)) \/ {(0. R)}

proof end;

Lm9: for f being Element of the carrier of (Polynom-Ring F_Rat) holds TRANQN .: (rng f) is non empty finite Subset of NAT

proof end;

definition

let f be Element of the carrier of (Polynom-Ring F_Rat);

func denomi-set f -> non empty finite Subset of NAT equals :: E_TRANS1:def 3
TRANQN .: (rng f);

coherence
TRANQN .: (rng f) is non empty finite Subset of NAT by Lm9;

end;

:: deftheorem defines denomi-set E_TRANS1:def 3 :
for f being Element of the carrier of (Polynom-Ring F_Rat) holds denomi-set f = TRANQN .: (rng f);

definition

let f be Element of the carrier of (Polynom-Ring F_Rat);

func denomi-seq f -> non empty FinSequence of NAT equals :: E_TRANS1:def 4
canFS (denomi-set f);

coherence
canFS (denomi-set f) is non empty FinSequence of NAT

proof end;

end;

:: deftheorem defines denomi-seq E_TRANS1:def 4 :
for f being Element of the carrier of (Polynom-Ring F_Rat) holds denomi-seq f = canFS (denomi-set f);

Lm10: for f being Element of the carrier of (Polynom-Ring F_Rat)
for i being Nat st i in dom (denomi-seq f) holds
( (denomi-seq f) . i in NAT & (denomi-seq f) . i <> 0 )

proof end;

theorem :: E_TRANS1:9

for f being Element of the carrier of (Polynom-Ring F_Rat) holds not Product (denomi-seq f) is zero

proof end;

theorem :: E_TRANS1:10

for f being Element of the carrier of (Polynom-Ring F_Rat)
for i being Nat holds
( denominator (f . i) in denomi-set f & ex z being Integer st z * (denominator (f . i)) = Product (denomi-seq f) )

proof end;

theorem :: E_TRANS1:11

for K, L being Field
for w being Element of L st K is Subring of L & w is_integral_over K holds
Ann_Poly (w,K) is maximal

proof end;

theorem :: E_TRANS1:12

for f being Element of (Polynom-Ring F_Rat)
for n being non zero Nat st f is irreducible holds
n * f is irreducible

proof end;

theorem :: E_TRANS1:13

for x being Element of F_Real st x is irrational holds
for g being non zero Polynomial of F_Rat st Ext_eval (g,x) = 0 holds
deg g >= 2

proof end;

theorem :: E_TRANS1:14

for g being Polynomial of F_Rat st deg g >= 2 & @ g is irreducible holds
g . 0 <> 0. F_Rat

proof end;

theorem Th12: :: E_TRANS1:15

for L being domRing
for n being non zero Nat
for a being non zero Element of L st Char L = 0 holds
n * a <> 0. L

proof end;

theorem Th15: :: E_TRANS1:16

for R being comRing
for f being Element of the carrier of (Polynom-Ring R)
for i being Nat st i >= 1 & i is_at_least_length_of f & f . (i - 1) <> 0. R holds
len f = i

proof end;

theorem :: E_TRANS1:17

for R being domRing
for f being Element of the carrier of (Polynom-Ring R) st len f > 1 & Char R = 0 holds
len ((Der1 R) . f) = (len f) - 1

proof end;

Lm12: for L being domRing
for y being Element of the carrier of L
for D being Derivation of L holds (D |^ 1) . y = D . y

proof end;

theorem Th18: :: E_TRANS1:18

for L being domRing
for D being Derivation of L
for f being Element of the carrier of L
for j, n being Nat holds (D |^ n) . (j * f) = j * ((D |^ n) . f)

proof end;

theorem Th19: :: E_TRANS1:19

for k being Nat
for f being Element of the carrier of (Polynom-Ring INT.Ring) st ((Der1 INT.Ring) |^ 1) . (f |^ 1) = 1. (Polynom-Ring INT.Ring) holds
for j being Nat st 1 <= j & j <= k holds
((Der1 INT.Ring) |^ j) . (f |^ k) = (eta (k,j)) * (f |^ (k -' j))

proof end;

theorem Th20: :: E_TRANS1:20

for k being Nat
for f being Element of the carrier of (Polynom-Ring INT.Ring) st ((Der1 INT.Ring) |^ 1) . (f |^ 1) = 1. (Polynom-Ring INT.Ring) holds
((Der1 INT.Ring) |^ k) . (f |^ k) = (k !) * (1. (Polynom-Ring INT.Ring))

proof end;

theorem :: E_TRANS1:21

for k, j being Nat st j > k holds
for f being Element of the carrier of (Polynom-Ring INT.Ring) st ((Der1 INT.Ring) |^ 1) . (f |^ 1) = 1. (Polynom-Ring INT.Ring) holds
((Der1 INT.Ring) |^ j) . (f |^ k) = 0. (Polynom-Ring INT.Ring)

proof end;

theorem Th22: :: E_TRANS1:22

for R being domRing
for f being Element of the carrier of (Polynom-Ring R)
for k, i being Nat holds (((Der1 R) |^ k) . f) . i = (eta ((i + k),k)) * (f . (i + k))

proof end;

theorem Th23: :: E_TRANS1:23

for R being domRing
for h being Function of R,R
for s being FinSequence of the carrier of R st h is additive holds
h . (Sum s) = Sum (h * s)

proof end;

Lm14: for R being comRing
for S being RingExtension of R
for f being Element of the carrier of (Polynom-Ring R) holds f is Element of the carrier of (Polynom-Ring S)

proof end;

theorem Th24: :: E_TRANS1:24

for R being domRing
for f being Element of the carrier of (Polynom-Ring R)
for j being Nat st len f > j & Char R = 0 holds
len (((Der1 R) |^ j) . f) = (len f) - j

proof end;

definition

let p be Element of the carrier of (Polynom-Ring INT.Ring);

func ^ p -> Element of the carrier of (Polynom-Ring F_Real) equals :: E_TRANS1:def 5
p;

coherence
p is Element of the carrier of (Polynom-Ring F_Real) by Lm14;

end;

:: deftheorem defines ^ E_TRANS1:def 5 :
for p being Element of the carrier of (Polynom-Ring INT.Ring) holds ^ p = p;

definition

let F be FinSequence of the carrier of (Polynom-Ring INT.Ring);

func ^ F -> FinSequence of the carrier of (Polynom-Ring F_Real) means :Def7: :: E_TRANS1:def 6
( dom it = dom F & ( for i being Nat st i in dom F holds
it . i = ^ (F /. i) ) );

existence
ex b₁ being FinSequence of the carrier of (Polynom-Ring F_Real) st
( dom b₁ = dom F & ( for i being Nat st i in dom F holds
b₁ . i = ^ (F /. i) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of the carrier of (Polynom-Ring F_Real) st dom b₁ = dom F & ( for i being Nat st i in dom F holds
b₁ . i = ^ (F /. i) ) & dom b₂ = dom F & ( for i being Nat st i in dom F holds
b₂ . i = ^ (F /. i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines ^ E_TRANS1:def 6 :
for F being FinSequence of the carrier of (Polynom-Ring INT.Ring)
for b₂ being FinSequence of the carrier of (Polynom-Ring F_Real) holds
( b₂ = ^ F iff ( dom b₂ = dom F & ( for i being Nat st i in dom F holds
b₂ . i = ^ (F /. i) ) ) );

definition

let L be comRing;
let F be FinSequence of the carrier of (Polynom-Ring L);
let x be Element of L;

func eval (F,x) -> FinSequence of the carrier of L means :Def8: :: E_TRANS1:def 7
( dom it = dom F & ( for i being Nat st i in dom F holds
it . i = eval ((~ (F /. i)),x) ) );

existence
ex b₁ being FinSequence of the carrier of L st
( dom b₁ = dom F & ( for i being Nat st i in dom F holds
b₁ . i = eval ((~ (F /. i)),x) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of the carrier of L st dom b₁ = dom F & ( for i being Nat st i in dom F holds
b₁ . i = eval ((~ (F /. i)),x) ) & dom b₂ = dom F & ( for i being Nat st i in dom F holds
b₂ . i = eval ((~ (F /. i)),x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines eval E_TRANS1:def 7 :
for L being comRing
for F being FinSequence of the carrier of (Polynom-Ring L)
for x being Element of L
for b₄ being FinSequence of the carrier of L holds
( b₄ = eval (F,x) iff ( dom b₄ = dom F & ( for i being Nat st i in dom F holds
b₄ . i = eval ((~ (F /. i)),x) ) ) );

Lm15: for L being comRing
for f, g being Element of (Polynom-Ring L)
for x being Element of L holds eval ((~ (f + g)),x) = (eval ((~ f),x)) + (eval ((~ g),x))

proof end;

theorem Th25: :: E_TRANS1:25

for N0 being Nat
for L being comRing
for F being FinSequence of the carrier of (Polynom-Ring L)
for x being Element of L st len F = N0 + 1 holds
eval (F,x) = (eval ((F | N0),x)) ^ <*(eval ((~ (F /. (len F))),x))*>

proof end;

theorem Th26: :: E_TRANS1:26

for L being comRing
for F being FinSequence of the carrier of (Polynom-Ring L)
for x being Element of L holds eval ((~ (Sum F)),x) = Sum (eval (F,x))

proof end;

theorem Th27: :: E_TRANS1:27

for p, q being Element of the carrier of (Polynom-Ring INT.Ring) holds
( ^ (p + q) = (^ p) + (^ q) & ^ (p * q) = (^ p) * (^ q) )

proof end;

definition

let f be Element of the carrier of (Polynom-Ring INT.Ring);

func 'G' f -> FinSequence of the carrier of (Polynom-Ring INT.Ring) means :Def9: :: E_TRANS1:def 8
( len it = len f & ( for i being Nat st i in dom it holds
it . i = ((Der1 INT.Ring) |^ (i -' 1)) . f ) );

existence
ex b₁ being FinSequence of the carrier of (Polynom-Ring INT.Ring) st
( len b₁ = len f & ( for i being Nat st i in dom b₁ holds
b₁ . i = ((Der1 INT.Ring) |^ (i -' 1)) . f ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of the carrier of (Polynom-Ring INT.Ring) st len b₁ = len f & ( for i being Nat st i in dom b₁ holds
b₁ . i = ((Der1 INT.Ring) |^ (i -' 1)) . f ) & len b₂ = len f & ( for i being Nat st i in dom b₂ holds
b₂ . i = ((Der1 INT.Ring) |^ (i -' 1)) . f ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines 'G' E_TRANS1:def 8 :
for f being Element of the carrier of (Polynom-Ring INT.Ring)
for b₂ being FinSequence of the carrier of (Polynom-Ring INT.Ring) holds
( b₂ = 'G' f iff ( len b₂ = len f & ( for i being Nat st i in dom b₂ holds
b₂ . i = ((Der1 INT.Ring) |^ (i -' 1)) . f ) ) );

theorem Th28: :: E_TRANS1:28

for F being FinSequence of the carrier of (Polynom-Ring INT.Ring)
for x being Element of INT.Ring
for x1 being Element of F_Real st x = x1 holds
eval ((^ F),x1) = eval (F,x)

proof end;

Lm16: for k being Nat
for F being FinSequence of the carrier of (Polynom-Ring INT.Ring) st len F = k + 1 holds
^ (F | k) = (^ F) | k

proof end;

theorem Th29: :: E_TRANS1:29

for F being FinSequence of the carrier of (Polynom-Ring INT.Ring) holds Sum (^ F) = ^ (Sum F)

proof end;

theorem :: E_TRANS1:30

for x0 being Element of INT.Ring
for x being Element of F_Real
for F being FinSequence of the carrier of (Polynom-Ring INT.Ring) st x = x0 holds
(Eval (~ (^ (Sum F)))) . x = Sum (eval (F,x0))

proof end;

Lm17: for f being Element of the carrier of (Polynom-Ring INT.Ring) st len f > 0 holds
('G' f) . (len f) is constant Element of the carrier of (Polynom-Ring INT.Ring)

proof end;

Lm18: for f being Element of the carrier of (Polynom-Ring INT.Ring) st len f > 0 holds
Del (('G' f),1) = ((Der1 INT.Ring) * ('G' f)) | ((len f) -' 1)

proof end;

Lm19: for f being Element of the carrier of (Polynom-Ring INT.Ring) st len f > 0 holds
( (Sum ('G' f)) - f = (Der1 INT.Ring) . (Sum ('G' f)) & (Sum ('G' f)) - f = (Der1 INT.Ring) . (Sum ('G' f)) & Sum ('G' f) = ((Der1 INT.Ring) . (Sum ('G' f))) + f )

proof end;

::$INSERT The Definition below corresponds to the Transformation (1) in \cite{HURWITZ:1893}

definition

let f be Element of the carrier of (Polynom-Ring INT.Ring);

func 'F' f -> Function of REAL,REAL equals :: E_TRANS1:def 9
Eval (~ (^ (Sum ('G' f))));

coherence
Eval (~ (^ (Sum ('G' f)))) is Function of REAL,REAL ;

end;

:: deftheorem defines 'F' E_TRANS1:def 9 :
for f being Element of the carrier of (Polynom-Ring INT.Ring) holds 'F' f = Eval (~ (^ (Sum ('G' f))));

Lm21: for q being Element of the carrier of (Polynom-Ring F_Real) holds (Der1 F_Real) . (@ (LM (~ q))) = (0_. F_Real) +* (((len (~ q)) -' 2),(((~ q) . ((len (~ q)) -' 1)) * ((len (~ q)) -' 1)))

proof end;

Lm22: for p being Element of the carrier of (Polynom-Ring F_Real) holds (Eval (LM (~ p))) `| = Eval (~ ((Der1 F_Real) . (@ (LM (~ p)))))

proof end;

theorem Th31: :: E_TRANS1:31

for p being Element of the carrier of (Polynom-Ring F_Real) holds (Eval (~ p)) `| = Eval (~ ((Der1 F_Real) . p))

proof end;

Lm23: for f being Element of the carrier of (Polynom-Ring INT.Ring) holds
( dom ('F' f) = REAL & dom ((exp_R ^) (#) ('F' f)) = REAL )

proof end;

definition

let f be Element of the carrier of (Polynom-Ring INT.Ring);

func Phi f -> Function of REAL,REAL equals :: E_TRANS1:def 10
exp_R1 (#) ('F' f);

coherence
exp_R1 (#) ('F' f) is Function of REAL,REAL ;

end;

:: deftheorem defines Phi E_TRANS1:def 10 :
for f being Element of the carrier of (Polynom-Ring INT.Ring) holds Phi f = exp_R1 (#) ('F' f);

Lm25: for f being Element of the carrier of (Polynom-Ring INT.Ring) holds 'F' f is_differentiable_on REAL

proof end;

registration

let f be Element of the carrier of (Polynom-Ring INT.Ring);

cluster 'F' f -> differentiable for Function of REAL,REAL;

coherence
for b₁ being Function of REAL,REAL st b₁ = 'F' f holds
b₁ is differentiable ;

end;

Lm30: for x0 being positive Real
for f being Element of the carrier of (Polynom-Ring INT.Ring) holds ('F' f) | [.0,x0.] is continuous

proof end;

theorem Th32: :: E_TRANS1:32

for x0 being positive Real
for f being Element of the carrier of (Polynom-Ring INT.Ring) holds (exp_R1 (#) ('F' f)) | [.0,x0.] is continuous

proof end;

Lm32: for x0 being positive Real
for f being Element of the carrier of (Polynom-Ring INT.Ring) holds 'F' f is_differentiable_on ].0,x0.[

proof end;

theorem Th33: :: E_TRANS1:33

for x0 being positive Real
for f being Element of the carrier of (Polynom-Ring INT.Ring) holds exp_R1 (#) ('F' f) is_differentiable_on ].0,x0.[

proof end;

Lm33: for x0 being positive Real
for f being Element of the carrier of (Polynom-Ring INT.Ring) ex s being Real st
( 0 < s & s < 1 & (exp_R1 (#) ('F' f)) . x0 = ((exp_R1 (#) ('F' f)) . 0) + (x0 * (diff ((exp_R1 (#) ('F' f)),(s * x0)))) )

proof end;

Lm34: for f being Element of the carrier of (Polynom-Ring INT.Ring) st len f > 0 holds
('F' f) - (Eval (~ (^ f))) = ('F' f) `|

proof end;

Lm36: for f being Element of the carrier of (Polynom-Ring INT.Ring) st len f > 0 holds
(exp_R1 (#) ('F' f)) `| REAL = - (exp_R1 (#) (Eval (~ (^ f))))

proof end;

:: The following theorem corresponds to the equation (2) in \cite{HURWITZ:1893}.

theorem :: E_TRANS1:34

for f being Element of the carrier of (Polynom-Ring INT.Ring)
for x0 being positive Real st len f > 0 holds
ex s being Real st
( 0 < s & s < 1 & (('F' f) . x0) - ((exp_R . x0) * (('F' f) . 0)) = - ((x0 * (exp_R . (x0 * (1 - s)))) * ((Eval (~ (^ f))) . (s * x0))) )

proof end;

::: Prepare calculation of the following Function
::: f_0(p,x) = \frac{1}{(p-1)!}x^{p-1}(1-x)^{p}(2-x)^{p}\cdots (n-x)^{p}
:: Ring Extended version of FIELD_13:13.

theorem Th37: :: E_TRANS1:35

for F being domRing
for E being RingExtension of F
for p being Polynomial of F
for q being Polynomial of E
for a being Element of F
for b being Element of E st p = q & a = b holds
a * p = b * q

proof end;

:: Ring Extension version of REALALG3:16.

theorem :: E_TRANS1:36

for F being domRing
for E being domRingExtension of F
for p being Polynomial of F
for a being Element of F
for x, b being Element of E st b = a holds
Ext_eval ((a * p),x) = b * (Ext_eval (p,x))

proof end;

Lm37: for L being non degenerated comRing
for f, g being Element of (Polynom-Ring L)
for x being Element of L holds eval ((~ (f * g)),x) = (eval ((~ f),x)) * (eval ((~ g),x))

proof end;

theorem Th39: :: E_TRANS1:37

for L being non degenerated comRing
for F being non empty FinSequence of the carrier of (Polynom-Ring L)
for x being Element of L holds eval ((~ (Product F)),x) = Product (eval (F,x))

proof end;

Lm38: for F being non empty FinSequence of the carrier of (Polynom-Ring INT.Ring) holds Product (^ F) = ^ (Product F)

proof end;

theorem :: E_TRANS1:38

for F being non empty FinSequence of the carrier of (Polynom-Ring INT.Ring)
for x being Element of F_Real holds eval ((~ (^ (Product F))),x) = Product (eval ((^ F),x))

proof end;