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 46277

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 7442	. . . . . 6 ⊢ (𝐿 / (!‘(𝑃 − 1))) = (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))
4	1, 3	eqtri 2764	. . . . 5 ⊢ 𝐾 = (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))
5	4	fveq2i 6908	. . . 4 ⊢ (abs‘𝐾) = (abs‘(Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1))))
6	5	a1i 11	. . 3 ⊢ (𝜑 → (abs‘𝐾) = (abs‘(Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))))
7		fzfid 14015	. . . . 5 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
8		etransclem23.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℤ)
9	8	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐴:ℕ₀⟶ℤ)
10		elfznn0 13661	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ₀)
11	10	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ₀)
12	9, 11	ffvelcdmd 7104	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℤ)
13	12	zcnd 12725	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℂ)
14		ere 16126	. . . . . . . . . 10 ⊢ e ∈ ℝ
15	14	recni 11276	. . . . . . . . 9 ⊢ e ∈ ℂ
16	15	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → e ∈ ℂ)
17		elfzelz 13565	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
18	17	zcnd 12725	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
19	18	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ)
20	16, 19	cxpcld 26751	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑_𝑐𝑗) ∈ ℂ)
21	13, 20	mulcld 11282	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑_𝑐𝑗)) ∈ ℂ)
22	15	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → e ∈ ℂ)
23		elioore 13418	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℝ)
24	23	recnd 11290	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℂ)
25	24	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℂ)
26	25	negcld 11608	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℂ)
27	22, 26	cxpcld 26751	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) ∈ ℂ)
28		ax-resscn 11213	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
29	28	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ ⊆ ℂ)
30		etransclem23.p	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℕ)
31		etransclem23.f	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))
32	29, 30, 31	etransclem8 46262	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
33	32	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝐹:ℝ⟶ℂ)
34	23	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
35	33, 34	ffvelcdmd 7104	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) ∈ ℂ)
36	35	adantlr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) ∈ ℂ)
37	27, 36	mulcld 11282	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
38		reelprrecn 11248	. . . . . . . . 9 ⊢ ℝ ∈ {ℝ, ℂ}
39	38	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℝ ∈ {ℝ, ℂ})
40		reopn 45306	. . . . . . . . . 10 ⊢ ℝ ∈ (topGen‘ran (,))
41		tgioo4 24827	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
42	40, 41	eleqtri 2838	. . . . . . . . 9 ⊢ ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ)
43	42	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
44	30	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑃 ∈ ℕ)
45		etransclem23.m	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℕ)
46	45	nnnn0d 12589	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
47	46	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℕ₀)
48		etransclem6 46260	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏ℎ ∈ (1...𝑀)((𝑦 − ℎ)↑𝑃)))
49		etransclem6 46260	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏ℎ ∈ (1...𝑀)((𝑦 − ℎ)↑𝑃))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))
50	31, 48, 49	3eqtri 2768	. . . . . . . 8 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))
51		0red 11265	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ)
52	17	zred 12724	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
53	52	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ)
54	39, 43, 44, 47, 50, 51, 53	etransclem18 46272	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ 𝐿¹)
55	37, 54	itgcl 25820	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥 ∈ ℂ)
56	21, 55	mulcld 11282	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ∈ ℂ)
57	7, 56	fsumcl 15770	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ∈ ℂ)
58		nnm1nn0 12569	. . . . . . 7 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
59	30, 58	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑃 − 1) ∈ ℕ₀)
60	59	faccld 14324	. . . . 5 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℕ)
61	60	nncnd 12283	. . . 4 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℂ)
62	60	nnne0d 12317	. . . 4 ⊢ (𝜑 → (!‘(𝑃 − 1)) ≠ 0)
63	57, 61, 62	absdivd 15495	. . 3 ⊢ (𝜑 → (abs‘(Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))) = ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (abs‘(!‘(𝑃 − 1)))))
64	60	nnred 12282	. . . . 5 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℝ)
65	60	nnnn0d 12589	. . . . . 6 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℕ₀)
66	65	nn0ge0d 12592	. . . . 5 ⊢ (𝜑 → 0 ≤ (!‘(𝑃 − 1)))
67	64, 66	absidd 15462	. . . 4 ⊢ (𝜑 → (abs‘(!‘(𝑃 − 1))) = (!‘(𝑃 − 1)))
68	67	oveq2d 7448	. . 3 ⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (abs‘(!‘(𝑃 − 1)))) = ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))))
69	6, 63, 68	3eqtrd 2780	. 2 ⊢ (𝜑 → (abs‘𝐾) = ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))))
70	2, 57	eqeltrid 2844	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ℂ)
71	70, 61, 62	divcld 12044	. . . . . 6 ⊢ (𝜑 → (𝐿 / (!‘(𝑃 − 1))) ∈ ℂ)
72	1, 71	eqeltrid 2844	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℂ)
73	72	abscld 15476	. . . 4 ⊢ (𝜑 → (abs‘𝐾) ∈ ℝ)
74	69, 73	eqeltrrd 2841	. . 3 ⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))) ∈ ℝ)
75	45	nnred 12282	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℝ)
76	30	nnnn0d 12589	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
77	75, 76	reexpcld 14204	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑𝑃) ∈ ℝ)
78		peano2nn0 12568	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ₀ → (𝑀 + 1) ∈ ℕ₀)
79	46, 78	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ₀)
80	77, 79	reexpcld 14204	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℝ)
81	80	recnd 11290	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ)
82	45	nncnd 12283	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℂ)
83	81, 82	mulcomd 11283	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) = (𝑀 · ((𝑀↑𝑃)↑(𝑀 + 1))))
84	30	nncnd 12283	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ ℂ)
85		1cnd 11257	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℂ)
86	84, 85	npcand 11625	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑃 − 1) + 1) = 𝑃)
87	86	eqcomd 2742	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 = ((𝑃 − 1) + 1))
88	87	oveq2d 7448	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑𝑃) = ((𝑀↑(𝑀 + 1))↑((𝑃 − 1) + 1)))
89	79	nn0cnd 12591	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 + 1) ∈ ℂ)
90	89, 84	mulcomd 11283	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀 + 1) · 𝑃) = (𝑃 · (𝑀 + 1)))
91	90	oveq2d 7448	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑((𝑀 + 1) · 𝑃)) = (𝑀↑(𝑃 · (𝑀 + 1))))
92	82, 76, 79	expmuld 14190	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑((𝑀 + 1) · 𝑃)) = ((𝑀↑(𝑀 + 1))↑𝑃))
93	82, 79, 76	expmuld 14190	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑(𝑃 · (𝑀 + 1))) = ((𝑀↑𝑃)↑(𝑀 + 1)))
94	91, 92, 93	3eqtr3d 2784	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑𝑃) = ((𝑀↑𝑃)↑(𝑀 + 1)))
95	75, 79	reexpcld 14204	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℝ)
96	95	recnd 11290	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℂ)
97	96, 59	expp1d 14188	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑((𝑃 − 1) + 1)) = (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1))))
98	88, 94, 97	3eqtr3d 2784	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀↑𝑃)↑(𝑀 + 1)) = (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1))))
99	98	oveq2d 7448	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 · ((𝑀↑𝑃)↑(𝑀 + 1))) = (𝑀 · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1)))))
100	96, 59	expcld 14187	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) ∈ ℂ)
101	82, 100, 96	mul12d 11471	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀 · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1)))) = (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀 · (𝑀↑(𝑀 + 1)))))
102	82, 96	mulcld 11282	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ)
103	100, 102	mulcomd 11283	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀 · (𝑀↑(𝑀 + 1)))) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
104	101, 103	eqtrd 2776	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1)))) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
105	83, 99, 104	3eqtrd 2780	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
106	105	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
107	106	oveq2d 7448	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)))))
108	21	abscld 15476	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) ∈ ℝ)
109	108	recnd 11290	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) ∈ ℂ)
110	102	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ)
111	100	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) ∈ ℂ)
112	109, 110, 111	mulassd 11285	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) = ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)))))
113	107, 112	eqtr4d 2779	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = (((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
114	113	sumeq2dv 15739	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = Σ𝑗 ∈ (0...𝑀)(((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
115	109, 110	mulcld 11282	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
116	7, 100, 115	fsummulc1 15822	. . . . . . 7 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) = Σ𝑗 ∈ (0...𝑀)(((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
117	114, 116	eqtr4d 2779	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
118	117	oveq1d 7447	. . . . 5 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))) = ((Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) / (!‘(𝑃 − 1))))
119	7, 115	fsumcl 15770	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
120	119, 100, 61, 62	divassd 12079	. . . . 5 ⊢ (𝜑 → ((Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) / (!‘(𝑃 − 1))) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))))
121	118, 120	eqtrd 2776	. . . 4 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))))
122	80	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℝ)
123	75	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℝ)
124	122, 123	remulcld 11292	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) ∈ ℝ)
125	108, 124	remulcld 11292	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) ∈ ℝ)
126	7, 125	fsumrecl 15771	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) ∈ ℝ)
127	126, 60	nndivred 12321	. . . 4 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))) ∈ ℝ)
128	121, 127	eqeltrrd 2841	. . 3 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))) ∈ ℝ)
129		1red 11263	. . 3 ⊢ (𝜑 → 1 ∈ ℝ)
130	57	abscld 15476	. . . . 5 ⊢ (𝜑 → (abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ∈ ℝ)
131	60	nnrpd 13076	. . . . 5 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℝ⁺)
132	56	abscld 15476	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ∈ ℝ)
133	7, 132	fsumrecl 15771	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ∈ ℝ)
134	7, 56	fsumabs 15838	. . . . . 6 ⊢ (𝜑 → (abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)))
135	80	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℝ)
136		ioombl 25601	. . . . . . . . . . . 12 ⊢ (0(,)𝑗) ∈ dom vol
137	136	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0(,)𝑗) ∈ dom vol)
138		0red 11265	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → 0 ∈ ℝ)
139		elfzle1 13568	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
140		volioo 25605	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ 𝑗 ∈ ℝ ∧ 0 ≤ 𝑗) → (vol‘(0(,)𝑗)) = (𝑗 − 0))
141	138, 52, 139, 140	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) = (𝑗 − 0))
142	52, 138	resubcld 11692	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 0) ∈ ℝ)
143	141, 142	eqeltrd 2840	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) ∈ ℝ)
144	143	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (vol‘(0(,)𝑗)) ∈ ℝ)
145	81	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ)
146		iblconstmpt 45976	. . . . . . . . . . 11 ⊢ (((0(,)𝑗) ∈ dom vol ∧ (vol‘(0(,)𝑗)) ∈ ℝ ∧ ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ) → (𝑥 ∈ (0(,)𝑗) ↦ ((𝑀↑𝑃)↑(𝑀 + 1))) ∈ 𝐿¹)
147	137, 144, 145, 146	syl3anc 1372	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((𝑀↑𝑃)↑(𝑀 + 1))) ∈ 𝐿¹)
148	135, 147	itgrecl 25834	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 ∈ ℝ)
149	108, 148	remulcld 11292	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ∈ ℝ)
150	7, 149	fsumrecl 15771	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ∈ ℝ)
151	21, 55	absmuld 15494	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) = ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)))
152	55	abscld 15476	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ∈ ℝ)
153	21	absge0d 15484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ (abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))))
154	37	abscld 15476	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ ℝ)
155	37, 54	iblabs 25865	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ (abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥)))) ∈ 𝐿¹)
156	154, 155	itgrecl 25834	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)(abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) d𝑥 ∈ ℝ)
157	37, 54	itgabs 25871	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ≤ ∫(0(,)𝑗)(abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) d𝑥)
158	27, 36	absmuld 15494	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = ((abs‘(e↑_𝑐-𝑥)) · (abs‘(𝐹‘𝑥))))
159	27	abscld 15476	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(e↑_𝑐-𝑥)) ∈ ℝ)
160		1red 11263	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 1 ∈ ℝ)
161	36	abscld 15476	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) ∈ ℝ)
162	27	absge0d 15484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ (abs‘(e↑_𝑐-𝑥)))
163	36	absge0d 15484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ (abs‘(𝐹‘𝑥)))
164	14	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0(,)𝑗) → e ∈ ℝ)
165		0re 11264	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℝ
166		epos 16244	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < e
167	165, 14, 166	ltleii 11385	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ≤ e
168	167	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0(,)𝑗) → 0 ≤ e)
169	23	renegcld 11691	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0(,)𝑗) → -𝑥 ∈ ℝ)
170	164, 168, 169	recxpcld 26766	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0(,)𝑗) → (e↑_𝑐-𝑥) ∈ ℝ)
171	164, 168, 169	cxpge0d 26767	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0(,)𝑗) → 0 ≤ (e↑_𝑐-𝑥))
172	170, 171	absidd 15462	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (0(,)𝑗) → (abs‘(e↑_𝑐-𝑥)) = (e↑_𝑐-𝑥))
173	172	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(e↑_𝑐-𝑥)) = (e↑_𝑐-𝑥))
174	170	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) ∈ ℝ)
175		1red 11263	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 1 ∈ ℝ)
176		0xr 11309	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℝ^*
177	176	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ∈ ℝ^*)
178	52	rexrd 11312	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ^*)
179	178	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑗 ∈ ℝ^*)
180		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ (0(,)𝑗))
181		ioogtlb 45513	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ∈ ℝ^* ∧ 𝑗 ∈ ℝ^* ∧ 𝑥 ∈ (0(,)𝑗)) → 0 < 𝑥)
182	177, 179, 180, 181	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 < 𝑥)
183	23	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
184	183	lt0neg2d 11834	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (0 < 𝑥 ↔ -𝑥 < 0))
185	182, 184	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 < 0)
186	14	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → e ∈ ℝ)
187		1lt2 12438	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 < 2
188		egt2lt3 16243	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2 < e ∧ e < 3)
189	188	simpli 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 < e
190		1re 11262	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℝ
191		2re 12341	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℝ
192	190, 191, 14	lttri 11388	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 < 2 ∧ 2 < e) → 1 < e)
193	187, 189, 192	mp2an 692	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 < e
194	193	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 1 < e)
195	169	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℝ)
196		0red 11265	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ∈ ℝ)
197	186, 194, 195, 196	cxpltd 26762	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (-𝑥 < 0 ↔ (e↑_𝑐-𝑥) < (e↑_𝑐0)))
198	185, 197	mpbid 232	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) < (e↑_𝑐0))
199		cxp0 26713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (e ∈ ℂ → (e↑_𝑐0) = 1)
200	15, 199	mp1i 13	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐0) = 1)
201	198, 200	breqtrd 5168	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) < 1)
202	174, 175, 201	ltled 11410	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) ≤ 1)
203	173, 202	eqbrtrd 5164	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(e↑_𝑐-𝑥)) ≤ 1)
204	203	adantll 714	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(e↑_𝑐-𝑥)) ≤ 1)
205	28	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ℝ ⊆ ℂ)
206	30	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑃 ∈ ℕ)
207	46	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑀 ∈ ℕ₀)
208	31, 48	eqtri 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏ℎ ∈ (1...𝑀)((𝑦 − ℎ)↑𝑃)))
209	23	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
210	205, 206, 207, 208, 209	etransclem13 46267	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) = ∏ℎ ∈ (0...𝑀)((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
211	210	fveq2d 6909	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) = (abs‘∏ℎ ∈ (0...𝑀)((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))))
212		nn0uz 12921	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ₀ = (ℤ_≥‘0)
213	23	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → 𝑥 ∈ ℝ)
214		nn0re 12537	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ ∈ ℕ₀ → ℎ ∈ ℝ)
215	214	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → ℎ ∈ ℝ)
216	213, 215	resubcld 11692	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → (𝑥 − ℎ) ∈ ℝ)
217	216	adantll 714	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → (𝑥 − ℎ) ∈ ℝ)
218	59, 76	ifcld 4571	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
219	218	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
220	217, 219	reexpcld 14204	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → ((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℝ)
221	220	recnd 11290	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → ((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℂ)
222	212, 207, 221	fprodabs 16011	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘∏ℎ ∈ (0...𝑀)((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))) = ∏ℎ ∈ (0...𝑀)(abs‘((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))))
223		elfznn0 13661	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ ∈ (0...𝑀) → ℎ ∈ ℕ₀)
224	24	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → 𝑥 ∈ ℂ)
225		nn0cn 12538	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ ∈ ℕ₀ → ℎ ∈ ℂ)
226	225	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → ℎ ∈ ℂ)
227	224, 226	subcld 11621	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → (𝑥 − ℎ) ∈ ℂ)
228	227	adantll 714	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → (𝑥 − ℎ) ∈ ℂ)
229	223, 228	sylan2 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ∈ ℂ)
230	218	ad3antrrr 730	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
231	229, 230	absexpd 15492	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (abs‘((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))) = ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
232	231	prodeq2dv 15959	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)(abs‘((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))) = ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
233	211, 222, 232	3eqtrd 2780	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) = ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
234		nfv 1913	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎℎ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗))
235		fzfid 14015	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (0...𝑀) ∈ Fin)
236	223, 227	sylan2 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ∈ ℂ)
237	236	abscld 15476	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → (abs‘(𝑥 − ℎ)) ∈ ℝ)
238	237	adantll 714	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (abs‘(𝑥 − ℎ)) ∈ ℝ)
239	238, 230	reexpcld 14204	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℝ)
240	236	absge0d 15484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ (abs‘(𝑥 − ℎ)))
241	240	adantll 714	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ (abs‘(𝑥 − ℎ)))
242	238, 230, 241	expge0d 14205	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
243	77	ad3antrrr 730	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀↑𝑃) ∈ ℝ)
244	75	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑀 ∈ ℝ)
245	244, 230	reexpcld 14204	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℝ)
246	223, 217	sylan2 593	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ∈ ℝ)
247	24	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → 𝑥 ∈ ℂ)
248	223, 226	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → ℎ ∈ ℂ)
249	247, 248	negsubdi2d 11637	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → -(𝑥 − ℎ) = (ℎ − 𝑥))
250	249	adantll 714	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → -(𝑥 − ℎ) = (ℎ − 𝑥))
251	223	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ℎ ∈ ℕ₀)
252	251	nn0red 12590	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ℎ ∈ ℝ)
253		0red 11265	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ∈ ℝ)
254	209	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑥 ∈ ℝ)
255		elfzle2 13569	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ ∈ (0...𝑀) → ℎ ≤ 𝑀)
256	255	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ℎ ≤ 𝑀)
257	196, 183, 182	ltled 11410	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ 𝑥)
258	257	adantll 714	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ 𝑥)
259	258	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ 𝑥)
260	252, 253, 244, 254, 256, 259	le2subd 11884	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (ℎ − 𝑥) ≤ (𝑀 − 0))
261	82	subid1d 11610	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑀 − 0) = 𝑀)
262	261	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀 − 0) = 𝑀)
263	260, 262	breqtrd 5168	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (ℎ − 𝑥) ≤ 𝑀)
264	250, 263	eqbrtrd 5164	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → -(𝑥 − ℎ) ≤ 𝑀)
265	246, 244, 264	lenegcon1d 11846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → -𝑀 ≤ (𝑥 − ℎ))
266		elfzel2 13563	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
267	266	zred 12724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
268	267	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑀 ∈ ℝ)
269	52	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑗 ∈ ℝ)
270		iooltub 45528	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0 ∈ ℝ^* ∧ 𝑗 ∈ ℝ^* ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 < 𝑗)
271	177, 179, 180, 270	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 < 𝑗)
272		elfzle2 13569	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀)
273	272	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑗 ≤ 𝑀)
274	183, 269, 268, 271, 273	ltletrd 11422	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 < 𝑀)
275	183, 268, 274	ltled 11410	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ≤ 𝑀)
276	275	adantll 714	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ≤ 𝑀)
277	276	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑥 ≤ 𝑀)
278	251	nn0ge0d 12592	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ ℎ)
279	254, 253, 244, 252, 277, 278	le2subd 11884	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ≤ (𝑀 − 0))
280	279, 262	breqtrd 5168	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ≤ 𝑀)
281	246, 244	absled 15470	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ)) ≤ 𝑀 ↔ (-𝑀 ≤ (𝑥 − ℎ) ∧ (𝑥 − ℎ) ≤ 𝑀)))
282	265, 280, 281	mpbir2and 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (abs‘(𝑥 − ℎ)) ≤ 𝑀)
283		leexp1a 14216	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((abs‘(𝑥 − ℎ)) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀) ∧ (0 ≤ (abs‘(𝑥 − ℎ)) ∧ (abs‘(𝑥 − ℎ)) ≤ 𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
284	238, 244, 230, 241, 282, 283	syl32anc 1379	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
285	45	nnge1d 12315	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ≤ 𝑀)
286	285	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 1 ≤ 𝑀)
287	218	nn0zd 12641	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℤ)
288	76	nn0zd 12641	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑃 ∈ ℤ)
289		iftrue 4530	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = 0 → if(ℎ = 0, (𝑃 − 1), 𝑃) = (𝑃 − 1))
290	289	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) = (𝑃 − 1))
291	30	nnred 12282	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑃 ∈ ℝ)
292	291	lem1d 12202	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑃 − 1) ≤ 𝑃)
293	292	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ℎ = 0) → (𝑃 − 1) ≤ 𝑃)
294	290, 293	eqbrtrd 5164	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃)
295		iffalse 4533	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ ℎ = 0 → if(ℎ = 0, (𝑃 − 1), 𝑃) = 𝑃)
296	295	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ¬ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) = 𝑃)
297	291	leidd 11830	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑃 ≤ 𝑃)
298	297	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ¬ ℎ = 0) → 𝑃 ≤ 𝑃)
299	296, 298	eqbrtrd 5164	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ¬ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃)
300	294, 299	pm2.61dan 812	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃)
301		eluz2 12885	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ (ℤ_≥‘if(ℎ = 0, (𝑃 − 1), 𝑃)) ↔ (if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃))
302	287, 288, 300, 301	syl3anbrc 1343	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑃 ∈ (ℤ_≥‘if(ℎ = 0, (𝑃 − 1), 𝑃)))
303	302	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑃 ∈ (ℤ_≥‘if(ℎ = 0, (𝑃 − 1), 𝑃)))
304	244, 286, 303	leexp2ad 14294	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑𝑃))
305	239, 245, 243, 284, 304	letrd 11419	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑𝑃))
306	234, 235, 239, 242, 243, 305	fprodle 16033	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃))
307	77	recnd 11290	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀↑𝑃) ∈ ℂ)
308		fprodconst 16015	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0...𝑀) ∈ Fin ∧ (𝑀↑𝑃) ∈ ℂ) → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(♯‘(0...𝑀))))
309	7, 307, 308	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(♯‘(0...𝑀))))
310		hashfz0 14472	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ ℕ₀ → (♯‘(0...𝑀)) = (𝑀 + 1))
311	46, 310	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (♯‘(0...𝑀)) = (𝑀 + 1))
312	311	oveq2d 7448	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑀↑𝑃)↑(♯‘(0...𝑀))) = ((𝑀↑𝑃)↑(𝑀 + 1)))
313	309, 312	eqtrd 2776	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(𝑀 + 1)))
314	313	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(𝑀 + 1)))
315	306, 314	breqtrd 5168	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
316	233, 315	eqbrtrd 5164	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
317	159, 160, 161, 135, 162, 163, 204, 316	lemul12ad 12211	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((abs‘(e↑_𝑐-𝑥)) · (abs‘(𝐹‘𝑥))) ≤ (1 · ((𝑀↑𝑃)↑(𝑀 + 1))))
318	81	mullidd 11280	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · ((𝑀↑𝑃)↑(𝑀 + 1))) = ((𝑀↑𝑃)↑(𝑀 + 1)))
319	318	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (1 · ((𝑀↑𝑃)↑(𝑀 + 1))) = ((𝑀↑𝑃)↑(𝑀 + 1)))
320	317, 319	breqtrd 5168	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((abs‘(e↑_𝑐-𝑥)) · (abs‘(𝐹‘𝑥))) ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
321	158, 320	eqbrtrd 5164	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
322	155, 147, 154, 135, 321	itgle 25846	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)(abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) d𝑥 ≤ ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥)
323	152, 156, 148, 157, 322	letrd 11419	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ≤ ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥)
324	152, 148, 108, 153, 323	lemul2ad 12209	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥))
325	151, 324	eqbrtrd 5164	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥))
326	7, 132, 149, 325	fsumle 15836	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥))
327		itgconst 25855	. . . . . . . . . . 11 ⊢ (((0(,)𝑗) ∈ dom vol ∧ (vol‘(0(,)𝑗)) ∈ ℝ ∧ ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 = (((𝑀↑𝑃)↑(𝑀 + 1)) · (vol‘(0(,)𝑗))))
328	137, 144, 145, 327	syl3anc 1372	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 = (((𝑀↑𝑃)↑(𝑀 + 1)) · (vol‘(0(,)𝑗))))
329	46	nn0ge0d 12592	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ≤ 𝑀)
330	75, 76, 329	expge0d 14205	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ (𝑀↑𝑃))
331	77, 79, 330	expge0d 14205	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
332	331	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
333	18	subid1d 11610	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 0) = 𝑗)
334	141, 333	eqtrd 2776	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) = 𝑗)
335	334, 272	eqbrtrd 5164	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) ≤ 𝑀)
336	335	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (vol‘(0(,)𝑗)) ≤ 𝑀)
337	144, 123, 122, 332, 336	lemul2ad 12209	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀↑𝑃)↑(𝑀 + 1)) · (vol‘(0(,)𝑗))) ≤ (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀))
338	328, 337	eqbrtrd 5164	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 ≤ (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀))
339	148, 124, 108, 153, 338	lemul2ad 12209	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ≤ ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)))
340	7, 149, 125, 339	fsumle 15836	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)))
341	133, 150, 126, 326, 340	letrd 11419	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)))
342	130, 133, 126, 134, 341	letrd 11419	. . . . 5 ⊢ (𝜑 → (abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)))
343	130, 126, 131, 342	lediv1dd 13136	. . . 4 ⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))) ≤ (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))))
344	343, 121	breqtrd 5168	. . 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 11420	. 2 ⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))) < 1)
347	69, 346	eqbrtrd 5164	1 ⊢ (𝜑 → (abs‘𝐾) < 1)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1539 ∈ wcel 2107 ⊆ wss 3950 ifcif 4524 {cpr 4627 class class class wbr 5142 ↦ cmpt 5224 dom cdm 5684 ran crn 5685 ⟶wf 6556 ‘cfv 6560 (class class class)co 7432 Fincfn 8986 ℂcc 11154 ℝcr 11155 0cc0 11156 1c1 11157 + caddc 11159 · cmul 11161 ℝ^*cxr 11295 < clt 11296 ≤ cle 11297 − cmin 11493 -cneg 11494 / cdiv 11921 ℕcn 12267 2c2 12322 3c3 12323 ℕ₀cn0 12528 ℤcz 12615 ℤ_≥cuz 12879 (,)cioo 13388 ...cfz 13548 ↑cexp 14103 !cfa 14313 ♯chash 14370 abscabs 15274 Σcsu 15723 ∏cprod 15940 eceu 16099 ↾_t crest 17466 TopOpenctopn 17467 topGenctg 17483 ℂ_fldccnfld 21365 volcvol 25499 𝐿¹cibl 25653 ∫citg 25654 ↑_𝑐ccxp 26598

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-rep 5278 ax-sep 5295 ax-nul 5305 ax-pow 5364 ax-pr 5431 ax-un 7756 ax-inf2 9682 ax-cc 10476 ax-cnex 11212 ax-resscn 11213 ax-1cn 11214 ax-icn 11215 ax-addcl 11216 ax-addrcl 11217 ax-mulcl 11218 ax-mulrcl 11219 ax-mulcom 11220 ax-addass 11221 ax-mulass 11222 ax-distr 11223 ax-i2m1 11224 ax-1ne0 11225 ax-1rid 11226 ax-rnegex 11227 ax-rrecex 11228 ax-cnre 11229 ax-pre-lttri 11230 ax-pre-lttrn 11231 ax-pre-ltadd 11232 ax-pre-mulgt0 11233 ax-pre-sup 11234 ax-addf 11235

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3379 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4601 df-sn 4626 df-pr 4628 df-tp 4630 df-op 4632 df-uni 4907 df-int 4946 df-iun 4992 df-iin 4993 df-disj 5110 df-br 5143 df-opab 5205 df-mpt 5225 df-tr 5259 df-id 5577 df-eprel 5583 df-po 5591 df-so 5592 df-fr 5636 df-se 5637 df-we 5638 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-pred 6320 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 df-fv 6568 df-isom 6569 df-riota 7389 df-ov 7435 df-oprab 7436 df-mpo 7437 df-of 7698 df-ofr 7699 df-om 7889 df-1st 8015 df-2nd 8016 df-supp 8187 df-frecs 8307 df-wrecs 8338 df-recs 8412 df-rdg 8451 df-1o 8507 df-2o 8508 df-oadd 8511 df-omul 8512 df-er 8746 df-map 8869 df-pm 8870 df-ixp 8939 df-en 8987 df-dom 8988 df-sdom 8989 df-fin 8990 df-fsupp 9403 df-fi 9452 df-sup 9483 df-inf 9484 df-oi 9551 df-dju 9942 df-card 9980 df-acn 9983 df-pnf 11298 df-mnf 11299 df-xr 11300 df-ltxr 11301 df-le 11302 df-sub 11495 df-neg 11496 df-div 11922 df-nn 12268 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12529 df-z 12616 df-dec 12736 df-uz 12880 df-q 12992 df-rp 13036 df-xneg 13155 df-xadd 13156 df-xmul 13157 df-ioo 13392 df-ioc 13393 df-ico 13394 df-icc 13395 df-fz 13549 df-fzo 13696 df-fl 13833 df-mod 13911 df-seq 14044 df-exp 14104 df-fac 14314 df-bc 14343 df-hash 14371 df-shft 15107 df-cj 15139 df-re 15140 df-im 15141 df-sqrt 15275 df-abs 15276 df-limsup 15508 df-clim 15525 df-rlim 15526 df-sum 15724 df-prod 15941 df-ef 16104 df-e 16105 df-sin 16106 df-cos 16107 df-tan 16108 df-pi 16109 df-struct 17185 df-sets 17202 df-slot 17220 df-ndx 17232 df-base 17249 df-ress 17276 df-plusg 17311 df-mulr 17312 df-starv 17313 df-sca 17314 df-vsca 17315 df-ip 17316 df-tset 17317 df-ple 17318 df-ds 17320 df-unif 17321 df-hom 17322 df-cco 17323 df-rest 17468 df-topn 17469 df-0g 17487 df-gsum 17488 df-topgen 17489 df-pt 17490 df-prds 17493 df-xrs 17548 df-qtop 17553 df-imas 17554 df-xps 17556 df-mre 17630 df-mrc 17631 df-acs 17633 df-mgm 18654 df-sgrp 18733 df-mnd 18749 df-submnd 18798 df-mulg 19087 df-cntz 19336 df-cmn 19801 df-psmet 21357 df-xmet 21358 df-met 21359 df-bl 21360 df-mopn 21361 df-fbas 21362 df-fg 21363 df-cnfld 21366 df-top 22901 df-topon 22918 df-topsp 22940 df-bases 22954 df-cld 23028 df-ntr 23029 df-cls 23030 df-nei 23107 df-lp 23145 df-perf 23146 df-cn 23236 df-cnp 23237 df-haus 23324 df-cmp 23396 df-tx 23571 df-hmeo 23764 df-fil 23855 df-fm 23947 df-flim 23948 df-flf 23949 df-xms 24331 df-ms 24332 df-tms 24333 df-cncf 24905 df-ovol 25500 df-vol 25501 df-mbf 25655 df-itg1 25656 df-itg2 25657 df-ibl 25658 df-itg 25659 df-0p 25706 df-limc 25902 df-dv 25903 df-log 26599 df-cxp 26600

This theorem is referenced by: etransclem47 46301

W3C validator