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 46524

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 7369	. . . . . . . . . . . . 13 ⊢ (ℝ D 𝑂) = (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
5	4	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) = (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))))
6		etransclem46.s	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
7	6	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℝ ∈ {ℝ, ℂ})
8		ere 16012	. . . . . . . . . . . . . . . . . . . 20 ⊢ e ∈ ℝ
9	8	recni 11146	. . . . . . . . . . . . . . . . . . 19 ⊢ e ∈ ℂ
10	9	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → e ∈ ℂ)
11		recn 11116	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
12	11	negcld 11479	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → -𝑥 ∈ ℂ)
13	10, 12	cxpcld 26673	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (e↑_𝑐-𝑥) ∈ ℂ)
14	13	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (e↑_𝑐-𝑥) ∈ ℂ)
15		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
16		fzfid 13896	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (0...𝑅) ∈ Fin)
17		elfznn0 13536	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ (0...𝑅) → 𝑖 ∈ ℕ₀)
18	6	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → ℝ ∈ {ℝ, ℂ})
19		etransclem46.x	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
20	19	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
21		etransclem46.p	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑃 ∈ ℕ)
22	21	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → 𝑃 ∈ ℕ)
23		etransclem46.m	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑀 = (deg‘𝑄)
24		etransclem46.q	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑄 ∈ ((Poly‘ℤ) ∖ {0_𝑝}))
25	24	eldifad 3913	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑄 ∈ (Poly‘ℤ))
26		dgrcl 26194	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑄 ∈ (Poly‘ℤ) → (deg‘𝑄) ∈ ℕ₀)
27	25, 26	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (deg‘𝑄) ∈ ℕ₀)
28	23, 27	eqeltrid 2840	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
29	28	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → 𝑀 ∈ ℕ₀)
30		etransclem46.f	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))
31		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → 𝑖 ∈ ℕ₀)
32	18, 20, 22, 29, 30, 31	etransclem33 46511	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
33	17, 32	sylan2 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
34	33	adantlr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
35		simplr 768	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → 𝑥 ∈ ℝ)
36	34, 35	ffvelcdmd 7030	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ)
37	16, 36	fsumcl 15656	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ)
38		etransclem46.g	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
39	38	fvmpt2 6952	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ) → (𝐺‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
40	15, 37, 39	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐺‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
41	40, 37	eqeltrd 2836	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐺‘𝑥) ∈ ℂ)
42	14, 41	mulcld 11152	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · (𝐺‘𝑥)) ∈ ℂ)
43	42	negcld 11479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) ∈ ℂ)
44	43	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ ℝ) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) ∈ ℂ)
45	6, 19	dvdmsscn 46180	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ℝ ⊆ ℂ)
46	45, 21, 30	etransclem8 46486	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
47	46	ffvelcdmda 7029	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℂ)
48	14, 47	mulcld 11152	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
49	48	negcld 11479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
50	49	negcld 11479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → --((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
51	50	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ ℝ) → --((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
52	8	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → e ∈ ℝ)
53		0re 11134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℝ
54		epos 16132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < e
55	53, 8, 54	ltleii 11256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ≤ e
56	55	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → 0 ≤ e)
57		renegcl 11444	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → -𝑥 ∈ ℝ)
58	52, 56, 57	recxpcld 26688	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → (e↑_𝑐-𝑥) ∈ ℝ)
59	58	renegcld 11564	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → -(e↑_𝑐-𝑥) ∈ ℝ)
60	59	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -(e↑_𝑐-𝑥) ∈ ℝ)
61		reelprrecn 11118	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℝ ∈ {ℝ, ℂ}
62	61	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → ℝ ∈ {ℝ, ℂ})
63		cnelprrecn 11119	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℂ ∈ {ℝ, ℂ}
64	63	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → ℂ ∈ {ℝ, ℂ})
65	12	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → -𝑥 ∈ ℂ)
66		neg1rr 12131	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ -1 ∈ ℝ
67	66	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → -1 ∈ ℝ)
68	9	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℂ → e ∈ ℂ)
69		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
70	68, 69	cxpcld 26673	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ℂ → (e↑_𝑐𝑦) ∈ ℂ)
71	70	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑦 ∈ ℂ) → (e↑_𝑐𝑦) ∈ ℂ)
72	11	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
73		1red 11133	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
74	62	dvmptid 25917	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
75	62, 72, 73, 74	dvmptneg 25926	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ -𝑥)) = (𝑥 ∈ ℝ ↦ -1))
76		epr 16133	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ e ∈ ℝ⁺
77		dvcxp2 26706	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (e ∈ ℝ⁺ → (ℂ D (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑_𝑐𝑦))))
78	76, 77	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℂ D (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑_𝑐𝑦)))
79		loge 26551	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (log‘e) = 1
80	79	oveq1i 7368	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((log‘e) · (e↑_𝑐𝑦)) = (1 · (e↑_𝑐𝑦))
81	70	mullidd 11150	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ ℂ → (1 · (e↑_𝑐𝑦)) = (e↑_𝑐𝑦))
82	80, 81	eqtrid 2783	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ℂ → ((log‘e) · (e↑_𝑐𝑦)) = (e↑_𝑐𝑦))
83	82	mpteq2ia 5193	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))
84	78, 83	eqtri 2759	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℂ D (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))
85	84	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)))
86		oveq2 7366	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = -𝑥 → (e↑_𝑐𝑦) = (e↑_𝑐-𝑥))
87	62, 64, 65, 67, 71, 71, 75, 85, 86, 86	dvmptco 25932	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ (e↑_𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -1)))
88	87	mptru 1548	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℝ D (𝑥 ∈ ℝ ↦ (e↑_𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -1))
89	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → -1 ∈ ℝ)
90	89	recnd 11160	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → -1 ∈ ℂ)
91	13, 90	mulcomd 11153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → ((e↑_𝑐-𝑥) · -1) = (-1 · (e↑_𝑐-𝑥)))
92	13	mulm1d 11589	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → (-1 · (e↑_𝑐-𝑥)) = -(e↑_𝑐-𝑥))
93	91, 92	eqtrd 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → ((e↑_𝑐-𝑥) · -1) = -(e↑_𝑐-𝑥))
94	93	mpteq2ia 5193	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -1)) = (𝑥 ∈ ℝ ↦ -(e↑_𝑐-𝑥))
95	88, 94	eqtri 2759	. . . . . . . . . . . . . . . . . 18 ⊢ (ℝ D (𝑥 ∈ ℝ ↦ (e↑_𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ -(e↑_𝑐-𝑥))
96	95	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (e↑_𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ -(e↑_𝑐-𝑥)))
97	17	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → 𝑖 ∈ ℕ₀)
98		peano2nn0 12441	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ ℕ₀ → (𝑖 + 1) ∈ ℕ₀)
99	97, 98	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → (𝑖 + 1) ∈ ℕ₀)
100		ovex 7391	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 + 1) ∈ V
101		eleq1 2824	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = (𝑖 + 1) → (𝑗 ∈ ℕ₀ ↔ (𝑖 + 1) ∈ ℕ₀))
102	101	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = (𝑖 + 1) → ((𝜑 ∧ 𝑗 ∈ ℕ₀) ↔ (𝜑 ∧ (𝑖 + 1) ∈ ℕ₀)))
103		fveq2 6834	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = (𝑖 + 1) → ((ℝ D^𝑛 𝐹)‘𝑗) = ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)))
104	103	feq1d 6644	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = (𝑖 + 1) → (((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ ↔ ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ))
105	102, 104	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖 + 1) → (((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ) ↔ ((𝜑 ∧ (𝑖 + 1) ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)))
106		eleq1 2824	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑗 → (𝑖 ∈ ℕ₀ ↔ 𝑗 ∈ ℕ₀))
107	106	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ ℕ₀) ↔ (𝜑 ∧ 𝑗 ∈ ℕ₀)))
108		fveq2 6834	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑗 → ((ℝ D^𝑛 𝐹)‘𝑖) = ((ℝ D^𝑛 𝐹)‘𝑗))
109	108	feq1d 6644	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖 = 𝑗 → (((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ ↔ ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ))
110	107, 109	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ) ↔ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ)))
111	110, 32	chvarvv 1990	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
112	100, 105, 111	vtocl 3515	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑖 + 1) ∈ ℕ₀) → ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
113	99, 112	syldan 591	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
114	113	adantlr 715	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
115	114, 35	ffvelcdmd 7030	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ)
116	16, 115	fsumcl 15656	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ)
117	21, 28, 30, 38	etransclem39 46517	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐺:ℝ⟶ℂ)
118	117	feqmptd 6902	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)))
119	118	eqcomd 2742	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)) = 𝐺)
120	119	oveq2d 7374	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝐺‘𝑥))) = (ℝ D 𝐺))
121		nfcv 2898	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥𝐹
122		elfznn0 13536	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 ∈ (0...(𝑅 + 1)) → 𝑖 ∈ ℕ₀)
123	122, 32	sylan2 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑅 + 1))) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
124	121, 46, 123, 38	etransclem2 46480	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℝ D 𝐺) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
125	120, 124	eqtrd 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝐺‘𝑥))) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
126	6, 14, 60, 96, 41, 116, 125	dvmptmul 25921	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ ℝ ↦ ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥)))))
127	116, 14	mulcomd 11153	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥)) = ((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
128	127	oveq2d 7374	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥))) = ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + ((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥))))
129	14	negcld 11479	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → -(e↑_𝑐-𝑥) ∈ ℂ)
130	129, 41	mulcld 11152	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) ∈ ℂ)
131	14, 116	mulcld 11152	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) ∈ ℂ)
132	130, 131	addcomd 11335	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + ((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) = (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑_𝑐-𝑥) · (𝐺‘𝑥))))
133	131, 42	negsubd 11498	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + -((e↑_𝑐-𝑥) · (𝐺‘𝑥))) = (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) − ((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
134	14, 41	mulneg1d 11590	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))
135	134	oveq2d 7374	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑_𝑐-𝑥) · (𝐺‘𝑥))) = (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + -((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
136	14, 116, 41	subdid 11593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥))) = (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) − ((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
137	133, 135, 136	3eqtr4d 2781	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑_𝑐-𝑥) · (𝐺‘𝑥))) = ((e↑_𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥))))
138	40	oveq2d 7374	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥)) = (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)))
139	16, 115, 36	fsumsub 15711	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)((((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)) = (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)))
140		fveq2 6834	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 𝑖 → ((ℝ D^𝑛 𝐹)‘𝑗) = ((ℝ D^𝑛 𝐹)‘𝑖))
141	140	fveq1d 6836	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 𝑖 → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥))
142	103	fveq1d 6836	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑖 + 1) → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥))
143		fveq2 6834	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = 0 → ((ℝ D^𝑛 𝐹)‘𝑗) = ((ℝ D^𝑛 𝐹)‘0))
144	143	fveq1d 6836	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 0 → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D^𝑛 𝐹)‘0)‘𝑥))
145		fveq2 6834	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 = (𝑅 + 1) → ((ℝ D^𝑛 𝐹)‘𝑗) = ((ℝ D^𝑛 𝐹)‘(𝑅 + 1)))
146	145	fveq1d 6836	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑅 + 1) → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥))
147		etransclem46.r	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑅 = ((𝑀 · 𝑃) + (𝑃 − 1))
148	21	nnnn0d 12462	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
149	28, 148	nn0mulcld 12467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℕ₀)
150		nnm1nn0 12442	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
151	21, 150	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑃 − 1) ∈ ℕ₀)
152	149, 151	nn0addcld 12466	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) ∈ ℕ₀)
153	147, 152	eqeltrid 2840	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑅 ∈ ℕ₀)
154	153	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑅 ∈ ℕ₀)
155	154	nn0zd 12513	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑅 ∈ ℤ)
156		peano2nn0 12441	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑅 ∈ ℕ₀ → (𝑅 + 1) ∈ ℕ₀)
157	153, 156	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑅 + 1) ∈ ℕ₀)
158		nn0uz 12789	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℕ₀ = (ℤ_≥‘0)
159	157, 158	eleqtrdi 2846	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑅 + 1) ∈ (ℤ_≥‘0))
160	159	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑅 + 1) ∈ (ℤ_≥‘0))
161		elfznn0 13536	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 ∈ (0...(𝑅 + 1)) → 𝑗 ∈ ℕ₀)
162	161, 111	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
163	162	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ D^𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
164		simplr 768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → 𝑥 ∈ ℝ)
165	163, 164	ffvelcdmd 7030	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → (((ℝ D^𝑛 𝐹)‘𝑗)‘𝑥) ∈ ℂ)
166	141, 142, 144, 146, 155, 160, 165	telfsum2 15728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)((((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥)) = ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥)))
167	138, 139, 166	3eqtr2d 2777	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥)) = ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥)))
168	167	oveq2d 7374	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺‘𝑥))) = ((e↑_𝑐-𝑥) · ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥))))
169	153	nn0red 12463	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑅 ∈ ℝ)
170	169	ltp1d 12072	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑅 < (𝑅 + 1))
171	147, 170	eqbrtrrid 5134	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) < (𝑅 + 1))
172		etransclem5 46483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))
173	6, 19, 21, 28, 30, 157, 171, 172	etransclem32 46510	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘(𝑅 + 1)) = (𝑥 ∈ ℝ ↦ 0))
174	173	fveq1d 6836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) = ((𝑥 ∈ ℝ ↦ 0)‘𝑥))
175		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ ℝ ↦ 0) = (𝑥 ∈ ℝ ↦ 0)
176	175	fvmpt2 6952	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ ℝ ∧ 0 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ 0)‘𝑥) = 0)
177	53, 176	mpan2 691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → ((𝑥 ∈ ℝ ↦ 0)‘𝑥) = 0)
178	174, 177	sylan9eq 2791	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) = 0)
179		cnex 11107	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ℂ ∈ V
180	179	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ℂ ∈ V)
181		etransclem46.rex	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ℝ ⊆ ℝ)
182	6, 181	ssexd 5269	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ℝ ∈ V)
183		elpm2r 8782	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:ℝ⟶ℂ ∧ ℝ ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑_pm ℝ))
184	180, 182, 46, 181, 183	syl22anc 838	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐹 ∈ (ℂ ↑_pm ℝ))
185		dvn0 25882	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℝ ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑_pm ℝ)) → ((ℝ D^𝑛 𝐹)‘0) = 𝐹)
186	45, 184, 185	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((ℝ D^𝑛 𝐹)‘0) = 𝐹)
187	186	fveq1d 6836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((ℝ D^𝑛 𝐹)‘0)‘𝑥) = (𝐹‘𝑥))
188	187	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((ℝ D^𝑛 𝐹)‘0)‘𝑥) = (𝐹‘𝑥))
189	178, 188	oveq12d 7376	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥)) = (0 − (𝐹‘𝑥)))
190		df-neg 11367	. . . . . . . . . . . . . . . . . . . . 21 ⊢ -(𝐹‘𝑥) = (0 − (𝐹‘𝑥))
191	189, 190	eqtr4di 2789	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥)) = -(𝐹‘𝑥))
192	191	oveq2d 7374	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · ((((ℝ D^𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D^𝑛 𝐹)‘0)‘𝑥))) = ((e↑_𝑐-𝑥) · -(𝐹‘𝑥)))
193	137, 168, 192	3eqtrd 2775	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((e↑_𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑_𝑐-𝑥) · (𝐺‘𝑥))) = ((e↑_𝑐-𝑥) · -(𝐹‘𝑥)))
194	128, 132, 193	3eqtrd 2775	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥))) = ((e↑_𝑐-𝑥) · -(𝐹‘𝑥)))
195	194	mpteq2dva 5191	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((-(e↑_𝑐-𝑥) · (𝐺‘𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑_𝑐-𝑥)))) = (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -(𝐹‘𝑥))))
196	14, 47	mulneg2d 11591	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((e↑_𝑐-𝑥) · -(𝐹‘𝑥)) = -((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
197	196	mpteq2dva 5191	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · -(𝐹‘𝑥))) = (𝑥 ∈ ℝ ↦ -((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
198	126, 195, 197	3eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ ℝ ↦ -((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
199	6, 42, 49, 198	dvmptneg 25926	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ ℝ ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
200	199	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D (𝑥 ∈ ℝ ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ ℝ ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
201		0red 11135	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ)
202		elfzelz 13440	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
203	202	zred 12596	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
204	203	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ)
205	201, 204	iccssred 13350	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℝ)
206		tgioo4 24749	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
207		eqid 2736	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
208		0red 11135	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 0 ∈ ℝ)
209		iccntr 24766	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ ∧ 𝑗 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
210	208, 203, 209	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
211	210	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
212	7, 44, 51, 200, 205, 206, 207, 211	dvmptres2 25922	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ (0(,)𝑗) ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
213	9	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → e ∈ ℂ)
214		elioore 13291	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℝ)
215	214	recnd 11160	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℂ)
216	215	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℂ)
217	216	negcld 11479	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℂ)
218	213, 217	cxpcld 26673	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) ∈ ℂ)
219	46	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝐹:ℝ⟶ℂ)
220	214	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
221	219, 220	ffvelcdmd 7030	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) ∈ ℂ)
222	218, 221	mulcld 11152	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
223	222	negnegd 11483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → --((e↑_𝑐-𝑥) · (𝐹‘𝑥)) = ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
224	223	mpteq2dva 5191	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (0(,)𝑗) ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
225	224	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ --((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
226	5, 212, 225	3eqtrd 2775	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))))
227	226	fveq1d 6836	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((ℝ D 𝑂)‘𝑥) = ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥))
228	227	adantr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((ℝ D 𝑂)‘𝑥) = ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥))
229		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ (0(,)𝑗))
230		eqid 2736	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
231	230	fvmpt2 6952	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥) = ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
232	229, 222, 231	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥) = ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
233	232	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))‘𝑥) = ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
234	228, 233	eqtr2d 2772	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) = ((ℝ D 𝑂)‘𝑥))
235	234	itgeq2dv 25739	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥 = ∫(0(,)𝑗)((ℝ D 𝑂)‘𝑥) d𝑥)
236		elfzle1 13443	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
237	236	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ 𝑗)
238		eqid 2736	. . . . . . . . . 10 ⊢ (𝑥 ∈ (0[,]𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = (𝑥 ∈ (0[,]𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥)))
239		eqidd 2737	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)) = (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)))
240	86	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) ∧ 𝑦 = -𝑥) → (e↑_𝑐𝑦) = (e↑_𝑐-𝑥))
241	208, 203	iccssred 13350	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑀) → (0[,]𝑗) ⊆ ℝ)
242		ax-resscn 11083	. . . . . . . . . . . . . . . . . . 19 ⊢ ℝ ⊆ ℂ
243	241, 242	sstrdi 3946	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑀) → (0[,]𝑗) ⊆ ℂ)
244	243	sselda 3933	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℂ)
245	244	negcld 11479	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → -𝑥 ∈ ℂ)
246	9	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → e ∈ ℂ)
247		negcl 11380	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → -𝑥 ∈ ℂ)
248	246, 247	cxpcld 26673	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → (e↑_𝑐-𝑥) ∈ ℂ)
249	244, 248	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑_𝑐-𝑥) ∈ ℂ)
250	239, 240, 245, 249	fvmptd 6948	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥) = (e↑_𝑐-𝑥))
251	250	eqcomd 2742	. . . . . . . . . . . . . 14 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑_𝑐-𝑥) = ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥))
252	251	adantll 714	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑_𝑐-𝑥) = ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥))
253	252	mpteq2dva 5191	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (e↑_𝑐-𝑥)) = (𝑥 ∈ (0[,]𝑗) ↦ ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥)))
254		mnfxr 11189	. . . . . . . . . . . . . . . . . 18 ⊢ -∞ ∈ ℝ^*
255	254	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℝ⁺ → -∞ ∈ ℝ^*)
256		0red 11135	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℝ⁺ → 0 ∈ ℝ)
257		rpxr 12915	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℝ⁺ → e ∈ ℝ^*)
258		rpgt0 12918	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℝ⁺ → 0 < e)
259	255, 256, 257, 258	gtnelioc 45737	. . . . . . . . . . . . . . . 16 ⊢ (e ∈ ℝ⁺ → ¬ e ∈ (-∞(,]0))
260	76, 259	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ¬ e ∈ (-∞(,]0)
261		eldif 3911	. . . . . . . . . . . . . . 15 ⊢ (e ∈ (ℂ ∖ (-∞(,]0)) ↔ (e ∈ ℂ ∧ ¬ e ∈ (-∞(,]0)))
262	9, 260, 261	mpbir2an 711	. . . . . . . . . . . . . 14 ⊢ e ∈ (ℂ ∖ (-∞(,]0))
263		cxpcncf2 46143	. . . . . . . . . . . . . 14 ⊢ (e ∈ (ℂ ∖ (-∞(,]0)) → (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)) ∈ (ℂ–cn→ℂ))
264	262, 263	mp1i 13	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦)) ∈ (ℂ–cn→ℂ))
265		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) = (𝑥 ∈ (0[,]𝑗) ↦ -𝑥)
266	265	negcncf 24871	. . . . . . . . . . . . . . 15 ⊢ ((0[,]𝑗) ⊆ ℂ → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
267	243, 266	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
268	267	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
269	264, 268	cncfmpt1f 24863	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((𝑦 ∈ ℂ ↦ (e↑_𝑐𝑦))‘-𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
270	253, 269	eqeltrd 2836	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (e↑_𝑐-𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
271	242	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → ℝ ⊆ ℂ)
272	21	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ)
273	28	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑀 ∈ ℕ₀)
274		etransclem6 46484	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦 − 𝑘)↑𝑃)))
275	30, 274	eqtri 2759	. . . . . . . . . . . . . 14 ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦 − 𝑘)↑𝑃)))
276	241	sselda 3933	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℝ)
277	276	adantll 714	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℝ)
278	271, 272, 273, 275, 277	etransclem13 46491	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝐹‘𝑥) = ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))
279	278	mpteq2dva 5191	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐹‘𝑥)) = (𝑥 ∈ (0[,]𝑗) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))))
280	243	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℂ)
281		fzfid 13896	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0...𝑀) ∈ Fin)
282	277	recnd 11160	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℂ)
283	282	3adant3 1132	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → 𝑥 ∈ ℂ)
284		elfzelz 13440	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ)
285	284	zcnd 12597	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ)
286	285	3ad2ant3 1135	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
287	283, 286	subcld 11492	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 − 𝑘) ∈ ℂ)
288	21	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ)
289	288, 150	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗)) → (𝑃 − 1) ∈ ℕ₀)
290	148	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ₀)
291	289, 290	ifcld 4526	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
292	291	3adant3 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
293	292	3adant1r 1178	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
294	287, 293	expcld 14069	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) ∈ ℂ)
295		nfv 1915	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀))
296	243	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℂ)
297		ssid 3956	. . . . . . . . . . . . . . . . . 18 ⊢ ℂ ⊆ ℂ
298	297	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
299	296, 298	idcncfg 46117	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ 𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
300	285	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
301	296, 300, 298	constcncfg 46116	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ 𝑘) ∈ ((0[,]𝑗)–cn→ℂ))
302	299, 301	subcncf 25401	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝑥 − 𝑘)) ∈ ((0[,]𝑗)–cn→ℂ))
303	302	adantll 714	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝑥 − 𝑘)) ∈ ((0[,]𝑗)–cn→ℂ))
304	151, 148	ifcld 4526	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
305		expcncf 24876	. . . . . . . . . . . . . . . 16 ⊢ (if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀ → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
306	304, 305	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
307	306	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
308	297	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
309		oveq1 7365	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑥 − 𝑘) → (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) = ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))
310	295, 303, 307, 308, 309	cncfcompt2 24857	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((0[,]𝑗)–cn→ℂ))
311	280, 281, 294, 310	fprodcncf 46144	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((0[,]𝑗)–cn→ℂ))
312	279, 311	eqeltrd 2836	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐹‘𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
313	270, 312	mulcncf 25402	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
314		ioossicc 13349	. . . . . . . . . . 11 ⊢ (0(,)𝑗) ⊆ (0[,]𝑗)
315	314	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0(,)𝑗) ⊆ (0[,]𝑗))
316	297	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
317	222	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
318	238, 313, 315, 316, 317	cncfmptssg 46115	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ ((0(,)𝑗)–cn→ℂ))
319	226, 318	eqeltrd 2836	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) ∈ ((0(,)𝑗)–cn→ℂ))
320	19	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
321	21	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑃 ∈ ℕ)
322	28	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℕ₀)
323		oveq2 7366	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑘 → (𝑥 − 𝑗) = (𝑥 − 𝑘))
324	323	oveq1d 7373	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑘 → ((𝑥 − 𝑗)↑𝑃) = ((𝑥 − 𝑘)↑𝑃))
325	324	cbvprodv 15837	. . . . . . . . . . . . 13 ⊢ ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃) = ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)
326	325	oveq2i 7369	. . . . . . . . . . . 12 ⊢ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)) = ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃))
327	326	mpteq2i 5194	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))
328	30, 327	eqtri 2759	. . . . . . . . . 10 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))
329	7, 320, 321, 322, 328, 201, 204	etransclem18 46496	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ 𝐿¹)
330	226, 329	eqeltrd 2836	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) ∈ 𝐿¹)
331		eqid 2736	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)) = (𝑥 ∈ ℝ ↦ (𝐺‘𝑥))
332	6, 19, 21, 28, 30, 38	etransclem43 46521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 ∈ (ℝ–cn→ℂ))
333	119, 332	eqeltrd 2836	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)) ∈ (ℝ–cn→ℂ))
334	333	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ ℝ ↦ (𝐺‘𝑥)) ∈ (ℝ–cn→ℂ))
335	117	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝐺:ℝ⟶ℂ)
336	335, 277	ffvelcdmd 7030	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝐺‘𝑥) ∈ ℂ)
337	331, 334, 205, 316, 336	cncfmptssg 46115	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐺‘𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
338	270, 337	mulcncf 25402	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐺‘𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
339	338	negcncfg 46125	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
340	3, 339	eqeltrid 2840	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑂 ∈ ((0[,]𝑗)–cn→ℂ))
341	201, 204, 237, 319, 330, 340	ftc2 26007	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((ℝ D 𝑂)‘𝑥) d𝑥 = ((𝑂‘𝑗) − (𝑂‘0)))
342		negeq 11372	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑗 → -𝑥 = -𝑗)
343	342	oveq2d 7374	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → (e↑_𝑐-𝑥) = (e↑_𝑐-𝑗))
344		fveq2 6834	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → (𝐺‘𝑥) = (𝐺‘𝑗))
345	343, 344	oveq12d 7376	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → ((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))
346	345	negeqd 11374	. . . . . . . . . 10 ⊢ (𝑥 = 𝑗 → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -((e↑_𝑐-𝑗) · (𝐺‘𝑗)))
347	201	rexrd 11182	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ^*)
348	204	rexrd 11182	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ^*)
349		ubicc2 13381	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ^* ∧ 𝑗 ∈ ℝ^* ∧ 0 ≤ 𝑗) → 𝑗 ∈ (0[,]𝑗))
350	347, 348, 237, 349	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0[,]𝑗))
351	9	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → e ∈ ℂ)
352	203	recnd 11160	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
353	352	negcld 11479	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → -𝑗 ∈ ℂ)
354	351, 353	cxpcld 26673	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐-𝑗) ∈ ℂ)
355	354	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑_𝑐-𝑗) ∈ ℂ)
356	117	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐺:ℝ⟶ℂ)
357	356, 204	ffvelcdmd 7030	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐺‘𝑗) ∈ ℂ)
358	355, 357	mulcld 11152	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((e↑_𝑐-𝑗) · (𝐺‘𝑗)) ∈ ℂ)
359	358	negcld 11479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → -((e↑_𝑐-𝑗) · (𝐺‘𝑗)) ∈ ℂ)
360	3, 346, 350, 359	fvmptd3 6964	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑂‘𝑗) = -((e↑_𝑐-𝑗) · (𝐺‘𝑗)))
361	3	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑂 = (𝑥 ∈ (0[,]𝑗) ↦ -((e↑_𝑐-𝑥) · (𝐺‘𝑥))))
362		negeq 11372	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 0 → -𝑥 = -0)
363	362	oveq2d 7374	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 0 → (e↑_𝑐-𝑥) = (e↑_𝑐-0))
364		neg0 11427	. . . . . . . . . . . . . . . . 17 ⊢ -0 = 0
365	364	oveq2i 7369	. . . . . . . . . . . . . . . 16 ⊢ (e↑_𝑐-0) = (e↑_𝑐0)
366		cxp0 26635	. . . . . . . . . . . . . . . . 17 ⊢ (e ∈ ℂ → (e↑_𝑐0) = 1)
367	9, 366	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (e↑_𝑐0) = 1
368	365, 367	eqtri 2759	. . . . . . . . . . . . . . 15 ⊢ (e↑_𝑐-0) = 1
369	363, 368	eqtrdi 2787	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 0 → (e↑_𝑐-𝑥) = 1)
370		fveq2 6834	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 0 → (𝐺‘𝑥) = (𝐺‘0))
371	369, 370	oveq12d 7376	. . . . . . . . . . . . 13 ⊢ (𝑥 = 0 → ((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = (1 · (𝐺‘0)))
372		0red 11135	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 0 ∈ ℝ)
373	117, 372	ffvelcdmd 7030	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺‘0) ∈ ℂ)
374	373	mullidd 11150	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 · (𝐺‘0)) = (𝐺‘0))
375	371, 374	sylan9eqr 2793	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 = 0) → ((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = (𝐺‘0))
376	375	negeqd 11374	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 = 0) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -(𝐺‘0))
377	376	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 = 0) → -((e↑_𝑐-𝑥) · (𝐺‘𝑥)) = -(𝐺‘0))
378		lbicc2 13380	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ^* ∧ 𝑗 ∈ ℝ^* ∧ 0 ≤ 𝑗) → 0 ∈ (0[,]𝑗))
379	347, 348, 237, 378	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ (0[,]𝑗))
380	373	negcld 11479	. . . . . . . . . . 11 ⊢ (𝜑 → -(𝐺‘0) ∈ ℂ)
381	380	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → -(𝐺‘0) ∈ ℂ)
382	361, 377, 379, 381	fvmptd 6948	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑂‘0) = -(𝐺‘0))
383	360, 382	oveq12d 7376	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑂‘𝑗) − (𝑂‘0)) = (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) − -(𝐺‘0)))
384	373	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐺‘0) ∈ ℂ)
385	359, 384	subnegd 11499	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) − -(𝐺‘0)) = (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) + (𝐺‘0)))
386	359, 384	addcomd 11335	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) + (𝐺‘0)) = ((𝐺‘0) + -((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
387	384, 358	negsubd 11498	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐺‘0) + -((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
388	386, 387	eqtrd 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (-((e↑_𝑐-𝑗) · (𝐺‘𝑗)) + (𝐺‘0)) = ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
389	383, 385, 388	3eqtrd 2775	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑂‘𝑗) − (𝑂‘0)) = ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
390	235, 341, 389	3eqtrd 2775	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥 = ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗))))
391	390	oveq2d 7374	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) = (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
392	25	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑄 ∈ (Poly‘ℤ))
393		0zd 12500	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℤ)
394		etransclem46.a	. . . . . . . . . . 11 ⊢ 𝐴 = (coeff‘𝑄)
395	394	coef2 26192	. . . . . . . . . 10 ⊢ ((𝑄 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → 𝐴:ℕ₀⟶ℤ)
396	392, 393, 395	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐴:ℕ₀⟶ℤ)
397		elfznn0 13536	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ₀)
398	397	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ₀)
399	396, 398	ffvelcdmd 7030	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℤ)
400	399	zcnd 12597	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℂ)
401	351, 352	cxpcld 26673	. . . . . . . 8 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐𝑗) ∈ ℂ)
402	401	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑_𝑐𝑗) ∈ ℂ)
403	400, 402	mulcld 11152	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑_𝑐𝑗)) ∈ ℂ)
404	403, 384, 358	subdid 11593	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((𝐺‘0) − ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))) = ((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
405	391, 404	eqtrd 2771	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) = ((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
406	405	sumeq2dv 15625	. . 3 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) = Σ𝑗 ∈ (0...𝑀)((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
407		fzfid 13896	. . . . 5 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
408	403, 384	mulcld 11152	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) ∈ ℂ)
409	403, 358	mulcld 11152	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) ∈ ℂ)
410	407, 408, 409	fsumsub 15711	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))) = (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))))
411		etransclem46.qe0	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘e) = 0)
412	411	eqcomd 2742	. . . . . . . 8 ⊢ (𝜑 → 0 = (𝑄‘e))
413	394, 23	coeid2 26200	. . . . . . . . 9 ⊢ ((𝑄 ∈ (Poly‘ℤ) ∧ e ∈ ℂ) → (𝑄‘e) = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑𝑗)))
414	25, 9, 413	sylancl 586	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘e) = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑𝑗)))
415		cxpexp 26633	. . . . . . . . . . . . 13 ⊢ ((e ∈ ℂ ∧ 𝑗 ∈ ℕ₀) → (e↑_𝑐𝑗) = (e↑𝑗))
416	351, 397, 415	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐𝑗) = (e↑𝑗))
417	416	eqcomd 2742	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...𝑀) → (e↑𝑗) = (e↑_𝑐𝑗))
418	417	oveq2d 7374	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...𝑀) → ((𝐴‘𝑗) · (e↑𝑗)) = ((𝐴‘𝑗) · (e↑_𝑐𝑗)))
419	418	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑𝑗)) = ((𝐴‘𝑗) · (e↑_𝑐𝑗)))
420	419	sumeq2dv 15625	. . . . . . . 8 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑𝑗)) = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑_𝑐𝑗)))
421	412, 414, 420	3eqtrd 2775	. . . . . . 7 ⊢ (𝜑 → 0 = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑_𝑐𝑗)))
422	421	oveq1d 7373	. . . . . 6 ⊢ (𝜑 → (0 · (𝐺‘0)) = (Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)))
423	373	mul02d 11331	. . . . . 6 ⊢ (𝜑 → (0 · (𝐺‘0)) = 0)
424	407, 373, 403	fsummulc1 15708	. . . . . 6 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)))
425	422, 423, 424	3eqtr3rd 2780	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) = 0)
426		fveq2 6834	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑗 → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) = (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
427	426	sumeq2sdv 15626	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑗 → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
428		fzfid 13896	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0...𝑅) ∈ Fin)
429	33	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D^𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
430	204	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → 𝑗 ∈ ℝ)
431	429, 430	ffvelcdmd 7030	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
432	428, 431	fsumcl 15656	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
433	38, 427, 204, 432	fvmptd3 6964	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐺‘𝑗) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
434	433	oveq2d 7374	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((e↑_𝑐-𝑗) · (𝐺‘𝑗)) = ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
435	434	oveq2d 7374	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))))
436	355, 432	mulcld 11152	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) ∈ ℂ)
437	400, 402, 436	mulassd 11155	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))) = ((𝐴‘𝑗) · ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))))
438	367	eqcomi 2745	. . . . . . . . . . . . . . 15 ⊢ 1 = (e↑_𝑐0)
439	438	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → 1 = (e↑_𝑐0))
440	352	negidd 11482	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 + -𝑗) = 0)
441	440	eqcomd 2742	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → 0 = (𝑗 + -𝑗))
442	441	oveq2d 7374	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐0) = (e↑_𝑐(𝑗 + -𝑗)))
443	53, 54	gtneii 11245	. . . . . . . . . . . . . . . 16 ⊢ e ≠ 0
444	443	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...𝑀) → e ≠ 0)
445	351, 444, 352, 353	cxpaddd 26682	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (e↑_𝑐(𝑗 + -𝑗)) = ((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)))
446	439, 442, 445	3eqtrd 2775	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → 1 = ((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)))
447	446	oveq1d 7373	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = (((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
448	447	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = (((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
449	432	mullidd 11150	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
450	402, 355, 432	mulassd 11155	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((e↑_𝑐𝑗) · (e↑_𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))))
451	448, 449, 450	3eqtr3rd 2780	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))) = Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
452	451	oveq2d 7374	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))) = ((𝐴‘𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
453	428, 400, 431	fsummulc2 15707	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
454	452, 453	eqtrd 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · ((e↑_𝑐𝑗) · ((e↑_𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))) = Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
455	435, 437, 454	3eqtrd 2775	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
456	455	sumeq2dv 15625	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = Σ𝑗 ∈ (0...𝑀)Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
457		vex 3444	. . . . . . . . . 10 ⊢ 𝑗 ∈ V
458		vex 3444	. . . . . . . . . 10 ⊢ 𝑖 ∈ V
459	457, 458	op1std 7943	. . . . . . . . 9 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → (1^st ‘𝑘) = 𝑗)
460	459	fveq2d 6838	. . . . . . . 8 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → (𝐴‘(1^st ‘𝑘)) = (𝐴‘𝑗))
461	457, 458	op2ndd 7944	. . . . . . . . . 10 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → (2^nd ‘𝑘) = 𝑖)
462	461	fveq2d 6838	. . . . . . . . 9 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → ((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘)) = ((ℝ D^𝑛 𝐹)‘𝑖))
463	462, 459	fveq12d 6841	. . . . . . . 8 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘)) = (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗))
464	460, 463	oveq12d 7376	. . . . . . 7 ⊢ (𝑘 = ⟨𝑗, 𝑖⟩ → ((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) = ((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)))
465		fzfid 13896	. . . . . . 7 ⊢ (𝜑 → (0...𝑅) ∈ Fin)
466	400	adantrr 717	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → (𝐴‘𝑗) ∈ ℂ)
467	431	anasss 466	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
468	466, 467	mulcld 11152	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → ((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) ∈ ℂ)
469	464, 407, 465, 468	fsumxp 15695	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)Σ𝑖 ∈ (0...𝑅)((𝐴‘𝑗) · (((ℝ D^𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
470	456, 469	eqtrd 2771	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗))) = Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
471	425, 470	oveq12d 7376	. . . 4 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))) = (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘)))))
472		df-neg 11367	. . . . . 6 ⊢ -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))) = (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
473	472	eqcomi 2745	. . . . 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 2775	. . 3 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((((𝐴‘𝑗) · (e↑_𝑐𝑗)) · (𝐺‘0)) − (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ((e↑_𝑐-𝑗) · (𝐺‘𝑗)))) = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
476	2, 406, 475	3eqtrd 2775	. 2 ⊢ (𝜑 → 𝐿 = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1^st ‘𝑘)) · (((ℝ D^𝑛 𝐹)‘(2^nd ‘𝑘))‘(1^st ‘𝑘))))
477	476	oveq1d 7373	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 395 ∧ w3a 1086 = wceq 1541 ⊤wtru 1542 ∈ wcel 2113 ≠ wne 2932 Vcvv 3440 ∖ cdif 3898 ⊆ wss 3901 ifcif 4479 {csn 4580 {cpr 4582 ⟨cop 4586 class class class wbr 5098 ↦ cmpt 5179 × cxp 5622 ran crn 5625 ⟶wf 6488 ‘cfv 6492 (class class class)co 7358 1^st c1st 7931 2^nd c2nd 7932 ↑_pm cpm 8764 ℂcc 11024 ℝcr 11025 0cc0 11026 1c1 11027 + caddc 11029 · cmul 11031 -∞cmnf 11164 ℝ^*cxr 11165 < clt 11166 ≤ cle 11167 − cmin 11364 -cneg 11365 / cdiv 11794 ℕcn 12145 ℕ₀cn0 12401 ℤcz 12488 ℤ_≥cuz 12751 ℝ⁺crp 12905 (,)cioo 13261 (,]cioc 13262 [,]cicc 13264 ...cfz 13423 ↑cexp 13984 !cfa 14196 Σcsu 15609 ∏cprod 15826 eceu 15985 ↾_t crest 17340 TopOpenctopn 17341 topGenctg 17357 ℂ_fldccnfld 21309 intcnt 22961 –cn→ccncf 24825 𝐿¹cibl 25574 ∫citg 25575 0_𝑝c0p 25626 D cdv 25820 D^𝑛 cdvn 25821 Polycply 26145 coeffccoe 26147 degcdgr 26148 logclog 26519 ↑_𝑐ccxp 26520

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-inf2 9550 ax-cc 10345 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103 ax-pre-sup 11104 ax-addf 11105

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-symdif 4205 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-tp 4585 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-iin 4949 df-disj 5066 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-se 5578 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-of 7622 df-ofr 7623 df-om 7809 df-1st 7933 df-2nd 7934 df-supp 8103 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-2o 8398 df-oadd 8401 df-omul 8402 df-er 8635 df-map 8765 df-pm 8766 df-ixp 8836 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fsupp 9265 df-fi 9314 df-sup 9345 df-inf 9346 df-oi 9415 df-dju 9813 df-card 9851 df-acn 9854 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-div 11795 df-nn 12146 df-2 12208 df-3 12209 df-4 12210 df-5 12211 df-6 12212 df-7 12213 df-8 12214 df-9 12215 df-n0 12402 df-z 12489 df-dec 12608 df-uz 12752 df-q 12862 df-rp 12906 df-xneg 13026 df-xadd 13027 df-xmul 13028 df-ioo 13265 df-ioc 13266 df-ico 13267 df-icc 13268 df-fz 13424 df-fzo 13571 df-fl 13712 df-mod 13790 df-seq 13925 df-exp 13985 df-fac 14197 df-bc 14226 df-hash 14254 df-shft 14990 df-cj 15022 df-re 15023 df-im 15024 df-sqrt 15158 df-abs 15159 df-limsup 15394 df-clim 15411 df-rlim 15412 df-sum 15610 df-prod 15827 df-ef 15990 df-e 15991 df-sin 15992 df-cos 15993 df-tan 15994 df-pi 15995 df-struct 17074 df-sets 17091 df-slot 17109 df-ndx 17121 df-base 17137 df-ress 17158 df-plusg 17190 df-mulr 17191 df-starv 17192 df-sca 17193 df-vsca 17194 df-ip 17195 df-tset 17196 df-ple 17197 df-ds 17199 df-unif 17200 df-hom 17201 df-cco 17202 df-rest 17342 df-topn 17343 df-0g 17361 df-gsum 17362 df-topgen 17363 df-pt 17364 df-prds 17367 df-xrs 17423 df-qtop 17428 df-imas 17429 df-xps 17431 df-mre 17505 df-mrc 17506 df-acs 17508 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-submnd 18709 df-mulg 18998 df-cntz 19246 df-cmn 19711 df-psmet 21301 df-xmet 21302 df-met 21303 df-bl 21304 df-mopn 21305 df-fbas 21306 df-fg 21307 df-cnfld 21310 df-top 22838 df-topon 22855 df-topsp 22877 df-bases 22890 df-cld 22963 df-ntr 22964 df-cls 22965 df-nei 23042 df-lp 23080 df-perf 23081 df-cn 23171 df-cnp 23172 df-haus 23259 df-cmp 23331 df-tx 23506 df-hmeo 23699 df-fil 23790 df-fm 23882 df-flim 23883 df-flf 23884 df-xms 24264 df-ms 24265 df-tms 24266 df-cncf 24827 df-ovol 25421 df-vol 25422 df-mbf 25576 df-itg1 25577 df-itg2 25578 df-ibl 25579 df-itg 25580 df-0p 25627 df-limc 25823 df-dv 25824 df-dvn 25825 df-ply 26149 df-coe 26151 df-dgr 26152 df-log 26521 df-cxp 26522

This theorem is referenced by: etransclem47 46525

W3C validator