etransclem46 - Mathbox for Glauco Siliprandi

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

Theorem etransclem46 43821

Description: This is the proof for equation *(7) in [Juillerat] p. 12. The proven equality will lead to a contradiction, because the left-hand side goes to 0 for large 𝑃, but the right-hand side is a nonzero integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)

**Hypotheses**
Ref	Expression
etransclem46.q	⊢ (𝜑 → 𝑄 ∈ ((Poly‘ℤ) ∖ {0_𝑝}))
etransclem46.qe0	⊢ (𝜑 → (𝑄‘e) = 0)
etransclem46.a	⊢ 𝐴 = (coeff‘𝑄)
etransclem46.m	⊢ 𝑀 = (deg‘𝑄)
etransclem46.rex	⊢ (𝜑 → ℝ ⊆ ℝ)
etransclem46.s	⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
etransclem46.x	⊢ (𝜑 → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
etransclem46.p	⊢ (𝜑 → 𝑃 ∈ ℕ)
etransclem46.f	⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))
etransclem46.l	⊢ 𝐿 = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)
etransclem46.r	⊢ 𝑅 = ((𝑀 · 𝑃) + (𝑃 − 1))
etransclem46.g	⊢ 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
etransclem46.h	⊢ 𝑂 = (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))

**Assertion**
Ref	Expression
etransclem46	⊢ (𝜑 → (𝐿 / (!‘(𝑃 − 1))) = (-Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) / (!‘(𝑃 − 1))))

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

Proof of Theorem etransclem46 Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		etransclem46.l	. . . 4 ⊢ 𝐿 = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)
2	1	a1i 11	. . 3 ⊢ (𝜑 → 𝐿 = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥))
3		etransclem46.h	. . . . . . . . . . . . . 14 ⊢ 𝑂 = (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))
4	3	oveq2i 7286	. . . . . . . . . . . . 13 ⊢ (ℝ D 𝑂) = (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
5	4	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) = (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))))
6		etransclem46.s	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
7	6	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℝ ∈ {ℝ, ℂ})
8		ere 15798	. . . . . . . . . . . . . . . . . . . 20 ⊢ e ∈ ℝ
9	8	recni 10989	. . . . . . . . . . . . . . . . . . 19 ⊢ e ∈ ℂ
10	9	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → e ∈ ℂ)
11		recn 10961	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
12	11	negcld 11319	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → -𝑥 ∈ ℂ)
13	10, 12	cxpcld 25863	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (e↑_𝑐-𝑥) ∈ ℂ)
14	13	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (e↑_𝑐-𝑥) ∈ ℂ)
15		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
16		fzfid 13693	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (0...𝑅) ∈ Fin)
17		elfznn0 13349	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ (0...𝑅) → 𝑖 ∈ ℕ₀)
18	6	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → ℝ ∈ {ℝ, ℂ})
19		etransclem46.x	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
20	19	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
21		etransclem46.p	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑃 ∈ ℕ)
22	21	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → 𝑃 ∈ ℕ)
23		etransclem46.m	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑀 = (deg‘𝑄)
24		etransclem46.q	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑄 ∈ ((Poly‘ℤ) ∖ {0_𝑝}))
25	24	eldifad 3899	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑄 ∈ (Poly‘ℤ))
26		dgrcl 25394	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑄 ∈ (Poly‘ℤ) → (deg‘𝑄) ∈ ℕ₀)
27	25, 26	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (deg‘𝑄) ∈ ℕ₀)
28	23, 27	eqeltrid 2843	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
29	28	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → 𝑀 ∈ ℕ₀)
30		etransclem46.f	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))
31		simpr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → 𝑖 ∈ ℕ₀)
32	18, 20, 22, 29, 30, 31	etransclem33 43808	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
33	17, 32	sylan2 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
34	33	adantlr 712	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
35		simplr 766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → 𝑥 ∈ ℝ)
36	34, 35	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ)
37	16, 36	fsumcl 15445	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ)
38		etransclem46.g	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
39	38	fvmpt2 6886	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ) → (𝐺‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
40	15, 37, 39	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐺‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
41	40, 37	eqeltrd 2839	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐺‘𝑥) ∈ ℂ)
42	14, 41	mulcld 10995	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · (𝐺‘𝑥)) ∈ ℂ)
43	42	negcld 11319	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) ∈ ℂ)
44	43	adantlr 712	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ ℝ) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) ∈ ℂ)
45	6, 19	dvdmsscn 43477	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ℝ ⊆ ℂ)
46	45, 21, 30	etransclem8 43783	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
47	46	ffvelrnda 6961	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℂ)
48	14, 47	mulcld 10995	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
49	48	negcld 11319	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
50	49	negcld 11319	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → --((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
51	50	adantlr 712	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ ℝ) → --((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
52	8	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → e ∈ ℝ)
53		0re 10977	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℝ
54		epos 15916	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < e
55	53, 8, 54	ltleii 11098	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ≤ e
56	55	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → 0 ≤ e)
57		renegcl 11284	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → -𝑥 ∈ ℝ)
58	52, 56, 57	recxpcld 25878	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → (e↑_𝑐-𝑥) ∈ ℝ)
59	58	renegcld 11402	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → -(e↑_𝑐-𝑥) ∈ ℝ)
60	59	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -(e↑_𝑐-𝑥) ∈ ℝ)
61		reelprrecn 10963	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℝ ∈ {ℝ, ℂ}
62	61	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → ℝ ∈ {ℝ, ℂ})
63		cnelprrecn 10964	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℂ ∈ {ℝ, ℂ}
64	63	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → ℂ ∈ {ℝ, ℂ})
65	12	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → -𝑥 ∈ ℂ)
66		neg1rr 12088	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -1 ∈ ℝ
67	66	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → -1 ∈ ℝ)
68	9	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℂ → e ∈ ℂ)
69		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
70	68, 69	cxpcld 25863	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ℂ → (e↑_𝑐𝑦) ∈ ℂ)
71	70	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑦 ∈ ℂ) → (e↑_𝑐𝑦) ∈ ℂ)
72	11	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
73		1red 10976	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
74	62	dvmptid 25121	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
75	62, 72, 73, 74	dvmptneg 25130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ -𝑥)) = (𝑥 ∈ ℝ ↦ -1))
76		epr 15917	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ e ∈ ℝ⁺
77		dvcxp2 25894	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (e ∈ ℝ⁺ → (ℂ D (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑_𝑐𝑦))))
78	76, 77	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℂ D (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑_𝑐𝑦)))
79		loge 25742	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (log‘e) = 1
80	79	oveq1i 7285	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((log‘e) · (e↑_𝑐𝑦)) = (1 · (e↑_𝑐𝑦))
81	70	mulid2d 10993	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ ℂ → (1 · (e↑_𝑐𝑦)) = (e↑_𝑐𝑦))
82	80, 81	eqtrid 2790	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ℂ → ((log‘e) · (e↑_𝑐𝑦)) = (e↑_𝑐𝑦))
83	82	mpteq2ia 5177	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))
84	78, 83	eqtri 2766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℂ D (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))
85	84	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)))
86		oveq2 7283	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = -𝑥 → (e↑_𝑐𝑦) = (e↑_𝑐-𝑥))
87	62, 64, 65, 67, 71, 71, 75, 85, 86, 86	dvmptco 25136	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ (e↑_𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -1)))
88	87	mptru 1546	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℝ D (𝑥 ∈ ℝ ↦ (e↑_𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -1))
89	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → -1 ∈ ℝ)
90	89	recnd 11003	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → -1 ∈ ℂ)
91	13, 90	mulcomd 10996	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → ((e↑_𝑐-𝑥) · -1) = (-1 · (e↑_𝑐-𝑥)))
92	13	mulm1d 11427	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → (-1 · (e↑_𝑐-𝑥)) = -(e↑_𝑐-𝑥))
93	91, 92	eqtrd 2778	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → ((e↑_𝑐-𝑥) · -1) = -(e↑_𝑐-𝑥))
94	93	mpteq2ia 5177	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -1)) = (𝑥 ∈ ℝ ↦ -(e↑_𝑐-𝑥))
95	88, 94	eqtri 2766	. . . . . . . . . . . . . . . . . 18 ⊢ (ℝ D (𝑥 ∈ ℝ ↦ (e↑_𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ -(e↑_𝑐-𝑥))
96	95	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (e↑_𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ -(e↑_𝑐-𝑥)))
97	17	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → 𝑖 ∈ ℕ₀)
98		peano2nn0 12273	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ ℕ₀ → (𝑖 + 1) ∈ ℕ₀)
99	97, 98	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → (𝑖 + 1) ∈ ℕ₀)
100		ovex 7308	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 + 1) ∈ V
101		eleq1 2826	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = (𝑖 + 1) → (𝑗 ∈ ℕ₀ ↔ (𝑖 + 1) ∈ ℕ₀))
102	101	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = (𝑖 + 1) → ((𝜑 ∧ 𝑗 ∈ ℕ₀) ↔ (𝜑 ∧ (𝑖 + 1) ∈ ℕ₀)))
103		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = (𝑖 + 1) → ((ℝ D^𝑛 𝐹)‘𝑗) = ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)))
104	103	feq1d 6585	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = (𝑖 + 1) → (((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ ↔ ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ))
105	102, 104	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖 + 1) → (((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ) ↔ ((𝜑 ∧ (𝑖 + 1) ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)))
106		eleq1 2826	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑗 → (𝑖 ∈ ℕ₀ ↔ 𝑗 ∈ ℕ₀))
107	106	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ ℕ₀) ↔ (𝜑 ∧ 𝑗 ∈ ℕ₀)))
108		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑗 → ((ℝ D^𝑛 𝐹)‘𝑖) = ((ℝ D^𝑛 𝐹)‘𝑗))
109	108	feq1d 6585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑗 → (((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ ↔ ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ))
110	107, 109	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ) ↔ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ)))
111	110, 32	chvarvv 2002	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
112	100, 105, 111	vtocl 3498	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑖 + 1) ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
113	99, 112	syldan 591	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
114	113	adantlr 712	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
115	114, 35	ffvelrnd 6962	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ)
116	16, 115	fsumcl 15445	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ)
117	21, 28, 30, 38	etransclem39 43814	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐺:ℝ⟶ℂ)
118	117	feqmptd 6837	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)))
119	118	eqcomd 2744	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)) = 𝐺)
120	119	oveq2d 7291	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝐺‘𝑥))) = (ℝ D 𝐺))
121		nfcv 2907	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥𝐹
122		elfznn0 13349	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0...(𝑅 + 1)) → 𝑖 ∈ ℕ₀)
123	122, 32	sylan2 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑅 + 1))) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
124	121, 46, 123, 38	etransclem2 43777	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℝ D 𝐺) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
125	120, 124	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝐺‘𝑥))) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
126	6, 14, 60, 96, 41, 116, 125	dvmptmul 25125	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ ℝ ↦ ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥)))))
127	116, 14	mulcomd 10996	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥)) = ((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
128	127	oveq2d 7291	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥))) = ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + ((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥))))
129	14	negcld 11319	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -(e↑_𝑐-𝑥) ∈ ℂ)
130	129, 41	mulcld 10995	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) ∈ ℂ)
131	14, 116	mulcld 10995	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) ∈ ℂ)
132	130, 131	addcomd 11177	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + ((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) = (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑_𝑐-𝑥) · (𝐺‘𝑥))))
133	131, 42	negsubd 11338	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + -((e↑_𝑐-𝑥) · (𝐺‘𝑥))) = (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) − ((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
134	14, 41	mulneg1d 11428	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))
135	134	oveq2d 7291	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑_𝑐-𝑥) · (𝐺‘𝑥))) = (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + -((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
136	14, 116, 41	subdid 11431	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥))) = (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) − ((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
137	133, 135, 136	3eqtr4d 2788	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑_𝑐-𝑥) · (𝐺‘𝑥))) = ((e↑_𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥))))
138	40	oveq2d 7291	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥)) = (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)))
139	16, 115, 36	fsumsub 15500	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)((((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)) = (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)))
140		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 𝑖 → ((ℝ D^𝑛 𝐹)‘𝑗) = ((ℝ D^𝑛 𝐹)‘𝑖))
141	140	fveq1d 6776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 𝑖 → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
142	103	fveq1d 6776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖 + 1) → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥))
143		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 0 → ((ℝ D^𝑛 𝐹)‘𝑗) = ((ℝ D^𝑛 𝐹)‘0))
144	143	fveq1d 6776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 0 → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D^𝑛 𝐹)‘0)‘𝑥))
145		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = (𝑅 + 1) → ((ℝ D^𝑛 𝐹)‘𝑗) = ((ℝ D^𝑛 𝐹)‘(𝑅 + 1)))
146	145	fveq1d 6776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑅 + 1) → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥))
147		etransclem46.r	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑅 = ((𝑀 · 𝑃) + (𝑃 − 1))
148	21	nnnn0d 12293	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
149	28, 148	nn0mulcld 12298	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℕ₀)
150		nnm1nn0 12274	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
151	21, 150	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑃 − 1) ∈ ℕ₀)
152	149, 151	nn0addcld 12297	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) ∈ ℕ₀)
153	147, 152	eqeltrid 2843	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
154	153	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑅 ∈ ℕ₀)
155	154	nn0zd 12424	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑅 ∈ ℤ)
156		peano2nn0 12273	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑅 ∈ ℕ₀ → (𝑅 + 1) ∈ ℕ₀)
157	153, 156	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑅 + 1) ∈ ℕ₀)
158		nn0uz 12620	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℕ₀ = (ℤ_≥‘0)
159	157, 158	eleqtrdi 2849	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑅 + 1) ∈ (ℤ_≥‘0))
160	159	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑅 + 1) ∈ (ℤ_≥‘0))
161		elfznn0 13349	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 ∈ (0...(𝑅 + 1)) → 𝑗 ∈ ℕ₀)
162	161, 111	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
163	162	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
164		simplr 766	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → 𝑥 ∈ ℝ)
165	163, 164	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) ∈ ℂ)
166	141, 142, 144, 146, 155, 160, 165	telfsum2 15517	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)((((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)) = ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥)))
167	138, 139, 166	3eqtr2d 2784	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥)) = ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥)))
168	167	oveq2d 7291	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥))) = ((e↑_𝑐-𝑥) · ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥))))
169	153	nn0red 12294	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑅 ∈ ℝ)
170	169	ltp1d 11905	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑅 < (𝑅 + 1))
171	147, 170	eqbrtrrid 5110	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) < (𝑅 + 1))
172		etransclem5 43780	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))
173	6, 19, 21, 28, 30, 157, 171, 172	etransclem32 43807	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘(𝑅 + 1)) = (𝑥 ∈ ℝ ↦ 0))
174	173	fveq1d 6776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) = ((𝑥 ∈ ℝ ↦ 0)‘𝑥))
175		eqid 2738	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℝ ↦ 0) = (𝑥 ∈ ℝ ↦ 0)
176	175	fvmpt2 6886	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℝ ∧ 0 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ 0)‘𝑥) = 0)
177	53, 176	mpan2 688	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → ((𝑥 ∈ ℝ ↦ 0)‘𝑥) = 0)
178	174, 177	sylan9eq 2798	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) = 0)
179		cnex 10952	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ℂ ∈ V
180	179	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ℂ ∈ V)
181		etransclem46.rex	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ℝ ⊆ ℝ)
182	6, 181	ssexd 5248	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ℝ ∈ V)
183		elpm2r 8633	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:ℝ⟶ℂ ∧ ℝ ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑_pm ℝ))
184	180, 182, 46, 181, 183	syl22anc 836	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐹 ∈ (ℂ ↑_pm ℝ))
185		dvn0 25088	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℝ ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm ℝ)) → ((ℝ D^𝑛 𝐹)‘0) = 𝐹)
186	45, 184, 185	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘0) = 𝐹)
187	186	fveq1d 6776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘0)‘𝑥) = (𝐹‘𝑥))
188	187	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((ℝ D^𝑛 𝐹)‘0)‘𝑥) = (𝐹‘𝑥))
189	178, 188	oveq12d 7293	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥)) = (0 − (𝐹‘𝑥)))
190		df-neg 11208	. . . . . . . . . . . . . . . . . . . . 21 ⊢ -(𝐹‘𝑥) = (0 − (𝐹‘𝑥))
191	189, 190	eqtr4di 2796	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥)) = -(𝐹‘𝑥))
192	191	oveq2d 7291	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥))) = ((e↑_𝑐-𝑥) · -(𝐹‘𝑥)))
193	137, 168, 192	3eqtrd 2782	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑_𝑐-𝑥) · (𝐺‘𝑥))) = ((e↑_𝑐-𝑥) · -(𝐹‘𝑥)))
194	128, 132, 193	3eqtrd 2782	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥))) = ((e↑_𝑐-𝑥) · -(𝐹‘𝑥)))
195	194	mpteq2dva 5174	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥)))) = (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -(𝐹‘𝑥))))
196	14, 47	mulneg2d 11429	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · -(𝐹‘𝑥)) = -((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
197	196	mpteq2dva 5174	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -(𝐹‘𝑥))) = (𝑥 ∈ ℝ ↦ -((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
198	126, 195, 197	3eqtrd 2782	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ ℝ ↦ -((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
199	6, 42, 49, 198	dvmptneg 25130	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ ℝ ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
200	199	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D (𝑥 ∈ ℝ ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ ℝ ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
201		0red 10978	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ)
202		elfzelz 13256	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
203	202	zred 12426	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
204	203	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ)
205	201, 204	iccssred 13166	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℝ)
206		eqid 2738	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
207	206	tgioo2 23966	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
208		0red 10978	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 0 ∈ ℝ)
209		iccntr 23984	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ ∧ 𝑗 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
210	208, 203, 209	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
211	210	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
212	7, 44, 51, 200, 205, 207, 206, 211	dvmptres2 25126	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ (0(,)𝑗) ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
213	9	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → e ∈ ℂ)
214		elioore 13109	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℝ)
215	214	recnd 11003	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℂ)
216	215	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℂ)
217	216	negcld 11319	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℂ)
218	213, 217	cxpcld 25863	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) ∈ ℂ)
219	46	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝐹:ℝ⟶ℂ)
220	214	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
221	219, 220	ffvelrnd 6962	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) ∈ ℂ)
222	218, 221	mulcld 10995	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
223	222	negnegd 11323	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → --((e↑_𝑐-𝑥) · (𝐹‘𝑥)) = ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
224	223	mpteq2dva 5174	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (0(,)𝑗) ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
225	224	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
226	5, 212, 225	3eqtrd 2782	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
227	226	fveq1d 6776	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((ℝ D 𝑂)‘𝑥) = ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥))
228	227	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((ℝ D 𝑂)‘𝑥) = ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥))
229		simpr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ (0(,)𝑗))
230		eqid 2738	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
231	230	fvmpt2 6886	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥) = ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
232	229, 222, 231	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥) = ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
233	232	adantlr 712	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥) = ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
234	228, 233	eqtr2d 2779	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) = ((ℝ D 𝑂)‘𝑥))
235	234	itgeq2dv 24946	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥 = ∫(0(,)𝑗)((ℝ D 𝑂)‘𝑥) d𝑥)
236		elfzle1 13259	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
237	236	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ 𝑗)
238		eqid 2738	. . . . . . . . . 10 ⊢ (𝑥 ∈ (0[,]𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = (𝑥 ∈ (0[,]𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
239		eqidd 2739	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)) = (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)))
240	86	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) ∧ 𝑦 = -𝑥) → (e↑_𝑐𝑦) = (e↑_𝑐-𝑥))
241	208, 203	iccssred 13166	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑀) → (0[,]𝑗) ⊆ ℝ)
242		ax-resscn 10928	. . . . . . . . . . . . . . . . . . 19 ⊢ ℝ ⊆ ℂ
243	241, 242	sstrdi 3933	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → (0[,]𝑗) ⊆ ℂ)
244	243	sselda 3921	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℂ)
245	244	negcld 11319	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → -𝑥 ∈ ℂ)
246	9	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → e ∈ ℂ)
247		negcl 11221	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → -𝑥 ∈ ℂ)
248	246, 247	cxpcld 25863	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → (e↑_𝑐-𝑥) ∈ ℂ)
249	244, 248	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑_𝑐-𝑥) ∈ ℂ)
250	239, 240, 245, 249	fvmptd 6882	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥) = (e↑_𝑐-𝑥))
251	250	eqcomd 2744	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑_𝑐-𝑥) = ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥))
252	251	adantll 711	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑_𝑐-𝑥) = ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥))
253	252	mpteq2dva 5174	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (e↑_𝑐-𝑥)) = (𝑥 ∈ (0[,]𝑗) ↦ ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥)))
254		mnfxr 11032	. . . . . . . . . . . . . . . . . 18 ⊢ -∞ ∈ ℝ^*
255	254	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℝ⁺ → -∞ ∈ ℝ^*)
256		0red 10978	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℝ⁺ → 0 ∈ ℝ)
257		rpxr 12739	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℝ⁺ → e ∈ ℝ^*)
258		rpgt0 12742	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℝ⁺ → 0 < e)
259	255, 256, 257, 258	gtnelioc 43029	. . . . . . . . . . . . . . . 16 ⊢ (e ∈ ℝ⁺ → ¬ e ∈ (-∞(,]0))
260	76, 259	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ¬ e ∈ (-∞(,]0)
261		eldif 3897	. . . . . . . . . . . . . . 15 ⊢ (e ∈ (ℂ ∖ (-∞(,]0)) ↔ (e ∈ ℂ ∧ ¬ e ∈ (-∞(,]0)))
262	9, 260, 261	mpbir2an 708	. . . . . . . . . . . . . 14 ⊢ e ∈ (ℂ ∖ (-∞(,]0))
263		cxpcncf2 43440	. . . . . . . . . . . . . 14 ⊢ (e ∈ (ℂ ∖ (-∞(,]0)) → (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)) ∈ (ℂ–cn→ℂ))
264	262, 263	mp1i 13	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)) ∈ (ℂ–cn→ℂ))
265		eqid 2738	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) = (𝑥 ∈ (0[,]𝑗) ↦ -𝑥)
266	265	negcncf 24085	. . . . . . . . . . . . . . 15 ⊢ ((0[,]𝑗) ⊆ ℂ → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
267	243, 266	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
268	267	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
269	264, 268	cncfmpt1f 24077	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
270	253, 269	eqeltrd 2839	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (e↑_𝑐-𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
271	242	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → ℝ ⊆ ℂ)
272	21	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ)
273	28	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑀 ∈ ℕ₀)
274		etransclem6 43781	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦 − 𝑘)↑𝑃)))
275	30, 274	eqtri 2766	. . . . . . . . . . . . . 14 ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦 − 𝑘)↑𝑃)))
276	241	sselda 3921	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℝ)
277	276	adantll 711	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℝ)
278	271, 272, 273, 275, 277	etransclem13 43788	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝐹‘𝑥) = ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))
279	278	mpteq2dva 5174	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐹‘𝑥)) = (𝑥 ∈ (0[,]𝑗) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))))
280	243	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℂ)
281		fzfid 13693	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0...𝑀) ∈ Fin)
282	277	recnd 11003	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℂ)
283	282	3adant3 1131	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → 𝑥 ∈ ℂ)
284		elfzelz 13256	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ)
285	284	zcnd 12427	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ)
286	285	3ad2ant3 1134	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
287	283, 286	subcld 11332	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 − 𝑘) ∈ ℂ)
288	21	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ)
289	288, 150	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗)) → (𝑃 − 1) ∈ ℕ₀)
290	148	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ₀)
291	289, 290	ifcld 4505	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
292	291	3adant3 1131	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
293	292	3adant1r 1176	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
294	287, 293	expcld 13864	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) ∈ ℂ)
295		nfv 1917	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀))
296	243	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℂ)
297		ssid 3943	. . . . . . . . . . . . . . . . . 18 ⊢ ℂ ⊆ ℂ
298	297	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
299	296, 298	idcncfg 43414	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ 𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
300	285	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
301	296, 300, 298	constcncfg 43413	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ 𝑘) ∈ ((0[,]𝑗)–cn→ℂ))
302	299, 301	subcncf 24609	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝑥 − 𝑘)) ∈ ((0[,]𝑗)–cn→ℂ))
303	302	adantll 711	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝑥 − 𝑘)) ∈ ((0[,]𝑗)–cn→ℂ))
304	151, 148	ifcld 4505	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
305		expcncf 24089	. . . . . . . . . . . . . . . 16 ⊢ (if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀ → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
306	304, 305	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
307	306	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
308	297	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
309		oveq1 7282	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 − 𝑘) → (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) = ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))
310	295, 303, 307, 308, 309	cncfcompt2 24071	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((0[,]𝑗)–cn→ℂ))
311	280, 281, 294, 310	fprodcncf 43441	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((0[,]𝑗)–cn→ℂ))
312	279, 311	eqeltrd 2839	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐹‘𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
313	270, 312	mulcncf 24610	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
314		ioossicc 13165	. . . . . . . . . . 11 ⊢ (0(,)𝑗) ⊆ (0[,]𝑗)
315	314	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0(,)𝑗) ⊆ (0[,]𝑗))
316	297	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
317	222	adantlr 712	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
318	238, 313, 315, 316, 317	cncfmptssg 43412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ ((0(,)𝑗)–cn→ℂ))
319	226, 318	eqeltrd 2839	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) ∈ ((0(,)𝑗)–cn→ℂ))
320	19	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
321	21	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑃 ∈ ℕ)
322	28	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℕ₀)
323		oveq2 7283	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑘 → (𝑥 − 𝑗) = (𝑥 − 𝑘))
324	323	oveq1d 7290	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → ((𝑥 − 𝑗)↑𝑃) = ((𝑥 − 𝑘)↑𝑃))
325	324	cbvprodv 15626	. . . . . . . . . . . . 13 ⊢ ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃) = ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)
326	325	oveq2i 7286	. . . . . . . . . . . 12 ⊢ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)) = ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃))
327	326	mpteq2i 5179	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))
328	30, 327	eqtri 2766	. . . . . . . . . 10 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))
329	7, 320, 321, 322, 328, 201, 204	etransclem18 43793	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ 𝐿¹)
330	226, 329	eqeltrd 2839	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) ∈ 𝐿¹)
331		eqid 2738	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)) = (𝑥 ∈ ℝ ↦ (𝐺‘𝑥))
332	6, 19, 21, 28, 30, 38	etransclem43 43818	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 ∈ (ℝ–cn→ℂ))
333	119, 332	eqeltrd 2839	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)) ∈ (ℝ–cn→ℂ))
334	333	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)) ∈ (ℝ–cn→ℂ))
335	117	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝐺:ℝ⟶ℂ)
336	335, 277	ffvelrnd 6962	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝐺‘𝑥) ∈ ℂ)
337	331, 334, 205, 316, 336	cncfmptssg 43412	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐺‘𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
338	270, 337	mulcncf 24610	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐺‘𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
339	338	negcncfg 43422	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
340	3, 339	eqeltrid 2843	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑂 ∈ ((0[,]𝑗)–cn→ℂ))
341	201, 204, 237, 319, 330, 340	ftc2 25208	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((ℝ D 𝑂)‘𝑥) d𝑥 = ((𝑂‘𝑗) − (𝑂‘0)))
342		negeq 11213	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑗 → -𝑥 = -𝑗)
343	342	oveq2d 7291	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → (e↑_𝑐-𝑥) = (e↑_𝑐-𝑗))
344		fveq2 6774	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → (𝐺‘𝑥) = (𝐺‘𝑗))
345	343, 344	oveq12d 7293	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → ((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))
346	345	negeqd 11215	. . . . . . . . . 10 ⊢ (𝑥 = 𝑗 → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -((e↑_𝑐-𝑗) · (𝐺‘𝑗)))
347	201	rexrd 11025	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ^*)
348	204	rexrd 11025	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ^*)
349		ubicc2 13197	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ^* ∧ 𝑗 ∈ ℝ^* ∧ 0 ≤ 𝑗) → 𝑗 ∈ (0[,]𝑗))
350	347, 348, 237, 349	syl3anc 1370	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0[,]𝑗))
351	9	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → e ∈ ℂ)
352	203	recnd 11003	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
353	352	negcld 11319	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → -𝑗 ∈ ℂ)
354	351, 353	cxpcld 25863	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐-𝑗) ∈ ℂ)
355	354	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑_𝑐-𝑗) ∈ ℂ)
356	117	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐺:ℝ⟶ℂ)
357	356, 204	ffvelrnd 6962	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐺‘𝑗) ∈ ℂ)
358	355, 357	mulcld 10995	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((e↑_𝑐-𝑗) · (𝐺‘𝑗)) ∈ ℂ)
359	358	negcld 11319	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → -((e↑_𝑐-𝑗) · (𝐺‘𝑗)) ∈ ℂ)
360	3, 346, 350, 359	fvmptd3 6898	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑂‘𝑗) = -((e↑_𝑐-𝑗) · (𝐺‘𝑗)))
361	3	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑂 = (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
362		negeq 11213	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 0 → -𝑥 = -0)
363	362	oveq2d 7291	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 0 → (e↑_𝑐-𝑥) = (e↑_𝑐-0))
364		neg0 11267	. . . . . . . . . . . . . . . . 17 ⊢ -0 = 0
365	364	oveq2i 7286	. . . . . . . . . . . . . . . 16 ⊢ (e↑_𝑐-0) = (e↑_𝑐0)
366		cxp0 25825	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℂ → (e↑_𝑐0) = 1)
367	9, 366	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (e↑_𝑐0) = 1
368	365, 367	eqtri 2766	. . . . . . . . . . . . . . 15 ⊢ (e↑_𝑐-0) = 1
369	363, 368	eqtrdi 2794	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 0 → (e↑_𝑐-𝑥) = 1)
370		fveq2 6774	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 0 → (𝐺‘𝑥) = (𝐺‘0))
371	369, 370	oveq12d 7293	. . . . . . . . . . . . 13 ⊢ (𝑥 = 0 → ((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = (1 · (𝐺‘0)))
372		0red 10978	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ ℝ)
373	117, 372	ffvelrnd 6962	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺‘0) ∈ ℂ)
374	373	mulid2d 10993	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 · (𝐺‘0)) = (𝐺‘0))
375	371, 374	sylan9eqr 2800	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 = 0) → ((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = (𝐺‘0))
376	375	negeqd 11215	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = 0) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -(𝐺‘0))
377	376	adantlr 712	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 = 0) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -(𝐺‘0))
378		lbicc2 13196	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ^* ∧ 𝑗 ∈ ℝ^* ∧ 0 ≤ 𝑗) → 0 ∈ (0[,]𝑗))
379	347, 348, 237, 378	syl3anc 1370	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ (0[,]𝑗))
380	373	negcld 11319	. . . . . . . . . . 11 ⊢ (𝜑 → -(𝐺‘0) ∈ ℂ)
381	380	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → -(𝐺‘0) ∈ ℂ)
382	361, 377, 379, 381	fvmptd 6882	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑂‘0) = -(𝐺‘0))
383	360, 382	oveq12d 7293	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑂‘𝑗) − (𝑂‘0)) = (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) − -(𝐺‘0)))
384	373	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐺‘0) ∈ ℂ)
385	359, 384	subnegd 11339	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) − -(𝐺‘0)) = (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) + (𝐺‘0)))
386	359, 384	addcomd 11177	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) + (𝐺‘0)) = ((𝐺‘0) + -((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
387	384, 358	negsubd 11338	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐺‘0) + -((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
388	386, 387	eqtrd 2778	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) + (𝐺‘0)) = ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
389	383, 385, 388	3eqtrd 2782	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑂‘𝑗) − (𝑂‘0)) = ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
390	235, 341, 389	3eqtrd 2782	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥 = ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
391	390	oveq2d 7291	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) = (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
392	25	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑄 ∈ (Poly‘ℤ))
393		0zd 12331	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℤ)
394		etransclem46.a	. . . . . . . . . . 11 ⊢ 𝐴 = (coeff‘𝑄)
395	394	coef2 25392	. . . . . . . . . 10 ⊢ ((𝑄 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → 𝐴:ℕ₀⟶ℤ)
396	392, 393, 395	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐴:ℕ₀⟶ℤ)
397		elfznn0 13349	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ₀)
398	397	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ₀)
399	396, 398	ffvelrnd 6962	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℤ)
400	399	zcnd 12427	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℂ)
401	351, 352	cxpcld 25863	. . . . . . . 8 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐𝑗) ∈ ℂ)
402	401	adantl 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑_𝑐𝑗) ∈ ℂ)
403	400, 402	mulcld 10995	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑_𝑐𝑗)) ∈ ℂ)
404	403, 384, 358	subdid 11431	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))) = ((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
405	391, 404	eqtrd 2778	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) = ((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
406	405	sumeq2dv 15415	. . 3 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) = Σ𝑗 ∈ (0...𝑀)((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
407		fzfid 13693	. . . . 5 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
408	403, 384	mulcld 10995	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) ∈ ℂ)
409	403, 358	mulcld 10995	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) ∈ ℂ)
410	407, 408, 409	fsumsub 15500	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))) = (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
411		etransclem46.qe0	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘e) = 0)
412	411	eqcomd 2744	. . . . . . . 8 ⊢ (𝜑 → 0 = (𝑄‘e))
413	394, 23	coeid2 25400	. . . . . . . . 9 ⊢ ((𝑄 ∈ (Poly‘ℤ) ∧ e ∈ ℂ) → (𝑄‘e) = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑𝑗)))
414	25, 9, 413	sylancl 586	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘e) = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑𝑗)))
415		cxpexp 25823	. . . . . . . . . . . . 13 ⊢ ((e ∈ ℂ ∧ 𝑗 ∈ ℕ₀) → (e↑_𝑐𝑗) = (e↑𝑗))
416	351, 397, 415	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐𝑗) = (e↑𝑗))
417	416	eqcomd 2744	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑀) → (e↑𝑗) = (e↑_𝑐𝑗))
418	417	oveq2d 7291	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...𝑀) → ((𝐴‘𝑗) · (e↑𝑗)) = ((𝐴‘𝑗) · (e↑_𝑐𝑗)))
419	418	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑𝑗)) = ((𝐴‘𝑗) · (e↑_𝑐𝑗)))
420	419	sumeq2dv 15415	. . . . . . . 8 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑𝑗)) = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑_𝑐𝑗)))
421	412, 414, 420	3eqtrd 2782	. . . . . . 7 ⊢ (𝜑 → 0 = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑_𝑐𝑗)))
422	421	oveq1d 7290	. . . . . 6 ⊢ (𝜑 → (0 · (𝐺‘0)) = (Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)))
423	373	mul02d 11173	. . . . . 6 ⊢ (𝜑 → (0 · (𝐺‘0)) = 0)
424	407, 373, 403	fsummulc1 15497	. . . . . 6 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)))
425	422, 423, 424	3eqtr3rd 2787	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) = 0)
426		fveq2 6774	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) = (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
427	426	sumeq2sdv 15416	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
428		fzfid 13693	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0...𝑅) ∈ Fin)
429	33	adantlr 712	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
430	204	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → 𝑗 ∈ ℝ)
431	429, 430	ffvelrnd 6962	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
432	428, 431	fsumcl 15445	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
433	38, 427, 204, 432	fvmptd3 6898	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐺‘𝑗) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
434	433	oveq2d 7291	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((e↑_𝑐-𝑗) · (𝐺‘𝑗)) = ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
435	434	oveq2d 7291	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))))
436	355, 432	mulcld 10995	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) ∈ ℂ)
437	400, 402, 436	mulassd 10998	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))) = ((𝐴‘𝑗) · ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))))
438	367	eqcomi 2747	. . . . . . . . . . . . . . 15 ⊢ 1 = (e↑_𝑐0)
439	438	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → 1 = (e↑_𝑐0))
440	352	negidd 11322	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 + -𝑗) = 0)
441	440	eqcomd 2744	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 0 = (𝑗 + -𝑗))
442	441	oveq2d 7291	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐0) = (e↑_𝑐(𝑗 + -𝑗)))
443	53, 54	gtneii 11087	. . . . . . . . . . . . . . . 16 ⊢ e ≠ 0
444	443	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → e ≠ 0)
445	351, 444, 352, 353	cxpaddd 25872	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐(𝑗 + -𝑗)) = ((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)))
446	439, 442, 445	3eqtrd 2782	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → 1 = ((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)))
447	446	oveq1d 7290	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = (((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
448	447	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = (((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
449	432	mulid2d 10993	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
450	402, 355, 432	mulassd 10998	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))))
451	448, 449, 450	3eqtr3rd 2787	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
452	451	oveq2d 7291	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))) = ((𝐴‘𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
453	428, 400, 431	fsummulc2 15496	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
454	452, 453	eqtrd 2778	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))) = Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
455	435, 437, 454	3eqtrd 2782	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
456	455	sumeq2dv 15415	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = Σ𝑗 ∈ (0...𝑀)Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
457		vex 3436	. . . . . . . . . 10 ⊢ 𝑗 ∈ V
458		vex 3436	. . . . . . . . . 10 ⊢ 𝑖 ∈ V
459	457, 458	op1std 7841	. . . . . . . . 9 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → (1^st ‘𝑘) = 𝑗)
460	459	fveq2d 6778	. . . . . . . 8 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → (𝐴‘(1^st ‘𝑘)) = (𝐴‘𝑗))
461	457, 458	op2ndd 7842	. . . . . . . . . 10 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → (2^nd ‘𝑘) = 𝑖)
462	461	fveq2d 6778	. . . . . . . . 9 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → ((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘)) = ((ℝ D^𝑛 𝐹)‘𝑖))
463	462, 459	fveq12d 6781	. . . . . . . 8 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘)) = (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
464	460, 463	oveq12d 7293	. . . . . . 7 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → ((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) = ((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
465		fzfid 13693	. . . . . . 7 ⊢ (𝜑 → (0...𝑅) ∈ Fin)
466	400	adantrr 714	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → (𝐴‘𝑗) ∈ ℂ)
467	431	anasss 467	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
468	466, 467	mulcld 10995	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → ((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) ∈ ℂ)
469	464, 407, 465, 468	fsumxp 15484	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
470	456, 469	eqtrd 2778	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
471	425, 470	oveq12d 7293	. . . 4 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))) = (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘)))))
472		df-neg 11208	. . . . . 6 ⊢ -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) = (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
473	472	eqcomi 2747	. . . . 5 ⊢ (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘)))) = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘)))
474	473	a1i 11	. . . 4 ⊢ (𝜑 → (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘)))) = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
475	410, 471, 474	3eqtrd 2782	. . 3 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))) = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
476	2, 406, 475	3eqtrd 2782	. 2 ⊢ (𝜑 → 𝐿 = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
477	476	oveq1d 7290	1 ⊢ (𝜑 → (𝐿 / (!‘(𝑃 − 1))) = (-Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) / (!‘(𝑃 − 1))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ⊤wtru 1540 ∈ wcel 2106 ≠ wne 2943 Vcvv 3432 ∖ cdif 3884 ⊆ wss 3887 ifcif 4459 {csn 4561 {cpr 4563 ⟨cop 4567 class class class wbr 5074 ↦ cmpt 5157 × cxp 5587 ran crn 5590 ⟶wf 6429 ‘cfv 6433 (class class class)co 7275 1^st c1st 7829 2^nd c2nd 7830 ↑_pm cpm 8616 ℂcc 10869 ℝcr 10870 0cc0 10871 1c1 10872 + caddc 10874 · cmul 10876 -∞cmnf 11007 ℝ^*cxr 11008 < clt 11009 ≤ cle 11010 − cmin 11205 -cneg 11206 / cdiv 11632 ℕcn 11973 ℕ₀cn0 12233 ℤcz 12319 ℤ_≥cuz 12582 ℝ⁺crp 12730 (,)cioo 13079 (,]cioc 13080 [,]cicc 13082 ...cfz 13239 ↑cexp 13782 !cfa 13987 Σcsu 15397 ∏cprod 15615 eceu 15772 ↾_t crest 17131 TopOpenctopn 17132 topGenctg 17148 ℂ_fldccnfld 20597 intcnt 22168 –cn→ccncf 24039 𝐿¹cibl 24781 ∫citg 24782 0_𝑝c0p 24833 D cdv 25027 D^𝑛 cdvn 25028 Polycply 25345 coeffccoe 25347 degcdgr 25348 logclog 25710 ↑_𝑐ccxp 25711

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-inf2 9399 ax-cc 10191 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949 ax-addf 10950 ax-mulf 10951

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-symdif 4176 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-iin 4927 df-disj 5040 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-se 5545 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-isom 6442 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-of 7533 df-ofr 7534 df-om 7713 df-1st 7831 df-2nd 7832 df-supp 7978 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-2o 8298 df-oadd 8301 df-omul 8302 df-er 8498 df-map 8617 df-pm 8618 df-ixp 8686 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-fsupp 9129 df-fi 9170 df-sup 9201 df-inf 9202 df-oi 9269 df-dju 9659 df-card 9697 df-acn 9700 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-4 12038 df-5 12039 df-6 12040 df-7 12041 df-8 12042 df-9 12043 df-n0 12234 df-z 12320 df-dec 12438 df-uz 12583 df-q 12689 df-rp 12731 df-xneg 12848 df-xadd 12849 df-xmul 12850 df-ioo 13083 df-ioc 13084 df-ico 13085 df-icc 13086 df-fz 13240 df-fzo 13383 df-fl 13512 df-mod 13590 df-seq 13722 df-exp 13783 df-fac 13988 df-bc 14017 df-hash 14045 df-shft 14778 df-cj 14810 df-re 14811 df-im 14812 df-sqrt 14946 df-abs 14947 df-limsup 15180 df-clim 15197 df-rlim 15198 df-sum 15398 df-prod 15616 df-ef 15777 df-e 15778 df-sin 15779 df-cos 15780 df-tan 15781 df-pi 15782 df-struct 16848 df-sets 16865 df-slot 16883 df-ndx 16895 df-base 16913 df-ress 16942 df-plusg 16975 df-mulr 16976 df-starv 16977 df-sca 16978 df-vsca 16979 df-ip 16980 df-tset 16981 df-ple 16982 df-ds 16984 df-unif 16985 df-hom 16986 df-cco 16987 df-rest 17133 df-topn 17134 df-0g 17152 df-gsum 17153 df-topgen 17154 df-pt 17155 df-prds 17158 df-xrs 17213 df-qtop 17218 df-imas 17219 df-xps 17221 df-mre 17295 df-mrc 17296 df-acs 17298 df-mgm 18326 df-sgrp 18375 df-mnd 18386 df-submnd 18431 df-mulg 18701 df-cntz 18923 df-cmn 19388 df-psmet 20589 df-xmet 20590 df-met 20591 df-bl 20592 df-mopn 20593 df-fbas 20594 df-fg 20595 df-cnfld 20598 df-top 22043 df-topon 22060 df-topsp 22082 df-bases 22096 df-cld 22170 df-ntr 22171 df-cls 22172 df-nei 22249 df-lp 22287 df-perf 22288 df-cn 22378 df-cnp 22379 df-haus 22466 df-cmp 22538 df-tx 22713 df-hmeo 22906 df-fil 22997 df-fm 23089 df-flim 23090 df-flf 23091 df-xms 23473 df-ms 23474 df-tms 23475 df-cncf 24041 df-ovol 24628 df-vol 24629 df-mbf 24783 df-itg1 24784 df-itg2 24785 df-ibl 24786 df-itg 24787 df-0p 24834 df-limc 25030 df-dv 25031 df-dvn 25032 df-ply 25349 df-coe 25351 df-dgr 25352 df-log 25712 df-cxp 25713

This theorem is referenced by: etransclem47 43822

W3C validator