etransclem23 - Mathbox for Glauco Siliprandi

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

Theorem etransclem23 46700

Description: This is the claim proof in [Juillerat] p. 14 (but in our proof, Stirling's approximation is not used). (Contributed by Glauco Siliprandi, 5-Apr-2020.)

**Hypotheses**
Ref	Expression
etransclem23.a	⊢ (𝜑 → 𝐴:ℕ₀⟶ℤ)
etransclem23.l	⊢ 𝐿 = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)
etransclem23.k	⊢ 𝐾 = (𝐿 / (!‘(𝑃 − 1)))
etransclem23.p	⊢ (𝜑 → 𝑃 ∈ ℕ)
etransclem23.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
etransclem23.f	⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))
etransclem23.lt1	⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))) < 1)

**Assertion**
Ref	Expression
etransclem23	⊢ (𝜑 → (abs‘𝐾) < 1)

Distinct variable groups: 𝑗,𝑀,𝑥 𝑃,𝑗,𝑥 𝜑,𝑗,𝑥 Allowed substitution hints: 𝐴(𝑥,𝑗) 𝐹(𝑥,𝑗) 𝐾(𝑥,𝑗) 𝐿(𝑥,𝑗)

Proof of Theorem etransclem23 Dummy variables ℎ 𝑘 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		etransclem23.k	. . . . . 6 ⊢ 𝐾 = (𝐿 / (!‘(𝑃 − 1)))
2		etransclem23.l	. . . . . . 7 ⊢ 𝐿 = Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)
3	2	oveq1i 7366	. . . . . 6 ⊢ (𝐿 / (!‘(𝑃 − 1))) = (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))
4	1, 3	eqtri 2762	. . . . 5 ⊢ 𝐾 = (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))
5	4	fveq2i 6830	. . . 4 ⊢ (abs‘𝐾) = (abs‘(Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1))))
6	5	a1i 11	. . 3 ⊢ (𝜑 → (abs‘𝐾) = (abs‘(Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))))
7		fzfid 13926	. . . . 5 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
8		etransclem23.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℤ)
9	8	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐴:ℕ₀⟶ℤ)
10		elfznn0 13565	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ₀)
11	10	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ₀)
12	9, 11	ffvelcdmd 7026	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℤ)
13	12	zcnd 12625	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℂ)
14		ere 16045	. . . . . . . . . 10 ⊢ e ∈ ℝ
15	14	recni 11150	. . . . . . . . 9 ⊢ e ∈ ℂ
16	15	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → e ∈ ℂ)
17		elfzelz 13469	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
18	17	zcnd 12625	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
19	18	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ)
20	16, 19	cxpcld 26690	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑_𝑐𝑗) ∈ ℂ)
21	13, 20	mulcld 11156	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑_𝑐𝑗)) ∈ ℂ)
22	15	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → e ∈ ℂ)
23		elioore 13319	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℝ)
24	23	recnd 11164	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℂ)
25	24	adantl 482	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℂ)
26	25	negcld 11483	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℂ)
27	22, 26	cxpcld 26690	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) ∈ ℂ)
28		ax-resscn 11086	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
29	28	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ ⊆ ℂ)
30		etransclem23.p	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℕ)
31		etransclem23.f	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))
32	29, 30, 31	etransclem8 46685	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
33	32	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝐹:ℝ⟶ℂ)
34	23	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
35	33, 34	ffvelcdmd 7026	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) ∈ ℂ)
36	35	adantlr 721	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) ∈ ℂ)
37	27, 36	mulcld 11156	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
38		reelprrecn 11121	. . . . . . . . 9 ⊢ ℝ ∈ {ℝ, ℂ}
39	38	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℝ ∈ {ℝ, ℂ})
40		reopn 45737	. . . . . . . . . 10 ⊢ ℝ ∈ (topGen‘ran (,))
41		tgioo4 24788	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
42	40, 41	eleqtri 2837	. . . . . . . . 9 ⊢ ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ)
43	42	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
44	30	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑃 ∈ ℕ)
45		etransclem23.m	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℕ)
46	45	nnnn0d 12489	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
47	46	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℕ₀)
48		etransclem6 46683	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏ℎ ∈ (1...𝑀)((𝑦 − ℎ)↑𝑃)))
49		etransclem6 46683	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏ℎ ∈ (1...𝑀)((𝑦 − ℎ)↑𝑃))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))
50	31, 48, 49	3eqtri 2766	. . . . . . . 8 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))
51		0red 11138	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ)
52	17	zred 12624	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
53	52	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ)
54	39, 43, 44, 47, 50, 51, 53	etransclem18 46695	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ 𝐿¹)
55	37, 54	itgcl 25769	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥 ∈ ℂ)
56	21, 55	mulcld 11156	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ∈ ℂ)
57	7, 56	fsumcl 15686	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ∈ ℂ)
58		nnm1nn0 12469	. . . . . . 7 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
59	30, 58	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑃 − 1) ∈ ℕ₀)
60	59	faccld 14237	. . . . 5 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℕ)
61	60	nncnd 12181	. . . 4 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℂ)
62	60	nnne0d 12218	. . . 4 ⊢ (𝜑 → (!‘(𝑃 − 1)) ≠ 0)
63	57, 61, 62	absdivd 15411	. . 3 ⊢ (𝜑 → (abs‘(Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))) = ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (abs‘(!‘(𝑃 − 1)))))
64	60	nnred 12180	. . . . 5 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℝ)
65	60	nnnn0d 12489	. . . . . 6 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℕ₀)
66	65	nn0ge0d 12492	. . . . 5 ⊢ (𝜑 → 0 ≤ (!‘(𝑃 − 1)))
67	64, 66	absidd 15376	. . . 4 ⊢ (𝜑 → (abs‘(!‘(𝑃 − 1))) = (!‘(𝑃 − 1)))
68	67	oveq2d 7372	. . 3 ⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (abs‘(!‘(𝑃 − 1)))) = ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))))
69	6, 63, 68	3eqtrd 2778	. 2 ⊢ (𝜑 → (abs‘𝐾) = ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))))
70	2, 57	eqeltrid 2843	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ℂ)
71	70, 61, 62	divcld 11922	. . . . . 6 ⊢ (𝜑 → (𝐿 / (!‘(𝑃 − 1))) ∈ ℂ)
72	1, 71	eqeltrid 2843	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℂ)
73	72	abscld 15392	. . . 4 ⊢ (𝜑 → (abs‘𝐾) ∈ ℝ)
74	69, 73	eqeltrrd 2840	. . 3 ⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))) ∈ ℝ)
75	45	nnred 12180	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℝ)
76	30	nnnn0d 12489	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
77	75, 76	reexpcld 14116	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑𝑃) ∈ ℝ)
78		peano2nn0 12468	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ₀ → (𝑀 + 1) ∈ ℕ₀)
79	46, 78	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ₀)
80	77, 79	reexpcld 14116	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℝ)
81	80	recnd 11164	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ)
82	45	nncnd 12181	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℂ)
83	81, 82	mulcomd 11157	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) = (𝑀 · ((𝑀↑𝑃)↑(𝑀 + 1))))
84	30	nncnd 12181	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ ℂ)
85		1cnd 11130	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℂ)
86	84, 85	npcand 11500	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑃 − 1) + 1) = 𝑃)
87	86	eqcomd 2745	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 = ((𝑃 − 1) + 1))
88	87	oveq2d 7372	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑𝑃) = ((𝑀↑(𝑀 + 1))↑((𝑃 − 1) + 1)))
89	79	nn0cnd 12491	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 + 1) ∈ ℂ)
90	89, 84	mulcomd 11157	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀 + 1) · 𝑃) = (𝑃 · (𝑀 + 1)))
91	90	oveq2d 7372	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑((𝑀 + 1) · 𝑃)) = (𝑀↑(𝑃 · (𝑀 + 1))))
92	82, 76, 79	expmuld 14102	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑((𝑀 + 1) · 𝑃)) = ((𝑀↑(𝑀 + 1))↑𝑃))
93	82, 79, 76	expmuld 14102	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑(𝑃 · (𝑀 + 1))) = ((𝑀↑𝑃)↑(𝑀 + 1)))
94	91, 92, 93	3eqtr3d 2782	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑𝑃) = ((𝑀↑𝑃)↑(𝑀 + 1)))
95	75, 79	reexpcld 14116	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℝ)
96	95	recnd 11164	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℂ)
97	96, 59	expp1d 14100	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑((𝑃 − 1) + 1)) = (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1))))
98	88, 94, 97	3eqtr3d 2782	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀↑𝑃)↑(𝑀 + 1)) = (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1))))
99	98	oveq2d 7372	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 · ((𝑀↑𝑃)↑(𝑀 + 1))) = (𝑀 · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1)))))
100	96, 59	expcld 14099	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) ∈ ℂ)
101	82, 100, 96	mul12d 11346	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀 · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1)))) = (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀 · (𝑀↑(𝑀 + 1)))))
102	82, 96	mulcld 11156	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ)
103	100, 102	mulcomd 11157	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀 · (𝑀↑(𝑀 + 1)))) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
104	101, 103	eqtrd 2774	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1)))) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
105	83, 99, 104	3eqtrd 2778	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
106	105	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
107	106	oveq2d 7372	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)))))
108	21	abscld 15392	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) ∈ ℝ)
109	108	recnd 11164	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) ∈ ℂ)
110	102	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ)
111	100	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) ∈ ℂ)
112	109, 110, 111	mulassd 11159	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) = ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)))))
113	107, 112	eqtr4d 2777	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = (((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
114	113	sumeq2dv 15655	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = Σ𝑗 ∈ (0...𝑀)(((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
115	109, 110	mulcld 11156	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
116	7, 100, 115	fsummulc1 15738	. . . . . . 7 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) = Σ𝑗 ∈ (0...𝑀)(((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
117	114, 116	eqtr4d 2777	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
118	117	oveq1d 7371	. . . . 5 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))) = ((Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) / (!‘(𝑃 − 1))))
119	7, 115	fsumcl 15686	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
120	119, 100, 61, 62	divassd 11957	. . . . 5 ⊢ (𝜑 → ((Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) / (!‘(𝑃 − 1))) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))))
121	118, 120	eqtrd 2774	. . . 4 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))))
122	80	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℝ)
123	75	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℝ)
124	122, 123	remulcld 11166	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) ∈ ℝ)
125	108, 124	remulcld 11166	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) ∈ ℝ)
126	7, 125	fsumrecl 15687	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) ∈ ℝ)
127	126, 60	nndivred 12222	. . . 4 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))) ∈ ℝ)
128	121, 127	eqeltrrd 2840	. . 3 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))) ∈ ℝ)
129		1red 11136	. . 3 ⊢ (𝜑 → 1 ∈ ℝ)
130	57	abscld 15392	. . . . 5 ⊢ (𝜑 → (abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ∈ ℝ)
131	60	nnrpd 12975	. . . . 5 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℝ⁺)
132	56	abscld 15392	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ∈ ℝ)
133	7, 132	fsumrecl 15687	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ∈ ℝ)
134	7, 56	fsumabs 15755	. . . . . 6 ⊢ (𝜑 → (abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)))
135	80	ad2antrr 732	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℝ)
136		ioombl 25550	. . . . . . . . . . . 12 ⊢ (0(,)𝑗) ∈ dom vol
137	136	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0(,)𝑗) ∈ dom vol)
138		0red 11138	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → 0 ∈ ℝ)
139		elfzle1 13472	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
140		volioo 25554	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ 𝑗 ∈ ℝ ∧ 0 ≤ 𝑗) → (vol‘(0(,)𝑗)) = (𝑗 − 0))
141	138, 52, 139, 140	syl3anc 1379	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) = (𝑗 − 0))
142	52, 138	resubcld 11569	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 0) ∈ ℝ)
143	141, 142	eqeltrd 2839	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) ∈ ℝ)
144	143	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (vol‘(0(,)𝑗)) ∈ ℝ)
145	81	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ)
146		iblconstmpt 46399	. . . . . . . . . . 11 ⊢ (((0(,)𝑗) ∈ dom vol ∧ (vol‘(0(,)𝑗)) ∈ ℝ ∧ ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ) → (𝑥 ∈ (0(,)𝑗) ↦ ((𝑀↑𝑃)↑(𝑀 + 1))) ∈ 𝐿¹)
147	137, 144, 145, 146	syl3anc 1379	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((𝑀↑𝑃)↑(𝑀 + 1))) ∈ 𝐿¹)
148	135, 147	itgrecl 25783	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 ∈ ℝ)
149	108, 148	remulcld 11166	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ∈ ℝ)
150	7, 149	fsumrecl 15687	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ∈ ℝ)
151	21, 55	absmuld 15410	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) = ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)))
152	55	abscld 15392	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ∈ ℝ)
153	21	absge0d 15400	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ (abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))))
154	37	abscld 15392	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ ℝ)
155	37, 54	iblabs 25814	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ (abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥)))) ∈ 𝐿¹)
156	154, 155	itgrecl 25783	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)(abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) d𝑥 ∈ ℝ)
157	37, 54	itgabs 25820	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ≤ ∫(0(,)𝑗)(abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) d𝑥)
158	27, 36	absmuld 15410	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = ((abs‘(e↑_𝑐-𝑥)) · (abs‘(𝐹‘𝑥))))
159	27	abscld 15392	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(e↑_𝑐-𝑥)) ∈ ℝ)
160		1red 11136	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 1 ∈ ℝ)
161	36	abscld 15392	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) ∈ ℝ)
162	27	absge0d 15400	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ (abs‘(e↑_𝑐-𝑥)))
163	36	absge0d 15400	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ (abs‘(𝐹‘𝑥)))
164	14	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0(,)𝑗) → e ∈ ℝ)
165		0re 11137	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℝ
166		epos 16165	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < e
167	165, 14, 166	ltleii 11260	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ≤ e
168	167	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0(,)𝑗) → 0 ≤ e)
169	23	renegcld 11568	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0(,)𝑗) → -𝑥 ∈ ℝ)
170	164, 168, 169	recxpcld 26705	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0(,)𝑗) → (e↑_𝑐-𝑥) ∈ ℝ)
171	164, 168, 169	cxpge0d 26706	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0(,)𝑗) → 0 ≤ (e↑_𝑐-𝑥))
172	170, 171	absidd 15376	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (0(,)𝑗) → (abs‘(e↑_𝑐-𝑥)) = (e↑_𝑐-𝑥))
173	172	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(e↑_𝑐-𝑥)) = (e↑_𝑐-𝑥))
174	170	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) ∈ ℝ)
175		1red 11136	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 1 ∈ ℝ)
176		0xr 11183	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℝ^*
177	176	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ∈ ℝ^*)
178	52	rexrd 11186	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ^*)
179	178	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑗 ∈ ℝ^*)
180		simpr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ (0(,)𝑗))
181		ioogtlb 45940	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ∈ ℝ^* ∧ 𝑗 ∈ ℝ^* ∧ 𝑥 ∈ (0(,)𝑗)) → 0 < 𝑥)
182	177, 179, 180, 181	syl3anc 1379	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 < 𝑥)
183	23	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
184	183	lt0neg2d 11711	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (0 < 𝑥 ↔ -𝑥 < 0))
185	182, 184	mpbid 233	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 < 0)
186	14	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → e ∈ ℝ)
187		1lt2 12338	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 < 2
188		egt2lt3 16164	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2 < e ∧ e < 3)
189	188	simpli 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 < e
190		1re 11135	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℝ
191		2re 12246	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℝ
192	190, 191, 14	lttri 11263	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 < 2 ∧ 2 < e) → 1 < e)
193	187, 189, 192	mp2an 698	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 < e
194	193	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 1 < e)
195	169	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℝ)
196		0red 11138	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ∈ ℝ)
197	186, 194, 195, 196	cxpltd 26701	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (-𝑥 < 0 ↔ (e↑_𝑐-𝑥) < (e↑_𝑐0)))
198	185, 197	mpbid 233	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) < (e↑_𝑐0))
199		cxp0 26652	. . . . . . . . . . . . . . . . . . . 20 ⊢ (e ∈ ℂ → (e↑_𝑐0) = 1)
200	15, 199	mp1i 13	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐0) = 1)
201	198, 200	breqtrd 5098	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) < 1)
202	174, 175, 201	ltled 11285	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) ≤ 1)
203	173, 202	eqbrtrd 5094	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(e↑_𝑐-𝑥)) ≤ 1)
204	203	adantll 720	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(e↑_𝑐-𝑥)) ≤ 1)
205	28	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ℝ ⊆ ℂ)
206	30	ad2antrr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑃 ∈ ℕ)
207	46	ad2antrr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑀 ∈ ℕ₀)
208	31, 48	eqtri 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏ℎ ∈ (1...𝑀)((𝑦 − ℎ)↑𝑃)))
209	23	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
210	205, 206, 207, 208, 209	etransclem13 46690	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) = ∏ℎ ∈ (0...𝑀)((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
211	210	fveq2d 6831	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) = (abs‘∏ℎ ∈ (0...𝑀)((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))))
212		nn0uz 12817	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ₀ = (ℤ_≥‘0)
213	23	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → 𝑥 ∈ ℝ)
214		nn0re 12437	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ ∈ ℕ₀ → ℎ ∈ ℝ)
215	214	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → ℎ ∈ ℝ)
216	213, 215	resubcld 11569	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → (𝑥 − ℎ) ∈ ℝ)
217	216	adantll 720	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → (𝑥 − ℎ) ∈ ℝ)
218	59, 76	ifcld 4501	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
219	218	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
220	217, 219	reexpcld 14116	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → ((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℝ)
221	220	recnd 11164	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → ((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℂ)
222	212, 207, 221	fprodabs 15930	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘∏ℎ ∈ (0...𝑀)((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))) = ∏ℎ ∈ (0...𝑀)(abs‘((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))))
223		elfznn0 13565	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ ∈ (0...𝑀) → ℎ ∈ ℕ₀)
224	24	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → 𝑥 ∈ ℂ)
225		nn0cn 12438	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ ∈ ℕ₀ → ℎ ∈ ℂ)
226	225	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → ℎ ∈ ℂ)
227	224, 226	subcld 11496	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → (𝑥 − ℎ) ∈ ℂ)
228	227	adantll 720	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → (𝑥 − ℎ) ∈ ℂ)
229	223, 228	sylan2 599	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ∈ ℂ)
230	218	ad3antrrr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
231	229, 230	absexpd 15408	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (abs‘((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))) = ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
232	231	prodeq2dv 15878	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)(abs‘((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))) = ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
233	211, 222, 232	3eqtrd 2778	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) = ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
234		nfv 1921	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎℎ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗))
235		fzfid 13926	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (0...𝑀) ∈ Fin)
236	223, 227	sylan2 599	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ∈ ℂ)
237	236	abscld 15392	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → (abs‘(𝑥 − ℎ)) ∈ ℝ)
238	237	adantll 720	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (abs‘(𝑥 − ℎ)) ∈ ℝ)
239	238, 230	reexpcld 14116	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℝ)
240	236	absge0d 15400	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ (abs‘(𝑥 − ℎ)))
241	240	adantll 720	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ (abs‘(𝑥 − ℎ)))
242	238, 230, 241	expge0d 14117	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
243	77	ad3antrrr 736	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀↑𝑃) ∈ ℝ)
244	75	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑀 ∈ ℝ)
245	244, 230	reexpcld 14116	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℝ)
246	223, 217	sylan2 599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ∈ ℝ)
247	24	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → 𝑥 ∈ ℂ)
248	223, 226	sylan2 599	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → ℎ ∈ ℂ)
249	247, 248	negsubdi2d 11512	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → -(𝑥 − ℎ) = (ℎ − 𝑥))
250	249	adantll 720	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → -(𝑥 − ℎ) = (ℎ − 𝑥))
251	223	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ℎ ∈ ℕ₀)
252	251	nn0red 12490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ℎ ∈ ℝ)
253		0red 11138	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ∈ ℝ)
254	209	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑥 ∈ ℝ)
255		elfzle2 13473	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ ∈ (0...𝑀) → ℎ ≤ 𝑀)
256	255	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ℎ ≤ 𝑀)
257	196, 183, 182	ltled 11285	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ 𝑥)
258	257	adantll 720	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ 𝑥)
259	258	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ 𝑥)
260	252, 253, 244, 254, 256, 259	le2subd 11761	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (ℎ − 𝑥) ≤ (𝑀 − 0))
261	82	subid1d 11485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑀 − 0) = 𝑀)
262	261	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀 − 0) = 𝑀)
263	260, 262	breqtrd 5098	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (ℎ − 𝑥) ≤ 𝑀)
264	250, 263	eqbrtrd 5094	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → -(𝑥 − ℎ) ≤ 𝑀)
265	246, 244, 264	lenegcon1d 11723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → -𝑀 ≤ (𝑥 − ℎ))
266		elfzel2 13467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
267	266	zred 12624	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
268	267	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑀 ∈ ℝ)
269	52	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑗 ∈ ℝ)
270		iooltub 45955	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0 ∈ ℝ^* ∧ 𝑗 ∈ ℝ^* ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 < 𝑗)
271	177, 179, 180, 270	syl3anc 1379	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 < 𝑗)
272		elfzle2 13473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀)
273	272	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑗 ≤ 𝑀)
274	183, 269, 268, 271, 273	ltletrd 11297	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 < 𝑀)
275	183, 268, 274	ltled 11285	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ≤ 𝑀)
276	275	adantll 720	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ≤ 𝑀)
277	276	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑥 ≤ 𝑀)
278	251	nn0ge0d 12492	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ ℎ)
279	254, 253, 244, 252, 277, 278	le2subd 11761	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ≤ (𝑀 − 0))
280	279, 262	breqtrd 5098	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ≤ 𝑀)
281	246, 244	absled 15386	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ)) ≤ 𝑀 ↔ (-𝑀 ≤ (𝑥 − ℎ) ∧ (𝑥 − ℎ) ≤ 𝑀)))
282	265, 280, 281	mpbir2and 719	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (abs‘(𝑥 − ℎ)) ≤ 𝑀)
283		leexp1a 14128	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((abs‘(𝑥 − ℎ)) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀) ∧ (0 ≤ (abs‘(𝑥 − ℎ)) ∧ (abs‘(𝑥 − ℎ)) ≤ 𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
284	238, 244, 230, 241, 282, 283	syl32anc 1386	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
285	45	nnge1d 12216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ≤ 𝑀)
286	285	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 1 ≤ 𝑀)
287	218	nn0zd 12540	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℤ)
288	76	nn0zd 12540	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑃 ∈ ℤ)
289		iftrue 4460	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = 0 → if(ℎ = 0, (𝑃 − 1), 𝑃) = (𝑃 − 1))
290	289	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) = (𝑃 − 1))
291	30	nnred 12180	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑃 ∈ ℝ)
292	291	lem1d 12080	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑃 − 1) ≤ 𝑃)
293	292	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ℎ = 0) → (𝑃 − 1) ≤ 𝑃)
294	290, 293	eqbrtrd 5094	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃)
295		iffalse 4463	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ ℎ = 0 → if(ℎ = 0, (𝑃 − 1), 𝑃) = 𝑃)
296	295	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ¬ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) = 𝑃)
297	291	leidd 11707	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑃 ≤ 𝑃)
298	297	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ¬ ℎ = 0) → 𝑃 ≤ 𝑃)
299	296, 298	eqbrtrd 5094	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ¬ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃)
300	294, 299	pm2.61dan 818	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃)
301		eluz2 12785	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ (ℤ_≥‘if(ℎ = 0, (𝑃 − 1), 𝑃)) ↔ (if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃))
302	287, 288, 300, 301	syl3anbrc 1350	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑃 ∈ (ℤ_≥‘if(ℎ = 0, (𝑃 − 1), 𝑃)))
303	302	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑃 ∈ (ℤ_≥‘if(ℎ = 0, (𝑃 − 1), 𝑃)))
304	244, 286, 303	leexp2ad 14207	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑𝑃))
305	239, 245, 243, 284, 304	letrd 11294	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑𝑃))
306	234, 235, 239, 242, 243, 305	fprodle 15952	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃))
307	77	recnd 11164	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀↑𝑃) ∈ ℂ)
308		fprodconst 15934	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0...𝑀) ∈ Fin ∧ (𝑀↑𝑃) ∈ ℂ) → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(♯‘(0...𝑀))))
309	7, 307, 308	syl2anc 590	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(♯‘(0...𝑀))))
310		hashfz0 14385	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ ℕ₀ → (♯‘(0...𝑀)) = (𝑀 + 1))
311	46, 310	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (♯‘(0...𝑀)) = (𝑀 + 1))
312	311	oveq2d 7372	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑀↑𝑃)↑(♯‘(0...𝑀))) = ((𝑀↑𝑃)↑(𝑀 + 1)))
313	309, 312	eqtrd 2774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(𝑀 + 1)))
314	313	ad2antrr 732	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(𝑀 + 1)))
315	306, 314	breqtrd 5098	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
316	233, 315	eqbrtrd 5094	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
317	159, 160, 161, 135, 162, 163, 204, 316	lemul12ad 12089	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((abs‘(e↑_𝑐-𝑥)) · (abs‘(𝐹‘𝑥))) ≤ (1 · ((𝑀↑𝑃)↑(𝑀 + 1))))
318	81	mullidd 11154	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · ((𝑀↑𝑃)↑(𝑀 + 1))) = ((𝑀↑𝑃)↑(𝑀 + 1)))
319	318	ad2antrr 732	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (1 · ((𝑀↑𝑃)↑(𝑀 + 1))) = ((𝑀↑𝑃)↑(𝑀 + 1)))
320	317, 319	breqtrd 5098	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((abs‘(e↑_𝑐-𝑥)) · (abs‘(𝐹‘𝑥))) ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
321	158, 320	eqbrtrd 5094	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
322	155, 147, 154, 135, 321	itgle 25795	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)(abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) d𝑥 ≤ ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥)
323	152, 156, 148, 157, 322	letrd 11294	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ≤ ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥)
324	152, 148, 108, 153, 323	lemul2ad 12087	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥))
325	151, 324	eqbrtrd 5094	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥))
326	7, 132, 149, 325	fsumle 15753	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥))
327		itgconst 25804	. . . . . . . . . . 11 ⊢ (((0(,)𝑗) ∈ dom vol ∧ (vol‘(0(,)𝑗)) ∈ ℝ ∧ ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 = (((𝑀↑𝑃)↑(𝑀 + 1)) · (vol‘(0(,)𝑗))))
328	137, 144, 145, 327	syl3anc 1379	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 = (((𝑀↑𝑃)↑(𝑀 + 1)) · (vol‘(0(,)𝑗))))
329	46	nn0ge0d 12492	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ≤ 𝑀)
330	75, 76, 329	expge0d 14117	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ (𝑀↑𝑃))
331	77, 79, 330	expge0d 14117	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
332	331	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
333	18	subid1d 11485	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 0) = 𝑗)
334	141, 333	eqtrd 2774	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) = 𝑗)
335	334, 272	eqbrtrd 5094	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) ≤ 𝑀)
336	335	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (vol‘(0(,)𝑗)) ≤ 𝑀)
337	144, 123, 122, 332, 336	lemul2ad 12087	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀↑𝑃)↑(𝑀 + 1)) · (vol‘(0(,)𝑗))) ≤ (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀))
338	328, 337	eqbrtrd 5094	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 ≤ (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀))
339	148, 124, 108, 153, 338	lemul2ad 12087	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ≤ ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)))
340	7, 149, 125, 339	fsumle 15753	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)))
341	133, 150, 126, 326, 340	letrd 11294	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)))
342	130, 133, 126, 134, 341	letrd 11294	. . . . 5 ⊢ (𝜑 → (abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)))
343	130, 126, 131, 342	lediv1dd 13035	. . . 4 ⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))) ≤ (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))))
344	343, 121	breqtrd 5098	. . 3 ⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))) ≤ (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))))
345		etransclem23.lt1	. . 3 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))) < 1)
346	74, 128, 129, 344, 345	lelttrd 11295	. 2 ⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))) < 1)
347	69, 346	eqbrtrd 5094	1 ⊢ (𝜑 → (abs‘𝐾) < 1)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 = wceq 1547 ∈ wcel 2119 ⊆ wss 3883 ifcif 4454 {cpr 4557 class class class wbr 5072 ↦ cmpt 5153 dom cdm 5618 ran crn 5619 ⟶wf 6481 ‘cfv 6485 (class class class)co 7356 Fincfn 8883 ℂcc 11027 ℝcr 11028 0cc0 11029 1c1 11030 + caddc 11032 · cmul 11034 ℝ^*cxr 11169 < clt 11170 ≤ cle 11171 − cmin 11368 -cneg 11369 / cdiv 11798 ℕcn 12165 2c2 12227 3c3 12228 ℕ₀cn0 12428 ℤcz 12515 ℤ_≥cuz 12779 (,)cioo 13289 ...cfz 13452 ↑cexp 14014 !cfa 14226 ♯chash 14283 abscabs 15187 Σcsu 15639 ∏cprod 15859 eceu 16018 ↾_t crest 17374 TopOpenctopn 17375 topGenctg 17391 ℂ_fldccnfld 21347 volcvol 25448 𝐿¹cibl 25602 ∫citg 25603 ↑_𝑐ccxp 26537

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-inf2 9553 ax-cc 10348 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107 ax-addf 11108

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-tp 4560 df-op 4562 df-uni 4839 df-int 4878 df-iun 4923 df-iin 4924 df-disj 5040 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-se 5572 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-isom 6494 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-of 7620 df-ofr 7621 df-om 7807 df-1st 7931 df-2nd 7932 df-supp 8101 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-oadd 8399 df-omul 8400 df-er 8633 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 9816 df-card 9854 df-acn 9857 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-3 12236 df-4 12237 df-5 12238 df-6 12239 df-7 12240 df-8 12241 df-9 12242 df-n0 12429 df-z 12516 df-dec 12636 df-uz 12780 df-q 12890 df-rp 12934 df-xneg 13054 df-xadd 13055 df-xmul 13056 df-ioo 13293 df-ioc 13294 df-ico 13295 df-icc 13296 df-fz 13453 df-fzo 13600 df-fl 13742 df-mod 13820 df-seq 13955 df-exp 14015 df-fac 14227 df-bc 14256 df-hash 14284 df-shft 15020 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-limsup 15424 df-clim 15441 df-rlim 15442 df-sum 15640 df-prod 15860 df-ef 16023 df-e 16024 df-sin 16025 df-cos 16026 df-tan 16027 df-pi 16028 df-struct 17108 df-sets 17125 df-slot 17143 df-ndx 17155 df-base 17171 df-ress 17192 df-plusg 17224 df-mulr 17225 df-starv 17226 df-sca 17227 df-vsca 17228 df-ip 17229 df-tset 17230 df-ple 17231 df-ds 17233 df-unif 17234 df-hom 17235 df-cco 17236 df-rest 17376 df-topn 17377 df-0g 17395 df-gsum 17396 df-topgen 17397 df-pt 17398 df-prds 17401 df-xrs 17457 df-qtop 17462 df-imas 17463 df-xps 17465 df-mre 17539 df-mrc 17540 df-acs 17542 df-mgm 18599 df-sgrp 18678 df-mnd 18694 df-submnd 18743 df-mulg 19035 df-cntz 19283 df-cmn 19748 df-psmet 21339 df-xmet 21340 df-met 21341 df-bl 21342 df-mopn 21343 df-fbas 21344 df-fg 21345 df-cnfld 21348 df-top 22877 df-topon 22894 df-topsp 22916 df-bases 22929 df-cld 23002 df-ntr 23003 df-cls 23004 df-nei 23081 df-lp 23119 df-perf 23120 df-cn 23210 df-cnp 23211 df-haus 23298 df-cmp 23370 df-tx 23545 df-hmeo 23738 df-fil 23829 df-fm 23921 df-flim 23922 df-flf 23923 df-xms 24303 df-ms 24304 df-tms 24305 df-cncf 24863 df-ovol 25449 df-vol 25450 df-mbf 25604 df-itg1 25605 df-itg2 25606 df-ibl 25607 df-itg 25608 df-0p 25655 df-limc 25851 df-dv 25852 df-log 26538 df-cxp 26539

This theorem is referenced by: etransclem47 46724

W3C validator