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 40497

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 6661	. . . . . . . . . . . . 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 14819	. . . . . . . . . . . . . . . . . . . 20 ⊢ e ∈ ℝ
9	8	recni 10052	. . . . . . . . . . . . . . . . . . 19 ⊢ e ∈ ℂ
10	9	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → e ∈ ℂ)
11		recn 10026	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
12	11	negcld 10379	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → -𝑥 ∈ ℂ)
13	10, 12	cxpcld 24454	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (e↑_𝑐-𝑥) ∈ ℂ)
14	13	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (e↑_𝑐-𝑥) ∈ ℂ)
15		simpr 477	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
16		fzfid 12772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (0...𝑅) ∈ Fin)
17		elfznn0 12433	. . . . . . . . . . . . . . . . . . . . . 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 3586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑄 ∈ (Poly‘ℤ))
26		dgrcl 23989	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑄 ∈ (Poly‘ℤ) → (deg‘𝑄) ∈ ℕ₀)
27	25, 26	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (deg‘𝑄) ∈ ℕ₀)
28	23, 27	syl5eqel 2705	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
29	28	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → 𝑀 ∈ ℕ₀)
30		etransclem46.f	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))
31		simpr 477	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → 𝑖 ∈ ℕ₀)
32	18, 20, 22, 29, 30, 31	etransclem33 40484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
33	17, 32	sylan2 491	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
34	33	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
35		simplr 792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → 𝑥 ∈ ℝ)
36	34, 35	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ)
37	16, 36	fsumcl 14464	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ)
38		etransclem46.g	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
39	38	fvmpt2 6291	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ) → (𝐺‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
40	15, 37, 39	syl2anc 693	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐺‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
41	40, 37	eqeltrd 2701	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐺‘𝑥) ∈ ℂ)
42	14, 41	mulcld 10060	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · (𝐺‘𝑥)) ∈ ℂ)
43	42	negcld 10379	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) ∈ ℂ)
44	43	adantlr 751	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ ℝ) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) ∈ ℂ)
45	6, 19	dvdmsscn 40151	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ℝ ⊆ ℂ)
46	45, 21, 30	etransclem8 40459	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
47	46	ffvelrnda 6359	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℂ)
48	14, 47	mulcld 10060	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
49	48	negcld 10379	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
50	49	negcld 10379	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → --((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
51	50	adantlr 751	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ ℝ) → --((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
52	8	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → e ∈ ℝ)
53		0re 10040	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℝ
54		epos 14935	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < e
55	53, 8, 54	ltleii 10160	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ≤ e
56	55	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → 0 ≤ e)
57		renegcl 10344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → -𝑥 ∈ ℝ)
58	52, 56, 57	recxpcld 24469	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → (e↑_𝑐-𝑥) ∈ ℝ)
59	58	renegcld 10457	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → -(e↑_𝑐-𝑥) ∈ ℝ)
60	59	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -(e↑_𝑐-𝑥) ∈ ℝ)
61		reelprrecn 10028	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℝ ∈ {ℝ, ℂ}
62	61	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → ℝ ∈ {ℝ, ℂ})
63		cnelprrecn 10029	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℂ ∈ {ℝ, ℂ}
64	63	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → ℂ ∈ {ℝ, ℂ})
65	12	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → -𝑥 ∈ ℂ)
66		neg1rr 11125	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -1 ∈ ℝ
67	66	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → -1 ∈ ℝ)
68	9	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℂ → e ∈ ℂ)
69		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
70	68, 69	cxpcld 24454	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ℂ → (e↑_𝑐𝑦) ∈ ℂ)
71	70	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑦 ∈ ℂ) → (e↑_𝑐𝑦) ∈ ℂ)
72	11	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
73		1red 10055	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
74	62	dvmptid 23720	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
75	62, 72, 73, 74	dvmptneg 23729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ -𝑥)) = (𝑥 ∈ ℝ ↦ -1))
76		epr 14936	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ e ∈ ℝ⁺
77		dvcxp2 24482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (e ∈ ℝ⁺ → (ℂ D (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑_𝑐𝑦))))
78	76, 77	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℂ D (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑_𝑐𝑦)))
79		loge 24333	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (log‘e) = 1
80	79	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((log‘e) · (e↑_𝑐𝑦)) = (1 · (e↑_𝑐𝑦))
81	70	mulid2d 10058	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ ℂ → (1 · (e↑_𝑐𝑦)) = (e↑_𝑐𝑦))
82	80, 81	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ℂ → ((log‘e) · (e↑_𝑐𝑦)) = (e↑_𝑐𝑦))
83	82	mpteq2ia 4740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))
84	78, 83	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℂ D (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))
85	84	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)))
86		oveq2 6658	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = -𝑥 → (e↑_𝑐𝑦) = (e↑_𝑐-𝑥))
87	62, 64, 65, 67, 71, 71, 75, 85, 86, 86	dvmptco 23735	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ (e↑_𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -1)))
88	87	trud 1493	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℝ D (𝑥 ∈ ℝ ↦ (e↑_𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -1))
89	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → -1 ∈ ℝ)
90	89	recnd 10068	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → -1 ∈ ℂ)
91	13, 90	mulcomd 10061	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → ((e↑_𝑐-𝑥) · -1) = (-1 · (e↑_𝑐-𝑥)))
92	13	mulm1d 10482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → (-1 · (e↑_𝑐-𝑥)) = -(e↑_𝑐-𝑥))
93	91, 92	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → ((e↑_𝑐-𝑥) · -1) = -(e↑_𝑐-𝑥))
94	93	mpteq2ia 4740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -1)) = (𝑥 ∈ ℝ ↦ -(e↑_𝑐-𝑥))
95	88, 94	eqtri 2644	. . . . . . . . . . . . . . . . . 18 ⊢ (ℝ D (𝑥 ∈ ℝ ↦ (e↑_𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ -(e↑_𝑐-𝑥))
96	95	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (e↑_𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ -(e↑_𝑐-𝑥)))
97	17	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → 𝑖 ∈ ℕ₀)
98		peano2nn0 11333	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ ℕ₀ → (𝑖 + 1) ∈ ℕ₀)
99	97, 98	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → (𝑖 + 1) ∈ ℕ₀)
100		ovex 6678	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 + 1) ∈ V
101		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = (𝑖 + 1) → (𝑗 ∈ ℕ₀ ↔ (𝑖 + 1) ∈ ℕ₀))
102	101	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = (𝑖 + 1) → ((𝜑 ∧ 𝑗 ∈ ℕ₀) ↔ (𝜑 ∧ (𝑖 + 1) ∈ ℕ₀)))
103		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = (𝑖 + 1) → ((ℝ D^𝑛 𝐹)‘𝑗) = ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)))
104	103	feq1d 6030	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = (𝑖 + 1) → (((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ ↔ ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ))
105	102, 104	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖 + 1) → (((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ) ↔ ((𝜑 ∧ (𝑖 + 1) ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)))
106		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑗 → (𝑖 ∈ ℕ₀ ↔ 𝑗 ∈ ℕ₀))
107	106	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ ℕ₀) ↔ (𝜑 ∧ 𝑗 ∈ ℕ₀)))
108		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑗 → ((ℝ D^𝑛 𝐹)‘𝑖) = ((ℝ D^𝑛 𝐹)‘𝑗))
109	108	feq1d 6030	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑗 → (((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ ↔ ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ))
110	107, 109	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ) ↔ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ)))
111	110, 32	chvarv 2263	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
112	100, 105, 111	vtocl 3259	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑖 + 1) ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
113	99, 112	syldan 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
114	113	adantlr 751	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
115	114, 35	ffvelrnd 6360	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ)
116	16, 115	fsumcl 14464	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ)
117	21, 28, 30, 38	etransclem39 40490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐺:ℝ⟶ℂ)
118	117	feqmptd 6249	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)))
119	118	eqcomd 2628	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)) = 𝐺)
120	119	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝐺‘𝑥))) = (ℝ D 𝐺))
121		nfcv 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥𝐹
122		elfznn0 12433	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0...(𝑅 + 1)) → 𝑖 ∈ ℕ₀)
123	122, 32	sylan2 491	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑅 + 1))) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
124	121, 46, 123, 38	etransclem2 40453	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℝ D 𝐺) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
125	120, 124	eqtrd 2656	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝐺‘𝑥))) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
126	6, 14, 60, 96, 41, 116, 125	dvmptmul 23724	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ ℝ ↦ ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥)))))
127	116, 14	mulcomd 10061	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥)) = ((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
128	127	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥))) = ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + ((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥))))
129	14	negcld 10379	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -(e↑_𝑐-𝑥) ∈ ℂ)
130	129, 41	mulcld 10060	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) ∈ ℂ)
131	14, 116	mulcld 10060	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) ∈ ℂ)
132	130, 131	addcomd 10238	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + ((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) = (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑_𝑐-𝑥) · (𝐺‘𝑥))))
133	131, 42	negsubd 10398	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + -((e↑_𝑐-𝑥) · (𝐺‘𝑥))) = (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) − ((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
134	14, 41	mulneg1d 10483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))
135	134	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑_𝑐-𝑥) · (𝐺‘𝑥))) = (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + -((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
136	116, 41, 14	subdir2d 10488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥))) = (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) − ((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
137	133, 135, 136	3eqtr4d 2666	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑_𝑐-𝑥) · (𝐺‘𝑥))) = ((e↑_𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥))))
138	40	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥)) = (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)))
139	16, 115, 36	fsumsub 14520	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)((((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)) = (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)))
140		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 𝑖 → ((ℝ D^𝑛 𝐹)‘𝑗) = ((ℝ D^𝑛 𝐹)‘𝑖))
141	140	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 𝑖 → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
142	103	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖 + 1) → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥))
143		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 0 → ((ℝ D^𝑛 𝐹)‘𝑗) = ((ℝ D^𝑛 𝐹)‘0))
144	143	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 0 → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D^𝑛 𝐹)‘0)‘𝑥))
145		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = (𝑅 + 1) → ((ℝ D^𝑛 𝐹)‘𝑗) = ((ℝ D^𝑛 𝐹)‘(𝑅 + 1)))
146	145	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑅 + 1) → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥))
147		etransclem46.r	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑅 = ((𝑀 · 𝑃) + (𝑃 − 1))
148	21	nnnn0d 11351	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
149	28, 148	nn0mulcld 11356	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℕ₀)
150		nnm1nn0 11334	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
151	21, 150	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑃 − 1) ∈ ℕ₀)
152	149, 151	nn0addcld 11355	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) ∈ ℕ₀)
153	147, 152	syl5eqel 2705	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
154	153	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑅 ∈ ℕ₀)
155	154	nn0zd 11480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑅 ∈ ℤ)
156		peano2nn0 11333	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑅 ∈ ℕ₀ → (𝑅 + 1) ∈ ℕ₀)
157	153, 156	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑅 + 1) ∈ ℕ₀)
158		nn0uz 11722	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℕ₀ = (ℤ_≥‘0)
159	157, 158	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑅 + 1) ∈ (ℤ_≥‘0))
160	159	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑅 + 1) ∈ (ℤ_≥‘0))
161		elfznn0 12433	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 ∈ (0...(𝑅 + 1)) → 𝑗 ∈ ℕ₀)
162	161, 111	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
163	162	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
164		simplr 792	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → 𝑥 ∈ ℝ)
165	163, 164	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) ∈ ℂ)
166	141, 142, 144, 146, 155, 160, 165	telfsum2 14537	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)((((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)) = ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥)))
167	138, 139, 166	3eqtr2d 2662	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥)) = ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥)))
168	167	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥))) = ((e↑_𝑐-𝑥) · ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥))))
169	153	nn0red 11352	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑅 ∈ ℝ)
170	169	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑅 < (𝑅 + 1))
171	147, 170	syl5eqbrr 4689	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) < (𝑅 + 1))
172		etransclem5 40456	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))
173	6, 19, 21, 28, 30, 157, 171, 172	etransclem32 40483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘(𝑅 + 1)) = (𝑥 ∈ ℝ ↦ 0))
174	173	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) = ((𝑥 ∈ ℝ ↦ 0)‘𝑥))
175		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℝ ↦ 0) = (𝑥 ∈ ℝ ↦ 0)
176	175	fvmpt2 6291	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℝ ∧ 0 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ 0)‘𝑥) = 0)
177	53, 176	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → ((𝑥 ∈ ℝ ↦ 0)‘𝑥) = 0)
178	174, 177	sylan9eq 2676	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) = 0)
179		cnex 10017	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ℂ ∈ V
180	179	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ℂ ∈ V)
181		etransclem46.rex	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ℝ ⊆ ℝ)
182	6, 181	ssexd 4805	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ℝ ∈ V)
183		elpm2r 7875	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:ℝ⟶ℂ ∧ ℝ ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑_pm ℝ))
184	180, 182, 46, 181, 183	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐹 ∈ (ℂ ↑_pm ℝ))
185		dvn0 23687	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℝ ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm ℝ)) → ((ℝ D^𝑛 𝐹)‘0) = 𝐹)
186	45, 184, 185	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘0) = 𝐹)
187	186	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘0)‘𝑥) = (𝐹‘𝑥))
188	187	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((ℝ D^𝑛 𝐹)‘0)‘𝑥) = (𝐹‘𝑥))
189	178, 188	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥)) = (0 − (𝐹‘𝑥)))
190		df-neg 10269	. . . . . . . . . . . . . . . . . . . . 21 ⊢ -(𝐹‘𝑥) = (0 − (𝐹‘𝑥))
191	189, 190	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥)) = -(𝐹‘𝑥))
192	191	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥))) = ((e↑_𝑐-𝑥) · -(𝐹‘𝑥)))
193	137, 168, 192	3eqtrd 2660	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑_𝑐-𝑥) · (𝐺‘𝑥))) = ((e↑_𝑐-𝑥) · -(𝐹‘𝑥)))
194	128, 132, 193	3eqtrd 2660	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥))) = ((e↑_𝑐-𝑥) · -(𝐹‘𝑥)))
195	194	mpteq2dva 4744	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥)))) = (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -(𝐹‘𝑥))))
196	14, 47	mulneg2d 10484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · -(𝐹‘𝑥)) = -((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
197	196	mpteq2dva 4744	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -(𝐹‘𝑥))) = (𝑥 ∈ ℝ ↦ -((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
198	126, 195, 197	3eqtrd 2660	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ ℝ ↦ -((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
199	6, 42, 49, 198	dvmptneg 23729	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ ℝ ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
200	199	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D (𝑥 ∈ ℝ ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ ℝ ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
201		0red 10041	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ)
202		elfzelz 12342	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
203	202	zred 11482	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
204	203	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ)
205	201, 204	iccssred 39727	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℝ)
206		eqid 2622	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
207	206	tgioo2 22606	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
208		0red 10041	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 0 ∈ ℝ)
209		iccntr 22624	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ ∧ 𝑗 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
210	208, 203, 209	syl2anc 693	. . . . . . . . . . . . . 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 23725	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ (0(,)𝑗) ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
213	9	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → e ∈ ℂ)
214		elioore 12205	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℝ)
215	214	recnd 10068	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℂ)
216	215	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℂ)
217	216	negcld 10379	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℂ)
218	213, 217	cxpcld 24454	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) ∈ ℂ)
219	46	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝐹:ℝ⟶ℂ)
220	214	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
221	219, 220	ffvelrnd 6360	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) ∈ ℂ)
222	218, 221	mulcld 10060	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
223	222	negnegd 10383	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → --((e↑_𝑐-𝑥) · (𝐹‘𝑥)) = ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
224	223	mpteq2dva 4744	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (0(,)𝑗) ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
225	224	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
226	5, 212, 225	3eqtrd 2660	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
227	226	fveq1d 6193	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((ℝ D 𝑂)‘𝑥) = ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥))
228	227	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((ℝ D 𝑂)‘𝑥) = ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥))
229		simpr 477	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ (0(,)𝑗))
230		eqid 2622	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
231	230	fvmpt2 6291	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥) = ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
232	229, 222, 231	syl2anc 693	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥) = ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
233	232	adantlr 751	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥) = ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
234	228, 233	eqtr2d 2657	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) = ((ℝ D 𝑂)‘𝑥))
235	234	itgeq2d 40199	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥 = ∫(0(,)𝑗)((ℝ D 𝑂)‘𝑥) d𝑥)
236		elfzle1 12344	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
237	236	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ 𝑗)
238		eqid 2622	. . . . . . . . . 10 ⊢ (𝑥 ∈ (0[,]𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = (𝑥 ∈ (0[,]𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
239		eqidd 2623	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)) = (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)))
240	86	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) ∧ 𝑦 = -𝑥) → (e↑_𝑐𝑦) = (e↑_𝑐-𝑥))
241	208, 203	iccssred 39727	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑀) → (0[,]𝑗) ⊆ ℝ)
242		ax-resscn 9993	. . . . . . . . . . . . . . . . . . 19 ⊢ ℝ ⊆ ℂ
243	241, 242	syl6ss 3615	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → (0[,]𝑗) ⊆ ℂ)
244	243	sselda 3603	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℂ)
245	244	negcld 10379	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → -𝑥 ∈ ℂ)
246	9	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → e ∈ ℂ)
247		negcl 10281	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → -𝑥 ∈ ℂ)
248	246, 247	cxpcld 24454	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → (e↑_𝑐-𝑥) ∈ ℂ)
249	244, 248	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑_𝑐-𝑥) ∈ ℂ)
250	239, 240, 245, 249	fvmptd 6288	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥) = (e↑_𝑐-𝑥))
251	250	eqcomd 2628	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑_𝑐-𝑥) = ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥))
252	251	adantll 750	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑_𝑐-𝑥) = ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥))
253	252	mpteq2dva 4744	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (e↑_𝑐-𝑥)) = (𝑥 ∈ (0[,]𝑗) ↦ ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥)))
254		mnfxr 10096	. . . . . . . . . . . . . . . . . 18 ⊢ -∞ ∈ ℝ^*
255	254	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℝ⁺ → -∞ ∈ ℝ^*)
256		0red 10041	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℝ⁺ → 0 ∈ ℝ)
257		rpxr 11840	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℝ⁺ → e ∈ ℝ^*)
258		rpgt0 11844	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℝ⁺ → 0 < e)
259	255, 256, 257, 258	gtnelioc 39712	. . . . . . . . . . . . . . . 16 ⊢ (e ∈ ℝ⁺ → ¬ e ∈ (-∞(,]0))
260	76, 259	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ¬ e ∈ (-∞(,]0)
261		eldif 3584	. . . . . . . . . . . . . . 15 ⊢ (e ∈ (ℂ ∖ (-∞(,]0)) ↔ (e ∈ ℂ ∧ ¬ e ∈ (-∞(,]0)))
262	9, 260, 261	mpbir2an 955	. . . . . . . . . . . . . 14 ⊢ e ∈ (ℂ ∖ (-∞(,]0))
263		cxpcncf2 40113	. . . . . . . . . . . . . 14 ⊢ (e ∈ (ℂ ∖ (-∞(,]0)) → (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)) ∈ (ℂ–cn→ℂ))
264	262, 263	mp1i 13	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)) ∈ (ℂ–cn→ℂ))
265		eqid 2622	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) = (𝑥 ∈ (0[,]𝑗) ↦ -𝑥)
266	265	negcncf 22721	. . . . . . . . . . . . . . 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 22716	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
270	253, 269	eqeltrd 2701	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (e↑_𝑐-𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
271	242	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → ℝ ⊆ ℂ)
272	21	ad2antrr 762	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ)
273	28	ad2antrr 762	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑀 ∈ ℕ₀)
274		etransclem6 40457	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦 − 𝑘)↑𝑃)))
275	30, 274	eqtri 2644	. . . . . . . . . . . . . 14 ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦 − 𝑘)↑𝑃)))
276	241	sselda 3603	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℝ)
277	276	adantll 750	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℝ)
278	271, 272, 273, 275, 277	etransclem13 40464	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝐹‘𝑥) = ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))
279	278	mpteq2dva 4744	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐹‘𝑥)) = (𝑥 ∈ (0[,]𝑗) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))))
280	243	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℂ)
281		fzfid 12772	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0...𝑀) ∈ Fin)
282	277	recnd 10068	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℂ)
283	282	3adant3 1081	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → 𝑥 ∈ ℂ)
284		elfzelz 12342	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ)
285	284	zcnd 11483	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ)
286	285	3ad2ant3 1084	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
287	283, 286	subcld 10392	. . . . . . . . . . . . . 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 4131	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
292	291	3adant3 1081	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
293	292	3adant1r 1319	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
294	287, 293	expcld 13008	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) ∈ ℂ)
295		nfv 1843	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀))
296	243	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℂ)
297		ssid 3624	. . . . . . . . . . . . . . . . . 18 ⊢ ℂ ⊆ ℂ
298	297	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
299	296, 298	idcncfg 40085	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ 𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
300	285	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
301	296, 300, 298	constcncfg 40084	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ 𝑘) ∈ ((0[,]𝑗)–cn→ℂ))
302	299, 301	subcncf 40082	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝑥 − 𝑘)) ∈ ((0[,]𝑗)–cn→ℂ))
303	302	adantll 750	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝑥 − 𝑘)) ∈ ((0[,]𝑗)–cn→ℂ))
304	151, 148	ifcld 4131	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
305		expcncf 22725	. . . . . . . . . . . . . . . 16 ⊢ (if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀ → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
306	304, 305	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
307	306	ad2antrr 762	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
308	297	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
309		oveq1 6657	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 − 𝑘) → (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) = ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))
310	295, 303, 307, 308, 309	cncfcompt2 40112	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((0[,]𝑗)–cn→ℂ))
311	280, 281, 294, 310	fprodcncf 40114	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((0[,]𝑗)–cn→ℂ))
312	279, 311	eqeltrd 2701	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐹‘𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
313	270, 312	mulcncf 23215	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
314		ioossicc 12259	. . . . . . . . . . 11 ⊢ (0(,)𝑗) ⊆ (0[,]𝑗)
315	314	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0(,)𝑗) ⊆ (0[,]𝑗))
316	297	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
317	222	adantlr 751	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
318	238, 313, 315, 316, 317	cncfmptssg 40083	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ ((0(,)𝑗)–cn→ℂ))
319	226, 318	eqeltrd 2701	. . . . . . . 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 6658	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑘 → (𝑥 − 𝑗) = (𝑥 − 𝑘))
324	323	oveq1d 6665	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → ((𝑥 − 𝑗)↑𝑃) = ((𝑥 − 𝑘)↑𝑃))
325	324	cbvprodv 14646	. . . . . . . . . . . . 13 ⊢ ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃) = ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)
326	325	oveq2i 6661	. . . . . . . . . . . 12 ⊢ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)) = ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃))
327	326	mpteq2i 4741	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))
328	30, 327	eqtri 2644	. . . . . . . . . 10 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))
329	7, 320, 321, 322, 328, 201, 204	etransclem18 40469	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ 𝐿¹)
330	226, 329	eqeltrd 2701	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) ∈ 𝐿¹)
331		eqid 2622	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)) = (𝑥 ∈ ℝ ↦ (𝐺‘𝑥))
332	6, 19, 21, 28, 30, 38	etransclem43 40494	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 ∈ (ℝ–cn→ℂ))
333	119, 332	eqeltrd 2701	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)) ∈ (ℝ–cn→ℂ))
334	333	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)) ∈ (ℝ–cn→ℂ))
335	117	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝐺:ℝ⟶ℂ)
336	335, 277	ffvelrnd 6360	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝐺‘𝑥) ∈ ℂ)
337	331, 334, 205, 316, 336	cncfmptssg 40083	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐺‘𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
338	270, 337	mulcncf 23215	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐺‘𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
339	338	negcncfg 40094	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
340	3, 339	syl5eqel 2705	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑂 ∈ ((0[,]𝑗)–cn→ℂ))
341	201, 204, 237, 319, 330, 340	ftc2 23807	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((ℝ D 𝑂)‘𝑥) d𝑥 = ((𝑂‘𝑗) − (𝑂‘0)))
342	3	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑂 = (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
343		negeq 10273	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑗 → -𝑥 = -𝑗)
344	343	oveq2d 6666	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑗 → (e↑_𝑐-𝑥) = (e↑_𝑐-𝑗))
345		fveq2 6191	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑗 → (𝐺‘𝑥) = (𝐺‘𝑗))
346	344, 345	oveq12d 6668	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → ((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))
347	346	negeqd 10275	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -((e↑_𝑐-𝑗) · (𝐺‘𝑗)))
348	347	adantl 482	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 = 𝑗) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -((e↑_𝑐-𝑗) · (𝐺‘𝑗)))
349	201	rexrd 10089	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ^*)
350	204	rexrd 10089	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ^*)
351		ubicc2 12289	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ^* ∧ 𝑗 ∈ ℝ^* ∧ 0 ≤ 𝑗) → 𝑗 ∈ (0[,]𝑗))
352	349, 350, 237, 351	syl3anc 1326	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0[,]𝑗))
353	9	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → e ∈ ℂ)
354	203	recnd 10068	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
355	354	negcld 10379	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → -𝑗 ∈ ℂ)
356	353, 355	cxpcld 24454	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐-𝑗) ∈ ℂ)
357	356	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑_𝑐-𝑗) ∈ ℂ)
358	117	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐺:ℝ⟶ℂ)
359	358, 204	ffvelrnd 6360	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐺‘𝑗) ∈ ℂ)
360	357, 359	mulcld 10060	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((e↑_𝑐-𝑗) · (𝐺‘𝑗)) ∈ ℂ)
361	360	negcld 10379	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → -((e↑_𝑐-𝑗) · (𝐺‘𝑗)) ∈ ℂ)
362	342, 348, 352, 361	fvmptd 6288	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑂‘𝑗) = -((e↑_𝑐-𝑗) · (𝐺‘𝑗)))
363		negeq 10273	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 0 → -𝑥 = -0)
364	363	oveq2d 6666	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 0 → (e↑_𝑐-𝑥) = (e↑_𝑐-0))
365		neg0 10327	. . . . . . . . . . . . . . . . 17 ⊢ -0 = 0
366	365	oveq2i 6661	. . . . . . . . . . . . . . . 16 ⊢ (e↑_𝑐-0) = (e↑_𝑐0)
367		cxp0 24416	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℂ → (e↑_𝑐0) = 1)
368	9, 367	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (e↑_𝑐0) = 1
369	366, 368	eqtri 2644	. . . . . . . . . . . . . . 15 ⊢ (e↑_𝑐-0) = 1
370	364, 369	syl6eq 2672	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 0 → (e↑_𝑐-𝑥) = 1)
371		fveq2 6191	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 0 → (𝐺‘𝑥) = (𝐺‘0))
372	370, 371	oveq12d 6668	. . . . . . . . . . . . 13 ⊢ (𝑥 = 0 → ((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = (1 · (𝐺‘0)))
373		0red 10041	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ ℝ)
374	117, 373	ffvelrnd 6360	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺‘0) ∈ ℂ)
375	374	mulid2d 10058	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 · (𝐺‘0)) = (𝐺‘0))
376	372, 375	sylan9eqr 2678	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 = 0) → ((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = (𝐺‘0))
377	376	negeqd 10275	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = 0) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -(𝐺‘0))
378	377	adantlr 751	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 = 0) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -(𝐺‘0))
379		lbicc2 12288	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ^* ∧ 𝑗 ∈ ℝ^* ∧ 0 ≤ 𝑗) → 0 ∈ (0[,]𝑗))
380	349, 350, 237, 379	syl3anc 1326	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ (0[,]𝑗))
381	374	negcld 10379	. . . . . . . . . . 11 ⊢ (𝜑 → -(𝐺‘0) ∈ ℂ)
382	381	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → -(𝐺‘0) ∈ ℂ)
383	342, 378, 380, 382	fvmptd 6288	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑂‘0) = -(𝐺‘0))
384	362, 383	oveq12d 6668	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑂‘𝑗) − (𝑂‘0)) = (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) − -(𝐺‘0)))
385	374	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐺‘0) ∈ ℂ)
386	361, 385	subnegd 10399	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) − -(𝐺‘0)) = (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) + (𝐺‘0)))
387	361, 385	addcomd 10238	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) + (𝐺‘0)) = ((𝐺‘0) + -((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
388	385, 360	negsubd 10398	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐺‘0) + -((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
389	387, 388	eqtrd 2656	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) + (𝐺‘0)) = ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
390	384, 386, 389	3eqtrd 2660	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑂‘𝑗) − (𝑂‘0)) = ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
391	235, 341, 390	3eqtrd 2660	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥 = ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
392	391	oveq2d 6666	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) = (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
393	25	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑄 ∈ (Poly‘ℤ))
394		0zd 11389	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℤ)
395		etransclem46.a	. . . . . . . . . . 11 ⊢ 𝐴 = (coeff‘𝑄)
396	395	coef2 23987	. . . . . . . . . 10 ⊢ ((𝑄 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → 𝐴:ℕ₀⟶ℤ)
397	393, 394, 396	syl2anc 693	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐴:ℕ₀⟶ℤ)
398		elfznn0 12433	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ₀)
399	398	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ₀)
400	397, 399	ffvelrnd 6360	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℤ)
401	400	zcnd 11483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℂ)
402	353, 354	cxpcld 24454	. . . . . . . 8 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐𝑗) ∈ ℂ)
403	402	adantl 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑_𝑐𝑗) ∈ ℂ)
404	401, 403	mulcld 10060	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑_𝑐𝑗)) ∈ ℂ)
405	404, 385, 360	subdid 10486	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))) = ((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
406	392, 405	eqtrd 2656	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) = ((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
407	406	sumeq2dv 14433	. . 3 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) = Σ𝑗 ∈ (0...𝑀)((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
408		fzfid 12772	. . . . 5 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
409	404, 385	mulcld 10060	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) ∈ ℂ)
410	404, 360	mulcld 10060	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) ∈ ℂ)
411	408, 409, 410	fsumsub 14520	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))) = (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
412		etransclem46.qe0	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘e) = 0)
413	412	eqcomd 2628	. . . . . . . 8 ⊢ (𝜑 → 0 = (𝑄‘e))
414	395, 23	coeid2 23995	. . . . . . . . 9 ⊢ ((𝑄 ∈ (Poly‘ℤ) ∧ e ∈ ℂ) → (𝑄‘e) = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑𝑗)))
415	25, 9, 414	sylancl 694	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘e) = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑𝑗)))
416		cxpexp 24414	. . . . . . . . . . . . 13 ⊢ ((e ∈ ℂ ∧ 𝑗 ∈ ℕ₀) → (e↑_𝑐𝑗) = (e↑𝑗))
417	353, 398, 416	syl2anc 693	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐𝑗) = (e↑𝑗))
418	417	eqcomd 2628	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑀) → (e↑𝑗) = (e↑_𝑐𝑗))
419	418	oveq2d 6666	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...𝑀) → ((𝐴‘𝑗) · (e↑𝑗)) = ((𝐴‘𝑗) · (e↑_𝑐𝑗)))
420	419	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑𝑗)) = ((𝐴‘𝑗) · (e↑_𝑐𝑗)))
421	420	sumeq2dv 14433	. . . . . . . 8 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑𝑗)) = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑_𝑐𝑗)))
422	413, 415, 421	3eqtrd 2660	. . . . . . 7 ⊢ (𝜑 → 0 = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑_𝑐𝑗)))
423	422	oveq1d 6665	. . . . . 6 ⊢ (𝜑 → (0 · (𝐺‘0)) = (Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)))
424	374	mul02d 10234	. . . . . 6 ⊢ (𝜑 → (0 · (𝐺‘0)) = 0)
425	408, 374, 404	fsummulc1 14517	. . . . . 6 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)))
426	423, 424, 425	3eqtr3rd 2665	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) = 0)
427	38	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)))
428		fveq2 6191	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑗 → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) = (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
429	428	sumeq2sdv 14435	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
430	429	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 = 𝑗) → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
431		fzfid 12772	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0...𝑅) ∈ Fin)
432	33	adantlr 751	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
433	204	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → 𝑗 ∈ ℝ)
434	432, 433	ffvelrnd 6360	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
435	431, 434	fsumcl 14464	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
436	427, 430, 204, 435	fvmptd 6288	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐺‘𝑗) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
437	436	oveq2d 6666	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((e↑_𝑐-𝑗) · (𝐺‘𝑗)) = ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
438	437	oveq2d 6666	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))))
439	357, 435	mulcld 10060	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) ∈ ℂ)
440	401, 403, 439	mulassd 10063	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))) = ((𝐴‘𝑗) · ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))))
441	368	eqcomi 2631	. . . . . . . . . . . . . . 15 ⊢ 1 = (e↑_𝑐0)
442	441	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → 1 = (e↑_𝑐0))
443	354	negidd 10382	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 + -𝑗) = 0)
444	443	eqcomd 2628	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 0 = (𝑗 + -𝑗))
445	444	oveq2d 6666	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐0) = (e↑_𝑐(𝑗 + -𝑗)))
446	53, 54	gtneii 10149	. . . . . . . . . . . . . . . 16 ⊢ e ≠ 0
447	446	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → e ≠ 0)
448	353, 447, 354, 355	cxpaddd 24463	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐(𝑗 + -𝑗)) = ((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)))
449	442, 445, 448	3eqtrd 2660	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → 1 = ((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)))
450	449	oveq1d 6665	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = (((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
451	450	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = (((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
452	435	mulid2d 10058	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
453	403, 357, 435	mulassd 10063	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))))
454	451, 452, 453	3eqtr3rd 2665	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
455	454	oveq2d 6666	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))) = ((𝐴‘𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
456	431, 401, 434	fsummulc2 14516	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
457	455, 456	eqtrd 2656	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))) = Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
458	438, 440, 457	3eqtrd 2660	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
459	458	sumeq2dv 14433	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = Σ𝑗 ∈ (0...𝑀)Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
460		vex 3203	. . . . . . . . . 10 ⊢ 𝑗 ∈ V
461		vex 3203	. . . . . . . . . 10 ⊢ 𝑖 ∈ V
462	460, 461	op1std 7178	. . . . . . . . 9 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → (1^st ‘𝑘) = 𝑗)
463	462	fveq2d 6195	. . . . . . . 8 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → (𝐴‘(1^st ‘𝑘)) = (𝐴‘𝑗))
464	460, 461	op2ndd 7179	. . . . . . . . . 10 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → (2^nd ‘𝑘) = 𝑖)
465	464	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → ((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘)) = ((ℝ D^𝑛 𝐹)‘𝑖))
466	465, 462	fveq12d 6197	. . . . . . . 8 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘)) = (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
467	463, 466	oveq12d 6668	. . . . . . 7 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → ((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) = ((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
468		fzfid 12772	. . . . . . 7 ⊢ (𝜑 → (0...𝑅) ∈ Fin)
469	401	adantrr 753	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → (𝐴‘𝑗) ∈ ℂ)
470	434	anasss 679	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
471	469, 470	mulcld 10060	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → ((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) ∈ ℂ)
472	467, 408, 468, 471	fsumxp 14503	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
473	459, 472	eqtrd 2656	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
474	426, 473	oveq12d 6668	. . . 4 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))) = (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘)))))
475		df-neg 10269	. . . . . 6 ⊢ -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) = (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
476	475	eqcomi 2631	. . . . 5 ⊢ (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘)))) = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘)))
477	476	a1i 11	. . . 4 ⊢ (𝜑 → (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘)))) = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
478	411, 474, 477	3eqtrd 2660	. . 3 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))) = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
479	2, 407, 478	3eqtrd 2660	. 2 ⊢ (𝜑 → 𝐿 = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
480	479	oveq1d 6665	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 384 ∧ w3a 1037 = wceq 1483 ⊤wtru 1484 ∈ wcel 1990 ≠ wne 2794 Vcvv 3200 ∖ cdif 3571 ⊆ wss 3574 ifcif 4086 {csn 4177 {cpr 4179 ⟨cop 4183 class class class wbr 4653 ↦ cmpt 4729 × cxp 5112 ran crn 5115 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 1^st c1st 7166 2^nd c2nd 7167 ↑_pm cpm 7858 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 -∞cmnf 10072 ℝ^*cxr 10073 < clt 10074 ≤ cle 10075 − cmin 10266 -cneg 10267 / cdiv 10684 ℕcn 11020 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ℝ⁺crp 11832 (,)cioo 12175 (,]cioc 12176 [,]cicc 12178 ...cfz 12326 ↑cexp 12860 !cfa 13060 Σcsu 14416 ∏cprod 14635 eceu 14793 ↾_t crest 16081 TopOpenctopn 16082 topGenctg 16098 ℂ_fldccnfld 19746 intcnt 20821 –cn→ccncf 22679 𝐿¹cibl 23386 ∫citg 23387 0_𝑝c0p 23436 D cdv 23627 D^𝑛 cdvn 23628 Polycply 23940 coeffccoe 23942 degcdgr 23943 logclog 24301 ↑_𝑐ccxp 24302

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cc 9257 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-disj 4621 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-ofr 6898 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-omul 7565 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-acn 8768 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ioc 12180 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-fac 13061 df-bc 13090 df-hash 13118 df-shft 13807 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-limsup 14202 df-clim 14219 df-rlim 14220 df-sum 14417 df-prod 14636 df-ef 14798 df-e 14799 df-sin 14800 df-cos 14801 df-tan 14802 df-pi 14803 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-perf 20941 df-cn 21031 df-cnp 21032 df-haus 21119 df-cmp 21190 df-tx 21365 df-hmeo 21558 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-xms 22125 df-ms 22126 df-tms 22127 df-cncf 22681 df-ovol 23233 df-vol 23234 df-mbf 23388 df-itg1 23389 df-itg2 23390 df-ibl 23391 df-itg 23392 df-0p 23437 df-limc 23630 df-dv 23631 df-dvn 23632 df-ply 23944 df-coe 23946 df-dgr 23947 df-log 24303 df-cxp 24304

This theorem is referenced by: etransclem47 40498

W3C validator