etransclem47 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > etransclem47		Structured version Visualization version GIF version

Theorem etransclem47 43451

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.)

**Hypotheses**
Ref	Expression
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**
Ref	Expression
etransclem47	⊢ (𝜑 → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1))

Distinct variable groups: 𝐴,𝑗,𝑘 𝑗,𝐹,𝑘,𝑥 𝑘,𝐾 𝑗,𝑀,𝑘,𝑥 𝑃,𝑗,𝑘,𝑥 𝑄,𝑗 𝜑,𝑗,𝑘,𝑥 Allowed substitution hints: 𝐴(𝑥) 𝑄(𝑥,𝑘) 𝐾(𝑥,𝑗) 𝐿(𝑥,𝑗,𝑘)

Proof of Theorem etransclem47 Dummy variables 𝑖 𝑦 𝑧 are mutually distinct and distinct from all other variables.

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 3913	. . . . . 6 ⊢ ℝ ⊆ ℝ
8	7	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ⊆ ℝ)
9		reelprrecn 10804	. . . . . 6 ⊢ ℝ ∈ {ℝ, ℂ}
10	9	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
11		reopn 42452	. . . . . . 7 ⊢ ℝ ∈ (topGen‘ran (,))
12		eqid 2734	. . . . . . . 8 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
13	12	tgioo2 23672	. . . . . . 7 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
14	11, 13	eleqtri 2832	. . . . . 6 ⊢ ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ)
15	14	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
16		etransclem47.p	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ ℙ)
17		prmnn 16212	. . . . . 6 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
18	16, 17	syl 17	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ ℕ)
19		etransclem47.f	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))
20		etransclem47.l	. . . . 5 ⊢ 𝐿 = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)
21		eqid 2734	. . . . 5 ⊢ ((𝑀 · 𝑃) + (𝑃 − 1)) = ((𝑀 · 𝑃) + (𝑃 − 1))
22		fveq2 6706	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑦) = (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
23	22	sumeq2sdv 15251	. . . . . 6 ⊢ (𝑦 = 𝑥 → Σ𝑖 ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1)))(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑦) = Σ𝑖 ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1)))(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
24	23	cbvmptv 5147	. . . . 5 ⊢ (𝑦 ∈ ℝ ↦ Σ𝑖 ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1)))(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑦)) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1)))(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
25		negeq 11053	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → -𝑧 = -𝑥)
26	25	oveq2d 7218	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (e↑_𝑐-𝑧) = (e↑_𝑐-𝑥))
27		fveq2 6706	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → ((𝑦 ∈ ℝ ↦ Σ𝑖 ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1)))(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑦))‘𝑧) = ((𝑦 ∈ ℝ ↦ Σ𝑖 ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1)))(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑦))‘𝑥))
28	26, 27	oveq12d 7220	. . . . . . 7 ⊢ (𝑧 = 𝑥 → ((e↑_𝑐-𝑧) · ((𝑦 ∈ ℝ ↦ Σ𝑖 ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1)))(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑦))‘𝑧)) = ((e↑_𝑐-𝑥) · ((𝑦 ∈ ℝ ↦ Σ𝑖 ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1)))(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑦))‘𝑥)))
29	28	negeqd 11055	. . . . . 6 ⊢ (𝑧 = 𝑥 → -((e↑_𝑐-𝑧) · ((𝑦 ∈ ℝ ↦ Σ𝑖 ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1)))(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑦))‘𝑧)) = -((e↑_𝑐-𝑥) · ((𝑦 ∈ ℝ ↦ Σ𝑖 ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1)))(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑦))‘𝑥)))
30	29	cbvmptv 5147	. . . . 5 ⊢ (𝑧 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑧) · ((𝑦 ∈ ℝ ↦ Σ𝑖 ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1)))(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑦))‘𝑧))) = (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · ((𝑦 ∈ ℝ ↦ Σ𝑖 ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1)))(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑦))‘𝑥)))
31	3, 4, 5, 6, 8, 10, 15, 18, 19, 20, 21, 24, 30	etransclem46 43450	. . . 4 ⊢ (𝜑 → (𝐿 / (!‘(𝑃 − 1))) = (-Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) / (!‘(𝑃 − 1))))
32		fzfid 13529	. . . . . . . 8 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
33		fzfid 13529	. . . . . . . 8 ⊢ (𝜑 → (0...((𝑀 · 𝑃) + (𝑃 − 1))) ∈ Fin)
34		xpfi 8931	. . . . . . . 8 ⊢ (((0...𝑀) ∈ Fin ∧ (0...((𝑀 · 𝑃) + (𝑃 − 1))) ∈ Fin) → ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∈ Fin)
35	32, 33, 34	syl2anc 587	. . . . . . 7 ⊢ (𝜑 → ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) ∈ Fin)
36	3	eldifad 3869	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ (Poly‘ℤ))
37		0zd 12171	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ∈ ℤ)
38	5	coef2 25097	. . . . . . . . . . . 12 ⊢ ((𝑄 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → 𝐴:ℕ₀⟶ℤ)
39	36, 37, 38	syl2anc 587	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℤ)
40	39	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → 𝐴:ℕ₀⟶ℤ)
41		xp1st 7782	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → (1^st ‘𝑘) ∈ (0...𝑀))
42		elfznn0 13188	. . . . . . . . . . . 12 ⊢ ((1^st ‘𝑘) ∈ (0...𝑀) → (1^st ‘𝑘) ∈ ℕ₀)
43	41, 42	syl 17	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → (1^st ‘𝑘) ∈ ℕ₀)
44	43	adantl 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (1^st ‘𝑘) ∈ ℕ₀)
45	40, 44	ffvelrnd 6894	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (𝐴‘(1^st ‘𝑘)) ∈ ℤ)
46	45	zcnd 12266	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (𝐴‘(1^st ‘𝑘)) ∈ ℂ)
47	9	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → ℝ ∈ {ℝ, ℂ})
48	14	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
49	18	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → 𝑃 ∈ ℕ)
50		dgrcl 25099	. . . . . . . . . . . . 13 ⊢ (𝑄 ∈ (Poly‘ℤ) → (deg‘𝑄) ∈ ℕ₀)
51	36, 50	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (deg‘𝑄) ∈ ℕ₀)
52	6, 51	eqeltrid 2838	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
53	52	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → 𝑀 ∈ ℕ₀)
54		xp2nd 7783	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → (2^nd ‘𝑘) ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1))))
55		elfznn0 13188	. . . . . . . . . . . 12 ⊢ ((2^nd ‘𝑘) ∈ (0...((𝑀 · 𝑃) + (𝑃 − 1))) → (2^nd ‘𝑘) ∈ ℕ₀)
56	54, 55	syl 17	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1)))) → (2^nd ‘𝑘) ∈ ℕ₀)
57	56	adantl 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (2^nd ‘𝑘) ∈ ℕ₀)
58	47, 48, 49, 53, 19, 57	etransclem33 43437	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → ((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘)):ℝ⟶ℂ)
59	44	nn0red 12134	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (1^st ‘𝑘) ∈ ℝ)
60	58, 59	ffvelrnd 6894	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘)) ∈ ℂ)
61	46, 60	mulcld 10836	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))) → ((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) ∈ ℂ)
62	35, 61	fsumcl 15280	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) ∈ ℂ)
63		nnm1nn0 12114	. . . . . . . . 9 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
64	18, 63	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑃 − 1) ∈ ℕ₀)
65	64	faccld 13833	. . . . . . 7 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℕ)
66	65	nncnd 11829	. . . . . 6 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℂ)
67	65	nnne0d 11863	. . . . . 6 ⊢ (𝜑 → (!‘(𝑃 − 1)) ≠ 0)
68	62, 66, 67	divnegd 11604	. . . . 5 ⊢ (𝜑 → -(Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) / (!‘(𝑃 − 1))) = (-Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) / (!‘(𝑃 − 1))))
69	68	eqcomd 2740	. . . 4 ⊢ (𝜑 → (-Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) / (!‘(𝑃 − 1))) = -(Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) / (!‘(𝑃 − 1))))
70	2, 31, 69	3eqtrd 2778	. . 3 ⊢ (𝜑 → 𝐾 = -(Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) / (!‘(𝑃 − 1))))
71		eqid 2734	. . . . 5 ⊢ (Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) / (!‘(𝑃 − 1))) = (Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) / (!‘(𝑃 − 1)))
72	18, 52, 19, 39, 71	etransclem45 43449	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) / (!‘(𝑃 − 1))) ∈ ℤ)
73	72	znegcld 12267	. . 3 ⊢ (𝜑 → -(Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) / (!‘(𝑃 − 1))) ∈ ℤ)
74	70, 73	eqeltrd 2834	. 2 ⊢ (𝜑 → 𝐾 ∈ ℤ)
75	1, 31	syl5eq 2786	. . 3 ⊢ (𝜑 → 𝐾 = (-Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) / (!‘(𝑃 − 1))))
76	62, 66, 67	divcld 11591	. . . . 5 ⊢ (𝜑 → (Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) / (!‘(𝑃 − 1))) ∈ ℂ)
77		etransclem47.a0	. . . . . 6 ⊢ (𝜑 → (𝐴‘0) ≠ 0)
78		etransclem47.ap	. . . . . 6 ⊢ (𝜑 → (abs‘(𝐴‘0)) < 𝑃)
79		etransclem47.mp	. . . . . 6 ⊢ (𝜑 → (!‘𝑀) < 𝑃)
80	39, 77, 52, 16, 78, 79, 19, 71	etransclem44 43448	. . . . 5 ⊢ (𝜑 → (Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) / (!‘(𝑃 − 1))) ≠ 0)
81	76, 80	negne0d 11170	. . . 4 ⊢ (𝜑 → -(Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) / (!‘(𝑃 − 1))) ≠ 0)
82	69, 81	eqnetrd 3002	. . 3 ⊢ (𝜑 → (-Σ𝑘 ∈ ((0...𝑀) × (0...((𝑀 · 𝑃) + (𝑃 − 1))))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) / (!‘(𝑃 − 1))) ≠ 0)
83	75, 82	eqnetrd 3002	. 2 ⊢ (𝜑 → 𝐾 ≠ 0)
84		eldifsni 4693	. . . . . 6 ⊢ (𝑄 ∈ ((Poly‘ℤ) ∖ {0_𝑝}) → 𝑄 ≠ 0_𝑝)
85	3, 84	syl 17	. . . . 5 ⊢ (𝜑 → 𝑄 ≠ 0_𝑝)
86		ere 15631	. . . . . . 7 ⊢ e ∈ ℝ
87	86	recni 10830	. . . . . 6 ⊢ e ∈ ℂ
88	87	a1i 11	. . . . 5 ⊢ (𝜑 → e ∈ ℂ)
89		dgrnznn 25113	. . . . 5 ⊢ (((𝑄 ∈ (Poly‘ℤ) ∧ 𝑄 ≠ 0_𝑝) ∧ (e ∈ ℂ ∧ (𝑄‘e) = 0)) → (deg‘𝑄) ∈ ℕ)
90	36, 85, 88, 4, 89	syl22anc 839	. . . 4 ⊢ (𝜑 → (deg‘𝑄) ∈ ℕ)
91	6, 90	eqeltrid 2838	. . 3 ⊢ (𝜑 → 𝑀 ∈ ℕ)
92		etransclem47.9	. . 3 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))) < 1)
93	39, 20, 1, 18, 91, 19, 92	etransclem23 43427	. 2 ⊢ (𝜑 → (abs‘𝐾) < 1)
94		neeq1 2997	. . . 4 ⊢ (𝑘 = 𝐾 → (𝑘 ≠ 0 ↔ 𝐾 ≠ 0))
95		fveq2 6706	. . . . 5 ⊢ (𝑘 = 𝐾 → (abs‘𝑘) = (abs‘𝐾))
96	95	breq1d 5053	. . . 4 ⊢ (𝑘 = 𝐾 → ((abs‘𝑘) < 1 ↔ (abs‘𝐾) < 1))
97	94, 96	anbi12d 634	. . 3 ⊢ (𝑘 = 𝐾 → ((𝑘 ≠ 0 ∧ (abs‘𝑘) < 1) ↔ (𝐾 ≠ 0 ∧ (abs‘𝐾) < 1)))
98	97	rspcev 3530	. 2 ⊢ ((𝐾 ∈ ℤ ∧ (𝐾 ≠ 0 ∧ (abs‘𝐾) < 1)) → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1))
99	74, 83, 93, 98	syl12anc 837	1 ⊢ (𝜑 → ∃𝑘 ∈ ℤ (𝑘 ≠ 0 ∧ (abs‘𝑘) < 1))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 = wceq 1543 ∈ wcel 2110 ≠ wne 2935 ∃wrex 3055 ∖ cdif 3854 ⊆ wss 3857 {csn 4531 {cpr 4533 class class class wbr 5043 ↦ cmpt 5124 × cxp 5538 ran crn 5541 ⟶wf 6365 ‘cfv 6369 (class class class)co 7202 1^st c1st 7748 2^nd c2nd 7749 Fincfn 8615 ℂcc 10710 ℝcr 10711 0cc0 10712 1c1 10713 + caddc 10715 · cmul 10717 < clt 10850 − cmin 11045 -cneg 11046 / cdiv 11472 ℕcn 11813 ℕ₀cn0 12073 ℤcz 12159 (,)cioo 12918 [,]cicc 12921 ...cfz 13078 ↑cexp 13618 !cfa 13822 abscabs 14780 Σcsu 15232 ∏cprod 15448 eceu 15605 ℙcprime 16209 ↾_t crest 16897 TopOpenctopn 16898 topGenctg 16914 ℂ_fldccnfld 20335 ∫citg 24487 0_𝑝c0p 24538 D^𝑛 cdvn 24733 Polycply 25050 coeffccoe 25052 degcdgr 25053 ↑_𝑐ccxp 25416

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2706 ax-rep 5168 ax-sep 5181 ax-nul 5188 ax-pow 5247 ax-pr 5311 ax-un 7512 ax-inf2 9245 ax-cc 10032 ax-cnex 10768 ax-resscn 10769 ax-1cn 10770 ax-icn 10771 ax-addcl 10772 ax-addrcl 10773 ax-mulcl 10774 ax-mulrcl 10775 ax-mulcom 10776 ax-addass 10777 ax-mulass 10778 ax-distr 10779 ax-i2m1 10780 ax-1ne0 10781 ax-1rid 10782 ax-rnegex 10783 ax-rrecex 10784 ax-cnre 10785 ax-pre-lttri 10786 ax-pre-lttrn 10787 ax-pre-ltadd 10788 ax-pre-mulgt0 10789 ax-pre-sup 10790 ax-addf 10791 ax-mulf 10792

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2537 df-eu 2566 df-clab 2713 df-cleq 2726 df-clel 2812 df-nfc 2882 df-ne 2936 df-nel 3040 df-ral 3059 df-rex 3060 df-reu 3061 df-rmo 3062 df-rab 3063 df-v 3403 df-sbc 3688 df-csb 3803 df-dif 3860 df-un 3862 df-in 3864 df-ss 3874 df-pss 3876 df-symdif 4147 df-nul 4228 df-if 4430 df-pw 4505 df-sn 4532 df-pr 4534 df-tp 4536 df-op 4538 df-uni 4810 df-int 4850 df-iun 4896 df-iin 4897 df-disj 5009 df-br 5044 df-opab 5106 df-mpt 5125 df-tr 5151 df-id 5444 df-eprel 5449 df-po 5457 df-so 5458 df-fr 5498 df-se 5499 df-we 5500 df-xp 5546 df-rel 5547 df-cnv 5548 df-co 5549 df-dm 5550 df-rn 5551 df-res 5552 df-ima 5553 df-pred 6149 df-ord 6205 df-on 6206 df-lim 6207 df-suc 6208 df-iota 6327 df-fun 6371 df-fn 6372 df-f 6373 df-f1 6374 df-fo 6375 df-f1o 6376 df-fv 6377 df-isom 6378 df-riota 7159 df-ov 7205 df-oprab 7206 df-mpo 7207 df-of 7458 df-ofr 7459 df-om 7634 df-1st 7750 df-2nd 7751 df-supp 7893 df-wrecs 8036 df-recs 8097 df-rdg 8135 df-1o 8191 df-2o 8192 df-oadd 8195 df-omul 8196 df-er 8380 df-map 8499 df-pm 8500 df-ixp 8568 df-en 8616 df-dom 8617 df-sdom 8618 df-fin 8619 df-fsupp 8975 df-fi 9016 df-sup 9047 df-inf 9048 df-oi 9115 df-dju 9500 df-card 9538 df-acn 9541 df-pnf 10852 df-mnf 10853 df-xr 10854 df-ltxr 10855 df-le 10856 df-sub 11047 df-neg 11048 df-div 11473 df-nn 11814 df-2 11876 df-3 11877 df-4 11878 df-5 11879 df-6 11880 df-7 11881 df-8 11882 df-9 11883 df-n0 12074 df-z 12160 df-dec 12277 df-uz 12422 df-q 12528 df-rp 12570 df-xneg 12687 df-xadd 12688 df-xmul 12689 df-ioo 12922 df-ioc 12923 df-ico 12924 df-icc 12925 df-fz 13079 df-fzo 13222 df-fl 13350 df-mod 13426 df-seq 13558 df-exp 13619 df-fac 13823 df-bc 13852 df-hash 13880 df-shft 14613 df-cj 14645 df-re 14646 df-im 14647 df-sqrt 14781 df-abs 14782 df-limsup 15015 df-clim 15032 df-rlim 15033 df-sum 15233 df-prod 15449 df-ef 15610 df-e 15611 df-sin 15612 df-cos 15613 df-tan 15614 df-pi 15615 df-dvds 15797 df-gcd 16035 df-prm 16210 df-struct 16686 df-ndx 16687 df-slot 16688 df-base 16690 df-sets 16691 df-ress 16692 df-plusg 16780 df-mulr 16781 df-starv 16782 df-sca 16783 df-vsca 16784 df-ip 16785 df-tset 16786 df-ple 16787 df-ds 16789 df-unif 16790 df-hom 16791 df-cco 16792 df-rest 16899 df-topn 16900 df-0g 16918 df-gsum 16919 df-topgen 16920 df-pt 16921 df-prds 16924 df-xrs 16979 df-qtop 16984 df-imas 16985 df-xps 16987 df-mre 17061 df-mrc 17062 df-acs 17064 df-mgm 18086 df-sgrp 18135 df-mnd 18146 df-submnd 18191 df-mulg 18461 df-cntz 18683 df-cmn 19144 df-psmet 20327 df-xmet 20328 df-met 20329 df-bl 20330 df-mopn 20331 df-fbas 20332 df-fg 20333 df-cnfld 20336 df-top 21763 df-topon 21780 df-topsp 21802 df-bases 21815 df-cld 21888 df-ntr 21889 df-cls 21890 df-nei 21967 df-lp 22005 df-perf 22006 df-cn 22096 df-cnp 22097 df-haus 22184 df-cmp 22256 df-tx 22431 df-hmeo 22624 df-fil 22715 df-fm 22807 df-flim 22808 df-flf 22809 df-xms 23190 df-ms 23191 df-tms 23192 df-cncf 23747 df-ovol 24333 df-vol 24334 df-mbf 24488 df-itg1 24489 df-itg2 24490 df-ibl 24491 df-itg 24492 df-0p 24539 df-limc 24735 df-dv 24736 df-dvn 24737 df-ply 25054 df-coe 25056 df-dgr 25057 df-log 25417 df-cxp 25418

This theorem is referenced by: etransclem48 43452

W3C validator