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