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 bitrid ⊢ ( 𝑗 = 𝑖 → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 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 ∈ ( ℂ ∖ 𝔸 )