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