Metamath Proof Explorer

Theorem etransclem47

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)

Ref Expression
Hypotheses etransclem47.q ⊢ ( 𝜑 → 𝑄 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) )
etransclem47.qe0 ⊢ ( 𝜑 → ( 𝑄 ‘ e ) = 0 )
etransclem47.a ⊢ 𝐴 = ( coeff ‘ 𝑄 )
etransclem47.a0 ⊢ ( 𝜑 → ( 𝐴 ‘ 0 ) ≠ 0 )
etransclem47.m ⊢ 𝑀 = ( deg ‘ 𝑄 )
etransclem47.p ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
etransclem47.ap ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 ‘ 0 ) ) < 𝑃 )
etransclem47.mp ⊢ ( 𝜑 → ( ! ‘ 𝑀 ) < 𝑃 )
etransclem47.9 ⊢ ( 𝜑 → ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) < 1 )
etransclem47.f ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
etransclem47.l ⊢ 𝐿 = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 )
etransclem47.k ⊢ 𝐾 = ( 𝐿 / ( ! ‘ ( 𝑃 − 1 ) ) )
Assertion etransclem47 ( 𝜑 → ∃ 𝑘 ∈ ℤ ( 𝑘 ≠ 0 ∧ ( abs ‘ 𝑘 ) < 1 ) )

Proof

Step Hyp Ref Expression
1 etransclem47.q ⊢ ( 𝜑 → 𝑄 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) )
2 etransclem47.qe0 ⊢ ( 𝜑 → ( 𝑄 ‘ e ) = 0 )
3 etransclem47.a ⊢ 𝐴 = ( coeff ‘ 𝑄 )
4 etransclem47.a0 ⊢ ( 𝜑 → ( 𝐴 ‘ 0 ) ≠ 0 )
5 etransclem47.m ⊢ 𝑀 = ( deg ‘ 𝑄 )
6 etransclem47.p ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
7 etransclem47.ap ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 ‘ 0 ) ) < 𝑃 )
8 etransclem47.mp ⊢ ( 𝜑 → ( ! ‘ 𝑀 ) < 𝑃 )
9 etransclem47.9 ⊢ ( 𝜑 → ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( abs ‘ ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) ) · ( 𝑀 · ( 𝑀 ↑ ( 𝑀 + 1 ) ) ) ) · ( ( ( 𝑀 ↑ ( 𝑀 + 1 ) ) ↑ ( 𝑃 − 1 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) < 1 )
10 etransclem47.f ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
11 etransclem47.l ⊢ 𝐿 = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 )
12 etransclem47.k ⊢ 𝐾 = ( 𝐿 / ( ! ‘ ( 𝑃 − 1 ) ) )
13 12 a1i ⊢ ( 𝜑 → 𝐾 = ( 𝐿 / ( ! ‘ ( 𝑃 − 1 ) ) ) )
14 ssid ⊢ ℝ ⊆ ℝ
15 14 a1i ⊢ ( 𝜑 → ℝ ⊆ ℝ )
16 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
17 16 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
18 reopn ⊢ ℝ ∈ ( topGen ‘ ran (,) )
19 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
20 18 19 eleqtri ⊢ ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
21 20 a1i ⊢ ( 𝜑 → ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
22 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
23 6 22 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
24 eqid ⊢ ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) = ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) )
25 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑦 ) = ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) )
26 25 sumeq2sdv ⊢ ( 𝑦 = 𝑥 → Σ 𝑖 ∈ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑦 ) = Σ 𝑖 ∈ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) )
27 26 cbvmptv ⊢ ( 𝑦 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑦 ) ) = ( 𝑥 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) )
28 negeq ⊢ ( 𝑧 = 𝑥 → - 𝑧 = - 𝑥 )
29 28 oveq2d ⊢ ( 𝑧 = 𝑥 → ( e ↑𝑐 - 𝑧 ) = ( e ↑𝑐 - 𝑥 ) )
30 fveq2 ⊢ ( 𝑧 = 𝑥 → ( ( 𝑦 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑦 ) ) ‘ 𝑧 ) = ( ( 𝑦 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑦 ) ) ‘ 𝑥 ) )
31 29 30 oveq12d ⊢ ( 𝑧 = 𝑥 → ( ( e ↑𝑐 - 𝑧 ) · ( ( 𝑦 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑦 ) ) ‘ 𝑧 ) ) = ( ( e ↑𝑐 - 𝑥 ) · ( ( 𝑦 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑦 ) ) ‘ 𝑥 ) ) )
32 31 negeqd ⊢ ( 𝑧 = 𝑥 → - ( ( e ↑𝑐 - 𝑧 ) · ( ( 𝑦 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑦 ) ) ‘ 𝑧 ) ) = - ( ( e ↑𝑐 - 𝑥 ) · ( ( 𝑦 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑦 ) ) ‘ 𝑥 ) ) )
33 32 cbvmptv ⊢ ( 𝑧 ∈ ( 0 [,] 𝑗 ) ↦ - ( ( e ↑𝑐 - 𝑧 ) · ( ( 𝑦 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑦 ) ) ‘ 𝑧 ) ) ) = ( 𝑥 ∈ ( 0 [,] 𝑗 ) ↦ - ( ( e ↑𝑐 - 𝑥 ) · ( ( 𝑦 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑦 ) ) ‘ 𝑥 ) ) )
34 1 2 3 5 15 17 21 23 10 11 24 27 33 etransclem46 ⊢ ( 𝜑 → ( 𝐿 / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( - Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
35 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ Fin )
36 fzfid ⊢ ( 𝜑 → ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ∈ Fin )
37 xpfi ⊢ ( ( ( 0 ... 𝑀 ) ∈ Fin ∧ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ∈ Fin ) → ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∈ Fin )
38 35 36 37 syl2anc ⊢ ( 𝜑 → ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∈ Fin )
39 1 eldifad ⊢ ( 𝜑 → 𝑄 ∈ ( Poly ‘ ℤ ) )
40 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
41 3 coef2 ⊢ ( ( 𝑄 ∈ ( Poly ‘ ℤ ) ∧ 0 ∈ ℤ ) → 𝐴 : ℕ0 ⟶ ℤ )
42 39 40 41 syl2anc ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℤ )
43 42 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → 𝐴 : ℕ0 ⟶ ℤ )
44 xp1st ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) → ( 1st ‘ 𝑘 ) ∈ ( 0 ... 𝑀 ) )
45 elfznn0 ⊢ ( ( 1st ‘ 𝑘 ) ∈ ( 0 ... 𝑀 ) → ( 1st ‘ 𝑘 ) ∈ ℕ0 )
46 44 45 syl ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) → ( 1st ‘ 𝑘 ) ∈ ℕ0 )
47 46 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ( 1st ‘ 𝑘 ) ∈ ℕ0 )
48 43 47 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) ∈ ℤ )
49 48 zcnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) ∈ ℂ )
50 16 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ℝ ∈ { ℝ , ℂ } )
51 20 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
52 23 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → 𝑃 ∈ ℕ )
53 dgrcl ⊢ ( 𝑄 ∈ ( Poly ‘ ℤ ) → ( deg ‘ 𝑄 ) ∈ ℕ0 )
54 39 53 syl ⊢ ( 𝜑 → ( deg ‘ 𝑄 ) ∈ ℕ0 )
55 5 54 eqeltrid ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
56 55 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → 𝑀 ∈ ℕ0 )
57 xp2nd ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) → ( 2nd ‘ 𝑘 ) ∈ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) )
58 elfznn0 ⊢ ( ( 2nd ‘ 𝑘 ) ∈ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) → ( 2nd ‘ 𝑘 ) ∈ ℕ0 )
59 57 58 syl ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) → ( 2nd ‘ 𝑘 ) ∈ ℕ0 )
60 59 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ( 2nd ‘ 𝑘 ) ∈ ℕ0 )
61 50 51 52 56 10 60 etransclem33 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) : ℝ ⟶ ℂ )
62 47 nn0red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ( 1st ‘ 𝑘 ) ∈ ℝ )
63 61 62 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ∈ ℂ )
64 49 63 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) ∈ ℂ )
65 38 64 fsumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) ∈ ℂ )
66 nnm1nn0 ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
67 23 66 syl ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
68 67 faccld ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℕ )
69 68 nncnd ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ )
70 68 nnne0d ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ≠ 0 )
71 65 69 70 divnegd ⊢ ( 𝜑 → - ( Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( - Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
72 71 eqcomd ⊢ ( 𝜑 → ( - Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = - ( Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
73 13 34 72 3eqtrd ⊢ ( 𝜑 → 𝐾 = - ( Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
74 eqid ⊢ ( Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) )
75 23 55 10 42 74 etransclem45 ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ )
76 75 znegcld ⊢ ( 𝜑 → - ( Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ )
77 73 76 eqeltrd ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
78 12 34 eqtrid ⊢ ( 𝜑 → 𝐾 = ( - Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
79 65 69 70 divcld ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℂ )
80 42 4 55 6 7 8 10 74 etransclem44 ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ≠ 0 )
81 79 80 negne0d ⊢ ( 𝜑 → - ( Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ≠ 0 )
82 72 81 eqnetrd ⊢ ( 𝜑 → ( - Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ≠ 0 )
83 78 82 eqnetrd ⊢ ( 𝜑 → 𝐾 ≠ 0 )
84 eldifsni ⊢ ( 𝑄 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) → 𝑄 ≠ 0𝑝 )
85 1 84 syl ⊢ ( 𝜑 → 𝑄 ≠ 0𝑝 )
86 ere ⊢ e ∈ ℝ
87 86 recni ⊢ e ∈ ℂ
88 87 a1i ⊢ ( 𝜑 → e ∈ ℂ )
89 dgrnznn ⊢ ( ( ( 𝑄 ∈ ( Poly ‘ ℤ ) ∧ 𝑄 ≠ 0𝑝 ) ∧ ( e ∈ ℂ ∧ ( 𝑄 ‘ e ) = 0 ) ) → ( deg ‘ 𝑄 ) ∈ ℕ )
90 39 85 88 2 89 syl22anc ⊢ ( 𝜑 → ( deg ‘ 𝑄 ) ∈ ℕ )
91 5 90 eqeltrid ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
92 42 11 12 23 91 10 9 etransclem23 ⊢ ( 𝜑 → ( abs ‘ 𝐾 ) < 1 )
93 neeq1 ⊢ ( 𝑘 = 𝐾 → ( 𝑘 ≠ 0 ↔ 𝐾 ≠ 0 ) )
94 fveq2 ⊢ ( 𝑘 = 𝐾 → ( abs ‘ 𝑘 ) = ( abs ‘ 𝐾 ) )
95 94 breq1d ⊢ ( 𝑘 = 𝐾 → ( ( abs ‘ 𝑘 ) < 1 ↔ ( abs ‘ 𝐾 ) < 1 ) )
96 93 95 anbi12d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑘 ≠ 0 ∧ ( abs ‘ 𝑘 ) < 1 ) ↔ ( 𝐾 ≠ 0 ∧ ( abs ‘ 𝐾 ) < 1 ) ) )
97 96 rspcev ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 ≠ 0 ∧ ( abs ‘ 𝐾 ) < 1 ) ) → ∃ 𝑘 ∈ ℤ ( 𝑘 ≠ 0 ∧ ( abs ‘ 𝑘 ) < 1 ) )
98 77 83 92 97 syl12anc ⊢ ( 𝜑 → ∃ 𝑘 ∈ ℤ ( 𝑘 ≠ 0 ∧ ( abs ‘ 𝑘 ) < 1 ) )