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 44931

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 7415	. . . . . . . . . . . . 13 ⊢ (ℝ D 𝑂) = (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
5	4	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) = (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))))
6		etransclem46.s	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
7	6	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℝ ∈ {ℝ, ℂ})
8		ere 16028	. . . . . . . . . . . . . . . . . . . 20 ⊢ e ∈ ℝ
9	8	recni 11224	. . . . . . . . . . . . . . . . . . 19 ⊢ e ∈ ℂ
10	9	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → e ∈ ℂ)
11		recn 11196	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
12	11	negcld 11554	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → -𝑥 ∈ ℂ)
13	10, 12	cxpcld 26198	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (e↑_𝑐-𝑥) ∈ ℂ)
14	13	adantl 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (e↑_𝑐-𝑥) ∈ ℂ)
15		simpr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
16		fzfid 13934	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (0...𝑅) ∈ Fin)
17		elfznn0 13590	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ (0...𝑅) → 𝑖 ∈ ℕ₀)
18	6	adantr 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → ℝ ∈ {ℝ, ℂ})
19		etransclem46.x	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
20	19	adantr 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
21		etransclem46.p	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑃 ∈ ℕ)
22	21	adantr 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → 𝑃 ∈ ℕ)
23		etransclem46.m	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑀 = (deg‘𝑄)
24		etransclem46.q	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑄 ∈ ((Poly‘ℤ) ∖ {0_𝑝}))
25	24	eldifad 3959	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑄 ∈ (Poly‘ℤ))
26		dgrcl 25729	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑄 ∈ (Poly‘ℤ) → (deg‘𝑄) ∈ ℕ₀)
27	25, 26	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (deg‘𝑄) ∈ ℕ₀)
28	23, 27	eqeltrid 2838	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
29	28	adantr 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → 𝑀 ∈ ℕ₀)
30		etransclem46.f	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))
31		simpr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → 𝑖 ∈ ℕ₀)
32	18, 20, 22, 29, 30, 31	etransclem33 44918	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
33	17, 32	sylan2 594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
34	33	adantlr 714	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
35		simplr 768	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → 𝑥 ∈ ℝ)
36	34, 35	ffvelcdmd 7083	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ)
37	16, 36	fsumcl 15675	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ)
38		etransclem46.g	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
39	38	fvmpt2 7005	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ) → (𝐺‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
40	15, 37, 39	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐺‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
41	40, 37	eqeltrd 2834	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐺‘𝑥) ∈ ℂ)
42	14, 41	mulcld 11230	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · (𝐺‘𝑥)) ∈ ℂ)
43	42	negcld 11554	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) ∈ ℂ)
44	43	adantlr 714	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ ℝ) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) ∈ ℂ)
45	6, 19	dvdmsscn 44587	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ℝ ⊆ ℂ)
46	45, 21, 30	etransclem8 44893	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
47	46	ffvelcdmda 7082	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℂ)
48	14, 47	mulcld 11230	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
49	48	negcld 11554	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
50	49	negcld 11554	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → --((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
51	50	adantlr 714	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ ℝ) → --((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
52	8	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → e ∈ ℝ)
53		0re 11212	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℝ
54		epos 16146	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < e
55	53, 8, 54	ltleii 11333	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ≤ e
56	55	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → 0 ≤ e)
57		renegcl 11519	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → -𝑥 ∈ ℝ)
58	52, 56, 57	recxpcld 26213	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → (e↑_𝑐-𝑥) ∈ ℝ)
59	58	renegcld 11637	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → -(e↑_𝑐-𝑥) ∈ ℝ)
60	59	adantl 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -(e↑_𝑐-𝑥) ∈ ℝ)
61		reelprrecn 11198	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℝ ∈ {ℝ, ℂ}
62	61	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → ℝ ∈ {ℝ, ℂ})
63		cnelprrecn 11199	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℂ ∈ {ℝ, ℂ}
64	63	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → ℂ ∈ {ℝ, ℂ})
65	12	adantl 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → -𝑥 ∈ ℂ)
66		neg1rr 12323	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -1 ∈ ℝ
67	66	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → -1 ∈ ℝ)
68	9	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℂ → e ∈ ℂ)
69		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
70	68, 69	cxpcld 26198	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ℂ → (e↑_𝑐𝑦) ∈ ℂ)
71	70	adantl 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑦 ∈ ℂ) → (e↑_𝑐𝑦) ∈ ℂ)
72	11	adantl 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
73		1red 11211	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
74	62	dvmptid 25456	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
75	62, 72, 73, 74	dvmptneg 25465	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ -𝑥)) = (𝑥 ∈ ℝ ↦ -1))
76		epr 16147	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ e ∈ ℝ⁺
77		dvcxp2 26229	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (e ∈ ℝ⁺ → (ℂ D (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑_𝑐𝑦))))
78	76, 77	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℂ D (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑_𝑐𝑦)))
79		loge 26077	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (log‘e) = 1
80	79	oveq1i 7414	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((log‘e) · (e↑_𝑐𝑦)) = (1 · (e↑_𝑐𝑦))
81	70	mullidd 11228	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ ℂ → (1 · (e↑_𝑐𝑦)) = (e↑_𝑐𝑦))
82	80, 81	eqtrid 2785	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ℂ → ((log‘e) · (e↑_𝑐𝑦)) = (e↑_𝑐𝑦))
83	82	mpteq2ia 5250	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))
84	78, 83	eqtri 2761	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℂ D (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))
85	84	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)))
86		oveq2 7412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = -𝑥 → (e↑_𝑐𝑦) = (e↑_𝑐-𝑥))
87	62, 64, 65, 67, 71, 71, 75, 85, 86, 86	dvmptco 25471	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ (e↑_𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -1)))
88	87	mptru 1549	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℝ D (𝑥 ∈ ℝ ↦ (e↑_𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -1))
89	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → -1 ∈ ℝ)
90	89	recnd 11238	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → -1 ∈ ℂ)
91	13, 90	mulcomd 11231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → ((e↑_𝑐-𝑥) · -1) = (-1 · (e↑_𝑐-𝑥)))
92	13	mulm1d 11662	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → (-1 · (e↑_𝑐-𝑥)) = -(e↑_𝑐-𝑥))
93	91, 92	eqtrd 2773	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → ((e↑_𝑐-𝑥) · -1) = -(e↑_𝑐-𝑥))
94	93	mpteq2ia 5250	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -1)) = (𝑥 ∈ ℝ ↦ -(e↑_𝑐-𝑥))
95	88, 94	eqtri 2761	. . . . . . . . . . . . . . . . . 18 ⊢ (ℝ D (𝑥 ∈ ℝ ↦ (e↑_𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ -(e↑_𝑐-𝑥))
96	95	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (e↑_𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ -(e↑_𝑐-𝑥)))
97	17	adantl 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → 𝑖 ∈ ℕ₀)
98		peano2nn0 12508	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ ℕ₀ → (𝑖 + 1) ∈ ℕ₀)
99	97, 98	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → (𝑖 + 1) ∈ ℕ₀)
100		ovex 7437	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 + 1) ∈ V
101		eleq1 2822	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = (𝑖 + 1) → (𝑗 ∈ ℕ₀ ↔ (𝑖 + 1) ∈ ℕ₀))
102	101	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = (𝑖 + 1) → ((𝜑 ∧ 𝑗 ∈ ℕ₀) ↔ (𝜑 ∧ (𝑖 + 1) ∈ ℕ₀)))
103		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = (𝑖 + 1) → ((ℝ D^𝑛 𝐹)‘𝑗) = ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)))
104	103	feq1d 6699	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = (𝑖 + 1) → (((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ ↔ ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ))
105	102, 104	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖 + 1) → (((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ) ↔ ((𝜑 ∧ (𝑖 + 1) ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)))
106		eleq1 2822	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑗 → (𝑖 ∈ ℕ₀ ↔ 𝑗 ∈ ℕ₀))
107	106	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ ℕ₀) ↔ (𝜑 ∧ 𝑗 ∈ ℕ₀)))
108		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑗 → ((ℝ D^𝑛 𝐹)‘𝑖) = ((ℝ D^𝑛 𝐹)‘𝑗))
109	108	feq1d 6699	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑗 → (((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ ↔ ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ))
110	107, 109	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ) ↔ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ)))
111	110, 32	chvarvv 2003	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
112	100, 105, 111	vtocl 3549	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑖 + 1) ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
113	99, 112	syldan 592	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
114	113	adantlr 714	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
115	114, 35	ffvelcdmd 7083	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ)
116	16, 115	fsumcl 15675	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ)
117	21, 28, 30, 38	etransclem39 44924	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐺:ℝ⟶ℂ)
118	117	feqmptd 6956	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)))
119	118	eqcomd 2739	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)) = 𝐺)
120	119	oveq2d 7420	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝐺‘𝑥))) = (ℝ D 𝐺))
121		nfcv 2904	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥𝐹
122		elfznn0 13590	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0...(𝑅 + 1)) → 𝑖 ∈ ℕ₀)
123	122, 32	sylan2 594	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑅 + 1))) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
124	121, 46, 123, 38	etransclem2 44887	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℝ D 𝐺) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
125	120, 124	eqtrd 2773	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝐺‘𝑥))) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
126	6, 14, 60, 96, 41, 116, 125	dvmptmul 25460	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ ℝ ↦ ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥)))))
127	116, 14	mulcomd 11231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥)) = ((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
128	127	oveq2d 7420	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥))) = ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + ((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥))))
129	14	negcld 11554	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -(e↑_𝑐-𝑥) ∈ ℂ)
130	129, 41	mulcld 11230	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) ∈ ℂ)
131	14, 116	mulcld 11230	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) ∈ ℂ)
132	130, 131	addcomd 11412	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + ((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) = (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑_𝑐-𝑥) · (𝐺‘𝑥))))
133	131, 42	negsubd 11573	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + -((e↑_𝑐-𝑥) · (𝐺‘𝑥))) = (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) − ((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
134	14, 41	mulneg1d 11663	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))
135	134	oveq2d 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑_𝑐-𝑥) · (𝐺‘𝑥))) = (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + -((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
136	14, 116, 41	subdid 11666	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥))) = (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) − ((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
137	133, 135, 136	3eqtr4d 2783	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑_𝑐-𝑥) · (𝐺‘𝑥))) = ((e↑_𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥))))
138	40	oveq2d 7420	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥)) = (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)))
139	16, 115, 36	fsumsub 15730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)((((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)) = (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)))
140		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 𝑖 → ((ℝ D^𝑛 𝐹)‘𝑗) = ((ℝ D^𝑛 𝐹)‘𝑖))
141	140	fveq1d 6890	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 𝑖 → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
142	103	fveq1d 6890	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖 + 1) → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥))
143		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 0 → ((ℝ D^𝑛 𝐹)‘𝑗) = ((ℝ D^𝑛 𝐹)‘0))
144	143	fveq1d 6890	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 0 → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D^𝑛 𝐹)‘0)‘𝑥))
145		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = (𝑅 + 1) → ((ℝ D^𝑛 𝐹)‘𝑗) = ((ℝ D^𝑛 𝐹)‘(𝑅 + 1)))
146	145	fveq1d 6890	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑅 + 1) → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥))
147		etransclem46.r	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑅 = ((𝑀 · 𝑃) + (𝑃 − 1))
148	21	nnnn0d 12528	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
149	28, 148	nn0mulcld 12533	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℕ₀)
150		nnm1nn0 12509	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
151	21, 150	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑃 − 1) ∈ ℕ₀)
152	149, 151	nn0addcld 12532	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) ∈ ℕ₀)
153	147, 152	eqeltrid 2838	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
154	153	adantr 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑅 ∈ ℕ₀)
155	154	nn0zd 12580	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑅 ∈ ℤ)
156		peano2nn0 12508	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑅 ∈ ℕ₀ → (𝑅 + 1) ∈ ℕ₀)
157	153, 156	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑅 + 1) ∈ ℕ₀)
158		nn0uz 12860	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℕ₀ = (ℤ_≥‘0)
159	157, 158	eleqtrdi 2844	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑅 + 1) ∈ (ℤ_≥‘0))
160	159	adantr 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑅 + 1) ∈ (ℤ_≥‘0))
161		elfznn0 13590	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 ∈ (0...(𝑅 + 1)) → 𝑗 ∈ ℕ₀)
162	161, 111	sylan2 594	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
163	162	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
164		simplr 768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → 𝑥 ∈ ℝ)
165	163, 164	ffvelcdmd 7083	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) ∈ ℂ)
166	141, 142, 144, 146, 155, 160, 165	telfsum2 15747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)((((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)) = ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥)))
167	138, 139, 166	3eqtr2d 2779	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥)) = ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥)))
168	167	oveq2d 7420	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥))) = ((e↑_𝑐-𝑥) · ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥))))
169	153	nn0red 12529	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑅 ∈ ℝ)
170	169	ltp1d 12140	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑅 < (𝑅 + 1))
171	147, 170	eqbrtrrid 5183	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) < (𝑅 + 1))
172		etransclem5 44890	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))
173	6, 19, 21, 28, 30, 157, 171, 172	etransclem32 44917	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘(𝑅 + 1)) = (𝑥 ∈ ℝ ↦ 0))
174	173	fveq1d 6890	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) = ((𝑥 ∈ ℝ ↦ 0)‘𝑥))
175		eqid 2733	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℝ ↦ 0) = (𝑥 ∈ ℝ ↦ 0)
176	175	fvmpt2 7005	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℝ ∧ 0 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ 0)‘𝑥) = 0)
177	53, 176	mpan2 690	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → ((𝑥 ∈ ℝ ↦ 0)‘𝑥) = 0)
178	174, 177	sylan9eq 2793	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) = 0)
179		cnex 11187	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ℂ ∈ V
180	179	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ℂ ∈ V)
181		etransclem46.rex	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ℝ ⊆ ℝ)
182	6, 181	ssexd 5323	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ℝ ∈ V)
183		elpm2r 8835	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:ℝ⟶ℂ ∧ ℝ ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑_pm ℝ))
184	180, 182, 46, 181, 183	syl22anc 838	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐹 ∈ (ℂ ↑_pm ℝ))
185		dvn0 25423	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℝ ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm ℝ)) → ((ℝ D^𝑛 𝐹)‘0) = 𝐹)
186	45, 184, 185	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘0) = 𝐹)
187	186	fveq1d 6890	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘0)‘𝑥) = (𝐹‘𝑥))
188	187	adantr 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((ℝ D^𝑛 𝐹)‘0)‘𝑥) = (𝐹‘𝑥))
189	178, 188	oveq12d 7422	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥)) = (0 − (𝐹‘𝑥)))
190		df-neg 11443	. . . . . . . . . . . . . . . . . . . . 21 ⊢ -(𝐹‘𝑥) = (0 − (𝐹‘𝑥))
191	189, 190	eqtr4di 2791	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥)) = -(𝐹‘𝑥))
192	191	oveq2d 7420	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥))) = ((e↑_𝑐-𝑥) · -(𝐹‘𝑥)))
193	137, 168, 192	3eqtrd 2777	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑_𝑐-𝑥) · (𝐺‘𝑥))) = ((e↑_𝑐-𝑥) · -(𝐹‘𝑥)))
194	128, 132, 193	3eqtrd 2777	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥))) = ((e↑_𝑐-𝑥) · -(𝐹‘𝑥)))
195	194	mpteq2dva 5247	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥)))) = (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -(𝐹‘𝑥))))
196	14, 47	mulneg2d 11664	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · -(𝐹‘𝑥)) = -((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
197	196	mpteq2dva 5247	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -(𝐹‘𝑥))) = (𝑥 ∈ ℝ ↦ -((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
198	126, 195, 197	3eqtrd 2777	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ ℝ ↦ -((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
199	6, 42, 49, 198	dvmptneg 25465	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ ℝ ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
200	199	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D (𝑥 ∈ ℝ ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ ℝ ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
201		0red 11213	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ)
202		elfzelz 13497	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
203	202	zred 12662	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
204	203	adantl 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ)
205	201, 204	iccssred 13407	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℝ)
206		eqid 2733	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
207	206	tgioo2 24301	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
208		0red 11213	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 0 ∈ ℝ)
209		iccntr 24319	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ ∧ 𝑗 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
210	208, 203, 209	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
211	210	adantl 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
212	7, 44, 51, 200, 205, 207, 206, 211	dvmptres2 25461	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ (0(,)𝑗) ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
213	9	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → e ∈ ℂ)
214		elioore 13350	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℝ)
215	214	recnd 11238	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℂ)
216	215	adantl 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℂ)
217	216	negcld 11554	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℂ)
218	213, 217	cxpcld 26198	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) ∈ ℂ)
219	46	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝐹:ℝ⟶ℂ)
220	214	adantl 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
221	219, 220	ffvelcdmd 7083	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) ∈ ℂ)
222	218, 221	mulcld 11230	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
223	222	negnegd 11558	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → --((e↑_𝑐-𝑥) · (𝐹‘𝑥)) = ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
224	223	mpteq2dva 5247	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (0(,)𝑗) ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
225	224	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
226	5, 212, 225	3eqtrd 2777	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
227	226	fveq1d 6890	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((ℝ D 𝑂)‘𝑥) = ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥))
228	227	adantr 482	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((ℝ D 𝑂)‘𝑥) = ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥))
229		simpr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ (0(,)𝑗))
230		eqid 2733	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
231	230	fvmpt2 7005	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥) = ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
232	229, 222, 231	syl2anc 585	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥) = ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
233	232	adantlr 714	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥) = ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
234	228, 233	eqtr2d 2774	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) = ((ℝ D 𝑂)‘𝑥))
235	234	itgeq2dv 25281	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥 = ∫(0(,)𝑗)((ℝ D 𝑂)‘𝑥) d𝑥)
236		elfzle1 13500	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
237	236	adantl 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ 𝑗)
238		eqid 2733	. . . . . . . . . 10 ⊢ (𝑥 ∈ (0[,]𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = (𝑥 ∈ (0[,]𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
239		eqidd 2734	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)) = (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)))
240	86	adantl 483	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) ∧ 𝑦 = -𝑥) → (e↑_𝑐𝑦) = (e↑_𝑐-𝑥))
241	208, 203	iccssred 13407	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑀) → (0[,]𝑗) ⊆ ℝ)
242		ax-resscn 11163	. . . . . . . . . . . . . . . . . . 19 ⊢ ℝ ⊆ ℂ
243	241, 242	sstrdi 3993	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → (0[,]𝑗) ⊆ ℂ)
244	243	sselda 3981	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℂ)
245	244	negcld 11554	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → -𝑥 ∈ ℂ)
246	9	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → e ∈ ℂ)
247		negcl 11456	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → -𝑥 ∈ ℂ)
248	246, 247	cxpcld 26198	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → (e↑_𝑐-𝑥) ∈ ℂ)
249	244, 248	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑_𝑐-𝑥) ∈ ℂ)
250	239, 240, 245, 249	fvmptd 7001	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥) = (e↑_𝑐-𝑥))
251	250	eqcomd 2739	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑_𝑐-𝑥) = ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥))
252	251	adantll 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑_𝑐-𝑥) = ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥))
253	252	mpteq2dva 5247	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (e↑_𝑐-𝑥)) = (𝑥 ∈ (0[,]𝑗) ↦ ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥)))
254		mnfxr 11267	. . . . . . . . . . . . . . . . . 18 ⊢ -∞ ∈ ℝ^*
255	254	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℝ⁺ → -∞ ∈ ℝ^*)
256		0red 11213	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℝ⁺ → 0 ∈ ℝ)
257		rpxr 12979	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℝ⁺ → e ∈ ℝ^*)
258		rpgt0 12982	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℝ⁺ → 0 < e)
259	255, 256, 257, 258	gtnelioc 44139	. . . . . . . . . . . . . . . 16 ⊢ (e ∈ ℝ⁺ → ¬ e ∈ (-∞(,]0))
260	76, 259	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ¬ e ∈ (-∞(,]0)
261		eldif 3957	. . . . . . . . . . . . . . 15 ⊢ (e ∈ (ℂ ∖ (-∞(,]0)) ↔ (e ∈ ℂ ∧ ¬ e ∈ (-∞(,]0)))
262	9, 260, 261	mpbir2an 710	. . . . . . . . . . . . . 14 ⊢ e ∈ (ℂ ∖ (-∞(,]0))
263		cxpcncf2 44550	. . . . . . . . . . . . . 14 ⊢ (e ∈ (ℂ ∖ (-∞(,]0)) → (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)) ∈ (ℂ–cn→ℂ))
264	262, 263	mp1i 13	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)) ∈ (ℂ–cn→ℂ))
265		eqid 2733	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) = (𝑥 ∈ (0[,]𝑗) ↦ -𝑥)
266	265	negcncf 24420	. . . . . . . . . . . . . . 15 ⊢ ((0[,]𝑗) ⊆ ℂ → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
267	243, 266	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
268	267	adantl 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
269	264, 268	cncfmpt1f 24412	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
270	253, 269	eqeltrd 2834	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (e↑_𝑐-𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
271	242	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → ℝ ⊆ ℂ)
272	21	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ)
273	28	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑀 ∈ ℕ₀)
274		etransclem6 44891	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦 − 𝑘)↑𝑃)))
275	30, 274	eqtri 2761	. . . . . . . . . . . . . 14 ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦 − 𝑘)↑𝑃)))
276	241	sselda 3981	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℝ)
277	276	adantll 713	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℝ)
278	271, 272, 273, 275, 277	etransclem13 44898	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝐹‘𝑥) = ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))
279	278	mpteq2dva 5247	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐹‘𝑥)) = (𝑥 ∈ (0[,]𝑗) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))))
280	243	adantl 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℂ)
281		fzfid 13934	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0...𝑀) ∈ Fin)
282	277	recnd 11238	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℂ)
283	282	3adant3 1133	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → 𝑥 ∈ ℂ)
284		elfzelz 13497	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ)
285	284	zcnd 12663	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ)
286	285	3ad2ant3 1136	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
287	283, 286	subcld 11567	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 − 𝑘) ∈ ℂ)
288	21	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ)
289	288, 150	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗)) → (𝑃 − 1) ∈ ℕ₀)
290	148	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ₀)
291	289, 290	ifcld 4573	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
292	291	3adant3 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
293	292	3adant1r 1178	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
294	287, 293	expcld 14107	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) ∈ ℂ)
295		nfv 1918	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀))
296	243	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℂ)
297		ssid 4003	. . . . . . . . . . . . . . . . . 18 ⊢ ℂ ⊆ ℂ
298	297	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
299	296, 298	idcncfg 44524	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ 𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
300	285	adantl 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
301	296, 300, 298	constcncfg 44523	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ 𝑘) ∈ ((0[,]𝑗)–cn→ℂ))
302	299, 301	subcncf 24944	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝑥 − 𝑘)) ∈ ((0[,]𝑗)–cn→ℂ))
303	302	adantll 713	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝑥 − 𝑘)) ∈ ((0[,]𝑗)–cn→ℂ))
304	151, 148	ifcld 4573	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
305		expcncf 24424	. . . . . . . . . . . . . . . 16 ⊢ (if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀ → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
306	304, 305	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
307	306	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
308	297	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
309		oveq1 7411	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 − 𝑘) → (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) = ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))
310	295, 303, 307, 308, 309	cncfcompt2 24406	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((0[,]𝑗)–cn→ℂ))
311	280, 281, 294, 310	fprodcncf 44551	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((0[,]𝑗)–cn→ℂ))
312	279, 311	eqeltrd 2834	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐹‘𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
313	270, 312	mulcncf 24945	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
314		ioossicc 13406	. . . . . . . . . . 11 ⊢ (0(,)𝑗) ⊆ (0[,]𝑗)
315	314	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0(,)𝑗) ⊆ (0[,]𝑗))
316	297	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
317	222	adantlr 714	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
318	238, 313, 315, 316, 317	cncfmptssg 44522	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ ((0(,)𝑗)–cn→ℂ))
319	226, 318	eqeltrd 2834	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) ∈ ((0(,)𝑗)–cn→ℂ))
320	19	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
321	21	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑃 ∈ ℕ)
322	28	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℕ₀)
323		oveq2 7412	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑘 → (𝑥 − 𝑗) = (𝑥 − 𝑘))
324	323	oveq1d 7419	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → ((𝑥 − 𝑗)↑𝑃) = ((𝑥 − 𝑘)↑𝑃))
325	324	cbvprodv 15856	. . . . . . . . . . . . 13 ⊢ ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃) = ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)
326	325	oveq2i 7415	. . . . . . . . . . . 12 ⊢ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)) = ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃))
327	326	mpteq2i 5252	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))
328	30, 327	eqtri 2761	. . . . . . . . . 10 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))
329	7, 320, 321, 322, 328, 201, 204	etransclem18 44903	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ 𝐿¹)
330	226, 329	eqeltrd 2834	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) ∈ 𝐿¹)
331		eqid 2733	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)) = (𝑥 ∈ ℝ ↦ (𝐺‘𝑥))
332	6, 19, 21, 28, 30, 38	etransclem43 44928	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 ∈ (ℝ–cn→ℂ))
333	119, 332	eqeltrd 2834	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)) ∈ (ℝ–cn→ℂ))
334	333	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)) ∈ (ℝ–cn→ℂ))
335	117	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝐺:ℝ⟶ℂ)
336	335, 277	ffvelcdmd 7083	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝐺‘𝑥) ∈ ℂ)
337	331, 334, 205, 316, 336	cncfmptssg 44522	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐺‘𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
338	270, 337	mulcncf 24945	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐺‘𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
339	338	negcncfg 44532	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
340	3, 339	eqeltrid 2838	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑂 ∈ ((0[,]𝑗)–cn→ℂ))
341	201, 204, 237, 319, 330, 340	ftc2 25543	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((ℝ D 𝑂)‘𝑥) d𝑥 = ((𝑂‘𝑗) − (𝑂‘0)))
342		negeq 11448	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑗 → -𝑥 = -𝑗)
343	342	oveq2d 7420	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → (e↑_𝑐-𝑥) = (e↑_𝑐-𝑗))
344		fveq2 6888	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → (𝐺‘𝑥) = (𝐺‘𝑗))
345	343, 344	oveq12d 7422	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → ((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))
346	345	negeqd 11450	. . . . . . . . . 10 ⊢ (𝑥 = 𝑗 → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -((e↑_𝑐-𝑗) · (𝐺‘𝑗)))
347	201	rexrd 11260	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ^*)
348	204	rexrd 11260	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ^*)
349		ubicc2 13438	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ^* ∧ 𝑗 ∈ ℝ^* ∧ 0 ≤ 𝑗) → 𝑗 ∈ (0[,]𝑗))
350	347, 348, 237, 349	syl3anc 1372	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0[,]𝑗))
351	9	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → e ∈ ℂ)
352	203	recnd 11238	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
353	352	negcld 11554	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → -𝑗 ∈ ℂ)
354	351, 353	cxpcld 26198	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐-𝑗) ∈ ℂ)
355	354	adantl 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑_𝑐-𝑗) ∈ ℂ)
356	117	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐺:ℝ⟶ℂ)
357	356, 204	ffvelcdmd 7083	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐺‘𝑗) ∈ ℂ)
358	355, 357	mulcld 11230	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((e↑_𝑐-𝑗) · (𝐺‘𝑗)) ∈ ℂ)
359	358	negcld 11554	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → -((e↑_𝑐-𝑗) · (𝐺‘𝑗)) ∈ ℂ)
360	3, 346, 350, 359	fvmptd3 7017	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑂‘𝑗) = -((e↑_𝑐-𝑗) · (𝐺‘𝑗)))
361	3	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑂 = (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
362		negeq 11448	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 0 → -𝑥 = -0)
363	362	oveq2d 7420	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 0 → (e↑_𝑐-𝑥) = (e↑_𝑐-0))
364		neg0 11502	. . . . . . . . . . . . . . . . 17 ⊢ -0 = 0
365	364	oveq2i 7415	. . . . . . . . . . . . . . . 16 ⊢ (e↑_𝑐-0) = (e↑_𝑐0)
366		cxp0 26160	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℂ → (e↑_𝑐0) = 1)
367	9, 366	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (e↑_𝑐0) = 1
368	365, 367	eqtri 2761	. . . . . . . . . . . . . . 15 ⊢ (e↑_𝑐-0) = 1
369	363, 368	eqtrdi 2789	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 0 → (e↑_𝑐-𝑥) = 1)
370		fveq2 6888	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 0 → (𝐺‘𝑥) = (𝐺‘0))
371	369, 370	oveq12d 7422	. . . . . . . . . . . . 13 ⊢ (𝑥 = 0 → ((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = (1 · (𝐺‘0)))
372		0red 11213	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ ℝ)
373	117, 372	ffvelcdmd 7083	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺‘0) ∈ ℂ)
374	373	mullidd 11228	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 · (𝐺‘0)) = (𝐺‘0))
375	371, 374	sylan9eqr 2795	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 = 0) → ((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = (𝐺‘0))
376	375	negeqd 11450	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = 0) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -(𝐺‘0))
377	376	adantlr 714	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 = 0) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -(𝐺‘0))
378		lbicc2 13437	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ^* ∧ 𝑗 ∈ ℝ^* ∧ 0 ≤ 𝑗) → 0 ∈ (0[,]𝑗))
379	347, 348, 237, 378	syl3anc 1372	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ (0[,]𝑗))
380	373	negcld 11554	. . . . . . . . . . 11 ⊢ (𝜑 → -(𝐺‘0) ∈ ℂ)
381	380	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → -(𝐺‘0) ∈ ℂ)
382	361, 377, 379, 381	fvmptd 7001	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑂‘0) = -(𝐺‘0))
383	360, 382	oveq12d 7422	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑂‘𝑗) − (𝑂‘0)) = (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) − -(𝐺‘0)))
384	373	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐺‘0) ∈ ℂ)
385	359, 384	subnegd 11574	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) − -(𝐺‘0)) = (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) + (𝐺‘0)))
386	359, 384	addcomd 11412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) + (𝐺‘0)) = ((𝐺‘0) + -((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
387	384, 358	negsubd 11573	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐺‘0) + -((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
388	386, 387	eqtrd 2773	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) + (𝐺‘0)) = ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
389	383, 385, 388	3eqtrd 2777	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑂‘𝑗) − (𝑂‘0)) = ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
390	235, 341, 389	3eqtrd 2777	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥 = ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
391	390	oveq2d 7420	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) = (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
392	25	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑄 ∈ (Poly‘ℤ))
393		0zd 12566	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℤ)
394		etransclem46.a	. . . . . . . . . . 11 ⊢ 𝐴 = (coeff‘𝑄)
395	394	coef2 25727	. . . . . . . . . 10 ⊢ ((𝑄 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → 𝐴:ℕ₀⟶ℤ)
396	392, 393, 395	syl2anc 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐴:ℕ₀⟶ℤ)
397		elfznn0 13590	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ₀)
398	397	adantl 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ₀)
399	396, 398	ffvelcdmd 7083	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℤ)
400	399	zcnd 12663	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℂ)
401	351, 352	cxpcld 26198	. . . . . . . 8 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐𝑗) ∈ ℂ)
402	401	adantl 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑_𝑐𝑗) ∈ ℂ)
403	400, 402	mulcld 11230	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑_𝑐𝑗)) ∈ ℂ)
404	403, 384, 358	subdid 11666	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))) = ((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
405	391, 404	eqtrd 2773	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) = ((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
406	405	sumeq2dv 15645	. . 3 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) = Σ𝑗 ∈ (0...𝑀)((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
407		fzfid 13934	. . . . 5 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
408	403, 384	mulcld 11230	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) ∈ ℂ)
409	403, 358	mulcld 11230	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) ∈ ℂ)
410	407, 408, 409	fsumsub 15730	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))) = (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
411		etransclem46.qe0	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘e) = 0)
412	411	eqcomd 2739	. . . . . . . 8 ⊢ (𝜑 → 0 = (𝑄‘e))
413	394, 23	coeid2 25735	. . . . . . . . 9 ⊢ ((𝑄 ∈ (Poly‘ℤ) ∧ e ∈ ℂ) → (𝑄‘e) = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑𝑗)))
414	25, 9, 413	sylancl 587	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘e) = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑𝑗)))
415		cxpexp 26158	. . . . . . . . . . . . 13 ⊢ ((e ∈ ℂ ∧ 𝑗 ∈ ℕ₀) → (e↑_𝑐𝑗) = (e↑𝑗))
416	351, 397, 415	syl2anc 585	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐𝑗) = (e↑𝑗))
417	416	eqcomd 2739	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑀) → (e↑𝑗) = (e↑_𝑐𝑗))
418	417	oveq2d 7420	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...𝑀) → ((𝐴‘𝑗) · (e↑𝑗)) = ((𝐴‘𝑗) · (e↑_𝑐𝑗)))
419	418	adantl 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑𝑗)) = ((𝐴‘𝑗) · (e↑_𝑐𝑗)))
420	419	sumeq2dv 15645	. . . . . . . 8 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑𝑗)) = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑_𝑐𝑗)))
421	412, 414, 420	3eqtrd 2777	. . . . . . 7 ⊢ (𝜑 → 0 = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑_𝑐𝑗)))
422	421	oveq1d 7419	. . . . . 6 ⊢ (𝜑 → (0 · (𝐺‘0)) = (Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)))
423	373	mul02d 11408	. . . . . 6 ⊢ (𝜑 → (0 · (𝐺‘0)) = 0)
424	407, 373, 403	fsummulc1 15727	. . . . . 6 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)))
425	422, 423, 424	3eqtr3rd 2782	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) = 0)
426		fveq2 6888	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) = (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
427	426	sumeq2sdv 15646	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
428		fzfid 13934	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0...𝑅) ∈ Fin)
429	33	adantlr 714	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
430	204	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → 𝑗 ∈ ℝ)
431	429, 430	ffvelcdmd 7083	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
432	428, 431	fsumcl 15675	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
433	38, 427, 204, 432	fvmptd3 7017	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐺‘𝑗) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
434	433	oveq2d 7420	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((e↑_𝑐-𝑗) · (𝐺‘𝑗)) = ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
435	434	oveq2d 7420	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))))
436	355, 432	mulcld 11230	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) ∈ ℂ)
437	400, 402, 436	mulassd 11233	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))) = ((𝐴‘𝑗) · ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))))
438	367	eqcomi 2742	. . . . . . . . . . . . . . 15 ⊢ 1 = (e↑_𝑐0)
439	438	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → 1 = (e↑_𝑐0))
440	352	negidd 11557	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 + -𝑗) = 0)
441	440	eqcomd 2739	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 0 = (𝑗 + -𝑗))
442	441	oveq2d 7420	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐0) = (e↑_𝑐(𝑗 + -𝑗)))
443	53, 54	gtneii 11322	. . . . . . . . . . . . . . . 16 ⊢ e ≠ 0
444	443	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → e ≠ 0)
445	351, 444, 352, 353	cxpaddd 26207	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐(𝑗 + -𝑗)) = ((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)))
446	439, 442, 445	3eqtrd 2777	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → 1 = ((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)))
447	446	oveq1d 7419	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = (((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
448	447	adantl 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = (((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
449	432	mullidd 11228	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
450	402, 355, 432	mulassd 11233	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))))
451	448, 449, 450	3eqtr3rd 2782	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
452	451	oveq2d 7420	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))) = ((𝐴‘𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
453	428, 400, 431	fsummulc2 15726	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
454	452, 453	eqtrd 2773	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))) = Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
455	435, 437, 454	3eqtrd 2777	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
456	455	sumeq2dv 15645	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = Σ𝑗 ∈ (0...𝑀)Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
457		vex 3479	. . . . . . . . . 10 ⊢ 𝑗 ∈ V
458		vex 3479	. . . . . . . . . 10 ⊢ 𝑖 ∈ V
459	457, 458	op1std 7980	. . . . . . . . 9 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → (1^st ‘𝑘) = 𝑗)
460	459	fveq2d 6892	. . . . . . . 8 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → (𝐴‘(1^st ‘𝑘)) = (𝐴‘𝑗))
461	457, 458	op2ndd 7981	. . . . . . . . . 10 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → (2^nd ‘𝑘) = 𝑖)
462	461	fveq2d 6892	. . . . . . . . 9 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → ((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘)) = ((ℝ D^𝑛 𝐹)‘𝑖))
463	462, 459	fveq12d 6895	. . . . . . . 8 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘)) = (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
464	460, 463	oveq12d 7422	. . . . . . 7 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → ((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) = ((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
465		fzfid 13934	. . . . . . 7 ⊢ (𝜑 → (0...𝑅) ∈ Fin)
466	400	adantrr 716	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → (𝐴‘𝑗) ∈ ℂ)
467	431	anasss 468	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
468	466, 467	mulcld 11230	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → ((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) ∈ ℂ)
469	464, 407, 465, 468	fsumxp 15714	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
470	456, 469	eqtrd 2773	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
471	425, 470	oveq12d 7422	. . . 4 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))) = (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘)))))
472		df-neg 11443	. . . . . 6 ⊢ -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) = (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
473	472	eqcomi 2742	. . . . 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 2777	. . 3 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))) = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
476	2, 406, 475	3eqtrd 2777	. 2 ⊢ (𝜑 → 𝐿 = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
477	476	oveq1d 7419	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 397 ∧ w3a 1088 = wceq 1542 ⊤wtru 1543 ∈ wcel 2107 ≠ wne 2941 Vcvv 3475 ∖ cdif 3944 ⊆ wss 3947 ifcif 4527 {csn 4627 {cpr 4629 ⟨cop 4633 class class class wbr 5147 ↦ cmpt 5230 × cxp 5673 ran crn 5676 ⟶wf 6536 ‘cfv 6540 (class class class)co 7404 1^st c1st 7968 2^nd c2nd 7969 ↑_pm cpm 8817 ℂcc 11104 ℝcr 11105 0cc0 11106 1c1 11107 + caddc 11109 · cmul 11111 -∞cmnf 11242 ℝ^*cxr 11243 < clt 11244 ≤ cle 11245 − cmin 11440 -cneg 11441 / cdiv 11867 ℕcn 12208 ℕ₀cn0 12468 ℤcz 12554 ℤ_≥cuz 12818 ℝ⁺crp 12970 (,)cioo 13320 (,]cioc 13321 [,]cicc 13323 ...cfz 13480 ↑cexp 14023 !cfa 14229 Σcsu 15628 ∏cprod 15845 eceu 16002 ↾_t crest 17362 TopOpenctopn 17363 topGenctg 17379 ℂ_fldccnfld 20929 intcnt 22503 –cn→ccncf 24374 𝐿¹cibl 25116 ∫citg 25117 0_𝑝c0p 25168 D cdv 25362 D^𝑛 cdvn 25363 Polycply 25680 coeffccoe 25682 degcdgr 25683 logclog 26045 ↑_𝑐ccxp 26046

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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7720 ax-inf2 9632 ax-cc 10426 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184 ax-addf 11185 ax-mulf 11186

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-symdif 4241 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-tp 4632 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-iin 4999 df-disj 5113 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7360 df-ov 7407 df-oprab 7408 df-mpo 7409 df-of 7665 df-ofr 7666 df-om 7851 df-1st 7970 df-2nd 7971 df-supp 8142 df-frecs 8261 df-wrecs 8292 df-recs 8366 df-rdg 8405 df-1o 8461 df-2o 8462 df-oadd 8465 df-omul 8466 df-er 8699 df-map 8818 df-pm 8819 df-ixp 8888 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-fsupp 9358 df-fi 9402 df-sup 9433 df-inf 9434 df-oi 9501 df-dju 9892 df-card 9930 df-acn 9933 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-div 11868 df-nn 12209 df-2 12271 df-3 12272 df-4 12273 df-5 12274 df-6 12275 df-7 12276 df-8 12277 df-9 12278 df-n0 12469 df-z 12555 df-dec 12674 df-uz 12819 df-q 12929 df-rp 12971 df-xneg 13088 df-xadd 13089 df-xmul 13090 df-ioo 13324 df-ioc 13325 df-ico 13326 df-icc 13327 df-fz 13481 df-fzo 13624 df-fl 13753 df-mod 13831 df-seq 13963 df-exp 14024 df-fac 14230 df-bc 14259 df-hash 14287 df-shft 15010 df-cj 15042 df-re 15043 df-im 15044 df-sqrt 15178 df-abs 15179 df-limsup 15411 df-clim 15428 df-rlim 15429 df-sum 15629 df-prod 15846 df-ef 16007 df-e 16008 df-sin 16009 df-cos 16010 df-tan 16011 df-pi 16012 df-struct 17076 df-sets 17093 df-slot 17111 df-ndx 17123 df-base 17141 df-ress 17170 df-plusg 17206 df-mulr 17207 df-starv 17208 df-sca 17209 df-vsca 17210 df-ip 17211 df-tset 17212 df-ple 17213 df-ds 17215 df-unif 17216 df-hom 17217 df-cco 17218 df-rest 17364 df-topn 17365 df-0g 17383 df-gsum 17384 df-topgen 17385 df-pt 17386 df-prds 17389 df-xrs 17444 df-qtop 17449 df-imas 17450 df-xps 17452 df-mre 17526 df-mrc 17527 df-acs 17529 df-mgm 18557 df-sgrp 18606 df-mnd 18622 df-submnd 18668 df-mulg 18945 df-cntz 19175 df-cmn 19643 df-psmet 20921 df-xmet 20922 df-met 20923 df-bl 20924 df-mopn 20925 df-fbas 20926 df-fg 20927 df-cnfld 20930 df-top 22378 df-topon 22395 df-topsp 22417 df-bases 22431 df-cld 22505 df-ntr 22506 df-cls 22507 df-nei 22584 df-lp 22622 df-perf 22623 df-cn 22713 df-cnp 22714 df-haus 22801 df-cmp 22873 df-tx 23048 df-hmeo 23241 df-fil 23332 df-fm 23424 df-flim 23425 df-flf 23426 df-xms 23808 df-ms 23809 df-tms 23810 df-cncf 24376 df-ovol 24963 df-vol 24964 df-mbf 25118 df-itg1 25119 df-itg2 25120 df-ibl 25121 df-itg 25122 df-0p 25169 df-limc 25365 df-dv 25366 df-dvn 25367 df-ply 25684 df-coe 25686 df-dgr 25687 df-log 26047 df-cxp 26048

This theorem is referenced by: etransclem47 44932

W3C validator