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 47109

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 7425	. . . . . . . . . . . . 13 ⊢ (ℝ D 𝑂) = (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
5	4	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) = (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))))
6		etransclem46.s	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
7	6	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℝ ∈ {ℝ, ℂ})
8		ere 16176	. . . . . . . . . . . . . . . . . . . 20 ⊢ e ∈ ℝ
9	8	recni 11248	. . . . . . . . . . . . . . . . . . 19 ⊢ e ∈ ℂ
10	9	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → e ∈ ℂ)
11		recn 11215	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
12	11	negcld 11581	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → -𝑥 ∈ ℂ)
13	10, 12	cxpcld 26946	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (e↑_𝑐-𝑥) ∈ ℂ)
14	13	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (e↑_𝑐-𝑥) ∈ ℂ)
15		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
16		fzfid 14038	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (0...𝑅) ∈ Fin)
17		elfznn0 13676	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ (0...𝑅) → 𝑖 ∈ ℕ₀)
18	6	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → ℝ ∈ {ℝ, ℂ})
19		etransclem46.x	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
20	19	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
21		etransclem46.p	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑃 ∈ ℕ)
22	21	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → 𝑃 ∈ ℕ)
23		etransclem46.m	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑀 = (deg‘𝑄)
24		etransclem46.q	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑄 ∈ ((Poly‘ℤ) ∖ {0_𝑝}))
25	24	eldifad 3911	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑄 ∈ (Poly‘ℤ))
26		dgrcl 26460	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑄 ∈ (Poly‘ℤ) → (deg‘𝑄) ∈ ℕ₀)
27	25, 26	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (deg‘𝑄) ∈ ℕ₀)
28	23, 27	eqeltrid 2864	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
29	28	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → 𝑀 ∈ ℕ₀)
30		etransclem46.f	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))
31		simpr 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → 𝑖 ∈ ℕ₀)
32	18, 20, 22, 29, 30, 31	etransclem33 47096	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
33	17, 32	sylan2 605	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
34	33	adantlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
35		simplr 781	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → 𝑥 ∈ ℝ)
36	34, 35	ffvelcdmd 7079	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ)
37	16, 36	fsumcl 15820	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ)
38		etransclem46.g	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
39	38	fvmpt2 6999	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ) → (𝐺‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
40	15, 37, 39	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐺‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
41	40, 37	eqeltrd 2860	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐺‘𝑥) ∈ ℂ)
42	14, 41	mulcld 11254	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · (𝐺‘𝑥)) ∈ ℂ)
43	42	negcld 11581	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) ∈ ℂ)
44	43	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ ℝ) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) ∈ ℂ)
45	6, 19	dvdmsscn 46765	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ℝ ⊆ ℂ)
46	45, 21, 30	etransclem8 47071	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
47	46	ffvelcdmda 7078	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℂ)
48	14, 47	mulcld 11254	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
49	48	negcld 11581	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
50	49	negcld 11581	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → --((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
51	50	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ ℝ) → --((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
52	8	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → e ∈ ℝ)
53		0re 11235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℝ
54		epos 16296	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < e
55	53, 8, 54	ltleii 11358	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ≤ e
56	55	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → 0 ≤ e)
57		renegcl 11546	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → -𝑥 ∈ ℝ)
58	52, 56, 57	recxpcld 26961	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → (e↑_𝑐-𝑥) ∈ ℝ)
59	58	renegcld 11666	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → -(e↑_𝑐-𝑥) ∈ ℝ)
60	59	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -(e↑_𝑐-𝑥) ∈ ℝ)
61		reelprrecn 11217	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℝ ∈ {ℝ, ℂ}
62	61	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → ℝ ∈ {ℝ, ℂ})
63		cnelprrecn 11218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℂ ∈ {ℝ, ℂ}
64	63	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → ℂ ∈ {ℝ, ℂ})
65	12	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → -𝑥 ∈ ℂ)
66		neg1rr 12229	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -1 ∈ ℝ
67	66	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → -1 ∈ ℝ)
68	9	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℂ → e ∈ ℂ)
69		id 23	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
70	68, 69	cxpcld 26946	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ℂ → (e↑_𝑐𝑦) ∈ ℂ)
71	70	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑦 ∈ ℂ) → (e↑_𝑐𝑦) ∈ ℂ)
72	11	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
73		1red 11234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
74	62	dvmptid 26185	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
75	62, 72, 73, 74	dvmptneg 26194	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ -𝑥)) = (𝑥 ∈ ℝ ↦ -1))
76		epr 16297	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ e ∈ ℝ⁺
77		dvcxp2 26979	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (e ∈ ℝ⁺ → (ℂ D (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑_𝑐𝑦))))
78	76, 77	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℂ D (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑_𝑐𝑦)))
79		loge 26824	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (log‘e) = 1
80	79	oveq1i 7424	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((log‘e) · (e↑_𝑐𝑦)) = (1 · (e↑_𝑐𝑦))
81	70	mullidd 11252	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ ℂ → (1 · (e↑_𝑐𝑦)) = (e↑_𝑐𝑦))
82	80, 81	eqtrid 2807	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ℂ → ((log‘e) · (e↑_𝑐𝑦)) = (e↑_𝑐𝑦))
83	82	mpteq2ia 5200	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))
84	78, 83	eqtri 2783	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℂ D (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))
85	84	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)))
86		oveq2 7422	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = -𝑥 → (e↑_𝑐𝑦) = (e↑_𝑐-𝑥))
87	62, 64, 65, 67, 71, 71, 75, 85, 86, 86	dvmptco 26200	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ (e↑_𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -1)))
88	87	mptru 1577	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℝ D (𝑥 ∈ ℝ ↦ (e↑_𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -1))
89	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → -1 ∈ ℝ)
90	89	recnd 11262	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → -1 ∈ ℂ)
91	13, 90	mulcomd 11255	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → ((e↑_𝑐-𝑥) · -1) = (-1 · (e↑_𝑐-𝑥)))
92	13	mulm1d 11691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → (-1 · (e↑_𝑐-𝑥)) = -(e↑_𝑐-𝑥))
93	91, 92	eqtrd 2795	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → ((e↑_𝑐-𝑥) · -1) = -(e↑_𝑐-𝑥))
94	93	mpteq2ia 5200	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -1)) = (𝑥 ∈ ℝ ↦ -(e↑_𝑐-𝑥))
95	88, 94	eqtri 2783	. . . . . . . . . . . . . . . . . 18 ⊢ (ℝ D (𝑥 ∈ ℝ ↦ (e↑_𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ -(e↑_𝑐-𝑥))
96	95	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (e↑_𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ -(e↑_𝑐-𝑥)))
97	17	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → 𝑖 ∈ ℕ₀)
98		peano2nn0 12569	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ ℕ₀ → (𝑖 + 1) ∈ ℕ₀)
99	97, 98	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → (𝑖 + 1) ∈ ℕ₀)
100		ovex 7447	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 + 1) ∈ V
101		eleq1 2848	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = (𝑖 + 1) → (𝑗 ∈ ℕ₀ ↔ (𝑖 + 1) ∈ ℕ₀))
102	101	anbi2d 642	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = (𝑖 + 1) → ((𝜑 ∧ 𝑗 ∈ ℕ₀) ↔ (𝜑 ∧ (𝑖 + 1) ∈ ℕ₀)))
103		fveq2 6879	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = (𝑖 + 1) → ((ℝ D^𝑛 𝐹)‘𝑗) = ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)))
104	103	feq1d 6685	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = (𝑖 + 1) → (((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ ↔ ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ))
105	102, 104	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖 + 1) → (((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ) ↔ ((𝜑 ∧ (𝑖 + 1) ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)))
106		eleq1 2848	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑗 → (𝑖 ∈ ℕ₀ ↔ 𝑗 ∈ ℕ₀))
107	106	anbi2d 642	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ ℕ₀) ↔ (𝜑 ∧ 𝑗 ∈ ℕ₀)))
108		fveq2 6879	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑗 → ((ℝ D^𝑛 𝐹)‘𝑖) = ((ℝ D^𝑛 𝐹)‘𝑗))
109	108	feq1d 6685	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑗 → (((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ ↔ ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ))
110	107, 109	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ) ↔ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ)))
111	110, 32	chvarvv 2022	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
112	100, 105, 111	vtocl 3520	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑖 + 1) ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
113	99, 112	syldan 603	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
114	113	adantlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
115	114, 35	ffvelcdmd 7079	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ)
116	16, 115	fsumcl 15820	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ)
117	21, 28, 30, 38	etransclem39 47102	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐺:ℝ⟶ℂ)
118	117	feqmptd 6947	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)))
119	118	eqcomd 2766	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)) = 𝐺)
120	119	oveq2d 7430	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝐺‘𝑥))) = (ℝ D 𝐺))
121		nfcv 2922	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥𝐹
122		elfznn0 13676	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0...(𝑅 + 1)) → 𝑖 ∈ ℕ₀)
123	122, 32	sylan2 605	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑅 + 1))) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
124	121, 46, 123, 38	etransclem2 47065	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℝ D 𝐺) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
125	120, 124	eqtrd 2795	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝐺‘𝑥))) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
126	6, 14, 60, 96, 41, 116, 125	dvmptmul 26189	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ ℝ ↦ ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥)))))
127	116, 14	mulcomd 11255	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥)) = ((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
128	127	oveq2d 7430	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥))) = ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + ((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥))))
129	14	negcld 11581	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -(e↑_𝑐-𝑥) ∈ ℂ)
130	129, 41	mulcld 11254	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) ∈ ℂ)
131	14, 116	mulcld 11254	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) ∈ ℂ)
132	130, 131	addcomd 11437	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + ((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) = (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑_𝑐-𝑥) · (𝐺‘𝑥))))
133	131, 42	negsubd 11600	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + -((e↑_𝑐-𝑥) · (𝐺‘𝑥))) = (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) − ((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
134	14, 41	mulneg1d 11692	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))
135	134	oveq2d 7430	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑_𝑐-𝑥) · (𝐺‘𝑥))) = (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + -((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
136	14, 116, 41	subdid 11695	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥))) = (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) − ((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
137	133, 135, 136	3eqtr4d 2805	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑_𝑐-𝑥) · (𝐺‘𝑥))) = ((e↑_𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥))))
138	40	oveq2d 7430	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥)) = (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)))
139	16, 115, 36	fsumsub 15875	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)((((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)) = (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)))
140		fveq2 6879	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 𝑖 → ((ℝ D^𝑛 𝐹)‘𝑗) = ((ℝ D^𝑛 𝐹)‘𝑖))
141	140	fveq1d 6881	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 𝑖 → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
142	103	fveq1d 6881	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖 + 1) → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥))
143		fveq2 6879	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 0 → ((ℝ D^𝑛 𝐹)‘𝑗) = ((ℝ D^𝑛 𝐹)‘0))
144	143	fveq1d 6881	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 0 → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D^𝑛 𝐹)‘0)‘𝑥))
145		fveq2 6879	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = (𝑅 + 1) → ((ℝ D^𝑛 𝐹)‘𝑗) = ((ℝ D^𝑛 𝐹)‘(𝑅 + 1)))
146	145	fveq1d 6881	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑅 + 1) → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥))
147		etransclem46.r	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑅 = ((𝑀 · 𝑃) + (𝑃 − 1))
148	21	nnnn0d 12590	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
149	28, 148	nn0mulcld 12595	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℕ₀)
150		nnm1nn0 12570	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
151	21, 150	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑃 − 1) ∈ ℕ₀)
152	149, 151	nn0addcld 12594	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) ∈ ℕ₀)
153	147, 152	eqeltrid 2864	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
154	153	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑅 ∈ ℕ₀)
155	154	nn0zd 12641	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑅 ∈ ℤ)
156		peano2nn0 12569	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑅 ∈ ℕ₀ → (𝑅 + 1) ∈ ℕ₀)
157	153, 156	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑅 + 1) ∈ ℕ₀)
158		nn0uz 12926	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℕ₀ = (ℤ_≥‘0)
159	157, 158	eleqtrdi 2870	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑅 + 1) ∈ (ℤ_≥‘0))
160	159	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑅 + 1) ∈ (ℤ_≥‘0))
161		elfznn0 13676	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 ∈ (0...(𝑅 + 1)) → 𝑗 ∈ ℕ₀)
162	161, 111	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
163	162	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
164		simplr 781	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → 𝑥 ∈ ℝ)
165	163, 164	ffvelcdmd 7079	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) ∈ ℂ)
166	141, 142, 144, 146, 155, 160, 165	telfsum2 15893	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)((((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)) = ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥)))
167	138, 139, 166	3eqtr2d 2801	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥)) = ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥)))
168	167	oveq2d 7430	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥))) = ((e↑_𝑐-𝑥) · ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥))))
169	153	nn0red 12591	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑅 ∈ ℝ)
170	169	ltp1d 12170	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑅 < (𝑅 + 1))
171	147, 170	eqbrtrrid 5141	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) < (𝑅 + 1))
172		etransclem5 47068	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))
173	6, 19, 21, 28, 30, 157, 171, 172	etransclem32 47095	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘(𝑅 + 1)) = (𝑥 ∈ ℝ ↦ 0))
174	173	fveq1d 6881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) = ((𝑥 ∈ ℝ ↦ 0)‘𝑥))
175		eqid 2760	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℝ ↦ 0) = (𝑥 ∈ ℝ ↦ 0)
176	175	fvmpt2 6999	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℝ ∧ 0 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ 0)‘𝑥) = 0)
177	53, 176	mpan2 704	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → ((𝑥 ∈ ℝ ↦ 0)‘𝑥) = 0)
178	174, 177	sylan9eq 2815	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) = 0)
179		cnex 11206	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ℂ ∈ V
180	179	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ℂ ∈ V)
181		etransclem46.rex	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ℝ ⊆ ℝ)
182	6, 181	ssexd 5289	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ℝ ∈ V)
183		elpm2r 8845	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:ℝ⟶ℂ ∧ ℝ ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑_pm ℝ))
184	180, 182, 46, 181, 183	syl22anc 852	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐹 ∈ (ℂ ↑_pm ℝ))
185		dvn0 26152	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℝ ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm ℝ)) → ((ℝ D^𝑛 𝐹)‘0) = 𝐹)
186	45, 184, 185	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘0) = 𝐹)
187	186	fveq1d 6881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘0)‘𝑥) = (𝐹‘𝑥))
188	187	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((ℝ D^𝑛 𝐹)‘0)‘𝑥) = (𝐹‘𝑥))
189	178, 188	oveq12d 7432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥)) = (0 − (𝐹‘𝑥)))
190		df-neg 11469	. . . . . . . . . . . . . . . . . . . . 21 ⊢ -(𝐹‘𝑥) = (0 − (𝐹‘𝑥))
191	189, 190	eqtr4di 2813	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥)) = -(𝐹‘𝑥))
192	191	oveq2d 7430	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥))) = ((e↑_𝑐-𝑥) · -(𝐹‘𝑥)))
193	137, 168, 192	3eqtrd 2799	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑_𝑐-𝑥) · (𝐺‘𝑥))) = ((e↑_𝑐-𝑥) · -(𝐹‘𝑥)))
194	128, 132, 193	3eqtrd 2799	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥))) = ((e↑_𝑐-𝑥) · -(𝐹‘𝑥)))
195	194	mpteq2dva 5198	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥)))) = (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -(𝐹‘𝑥))))
196	14, 47	mulneg2d 11693	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · -(𝐹‘𝑥)) = -((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
197	196	mpteq2dva 5198	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -(𝐹‘𝑥))) = (𝑥 ∈ ℝ ↦ -((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
198	126, 195, 197	3eqtrd 2799	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ ℝ ↦ -((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
199	6, 42, 49, 198	dvmptneg 26194	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ ℝ ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
200	199	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D (𝑥 ∈ ℝ ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ ℝ ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
201		0red 11236	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ)
202		elfzelz 13579	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
203	202	zred 12726	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
204	203	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ)
205	201, 204	iccssred 13488	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℝ)
206		tgioo4 25032	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
207		eqid 2760	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
208		0red 11236	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 0 ∈ ℝ)
209		iccntr 25049	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ ∧ 𝑗 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
210	208, 203, 209	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
211	210	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
212	7, 44, 51, 200, 205, 206, 207, 211	dvmptres2 26190	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ (0(,)𝑗) ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
213	9	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → e ∈ ℂ)
214		elioore 13429	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℝ)
215	214	recnd 11262	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℂ)
216	215	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℂ)
217	216	negcld 11581	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℂ)
218	213, 217	cxpcld 26946	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) ∈ ℂ)
219	46	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝐹:ℝ⟶ℂ)
220	214	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
221	219, 220	ffvelcdmd 7079	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) ∈ ℂ)
222	218, 221	mulcld 11254	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
223	222	negnegd 11585	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → --((e↑_𝑐-𝑥) · (𝐹‘𝑥)) = ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
224	223	mpteq2dva 5198	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (0(,)𝑗) ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
225	224	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
226	5, 212, 225	3eqtrd 2799	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
227	226	fveq1d 6881	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((ℝ D 𝑂)‘𝑥) = ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥))
228	227	adantr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((ℝ D 𝑂)‘𝑥) = ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥))
229		simpr 490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ (0(,)𝑗))
230		eqid 2760	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
231	230	fvmpt2 6999	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥) = ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
232	229, 222, 231	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥) = ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
233	232	adantlr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥) = ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
234	228, 233	eqtr2d 2796	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) = ((ℝ D 𝑂)‘𝑥))
235	234	itgeq2dv 26010	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥 = ∫(0(,)𝑗)((ℝ D 𝑂)‘𝑥) d𝑥)
236		elfzle1 13582	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
237	236	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ 𝑗)
238		eqid 2760	. . . . . . . . . 10 ⊢ (𝑥 ∈ (0[,]𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = (𝑥 ∈ (0[,]𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
239		eqidd 2761	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)) = (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)))
240	86	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) ∧ 𝑦 = -𝑥) → (e↑_𝑐𝑦) = (e↑_𝑐-𝑥))
241	208, 203	iccssred 13488	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑀) → (0[,]𝑗) ⊆ ℝ)
242		ax-resscn 11182	. . . . . . . . . . . . . . . . . . 19 ⊢ ℝ ⊆ ℂ
243	241, 242	sstrdi 3943	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → (0[,]𝑗) ⊆ ℂ)
244	243	sselda 3931	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℂ)
245	244	negcld 11581	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → -𝑥 ∈ ℂ)
246	9	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → e ∈ ℂ)
247		negcl 11482	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → -𝑥 ∈ ℂ)
248	246, 247	cxpcld 26946	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → (e↑_𝑐-𝑥) ∈ ℂ)
249	244, 248	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑_𝑐-𝑥) ∈ ℂ)
250	239, 240, 245, 249	fvmptd 6995	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥) = (e↑_𝑐-𝑥))
251	250	eqcomd 2766	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑_𝑐-𝑥) = ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥))
252	251	adantll 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑_𝑐-𝑥) = ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥))
253	252	mpteq2dva 5198	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (e↑_𝑐-𝑥)) = (𝑥 ∈ (0[,]𝑗) ↦ ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥)))
254		mnfxr 11291	. . . . . . . . . . . . . . . . . 18 ⊢ -∞ ∈ ℝ^*
255	254	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℝ⁺ → -∞ ∈ ℝ^*)
256		0red 11236	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℝ⁺ → 0 ∈ ℝ)
257		rpxr 13053	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℝ⁺ → e ∈ ℝ^*)
258		rpgt0 13056	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℝ⁺ → 0 < e)
259	255, 256, 257, 258	gtnelioc 46322	. . . . . . . . . . . . . . . 16 ⊢ (e ∈ ℝ⁺ → ¬ e ∈ (-∞(,]0))
260	76, 259	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ¬ e ∈ (-∞(,]0)
261		eldif 3909	. . . . . . . . . . . . . . 15 ⊢ (e ∈ (ℂ ∖ (-∞(,]0)) ↔ (e ∈ ℂ ∧ ¬ e ∈ (-∞(,]0)))
262	9, 260, 261	mpbir2an 724	. . . . . . . . . . . . . 14 ⊢ e ∈ (ℂ ∖ (-∞(,]0))
263		cxpcncf2 46728	. . . . . . . . . . . . . 14 ⊢ (e ∈ (ℂ ∖ (-∞(,]0)) → (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)) ∈ (ℂ–cn→ℂ))
264	262, 263	mp1i 14	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)) ∈ (ℂ–cn→ℂ))
265		eqid 2760	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) = (𝑥 ∈ (0[,]𝑗) ↦ -𝑥)
266	265	negcncf 25151	. . . . . . . . . . . . . . 15 ⊢ ((0[,]𝑗) ⊆ ℂ → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
267	243, 266	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
268	267	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
269	264, 268	cncfmpt1f 25143	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
270	253, 269	eqeltrd 2860	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (e↑_𝑐-𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
271	242	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → ℝ ⊆ ℂ)
272	21	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ)
273	28	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑀 ∈ ℕ₀)
274		etransclem6 47069	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦 − 𝑘)↑𝑃)))
275	30, 274	eqtri 2783	. . . . . . . . . . . . . 14 ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦 − 𝑘)↑𝑃)))
276	241	sselda 3931	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℝ)
277	276	adantll 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℝ)
278	271, 272, 273, 275, 277	etransclem13 47076	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝐹‘𝑥) = ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))
279	278	mpteq2dva 5198	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐹‘𝑥)) = (𝑥 ∈ (0[,]𝑗) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))))
280	243	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℂ)
281		fzfid 14038	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0...𝑀) ∈ Fin)
282	277	recnd 11262	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℂ)
283	282	3adant3 1150	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → 𝑥 ∈ ℂ)
284		elfzelz 13579	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ)
285	284	zcnd 12727	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ)
286	285	3ad2ant3 1153	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
287	283, 286	subcld 11594	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 − 𝑘) ∈ ℂ)
288	21	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ)
289	288, 150	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗)) → (𝑃 − 1) ∈ ℕ₀)
290	148	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ₀)
291	289, 290	ifcld 4529	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
292	291	3adant3 1150	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
293	292	3adant1r 1196	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
294	287, 293	expcld 14211	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) ∈ ℂ)
295		nfv 1947	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀))
296	243	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℂ)
297		ssid 3953	. . . . . . . . . . . . . . . . . 18 ⊢ ℂ ⊆ ℂ
298	297	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
299	296, 298	idcncfg 46702	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ 𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
300	285	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
301	296, 300, 298	constcncfg 46701	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ 𝑘) ∈ ((0[,]𝑗)–cn→ℂ))
302	299, 301	subcncf 25674	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝑥 − 𝑘)) ∈ ((0[,]𝑗)–cn→ℂ))
303	302	adantll 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝑥 − 𝑘)) ∈ ((0[,]𝑗)–cn→ℂ))
304	151, 148	ifcld 4529	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
305		expcncf 25155	. . . . . . . . . . . . . . . 16 ⊢ (if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀ → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
306	304, 305	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
307	306	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
308	297	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
309		oveq1 7421	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 − 𝑘) → (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) = ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))
310	295, 303, 307, 308, 309	cncfcompt2 25137	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((0[,]𝑗)–cn→ℂ))
311	280, 281, 294, 310	fprodcncf 46729	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((0[,]𝑗)–cn→ℂ))
312	279, 311	eqeltrd 2860	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐹‘𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
313	270, 312	mulcncf 25675	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
314		ioossicc 13487	. . . . . . . . . . 11 ⊢ (0(,)𝑗) ⊆ (0[,]𝑗)
315	314	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0(,)𝑗) ⊆ (0[,]𝑗))
316	297	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
317	222	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
318	238, 313, 315, 316, 317	cncfmptssg 46700	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ ((0(,)𝑗)–cn→ℂ))
319	226, 318	eqeltrd 2860	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) ∈ ((0(,)𝑗)–cn→ℂ))
320	19	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
321	21	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑃 ∈ ℕ)
322	28	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℕ₀)
323		oveq2 7422	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑘 → (𝑥 − 𝑗) = (𝑥 − 𝑘))
324	323	oveq1d 7429	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → ((𝑥 − 𝑗)↑𝑃) = ((𝑥 − 𝑘)↑𝑃))
325	324	cbvprodv 16004	. . . . . . . . . . . . 13 ⊢ ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃) = ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)
326	325	oveq2i 7425	. . . . . . . . . . . 12 ⊢ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)) = ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃))
327	326	mpteq2i 5201	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))
328	30, 327	eqtri 2783	. . . . . . . . . 10 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))
329	7, 320, 321, 322, 328, 201, 204	etransclem18 47081	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ 𝐿¹)
330	226, 329	eqeltrd 2860	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) ∈ 𝐿¹)
331		eqid 2760	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)) = (𝑥 ∈ ℝ ↦ (𝐺‘𝑥))
332	6, 19, 21, 28, 30, 38	etransclem43 47106	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 ∈ (ℝ–cn→ℂ))
333	119, 332	eqeltrd 2860	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)) ∈ (ℝ–cn→ℂ))
334	333	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)) ∈ (ℝ–cn→ℂ))
335	117	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝐺:ℝ⟶ℂ)
336	335, 277	ffvelcdmd 7079	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝐺‘𝑥) ∈ ℂ)
337	331, 334, 205, 316, 336	cncfmptssg 46700	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐺‘𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
338	270, 337	mulcncf 25675	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐺‘𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
339	338	negcncfg 46710	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
340	3, 339	eqeltrid 2864	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑂 ∈ ((0[,]𝑗)–cn→ℂ))
341	201, 204, 237, 319, 330, 340	ftc2 26272	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((ℝ D 𝑂)‘𝑥) d𝑥 = ((𝑂‘𝑗) − (𝑂‘0)))
342		negeq 11474	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑗 → -𝑥 = -𝑗)
343	342	oveq2d 7430	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → (e↑_𝑐-𝑥) = (e↑_𝑐-𝑗))
344		fveq2 6879	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → (𝐺‘𝑥) = (𝐺‘𝑗))
345	343, 344	oveq12d 7432	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → ((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))
346	345	negeqd 11476	. . . . . . . . . 10 ⊢ (𝑥 = 𝑗 → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -((e↑_𝑐-𝑗) · (𝐺‘𝑗)))
347	201	rexrd 11284	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ^*)
348	204	rexrd 11284	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ^*)
349		ubicc2 13519	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ^* ∧ 𝑗 ∈ ℝ^* ∧ 0 ≤ 𝑗) → 𝑗 ∈ (0[,]𝑗))
350	347, 348, 237, 349	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0[,]𝑗))
351	9	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → e ∈ ℂ)
352	203	recnd 11262	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
353	352	negcld 11581	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → -𝑗 ∈ ℂ)
354	351, 353	cxpcld 26946	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐-𝑗) ∈ ℂ)
355	354	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑_𝑐-𝑗) ∈ ℂ)
356	117	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐺:ℝ⟶ℂ)
357	356, 204	ffvelcdmd 7079	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐺‘𝑗) ∈ ℂ)
358	355, 357	mulcld 11254	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((e↑_𝑐-𝑗) · (𝐺‘𝑗)) ∈ ℂ)
359	358	negcld 11581	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → -((e↑_𝑐-𝑗) · (𝐺‘𝑗)) ∈ ℂ)
360	3, 346, 350, 359	fvmptd3 7011	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑂‘𝑗) = -((e↑_𝑐-𝑗) · (𝐺‘𝑗)))
361	3	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑂 = (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
362		negeq 11474	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 0 → -𝑥 = -0)
363	362	oveq2d 7430	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 0 → (e↑_𝑐-𝑥) = (e↑_𝑐-0))
364		neg0 11529	. . . . . . . . . . . . . . . . 17 ⊢ -0 = 0
365	364	oveq2i 7425	. . . . . . . . . . . . . . . 16 ⊢ (e↑_𝑐-0) = (e↑_𝑐0)
366		cxp0 26908	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℂ → (e↑_𝑐0) = 1)
367	9, 366	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (e↑_𝑐0) = 1
368	365, 367	eqtri 2783	. . . . . . . . . . . . . . 15 ⊢ (e↑_𝑐-0) = 1
369	363, 368	eqtrdi 2811	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 0 → (e↑_𝑐-𝑥) = 1)
370		fveq2 6879	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 0 → (𝐺‘𝑥) = (𝐺‘0))
371	369, 370	oveq12d 7432	. . . . . . . . . . . . 13 ⊢ (𝑥 = 0 → ((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = (1 · (𝐺‘0)))
372		0red 11236	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ ℝ)
373	117, 372	ffvelcdmd 7079	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺‘0) ∈ ℂ)
374	373	mullidd 11252	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 · (𝐺‘0)) = (𝐺‘0))
375	371, 374	sylan9eqr 2817	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 = 0) → ((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = (𝐺‘0))
376	375	negeqd 11476	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = 0) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -(𝐺‘0))
377	376	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 = 0) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -(𝐺‘0))
378		lbicc2 13518	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ^* ∧ 𝑗 ∈ ℝ^* ∧ 0 ≤ 𝑗) → 0 ∈ (0[,]𝑗))
379	347, 348, 237, 378	syl3anc 1398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ (0[,]𝑗))
380	373	negcld 11581	. . . . . . . . . . 11 ⊢ (𝜑 → -(𝐺‘0) ∈ ℂ)
381	380	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → -(𝐺‘0) ∈ ℂ)
382	361, 377, 379, 381	fvmptd 6995	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑂‘0) = -(𝐺‘0))
383	360, 382	oveq12d 7432	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑂‘𝑗) − (𝑂‘0)) = (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) − -(𝐺‘0)))
384	373	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐺‘0) ∈ ℂ)
385	359, 384	subnegd 11601	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) − -(𝐺‘0)) = (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) + (𝐺‘0)))
386	359, 384	addcomd 11437	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) + (𝐺‘0)) = ((𝐺‘0) + -((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
387	384, 358	negsubd 11600	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐺‘0) + -((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
388	386, 387	eqtrd 2795	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) + (𝐺‘0)) = ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
389	383, 385, 388	3eqtrd 2799	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑂‘𝑗) − (𝑂‘0)) = ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
390	235, 341, 389	3eqtrd 2799	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥 = ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
391	390	oveq2d 7430	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) = (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
392	25	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑄 ∈ (Poly‘ℤ))
393		0zd 12628	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℤ)
394		etransclem46.a	. . . . . . . . . . 11 ⊢ 𝐴 = (coeff‘𝑄)
395	394	coef2 26458	. . . . . . . . . 10 ⊢ ((𝑄 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → 𝐴:ℕ₀⟶ℤ)
396	392, 393, 395	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐴:ℕ₀⟶ℤ)
397		elfznn0 13676	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ₀)
398	397	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ₀)
399	396, 398	ffvelcdmd 7079	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℤ)
400	399	zcnd 12727	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℂ)
401	351, 352	cxpcld 26946	. . . . . . . 8 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐𝑗) ∈ ℂ)
402	401	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑_𝑐𝑗) ∈ ℂ)
403	400, 402	mulcld 11254	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑_𝑐𝑗)) ∈ ℂ)
404	403, 384, 358	subdid 11695	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))) = ((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
405	391, 404	eqtrd 2795	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) = ((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
406	405	sumeq2dv 15790	. . 3 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) = Σ𝑗 ∈ (0...𝑀)((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
407		fzfid 14038	. . . . 5 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
408	403, 384	mulcld 11254	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) ∈ ℂ)
409	403, 358	mulcld 11254	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) ∈ ℂ)
410	407, 408, 409	fsumsub 15875	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))) = (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
411		etransclem46.qe0	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘e) = 0)
412	411	eqcomd 2766	. . . . . . . 8 ⊢ (𝜑 → 0 = (𝑄‘e))
413	394, 23	coeid2 26466	. . . . . . . . 9 ⊢ ((𝑄 ∈ (Poly‘ℤ) ∧ e ∈ ℂ) → (𝑄‘e) = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑𝑗)))
414	25, 9, 413	sylancl 598	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘e) = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑𝑗)))
415		cxpexp 26906	. . . . . . . . . . . . 13 ⊢ ((e ∈ ℂ ∧ 𝑗 ∈ ℕ₀) → (e↑_𝑐𝑗) = (e↑𝑗))
416	351, 397, 415	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐𝑗) = (e↑𝑗))
417	416	eqcomd 2766	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑀) → (e↑𝑗) = (e↑_𝑐𝑗))
418	417	oveq2d 7430	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...𝑀) → ((𝐴‘𝑗) · (e↑𝑗)) = ((𝐴‘𝑗) · (e↑_𝑐𝑗)))
419	418	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑𝑗)) = ((𝐴‘𝑗) · (e↑_𝑐𝑗)))
420	419	sumeq2dv 15790	. . . . . . . 8 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑𝑗)) = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑_𝑐𝑗)))
421	412, 414, 420	3eqtrd 2799	. . . . . . 7 ⊢ (𝜑 → 0 = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑_𝑐𝑗)))
422	421	oveq1d 7429	. . . . . 6 ⊢ (𝜑 → (0 · (𝐺‘0)) = (Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)))
423	373	mul02d 11433	. . . . . 6 ⊢ (𝜑 → (0 · (𝐺‘0)) = 0)
424	407, 373, 403	fsummulc1 15872	. . . . . 6 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)))
425	422, 423, 424	3eqtr3rd 2804	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) = 0)
426		fveq2 6879	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) = (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
427	426	sumeq2sdv 15791	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
428		fzfid 14038	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0...𝑅) ∈ Fin)
429	33	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
430	204	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → 𝑗 ∈ ℝ)
431	429, 430	ffvelcdmd 7079	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
432	428, 431	fsumcl 15820	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
433	38, 427, 204, 432	fvmptd3 7011	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐺‘𝑗) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
434	433	oveq2d 7430	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((e↑_𝑐-𝑗) · (𝐺‘𝑗)) = ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
435	434	oveq2d 7430	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))))
436	355, 432	mulcld 11254	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) ∈ ℂ)
437	400, 402, 436	mulassd 11257	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))) = ((𝐴‘𝑗) · ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))))
438	367	eqcomi 2769	. . . . . . . . . . . . . . 15 ⊢ 1 = (e↑_𝑐0)
439	438	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → 1 = (e↑_𝑐0))
440	352	negidd 11584	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 + -𝑗) = 0)
441	440	eqcomd 2766	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 0 = (𝑗 + -𝑗))
442	441	oveq2d 7430	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐0) = (e↑_𝑐(𝑗 + -𝑗)))
443	53, 54	gtneii 11347	. . . . . . . . . . . . . . . 16 ⊢ e ≠ 0
444	443	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → e ≠ 0)
445	351, 444, 352, 353	cxpaddd 26955	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐(𝑗 + -𝑗)) = ((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)))
446	439, 442, 445	3eqtrd 2799	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → 1 = ((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)))
447	446	oveq1d 7429	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = (((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
448	447	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = (((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
449	432	mullidd 11252	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
450	402, 355, 432	mulassd 11257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))))
451	448, 449, 450	3eqtr3rd 2804	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
452	451	oveq2d 7430	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))) = ((𝐴‘𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
453	428, 400, 431	fsummulc2 15871	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
454	452, 453	eqtrd 2795	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))) = Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
455	435, 437, 454	3eqtrd 2799	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
456	455	sumeq2dv 15790	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = Σ𝑗 ∈ (0...𝑀)Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
457		vex 3454	. . . . . . . . . 10 ⊢ 𝑗 ∈ V
458		vex 3454	. . . . . . . . . 10 ⊢ 𝑖 ∈ V
459	457, 458	op1std 7997	. . . . . . . . 9 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → (1^st ‘𝑘) = 𝑗)
460	459	fveq2d 6883	. . . . . . . 8 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → (𝐴‘(1^st ‘𝑘)) = (𝐴‘𝑗))
461	457, 458	op2ndd 7998	. . . . . . . . . 10 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → (2^nd ‘𝑘) = 𝑖)
462	461	fveq2d 6883	. . . . . . . . 9 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → ((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘)) = ((ℝ D^𝑛 𝐹)‘𝑖))
463	462, 459	fveq12d 6886	. . . . . . . 8 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘)) = (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
464	460, 463	oveq12d 7432	. . . . . . 7 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → ((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) = ((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
465		fzfid 14038	. . . . . . 7 ⊢ (𝜑 → (0...𝑅) ∈ Fin)
466	400	adantrr 730	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → (𝐴‘𝑗) ∈ ℂ)
467	431	anasss 472	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
468	466, 467	mulcld 11254	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → ((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) ∈ ℂ)
469	464, 407, 465, 468	fsumxp 15859	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
470	456, 469	eqtrd 2795	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
471	425, 470	oveq12d 7432	. . . 4 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))) = (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘)))))
472		df-neg 11469	. . . . . 6 ⊢ -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) = (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
473	472	eqcomi 2769	. . . . 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 2799	. . 3 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))) = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
476	2, 406, 475	3eqtrd 2799	. 2 ⊢ (𝜑 → 𝐿 = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
477	476	oveq1d 7429	1 ⊢ (𝜑 → (𝐿 / (!‘(𝑃 − 1))) = (-Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) / (!‘(𝑃 − 1))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ⊤wtru 1571 ∈ wcel 2145 ≠ wne 2955 Vcvv 3450 ∖ cdif 3896 ⊆ wss 3899 ifcif 4482 {csn 4584 {cpr 4586 ⟨cop 4590 class class class wbr 5103 ↦ cmpt 5186 × cxp 5653 ran crn 5656 ⟶wf 6529 ‘cfv 6533 (class class class)co 7414 1^st c1st 7985 2^nd c2nd 7986 ↑_pm cpm 8828 ℂcc 11123 ℝcr 11124 0cc0 11125 1c1 11126 + caddc 11128 · cmul 11130 -∞cmnf 11266 ℝ^*cxr 11267 < clt 11268 ≤ cle 11269 − cmin 11466 -cneg 11467 / cdiv 11896 ℕcn 12258 ℕ₀cn0 12529 ℤcz 12616 ℤ_≥cuz 12888 ℝ⁺crp 13043 (,)cioo 13399 (,]cioc 13400 [,]cicc 13402 ...cfz 13562 ↑cexp 14126 !cfa 14338 Σcsu 15774 ∏cprod 15993 eceu 16149 ↾_t crest 17506 TopOpenctopn 17507 topGenctg 17523 ℂ_fldccnfld 21586 intcnt 23243 –cn→ccncf 25105 𝐿¹cibl 25846 ∫citg 25847 0_𝑝c0p 25898 D cdv 26091 D^𝑛 cdvn 26092 Polycply 26410 coeffccoe 26412 degcdgr 26413 logclog 26792 ↑_𝑐ccxp 26793

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737 ax-inf2 9621 ax-cc 10438 ax-cnex 11181 ax-resscn 11182 ax-1cn 11183 ax-icn 11184 ax-addcl 11185 ax-addrcl 11186 ax-mulcl 11187 ax-mulrcl 11188 ax-mulcom 11189 ax-addass 11190 ax-mulass 11191 ax-distr 11192 ax-i2m1 11193 ax-1ne0 11194 ax-1rid 11195 ax-rnegex 11196 ax-rrecex 11197 ax-cnre 11198 ax-pre-lttri 11199 ax-pre-lttrn 11200 ax-pre-ltadd 11201 ax-pre-mulgt0 11202 ax-pre-sup 11203 ax-addf 11204

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-symdif 4199 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-disj 5071 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-isom 6542 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-of 7679 df-ofr 7680 df-om 7864 df-1st 7987 df-2nd 7988 df-supp 8160 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-1o 8456 df-2o 8457 df-oadd 8460 df-omul 8461 df-er 8697 df-map 8829 df-pm 8830 df-ixp 8906 df-en 8954 df-dom 8955 df-sdom 8956 df-fin 8957 df-fsupp 9333 df-fi 9382 df-sup 9413 df-inf 9414 df-oi 9483 df-dju 9907 df-card 9945 df-acn 9948 df-pnf 11270 df-mnf 11271 df-xr 11272 df-ltxr 11273 df-le 11274 df-sub 11468 df-neg 11469 df-div 11897 df-nn 12259 df-2 12328 df-3 12329 df-4 12330 df-5 12331 df-6 12332 df-7 12333 df-8 12334 df-9 12335 df-n0 12530 df-z 12617 df-dec 12738 df-uz 12889 df-q 12999 df-rp 13044 df-xneg 13164 df-xadd 13165 df-xmul 13166 df-ioo 13403 df-ioc 13404 df-ico 13405 df-icc 13406 df-fz 13563 df-fzo 13711 df-fl 13854 df-mod 13932 df-seq 14067 df-exp 14127 df-fac 14339 df-bc 14368 df-hash 14396 df-shft 15141 df-cj 15187 df-re 15188 df-im 15189 df-sqrt 15323 df-abs 15324 df-limsup 15559 df-clim 15576 df-rlim 15577 df-sum 15775 df-prod 15994 df-ef 16154 df-e 16155 df-sin 16156 df-cos 16157 df-tan 16158 df-pi 16159 df-struct 17240 df-sets 17257 df-slot 17275 df-ndx 17287 df-base 17303 df-ress 17324 df-plusg 17356 df-mulr 17357 df-starv 17358 df-sca 17359 df-vsca 17360 df-ip 17361 df-tset 17362 df-ple 17363 df-ds 17365 df-unif 17366 df-hom 17367 df-cco 17368 df-rest 17508 df-topn 17509 df-0g 17527 df-gsum 17528 df-topgen 17529 df-pt 17530 df-prds 17533 df-xrs 17589 df-qtop 17594 df-imas 17595 df-xps 17597 df-mre 17671 df-mrc 17672 df-acs 17674 df-mgm 18731 df-sgrp 18822 df-mnd 18838 df-submnd 18893 df-mulg 19192 df-cntz 19445 df-cmn 19910 df-psmet 21578 df-xmet 21579 df-met 21580 df-bl 21581 df-mopn 21582 df-fbas 21583 df-fg 21584 df-cnfld 21587 df-top 23120 df-topon 23137 df-topsp 23159 df-bases 23172 df-cld 23245 df-ntr 23246 df-cls 23247 df-nei 23324 df-lp 23362 df-perf 23363 df-cn 23453 df-cnp 23454 df-haus 23541 df-cmp 23613 df-tx 23789 df-hmeo 23982 df-fil 24073 df-fm 24165 df-flim 24166 df-flf 24167 df-xms 24547 df-ms 24548 df-tms 24549 df-cncf 25107 df-ovol 25693 df-vol 25694 df-mbf 25848 df-itg1 25849 df-itg2 25850 df-ibl 25851 df-itg 25852 df-0p 25899 df-limc 26094 df-dv 26095 df-dvn 26096 df-ply 26414 df-coe 26416 df-dgr 26417 df-log 26794 df-cxp 26795

This theorem is used by: etransclem47 47110

W3C validator