@MISC{E_TRANS2.MIZ,
  AUTHOR = {Watase, Yasushige},
  TITLE = {Formal Proof of Transcendence of the Number $e$. {P}art {II}},
  DAY = {17},
  MONTH = {November},
  YEAR = {2024},
  ADDRESS1 = {Suginami-ku Matsunoki 6, 3-21 Tokyo\\Japan},
  SUMMARY = {This article is continuation of \cite{E_TRANS1.ABS} and we formalize the main part of Hurwitz's 
   proof \cite{HURWITZ:1893} using the Mizar formalism \cite{Mizar-State-2015}. The following is a summary of the formalized proof: \\
   In the first chapter we define a polynomial $f_{0}$ over $\mathbb{Z}$ and observe properties of $f_{0}$. 
   It is defined by $f_{0}(x) = x^{p-1}(x-1)^{p}(x-2)^{p}\cdots (x-m)^{p}$, where $p$ is an 
   odd prime number and $m+1$ is the number of component of the products. 
   The $f_{0}$ is defined as $\mathrm{E\_TRANS2:def 4)}$. 
   The component $(x - j)_{(j = 0,1,...,m)}$ are represented by $\tau(j)$ in the article and obtain:
     $$f_0 = \tau(0)^{p-1} \prod_{j=1}^m{\tau(j)}^p$$ 
    The second chapter is about properties of $f_0$ and $F(f_0)$ where $F$ is introduced 
    \cite{E_TRANS1.ABS}, the transformation $F(f) = f + f^{\prime} + f^{\prime \prime} + \cdots + f^{(deg \ f)} $. \\
    We observe $k^{th}$ differentiation of the $f_0$ and evaluate by a number $j$. The following number-theoretical properties are obtained: 
   \begin{enumerate}
   \item $\prod_{j=1}^m{\tau(j)}^p(0) = (((-1)|^m)*(m!))|^p$ \ $\mathrm{(E\_TRANS2:20)}$,
    \item $f_{0}^{(k)}(0) = 0$ if $0 \leq k \leq p-2$ \ $\mathrm{(E\_TRANS2:21)}$,
    \item $f_{0}^{(k)}(0) = k! (\prod_{j=1}^{m}{\tau(j)})(k-p+1)$ if $p \leq k$ \ $\mathrm{(E\_TRANS2:24)}$,
     \item $f_{0}^{(k)}(j) = 0$ if $k \leq p, 1 \leq j \leq m$ \ $\mathrm{(E\_TRANS2:26})$,
     \item $f_{0}^{(k)} = \tau(j)u + p!v \ (\exists u,v \in \mathbb{Z}[X])$ if $p \leq k, 1 \leq j \leq m$ \ $\mathrm{(E\_TRANS2:30})$,
     \item $f_{0}^{(k)}(j) \in (p!) $ if $p \leq k, 1 \leq j \leq m$ \ $\mathrm{(E\_TRANS2:32})$.
    \end{enumerate}
    We denote $\mathbf{F}$ for $F(f_0)$ for simplicity.
    \begin{enumerate}
    \setcounter{enumi}{6} 
     \item $\mathbf{F}(0) = (p-1)!(((-1)|^m)*(m!))|^p + p!u \ (\exists u \in \mathbb{Z}[X])$ \ $\mathrm{(E\_TRANS2:33})$,
    \item $\mathbf{F}(j) \in (p!)$ if $1 \leq j \leq m$ \ $\mathrm{(E\_TRANS2:34)}$,
    \end{enumerate}\par
    We then obtain an equation system shown as below: 
     where $C_i$ stands for coefficient of the $i^{ith}$ coefficient of $g_0$. 
    This is based on the equation system (4) stated in Hurwitz's proof \cite{HURWITZ:1893}. 
    \begin{align*}
    \left\{
    \begin{array}{llll}
     \frac{1}{(p-1)!}C_0 \mathbf{F}(0)& - & \frac{1}{(p-1)!}C_0 e^{0}\mathbf{F}(0) & = \frac{1}{(p-1)!}C_0 \varepsilon_{0} \\
     \frac{1}{(p-1)!}C_1 \mathbf{F}(1)& - & \frac{1}{(p-1)!}C_1 e^{1}\mathbf{F}(0) & = \frac{1}{(p-1)!}C_1 \varepsilon_{1} \\
      \ \ \ \ \vdots & \ \ \ \ & \ \ \vdots & \ \ \ \ \vdots \\
      \frac{1}{(p-1)!}C_m \mathbf{F}(m)& - & \frac{1}{(p-1)!}C_m e^{m}\mathbf{F}(0) & = \frac{1}{(p-1)!}C_m \varepsilon_{m} 
      \end{array}
      \right.
     \end{align*}
     where each equation is a product of $i^{th}$ coefficient of 
    $g_{0}$ and $\mathbf{F}(i) - e^{x}\mathbf{F}(i) (= -ie^{(i-\vartheta) i }{f_{0}(\vartheta i)})$ 
    which is from the result of the mean value theorem to $e^{x}\mathbf{F}(x)$. 
   In actual coding the sequence $C_m \mathbf{F}(m)$ and ${(p-1)!}C_m e^{m}\mathbf{F}(0)$ 
    are defined as $\mathrm{delta\_1}$ and $\mathrm{delta\_2}$ respectively. \\ 
    We have new equation by adding each term of the equation system vertically:
    $$\frac{1}{(p-1)!}\sum_{i=1}^m C_i \mathbf{F}(i) \ - \ \frac{1}{(p-1)!}\sum_{i=1}^m C_i e^{i}\mathbf{F}(0) = 
   \frac{1}{(p-1)!}\sum_{i=1}^m C_i \varepsilon_{i}$$
    One can verify and formalize that the left hand side is not divided by $p$, 
    because the first term of $p | \frac{1}{(p-1)!}\Sigma C_i \mathbf{F}(i)$ and $p \mathrel{\not|} \ \frac{1}{(p-1)!}\Sigma e^{i}C_i \mathbf{F}(0)$. 
    The right-hand side is a member of $\mathbb{Z}$ and bounded by $1/2$ by choosing 
    sufficiently large $p$, this means it is 0. 
    This contradicts the left-hand side nature. Therefore $e$ is transcendental number.},
  MSC2010 = {11J81,03B35},
  KEYWORDS = {Transcendental Number; Algebraic Number; Hurwitz}}

@BOOK{HardyWright:2008,
    AUTHOR = {Hardy, G.H. and Wright, E.M.},
     TITLE = {An Introduction to the Theory of Numbers},
 PUBLISHER = {Oxford University Press},
  edition = {6th},
      YEAR = 2008}

@BOOK{FUJIWARA:1929,
    AUTHOR = {Fujiwara, M.},
     TITLE = {Algebra vol 2, Japanese},
 PUBLISHER = {Uchida Rokakuho Publishing Co.,LTD},
  edition = {1st},
      YEAR = 1929}

@article{HURWITZ:1893,
author = {Hurwitz, Adolf},
journal = {Mathematische Annalen},,
pages = {220--221},
title = {Beweis der Transcendenz der Zahl e.},
url = {http://eudml.org/doc/157680},
volume = {43},
year = {1893}}

