# 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 e ∈ ( ℂ ∖ 𝔸 )

### Proof

Step Hyp Ref Expression
1 1red ( ( 𝑘 ∈ ℤ ∧ 𝑘 ≠ 0 ) → 1 ∈ ℝ )
2 nn0abscl ( 𝑘 ∈ ℤ → ( abs ‘ 𝑘 ) ∈ ℕ0 )
3 2 nn0red ( 𝑘 ∈ ℤ → ( abs ‘ 𝑘 ) ∈ ℝ )
4 3 adantr ( ( 𝑘 ∈ ℤ ∧ 𝑘 ≠ 0 ) → ( abs ‘ 𝑘 ) ∈ ℝ )
5 nnabscl ( ( 𝑘 ∈ ℤ ∧ 𝑘 ≠ 0 ) → ( abs ‘ 𝑘 ) ∈ ℕ )
6 5 nnge1d ( ( 𝑘 ∈ ℤ ∧ 𝑘 ≠ 0 ) → 1 ≤ ( abs ‘ 𝑘 ) )
7 1 4 6 lensymd ( ( 𝑘 ∈ ℤ ∧ 𝑘 ≠ 0 ) → ¬ ( abs ‘ 𝑘 ) < 1 )
8 nan ( ( 𝑘 ∈ ℤ → ¬ ( 𝑘 ≠ 0 ∧ ( abs ‘ 𝑘 ) < 1 ) ) ↔ ( ( 𝑘 ∈ ℤ ∧ 𝑘 ≠ 0 ) → ¬ ( abs ‘ 𝑘 ) < 1 ) )
9 7 8 mpbir ( 𝑘 ∈ ℤ → ¬ ( 𝑘 ≠ 0 ∧ ( abs ‘ 𝑘 ) < 1 ) )
10 9 nrex ¬ ∃ 𝑘 ∈ ℤ ( 𝑘 ≠ 0 ∧ ( abs ‘ 𝑘 ) < 1 )
11 ere e ∈ ℝ
12 11 recni e ∈ ℂ
13 neldif ( ( e ∈ ℂ ∧ ¬ e ∈ ( ℂ ∖ 𝔸 ) ) → e ∈ 𝔸 )
14 12 13 mpan ( ¬ e ∈ ( ℂ ∖ 𝔸 ) → e ∈ 𝔸 )
15 ene0 e ≠ 0
16 elsng ( e ∈ ℂ → ( e ∈ { 0 } ↔ e = 0 ) )
17 12 16 ax-mp ( e ∈ { 0 } ↔ e = 0 )
18 15 17 nemtbir ¬ e ∈ { 0 }
19 18 a1i ( ¬ e ∈ ( ℂ ∖ 𝔸 ) → ¬ e ∈ { 0 } )
20 14 19 eldifd ( ¬ e ∈ ( ℂ ∖ 𝔸 ) → e ∈ ( 𝔸 ∖ { 0 } ) )
21 elaa2 ( e ∈ ( 𝔸 ∖ { 0 } ) ↔ ( e ∈ ℂ ∧ ∃ 𝑞 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑞 ) ‘ 0 ) ≠ 0 ∧ ( 𝑞 ‘ e ) = 0 ) ) )
22 20 21 sylib ( ¬ e ∈ ( ℂ ∖ 𝔸 ) → ( e ∈ ℂ ∧ ∃ 𝑞 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑞 ) ‘ 0 ) ≠ 0 ∧ ( 𝑞 ‘ e ) = 0 ) ) )
23 22 simprd ( ¬ e ∈ ( ℂ ∖ 𝔸 ) → ∃ 𝑞 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑞 ) ‘ 0 ) ≠ 0 ∧ ( 𝑞 ‘ e ) = 0 ) )
24 simpl ( ( 𝑞 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑞 ) ‘ 0 ) ≠ 0 ) → 𝑞 ∈ ( Poly ‘ ℤ ) )
25 0nn0 0 ∈ ℕ0
26 n0p ( ( 𝑞 ∈ ( Poly ‘ ℤ ) ∧ 0 ∈ ℕ0 ∧ ( ( coeff ‘ 𝑞 ) ‘ 0 ) ≠ 0 ) → 𝑞 ≠ 0𝑝 )
27 25 26 mp3an2 ( ( 𝑞 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑞 ) ‘ 0 ) ≠ 0 ) → 𝑞 ≠ 0𝑝 )
28 nelsn ( 𝑞 ≠ 0𝑝 → ¬ 𝑞 ∈ { 0𝑝 } )
29 27 28 syl ( ( 𝑞 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑞 ) ‘ 0 ) ≠ 0 ) → ¬ 𝑞 ∈ { 0𝑝 } )
30 24 29 eldifd ( ( 𝑞 ∈ ( Poly ‘ ℤ ) ∧ ( ( coeff ‘ 𝑞 ) ‘ 0 ) ≠ 0 ) → 𝑞 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) )
31 30 adantrr ( ( 𝑞 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑞 ) ‘ 0 ) ≠ 0 ∧ ( 𝑞 ‘ e ) = 0 ) ) → 𝑞 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) )
32 simprr ( ( 𝑞 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑞 ) ‘ 0 ) ≠ 0 ∧ ( 𝑞 ‘ e ) = 0 ) ) → ( 𝑞 ‘ e ) = 0 )
33 eqid ( coeff ‘ 𝑞 ) = ( coeff ‘ 𝑞 )
34 simprl ( ( 𝑞 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑞 ) ‘ 0 ) ≠ 0 ∧ ( 𝑞 ‘ e ) = 0 ) ) → ( ( coeff ‘ 𝑞 ) ‘ 0 ) ≠ 0 )
35 eqid ( deg ‘ 𝑞 ) = ( deg ‘ 𝑞 )
36 eqid Σ 𝑙 ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) = Σ 𝑙 ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) )
37 eqid ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑙 ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑙 ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) )
38 fveq2 ( = 𝑙 → ( ( coeff ‘ 𝑞 ) ‘ ) = ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) )
39 oveq2 ( = 𝑙 → ( e ↑𝑐 ) = ( e ↑𝑐 𝑙 ) )
40 38 39 oveq12d ( = 𝑙 → ( ( ( coeff ‘ 𝑞 ) ‘ ) · ( e ↑𝑐 ) ) = ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) )
41 40 fveq2d ( = 𝑙 → ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ ) · ( e ↑𝑐 ) ) ) = ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) ) )
42 41 oveq1d ( = 𝑙 → ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ ) · ( e ↑𝑐 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) = ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) )
43 42 cbvsumv Σ ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ ) · ( e ↑𝑐 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) = Σ 𝑙 ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) )
44 43 a1i ( 𝑚 = 𝑛 → Σ ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ ) · ( e ↑𝑐 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) = Σ 𝑙 ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) )
45 oveq2 ( 𝑚 = 𝑛 → ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑚 ) = ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑛 ) )
46 fveq2 ( 𝑚 = 𝑛 → ( ! ‘ 𝑚 ) = ( ! ‘ 𝑛 ) )
47 45 46 oveq12d ( 𝑚 = 𝑛 → ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑚 ) / ( ! ‘ 𝑚 ) ) = ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
48 44 47 oveq12d ( 𝑚 = 𝑛 → ( Σ ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ ) · ( e ↑𝑐 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑚 ) / ( ! ‘ 𝑚 ) ) ) = ( Σ 𝑙 ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) )
49 48 cbvmptv ( 𝑚 ∈ ℕ0 ↦ ( Σ ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ ) · ( e ↑𝑐 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑚 ) / ( ! ‘ 𝑚 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑙 ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) )
50 49 a1i ( 𝑚 = 𝑛 → ( 𝑚 ∈ ℕ0 ↦ ( Σ ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ ) · ( e ↑𝑐 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑚 ) / ( ! ‘ 𝑚 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑙 ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) )
51 id ( 𝑚 = 𝑛𝑚 = 𝑛 )
52 50 51 fveq12d ( 𝑚 = 𝑛 → ( ( 𝑚 ∈ ℕ0 ↦ ( Σ ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ ) · ( e ↑𝑐 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑚 ) / ( ! ‘ 𝑚 ) ) ) ) ‘ 𝑚 ) = ( ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑙 ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 𝑛 ) )
53 52 fveq2d ( 𝑚 = 𝑛 → ( abs ‘ ( ( 𝑚 ∈ ℕ0 ↦ ( Σ ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ ) · ( e ↑𝑐 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑚 ) / ( ! ‘ 𝑚 ) ) ) ) ‘ 𝑚 ) ) = ( abs ‘ ( ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑙 ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 𝑛 ) ) )
54 53 breq1d ( 𝑚 = 𝑛 → ( ( abs ‘ ( ( 𝑚 ∈ ℕ0 ↦ ( Σ ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ ) · ( e ↑𝑐 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑚 ) / ( ! ‘ 𝑚 ) ) ) ) ‘ 𝑚 ) ) < 1 ↔ ( abs ‘ ( ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑙 ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 𝑛 ) ) < 1 ) )
55 54 cbvralvw ( ∀ 𝑚 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝑚 ∈ ℕ0 ↦ ( Σ ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ ) · ( e ↑𝑐 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑚 ) / ( ! ‘ 𝑚 ) ) ) ) ‘ 𝑚 ) ) < 1 ↔ ∀ 𝑛 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑙 ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 𝑛 ) ) < 1 )
56 fveq2 ( 𝑗 = 𝑖 → ( ℤ𝑗 ) = ( ℤ𝑖 ) )
57 56 raleqdv ( 𝑗 = 𝑖 → ( ∀ 𝑛 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑙 ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 𝑛 ) ) < 1 ↔ ∀ 𝑛 ∈ ( ℤ𝑖 ) ( abs ‘ ( ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑙 ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 𝑛 ) ) < 1 ) )
58 55 57 syl5bb ( 𝑗 = 𝑖 → ( ∀ 𝑚 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝑚 ∈ ℕ0 ↦ ( Σ ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ ) · ( e ↑𝑐 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑚 ) / ( ! ‘ 𝑚 ) ) ) ) ‘ 𝑚 ) ) < 1 ↔ ∀ 𝑛 ∈ ( ℤ𝑖 ) ( abs ‘ ( ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑙 ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 𝑛 ) ) < 1 ) )
59 58 cbvrabv { 𝑗 ∈ ℕ0 ∣ ∀ 𝑚 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝑚 ∈ ℕ0 ↦ ( Σ ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ ) · ( e ↑𝑐 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑚 ) / ( ! ‘ 𝑚 ) ) ) ) ‘ 𝑚 ) ) < 1 } = { 𝑖 ∈ ℕ0 ∣ ∀ 𝑛 ∈ ( ℤ𝑖 ) ( abs ‘ ( ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑙 ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 𝑛 ) ) < 1 }
60 59 infeq1i inf ( { 𝑗 ∈ ℕ0 ∣ ∀ 𝑚 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝑚 ∈ ℕ0 ↦ ( Σ ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ ) · ( e ↑𝑐 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑚 ) / ( ! ‘ 𝑚 ) ) ) ) ‘ 𝑚 ) ) < 1 } , ℝ , < ) = inf ( { 𝑖 ∈ ℕ0 ∣ ∀ 𝑛 ∈ ( ℤ𝑖 ) ( abs ‘ ( ( 𝑛 ∈ ℕ0 ↦ ( Σ 𝑙 ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ 𝑙 ) · ( e ↑𝑐 𝑙 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ‘ 𝑛 ) ) < 1 } , ℝ , < )
61 eqid sup ( { ( abs ‘ ( ( coeff ‘ 𝑞 ) ‘ 0 ) ) , ( ! ‘ ( deg ‘ 𝑞 ) ) , inf ( { 𝑗 ∈ ℕ0 ∣ ∀ 𝑚 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝑚 ∈ ℕ0 ↦ ( Σ ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ ) · ( e ↑𝑐 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑚 ) / ( ! ‘ 𝑚 ) ) ) ) ‘ 𝑚 ) ) < 1 } , ℝ , < ) } , ℝ* , < ) = sup ( { ( abs ‘ ( ( coeff ‘ 𝑞 ) ‘ 0 ) ) , ( ! ‘ ( deg ‘ 𝑞 ) ) , inf ( { 𝑗 ∈ ℕ0 ∣ ∀ 𝑚 ∈ ( ℤ𝑗 ) ( abs ‘ ( ( 𝑚 ∈ ℕ0 ↦ ( Σ ∈ ( 0 ... ( deg ‘ 𝑞 ) ) ( ( abs ‘ ( ( ( coeff ‘ 𝑞 ) ‘ ) · ( e ↑𝑐 ) ) ) · ( ( deg ‘ 𝑞 ) · ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ) ) · ( ( ( ( deg ‘ 𝑞 ) ↑ ( ( deg ‘ 𝑞 ) + 1 ) ) ↑ 𝑚 ) / ( ! ‘ 𝑚 ) ) ) ) ‘ 𝑚 ) ) < 1 } , ℝ , < ) } , ℝ* , < )
62 31 32 33 34 35 36 37 60 61 etransclem48 ( ( 𝑞 ∈ ( Poly ‘ ℤ ) ∧ ( ( ( coeff ‘ 𝑞 ) ‘ 0 ) ≠ 0 ∧ ( 𝑞 ‘ e ) = 0 ) ) → ∃ 𝑘 ∈ ℤ ( 𝑘 ≠ 0 ∧ ( abs ‘ 𝑘 ) < 1 ) )
63 62 rexlimiva ( ∃ 𝑞 ∈ ( Poly ‘ ℤ ) ( ( ( coeff ‘ 𝑞 ) ‘ 0 ) ≠ 0 ∧ ( 𝑞 ‘ e ) = 0 ) → ∃ 𝑘 ∈ ℤ ( 𝑘 ≠ 0 ∧ ( abs ‘ 𝑘 ) < 1 ) )
64 23 63 syl ( ¬ e ∈ ( ℂ ∖ 𝔸 ) → ∃ 𝑘 ∈ ℤ ( 𝑘 ≠ 0 ∧ ( abs ‘ 𝑘 ) < 1 ) )
65 10 64 mt3 e ∈ ( ℂ ∖ 𝔸 )