# Metamath Proof Explorer

## Theorem etransc

Description: _e is transcendental. Section *5 of Juillerat p. 11 can be used as a reference for this proof. (Contributed by Glauco Siliprandi, 5-Apr-2020) (Proof shortened by AV, 28-Sep-2020)

Ref Expression
Assertion etransc ${⊢}\mathrm{e}\in \left(ℂ\setminus 𝔸\right)$

### Proof

Step Hyp Ref Expression
1 1red ${⊢}\left({k}\in ℤ\wedge {k}\ne 0\right)\to 1\in ℝ$
2 nn0abscl ${⊢}{k}\in ℤ\to \left|{k}\right|\in {ℕ}_{0}$
3 2 nn0red ${⊢}{k}\in ℤ\to \left|{k}\right|\in ℝ$
4 3 adantr ${⊢}\left({k}\in ℤ\wedge {k}\ne 0\right)\to \left|{k}\right|\in ℝ$
5 nnabscl ${⊢}\left({k}\in ℤ\wedge {k}\ne 0\right)\to \left|{k}\right|\in ℕ$
6 5 nnge1d ${⊢}\left({k}\in ℤ\wedge {k}\ne 0\right)\to 1\le \left|{k}\right|$
7 1 4 6 lensymd ${⊢}\left({k}\in ℤ\wedge {k}\ne 0\right)\to ¬\left|{k}\right|<1$
8 nan ${⊢}\left({k}\in ℤ\to ¬\left({k}\ne 0\wedge \left|{k}\right|<1\right)\right)↔\left(\left({k}\in ℤ\wedge {k}\ne 0\right)\to ¬\left|{k}\right|<1\right)$
9 7 8 mpbir ${⊢}{k}\in ℤ\to ¬\left({k}\ne 0\wedge \left|{k}\right|<1\right)$
10 9 nrex ${⊢}¬\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}\left({k}\ne 0\wedge \left|{k}\right|<1\right)$
11 ere ${⊢}\mathrm{e}\in ℝ$
12 11 recni ${⊢}\mathrm{e}\in ℂ$
13 neldif ${⊢}\left(\mathrm{e}\in ℂ\wedge ¬\mathrm{e}\in \left(ℂ\setminus 𝔸\right)\right)\to \mathrm{e}\in 𝔸$
14 12 13 mpan ${⊢}¬\mathrm{e}\in \left(ℂ\setminus 𝔸\right)\to \mathrm{e}\in 𝔸$
15 ene0 ${⊢}\mathrm{e}\ne 0$
16 elsng ${⊢}\mathrm{e}\in ℂ\to \left(\mathrm{e}\in \left\{0\right\}↔\mathrm{e}=0\right)$
17 12 16 ax-mp ${⊢}\mathrm{e}\in \left\{0\right\}↔\mathrm{e}=0$
18 15 17 nemtbir ${⊢}¬\mathrm{e}\in \left\{0\right\}$
19 18 a1i ${⊢}¬\mathrm{e}\in \left(ℂ\setminus 𝔸\right)\to ¬\mathrm{e}\in \left\{0\right\}$
20 14 19 eldifd ${⊢}¬\mathrm{e}\in \left(ℂ\setminus 𝔸\right)\to \mathrm{e}\in \left(𝔸\setminus \left\{0\right\}\right)$
21 elaa2 ${⊢}\mathrm{e}\in \left(𝔸\setminus \left\{0\right\}\right)↔\left(\mathrm{e}\in ℂ\wedge \exists {q}\in \mathrm{Poly}\left(ℤ\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{coeff}\left({q}\right)\left(0\right)\ne 0\wedge {q}\left(\mathrm{e}\right)=0\right)\right)$
22 20 21 sylib ${⊢}¬\mathrm{e}\in \left(ℂ\setminus 𝔸\right)\to \left(\mathrm{e}\in ℂ\wedge \exists {q}\in \mathrm{Poly}\left(ℤ\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{coeff}\left({q}\right)\left(0\right)\ne 0\wedge {q}\left(\mathrm{e}\right)=0\right)\right)$
23 22 simprd ${⊢}¬\mathrm{e}\in \left(ℂ\setminus 𝔸\right)\to \exists {q}\in \mathrm{Poly}\left(ℤ\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{coeff}\left({q}\right)\left(0\right)\ne 0\wedge {q}\left(\mathrm{e}\right)=0\right)$
24 simpl ${⊢}\left({q}\in \mathrm{Poly}\left(ℤ\right)\wedge \mathrm{coeff}\left({q}\right)\left(0\right)\ne 0\right)\to {q}\in \mathrm{Poly}\left(ℤ\right)$
25 0nn0 ${⊢}0\in {ℕ}_{0}$
26 n0p ${⊢}\left({q}\in \mathrm{Poly}\left(ℤ\right)\wedge 0\in {ℕ}_{0}\wedge \mathrm{coeff}\left({q}\right)\left(0\right)\ne 0\right)\to {q}\ne {0}_{𝑝}$
27 25 26 mp3an2 ${⊢}\left({q}\in \mathrm{Poly}\left(ℤ\right)\wedge \mathrm{coeff}\left({q}\right)\left(0\right)\ne 0\right)\to {q}\ne {0}_{𝑝}$
28 nelsn ${⊢}{q}\ne {0}_{𝑝}\to ¬{q}\in \left\{{0}_{𝑝}\right\}$
29 27 28 syl ${⊢}\left({q}\in \mathrm{Poly}\left(ℤ\right)\wedge \mathrm{coeff}\left({q}\right)\left(0\right)\ne 0\right)\to ¬{q}\in \left\{{0}_{𝑝}\right\}$
30 24 29 eldifd ${⊢}\left({q}\in \mathrm{Poly}\left(ℤ\right)\wedge \mathrm{coeff}\left({q}\right)\left(0\right)\ne 0\right)\to {q}\in \left(\mathrm{Poly}\left(ℤ\right)\setminus \left\{{0}_{𝑝}\right\}\right)$
31 30 adantrr ${⊢}\left({q}\in \mathrm{Poly}\left(ℤ\right)\wedge \left(\mathrm{coeff}\left({q}\right)\left(0\right)\ne 0\wedge {q}\left(\mathrm{e}\right)=0\right)\right)\to {q}\in \left(\mathrm{Poly}\left(ℤ\right)\setminus \left\{{0}_{𝑝}\right\}\right)$
32 simprr ${⊢}\left({q}\in \mathrm{Poly}\left(ℤ\right)\wedge \left(\mathrm{coeff}\left({q}\right)\left(0\right)\ne 0\wedge {q}\left(\mathrm{e}\right)=0\right)\right)\to {q}\left(\mathrm{e}\right)=0$
33 eqid ${⊢}\mathrm{coeff}\left({q}\right)=\mathrm{coeff}\left({q}\right)$
34 simprl ${⊢}\left({q}\in \mathrm{Poly}\left(ℤ\right)\wedge \left(\mathrm{coeff}\left({q}\right)\left(0\right)\ne 0\wedge {q}\left(\mathrm{e}\right)=0\right)\right)\to \mathrm{coeff}\left({q}\right)\left(0\right)\ne 0$
35 eqid ${⊢}\mathrm{deg}\left({q}\right)=\mathrm{deg}\left({q}\right)$
36 eqid ${⊢}\sum _{{l}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}=\sum _{{l}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}$
37 eqid ${⊢}\left({n}\in {ℕ}_{0}⟼\sum _{{l}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{n}}}{{n}!}\right)\right)=\left({n}\in {ℕ}_{0}⟼\sum _{{l}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{n}}}{{n}!}\right)\right)$
38 fveq2 ${⊢}{h}={l}\to \mathrm{coeff}\left({q}\right)\left({h}\right)=\mathrm{coeff}\left({q}\right)\left({l}\right)$
39 oveq2 ${⊢}{h}={l}\to {\mathrm{e}}^{{h}}={\mathrm{e}}^{{l}}$
40 38 39 oveq12d ${⊢}{h}={l}\to \mathrm{coeff}\left({q}\right)\left({h}\right){\mathrm{e}}^{{h}}=\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}$
41 40 fveq2d ${⊢}{h}={l}\to \left|\mathrm{coeff}\left({q}\right)\left({h}\right){\mathrm{e}}^{{h}}\right|=\left|\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}\right|$
42 41 oveq1d ${⊢}{h}={l}\to \left|\mathrm{coeff}\left({q}\right)\left({h}\right){\mathrm{e}}^{{h}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}=\left|\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}$
43 42 cbvsumv ${⊢}\sum _{{h}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({h}\right){\mathrm{e}}^{{h}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}=\sum _{{l}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}$
44 43 a1i ${⊢}{m}={n}\to \sum _{{h}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({h}\right){\mathrm{e}}^{{h}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}=\sum _{{l}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}$
45 oveq2 ${⊢}{m}={n}\to {\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{m}}={\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{n}}$
46 fveq2 ${⊢}{m}={n}\to {m}!={n}!$
47 45 46 oveq12d ${⊢}{m}={n}\to \frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{m}}}{{m}!}=\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{n}}}{{n}!}$
48 44 47 oveq12d ${⊢}{m}={n}\to \sum _{{h}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({h}\right){\mathrm{e}}^{{h}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{m}}}{{m}!}\right)=\sum _{{l}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{n}}}{{n}!}\right)$
49 48 cbvmptv ${⊢}\left({m}\in {ℕ}_{0}⟼\sum _{{h}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({h}\right){\mathrm{e}}^{{h}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{m}}}{{m}!}\right)\right)=\left({n}\in {ℕ}_{0}⟼\sum _{{l}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{n}}}{{n}!}\right)\right)$
50 49 a1i ${⊢}{m}={n}\to \left({m}\in {ℕ}_{0}⟼\sum _{{h}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({h}\right){\mathrm{e}}^{{h}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{m}}}{{m}!}\right)\right)=\left({n}\in {ℕ}_{0}⟼\sum _{{l}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{n}}}{{n}!}\right)\right)$
51 id ${⊢}{m}={n}\to {m}={n}$
52 50 51 fveq12d ${⊢}{m}={n}\to \left({m}\in {ℕ}_{0}⟼\sum _{{h}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({h}\right){\mathrm{e}}^{{h}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{m}}}{{m}!}\right)\right)\left({m}\right)=\left({n}\in {ℕ}_{0}⟼\sum _{{l}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{n}}}{{n}!}\right)\right)\left({n}\right)$
53 52 fveq2d ${⊢}{m}={n}\to \left|\left({m}\in {ℕ}_{0}⟼\sum _{{h}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({h}\right){\mathrm{e}}^{{h}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{m}}}{{m}!}\right)\right)\left({m}\right)\right|=\left|\left({n}\in {ℕ}_{0}⟼\sum _{{l}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{n}}}{{n}!}\right)\right)\left({n}\right)\right|$
54 53 breq1d ${⊢}{m}={n}\to \left(\left|\left({m}\in {ℕ}_{0}⟼\sum _{{h}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({h}\right){\mathrm{e}}^{{h}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{m}}}{{m}!}\right)\right)\left({m}\right)\right|<1↔\left|\left({n}\in {ℕ}_{0}⟼\sum _{{l}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{n}}}{{n}!}\right)\right)\left({n}\right)\right|<1\right)$
55 54 cbvralvw ${⊢}\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|\left({m}\in {ℕ}_{0}⟼\sum _{{h}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({h}\right){\mathrm{e}}^{{h}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{m}}}{{m}!}\right)\right)\left({m}\right)\right|<1↔\forall {n}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|\left({n}\in {ℕ}_{0}⟼\sum _{{l}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{n}}}{{n}!}\right)\right)\left({n}\right)\right|<1$
56 fveq2 ${⊢}{j}={i}\to {ℤ}_{\ge {j}}={ℤ}_{\ge {i}}$
57 56 raleqdv ${⊢}{j}={i}\to \left(\forall {n}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|\left({n}\in {ℕ}_{0}⟼\sum _{{l}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{n}}}{{n}!}\right)\right)\left({n}\right)\right|<1↔\forall {n}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left|\left({n}\in {ℕ}_{0}⟼\sum _{{l}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{n}}}{{n}!}\right)\right)\left({n}\right)\right|<1\right)$
58 55 57 syl5bb ${⊢}{j}={i}\to \left(\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|\left({m}\in {ℕ}_{0}⟼\sum _{{h}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({h}\right){\mathrm{e}}^{{h}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{m}}}{{m}!}\right)\right)\left({m}\right)\right|<1↔\forall {n}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left|\left({n}\in {ℕ}_{0}⟼\sum _{{l}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{n}}}{{n}!}\right)\right)\left({n}\right)\right|<1\right)$
59 58 cbvrabv ${⊢}\left\{{j}\in {ℕ}_{0}|\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|\left({m}\in {ℕ}_{0}⟼\sum _{{h}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({h}\right){\mathrm{e}}^{{h}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{m}}}{{m}!}\right)\right)\left({m}\right)\right|<1\right\}=\left\{{i}\in {ℕ}_{0}|\forall {n}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left|\left({n}\in {ℕ}_{0}⟼\sum _{{l}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{n}}}{{n}!}\right)\right)\left({n}\right)\right|<1\right\}$
60 59 infeq1i ${⊢}sup\left(\left\{{j}\in {ℕ}_{0}|\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|\left({m}\in {ℕ}_{0}⟼\sum _{{h}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({h}\right){\mathrm{e}}^{{h}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{m}}}{{m}!}\right)\right)\left({m}\right)\right|<1\right\},ℝ,<\right)=sup\left(\left\{{i}\in {ℕ}_{0}|\forall {n}\in {ℤ}_{\ge {i}}\phantom{\rule{.4em}{0ex}}\left|\left({n}\in {ℕ}_{0}⟼\sum _{{l}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({l}\right){\mathrm{e}}^{{l}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{n}}}{{n}!}\right)\right)\left({n}\right)\right|<1\right\},ℝ,<\right)$
61 eqid ${⊢}sup\left(\left\{\left|\mathrm{coeff}\left({q}\right)\left(0\right)\right|,\mathrm{deg}\left({q}\right)!,sup\left(\left\{{j}\in {ℕ}_{0}|\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|\left({m}\in {ℕ}_{0}⟼\sum _{{h}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({h}\right){\mathrm{e}}^{{h}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{m}}}{{m}!}\right)\right)\left({m}\right)\right|<1\right\},ℝ,<\right)\right\},{ℝ}^{*},<\right)=sup\left(\left\{\left|\mathrm{coeff}\left({q}\right)\left(0\right)\right|,\mathrm{deg}\left({q}\right)!,sup\left(\left\{{j}\in {ℕ}_{0}|\forall {m}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left|\left({m}\in {ℕ}_{0}⟼\sum _{{h}=0}^{\mathrm{deg}\left({q}\right)}\left|\mathrm{coeff}\left({q}\right)\left({h}\right){\mathrm{e}}^{{h}}\right|\mathrm{deg}\left({q}\right){\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\left(\frac{{\left({\mathrm{deg}\left({q}\right)}^{\mathrm{deg}\left({q}\right)+1}\right)}^{{m}}}{{m}!}\right)\right)\left({m}\right)\right|<1\right\},ℝ,<\right)\right\},{ℝ}^{*},<\right)$
62 31 32 33 34 35 36 37 60 61 etransclem48 ${⊢}\left({q}\in \mathrm{Poly}\left(ℤ\right)\wedge \left(\mathrm{coeff}\left({q}\right)\left(0\right)\ne 0\wedge {q}\left(\mathrm{e}\right)=0\right)\right)\to \exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}\left({k}\ne 0\wedge \left|{k}\right|<1\right)$
63 62 rexlimiva ${⊢}\exists {q}\in \mathrm{Poly}\left(ℤ\right)\phantom{\rule{.4em}{0ex}}\left(\mathrm{coeff}\left({q}\right)\left(0\right)\ne 0\wedge {q}\left(\mathrm{e}\right)=0\right)\to \exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}\left({k}\ne 0\wedge \left|{k}\right|<1\right)$
64 23 63 syl ${⊢}¬\mathrm{e}\in \left(ℂ\setminus 𝔸\right)\to \exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}\left({k}\ne 0\wedge \left|{k}\right|<1\right)$
65 10 64 mt3 ${⊢}\mathrm{e}\in \left(ℂ\setminus 𝔸\right)$