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 43340

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 7180	. . . . . 6 ⊢ (𝐿 / (!‘(𝑃 − 1))) = (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))
4	1, 3	eqtri 2761	. . . . 5 ⊢ 𝐾 = (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))
5	4	fveq2i 6677	. . . 4 ⊢ (abs‘𝐾) = (abs‘(Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1))))
6	5	a1i 11	. . 3 ⊢ (𝜑 → (abs‘𝐾) = (abs‘(Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))))
7		fzfid 13432	. . . . 5 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
8		etransclem23.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℤ)
9	8	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐴:ℕ₀⟶ℤ)
10		elfznn0 13091	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ₀)
11	10	adantl 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ₀)
12	9, 11	ffvelrnd 6862	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℤ)
13	12	zcnd 12169	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℂ)
14		ere 15534	. . . . . . . . . 10 ⊢ e ∈ ℝ
15	14	recni 10733	. . . . . . . . 9 ⊢ e ∈ ℂ
16	15	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → e ∈ ℂ)
17		elfzelz 12998	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
18	17	zcnd 12169	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
19	18	adantl 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ)
20	16, 19	cxpcld 25451	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑_𝑐𝑗) ∈ ℂ)
21	13, 20	mulcld 10739	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑_𝑐𝑗)) ∈ ℂ)
22	15	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → e ∈ ℂ)
23		elioore 12851	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℝ)
24	23	recnd 10747	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℂ)
25	24	adantl 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℂ)
26	25	negcld 11062	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℂ)
27	22, 26	cxpcld 25451	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) ∈ ℂ)
28		ax-resscn 10672	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
29	28	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ ⊆ ℂ)
30		etransclem23.p	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℕ)
31		etransclem23.f	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))
32	29, 30, 31	etransclem8 43325	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
33	32	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝐹:ℝ⟶ℂ)
34	23	adantl 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
35	33, 34	ffvelrnd 6862	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) ∈ ℂ)
36	35	adantlr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) ∈ ℂ)
37	27, 36	mulcld 10739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
38		reelprrecn 10707	. . . . . . . . 9 ⊢ ℝ ∈ {ℝ, ℂ}
39	38	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℝ ∈ {ℝ, ℂ})
40		reopn 42365	. . . . . . . . . 10 ⊢ ℝ ∈ (topGen‘ran (,))
41		eqid 2738	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
42	41	tgioo2 23555	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
43	40, 42	eleqtri 2831	. . . . . . . . 9 ⊢ ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ)
44	43	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
45	30	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑃 ∈ ℕ)
46		etransclem23.m	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℕ)
47	46	nnnn0d 12036	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
48	47	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℕ₀)
49		etransclem6 43323	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏ℎ ∈ (1...𝑀)((𝑦 − ℎ)↑𝑃)))
50		etransclem6 43323	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏ℎ ∈ (1...𝑀)((𝑦 − ℎ)↑𝑃))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))
51	31, 49, 50	3eqtri 2765	. . . . . . . 8 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))
52		0red 10722	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ)
53	17	zred 12168	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
54	53	adantl 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ)
55	39, 44, 45, 48, 51, 52, 54	etransclem18 43335	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ 𝐿¹)
56	37, 55	itgcl 24536	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥 ∈ ℂ)
57	21, 56	mulcld 10739	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ∈ ℂ)
58	7, 57	fsumcl 15183	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ∈ ℂ)
59		nnm1nn0 12017	. . . . . . 7 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
60	30, 59	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑃 − 1) ∈ ℕ₀)
61	60	faccld 13736	. . . . 5 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℕ)
62	61	nncnd 11732	. . . 4 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℂ)
63	61	nnne0d 11766	. . . 4 ⊢ (𝜑 → (!‘(𝑃 − 1)) ≠ 0)
64	58, 62, 63	absdivd 14905	. . 3 ⊢ (𝜑 → (abs‘(Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))) = ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (abs‘(!‘(𝑃 − 1)))))
65	61	nnred 11731	. . . . 5 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℝ)
66	61	nnnn0d 12036	. . . . . 6 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℕ₀)
67	66	nn0ge0d 12039	. . . . 5 ⊢ (𝜑 → 0 ≤ (!‘(𝑃 − 1)))
68	65, 67	absidd 14872	. . . 4 ⊢ (𝜑 → (abs‘(!‘(𝑃 − 1))) = (!‘(𝑃 − 1)))
69	68	oveq2d 7186	. . 3 ⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (abs‘(!‘(𝑃 − 1)))) = ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))))
70	6, 64, 69	3eqtrd 2777	. 2 ⊢ (𝜑 → (abs‘𝐾) = ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))))
71	2, 58	eqeltrid 2837	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ℂ)
72	71, 62, 63	divcld 11494	. . . . . 6 ⊢ (𝜑 → (𝐿 / (!‘(𝑃 − 1))) ∈ ℂ)
73	1, 72	eqeltrid 2837	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℂ)
74	73	abscld 14886	. . . 4 ⊢ (𝜑 → (abs‘𝐾) ∈ ℝ)
75	70, 74	eqeltrrd 2834	. . 3 ⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))) ∈ ℝ)
76	46	nnred 11731	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℝ)
77	30	nnnn0d 12036	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
78	76, 77	reexpcld 13619	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑𝑃) ∈ ℝ)
79		peano2nn0 12016	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ₀ → (𝑀 + 1) ∈ ℕ₀)
80	47, 79	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ₀)
81	78, 80	reexpcld 13619	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℝ)
82	81	recnd 10747	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ)
83	46	nncnd 11732	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℂ)
84	82, 83	mulcomd 10740	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) = (𝑀 · ((𝑀↑𝑃)↑(𝑀 + 1))))
85	30	nncnd 11732	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ ℂ)
86		1cnd 10714	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℂ)
87	85, 86	npcand 11079	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑃 − 1) + 1) = 𝑃)
88	87	eqcomd 2744	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 = ((𝑃 − 1) + 1))
89	88	oveq2d 7186	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑𝑃) = ((𝑀↑(𝑀 + 1))↑((𝑃 − 1) + 1)))
90	80	nn0cnd 12038	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 + 1) ∈ ℂ)
91	90, 85	mulcomd 10740	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀 + 1) · 𝑃) = (𝑃 · (𝑀 + 1)))
92	91	oveq2d 7186	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑((𝑀 + 1) · 𝑃)) = (𝑀↑(𝑃 · (𝑀 + 1))))
93	83, 77, 80	expmuld 13605	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑((𝑀 + 1) · 𝑃)) = ((𝑀↑(𝑀 + 1))↑𝑃))
94	83, 80, 77	expmuld 13605	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑(𝑃 · (𝑀 + 1))) = ((𝑀↑𝑃)↑(𝑀 + 1)))
95	92, 93, 94	3eqtr3d 2781	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑𝑃) = ((𝑀↑𝑃)↑(𝑀 + 1)))
96	76, 80	reexpcld 13619	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℝ)
97	96	recnd 10747	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℂ)
98	97, 60	expp1d 13603	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑((𝑃 − 1) + 1)) = (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1))))
99	89, 95, 98	3eqtr3d 2781	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀↑𝑃)↑(𝑀 + 1)) = (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1))))
100	99	oveq2d 7186	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 · ((𝑀↑𝑃)↑(𝑀 + 1))) = (𝑀 · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1)))))
101	97, 60	expcld 13602	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) ∈ ℂ)
102	83, 101, 97	mul12d 10927	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀 · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1)))) = (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀 · (𝑀↑(𝑀 + 1)))))
103	83, 97	mulcld 10739	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ)
104	101, 103	mulcomd 10740	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀 · (𝑀↑(𝑀 + 1)))) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
105	102, 104	eqtrd 2773	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1)))) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
106	84, 100, 105	3eqtrd 2777	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
107	106	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
108	107	oveq2d 7186	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)))))
109	21	abscld 14886	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) ∈ ℝ)
110	109	recnd 10747	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) ∈ ℂ)
111	103	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ)
112	101	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) ∈ ℂ)
113	110, 111, 112	mulassd 10742	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) = ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)))))
114	108, 113	eqtr4d 2776	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = (((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
115	114	sumeq2dv 15153	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = Σ𝑗 ∈ (0...𝑀)(((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
116	110, 111	mulcld 10739	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
117	7, 101, 116	fsummulc1 15233	. . . . . . 7 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) = Σ𝑗 ∈ (0...𝑀)(((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
118	115, 117	eqtr4d 2776	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
119	118	oveq1d 7185	. . . . 5 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))) = ((Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) / (!‘(𝑃 − 1))))
120	7, 116	fsumcl 15183	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
121	120, 101, 62, 63	divassd 11529	. . . . 5 ⊢ (𝜑 → ((Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) / (!‘(𝑃 − 1))) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))))
122	119, 121	eqtrd 2773	. . . 4 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))))
123	81	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℝ)
124	76	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℝ)
125	123, 124	remulcld 10749	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) ∈ ℝ)
126	109, 125	remulcld 10749	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) ∈ ℝ)
127	7, 126	fsumrecl 15184	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) ∈ ℝ)
128	127, 61	nndivred 11770	. . . 4 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))) ∈ ℝ)
129	122, 128	eqeltrrd 2834	. . 3 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))) ∈ ℝ)
130		1red 10720	. . 3 ⊢ (𝜑 → 1 ∈ ℝ)
131	58	abscld 14886	. . . . 5 ⊢ (𝜑 → (abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ∈ ℝ)
132	61	nnrpd 12512	. . . . 5 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℝ⁺)
133	57	abscld 14886	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ∈ ℝ)
134	7, 133	fsumrecl 15184	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ∈ ℝ)
135	7, 57	fsumabs 15249	. . . . . 6 ⊢ (𝜑 → (abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)))
136	81	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℝ)
137		ioombl 24317	. . . . . . . . . . . 12 ⊢ (0(,)𝑗) ∈ dom vol
138	137	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0(,)𝑗) ∈ dom vol)
139		0red 10722	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → 0 ∈ ℝ)
140		elfzle1 13001	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
141		volioo 24321	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ 𝑗 ∈ ℝ ∧ 0 ≤ 𝑗) → (vol‘(0(,)𝑗)) = (𝑗 − 0))
142	139, 53, 140, 141	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) = (𝑗 − 0))
143	53, 139	resubcld 11146	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 0) ∈ ℝ)
144	142, 143	eqeltrd 2833	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) ∈ ℝ)
145	144	adantl 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (vol‘(0(,)𝑗)) ∈ ℝ)
146	82	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ)
147		iblconstmpt 43039	. . . . . . . . . . 11 ⊢ (((0(,)𝑗) ∈ dom vol ∧ (vol‘(0(,)𝑗)) ∈ ℝ ∧ ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ) → (𝑥 ∈ (0(,)𝑗) ↦ ((𝑀↑𝑃)↑(𝑀 + 1))) ∈ 𝐿¹)
148	138, 145, 146, 147	syl3anc 1372	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((𝑀↑𝑃)↑(𝑀 + 1))) ∈ 𝐿¹)
149	136, 148	itgrecl 24550	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 ∈ ℝ)
150	109, 149	remulcld 10749	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ∈ ℝ)
151	7, 150	fsumrecl 15184	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ∈ ℝ)
152	21, 56	absmuld 14904	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) = ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)))
153	56	abscld 14886	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ∈ ℝ)
154	21	absge0d 14894	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ (abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))))
155	37	abscld 14886	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ ℝ)
156	37, 55	iblabs 24581	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ (abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥)))) ∈ 𝐿¹)
157	155, 156	itgrecl 24550	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)(abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) d𝑥 ∈ ℝ)
158	37, 55	itgabs 24587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ≤ ∫(0(,)𝑗)(abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) d𝑥)
159	27, 36	absmuld 14904	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = ((abs‘(e↑_𝑐-𝑥)) · (abs‘(𝐹‘𝑥))))
160	27	abscld 14886	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(e↑_𝑐-𝑥)) ∈ ℝ)
161		1red 10720	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 1 ∈ ℝ)
162	36	abscld 14886	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) ∈ ℝ)
163	27	absge0d 14894	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ (abs‘(e↑_𝑐-𝑥)))
164	36	absge0d 14894	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ (abs‘(𝐹‘𝑥)))
165	14	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0(,)𝑗) → e ∈ ℝ)
166		0re 10721	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℝ
167		epos 15652	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < e
168	166, 14, 167	ltleii 10841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ≤ e
169	168	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0(,)𝑗) → 0 ≤ e)
170	23	renegcld 11145	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0(,)𝑗) → -𝑥 ∈ ℝ)
171	165, 169, 170	recxpcld 25466	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0(,)𝑗) → (e↑_𝑐-𝑥) ∈ ℝ)
172	165, 169, 170	cxpge0d 25467	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0(,)𝑗) → 0 ≤ (e↑_𝑐-𝑥))
173	171, 172	absidd 14872	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (0(,)𝑗) → (abs‘(e↑_𝑐-𝑥)) = (e↑_𝑐-𝑥))
174	173	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(e↑_𝑐-𝑥)) = (e↑_𝑐-𝑥))
175	171	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) ∈ ℝ)
176		1red 10720	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 1 ∈ ℝ)
177		0xr 10766	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℝ^*
178	177	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ∈ ℝ^*)
179	53	rexrd 10769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ^*)
180	179	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑗 ∈ ℝ^*)
181		simpr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ (0(,)𝑗))
182		ioogtlb 42573	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ∈ ℝ^* ∧ 𝑗 ∈ ℝ^* ∧ 𝑥 ∈ (0(,)𝑗)) → 0 < 𝑥)
183	178, 180, 181, 182	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 < 𝑥)
184	23	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
185	184	lt0neg2d 11288	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (0 < 𝑥 ↔ -𝑥 < 0))
186	183, 185	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 < 0)
187	14	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → e ∈ ℝ)
188		1lt2 11887	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 < 2
189		egt2lt3 15651	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2 < e ∧ e < 3)
190	189	simpli 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 < e
191		1re 10719	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℝ
192		2re 11790	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℝ
193	191, 192, 14	lttri 10844	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 < 2 ∧ 2 < e) → 1 < e)
194	188, 190, 193	mp2an 692	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 < e
195	194	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 1 < e)
196	170	adantl 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℝ)
197		0red 10722	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ∈ ℝ)
198	187, 195, 196, 197	cxpltd 25462	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (-𝑥 < 0 ↔ (e↑_𝑐-𝑥) < (e↑_𝑐0)))
199	186, 198	mpbid 235	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) < (e↑_𝑐0))
200		cxp0 25413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (e ∈ ℂ → (e↑_𝑐0) = 1)
201	15, 200	mp1i 13	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐0) = 1)
202	199, 201	breqtrd 5056	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) < 1)
203	175, 176, 202	ltled 10866	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) ≤ 1)
204	174, 203	eqbrtrd 5052	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(e↑_𝑐-𝑥)) ≤ 1)
205	204	adantll 714	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(e↑_𝑐-𝑥)) ≤ 1)
206	28	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ℝ ⊆ ℂ)
207	30	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑃 ∈ ℕ)
208	47	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑀 ∈ ℕ₀)
209	31, 49	eqtri 2761	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏ℎ ∈ (1...𝑀)((𝑦 − ℎ)↑𝑃)))
210	23	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
211	206, 207, 208, 209, 210	etransclem13 43330	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) = ∏ℎ ∈ (0...𝑀)((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
212	211	fveq2d 6678	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) = (abs‘∏ℎ ∈ (0...𝑀)((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))))
213		nn0uz 12362	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ₀ = (ℤ_≥‘0)
214	23	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → 𝑥 ∈ ℝ)
215		nn0re 11985	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ ∈ ℕ₀ → ℎ ∈ ℝ)
216	215	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → ℎ ∈ ℝ)
217	214, 216	resubcld 11146	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → (𝑥 − ℎ) ∈ ℝ)
218	217	adantll 714	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → (𝑥 − ℎ) ∈ ℝ)
219	60, 77	ifcld 4460	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
220	219	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
221	218, 220	reexpcld 13619	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → ((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℝ)
222	221	recnd 10747	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → ((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℂ)
223	213, 208, 222	fprodabs 15420	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘∏ℎ ∈ (0...𝑀)((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))) = ∏ℎ ∈ (0...𝑀)(abs‘((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))))
224		elfznn0 13091	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ ∈ (0...𝑀) → ℎ ∈ ℕ₀)
225	24	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → 𝑥 ∈ ℂ)
226		nn0cn 11986	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ ∈ ℕ₀ → ℎ ∈ ℂ)
227	226	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → ℎ ∈ ℂ)
228	225, 227	subcld 11075	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → (𝑥 − ℎ) ∈ ℂ)
229	228	adantll 714	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → (𝑥 − ℎ) ∈ ℂ)
230	224, 229	sylan2 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ∈ ℂ)
231	219	ad3antrrr 730	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
232	230, 231	absexpd 14902	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (abs‘((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))) = ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
233	232	prodeq2dv 15369	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)(abs‘((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))) = ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
234	212, 223, 233	3eqtrd 2777	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) = ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
235		nfv 1921	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎℎ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗))
236		fzfid 13432	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (0...𝑀) ∈ Fin)
237	224, 228	sylan2 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ∈ ℂ)
238	237	abscld 14886	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → (abs‘(𝑥 − ℎ)) ∈ ℝ)
239	238	adantll 714	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (abs‘(𝑥 − ℎ)) ∈ ℝ)
240	239, 231	reexpcld 13619	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℝ)
241	237	absge0d 14894	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ (abs‘(𝑥 − ℎ)))
242	241	adantll 714	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ (abs‘(𝑥 − ℎ)))
243	239, 231, 242	expge0d 13620	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
244	78	ad3antrrr 730	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀↑𝑃) ∈ ℝ)
245	76	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑀 ∈ ℝ)
246	245, 231	reexpcld 13619	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℝ)
247	224, 218	sylan2 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ∈ ℝ)
248	24	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → 𝑥 ∈ ℂ)
249	224, 227	sylan2 596	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → ℎ ∈ ℂ)
250	248, 249	negsubdi2d 11091	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → -(𝑥 − ℎ) = (ℎ − 𝑥))
251	250	adantll 714	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → -(𝑥 − ℎ) = (ℎ − 𝑥))
252	224	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ℎ ∈ ℕ₀)
253	252	nn0red 12037	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ℎ ∈ ℝ)
254		0red 10722	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ∈ ℝ)
255	210	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑥 ∈ ℝ)
256		elfzle2 13002	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ ∈ (0...𝑀) → ℎ ≤ 𝑀)
257	256	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ℎ ≤ 𝑀)
258	197, 184, 183	ltled 10866	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ 𝑥)
259	258	adantll 714	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ 𝑥)
260	259	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ 𝑥)
261	253, 254, 245, 255, 257, 260	le2subd 11338	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (ℎ − 𝑥) ≤ (𝑀 − 0))
262	83	subid1d 11064	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑀 − 0) = 𝑀)
263	262	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀 − 0) = 𝑀)
264	261, 263	breqtrd 5056	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (ℎ − 𝑥) ≤ 𝑀)
265	251, 264	eqbrtrd 5052	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → -(𝑥 − ℎ) ≤ 𝑀)
266	247, 245, 265	lenegcon1d 11300	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → -𝑀 ≤ (𝑥 − ℎ))
267		elfzel2 12996	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
268	267	zred 12168	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
269	268	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑀 ∈ ℝ)
270	53	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑗 ∈ ℝ)
271		iooltub 42588	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0 ∈ ℝ^* ∧ 𝑗 ∈ ℝ^* ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 < 𝑗)
272	178, 180, 181, 271	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 < 𝑗)
273		elfzle2 13002	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀)
274	273	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑗 ≤ 𝑀)
275	184, 270, 269, 272, 274	ltletrd 10878	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 < 𝑀)
276	184, 269, 275	ltled 10866	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ≤ 𝑀)
277	276	adantll 714	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ≤ 𝑀)
278	277	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑥 ≤ 𝑀)
279	252	nn0ge0d 12039	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ ℎ)
280	255, 254, 245, 253, 278, 279	le2subd 11338	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ≤ (𝑀 − 0))
281	280, 263	breqtrd 5056	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ≤ 𝑀)
282	247, 245	absled 14880	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ)) ≤ 𝑀 ↔ (-𝑀 ≤ (𝑥 − ℎ) ∧ (𝑥 − ℎ) ≤ 𝑀)))
283	266, 281, 282	mpbir2and 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (abs‘(𝑥 − ℎ)) ≤ 𝑀)
284		leexp1a 13631	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((abs‘(𝑥 − ℎ)) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀) ∧ (0 ≤ (abs‘(𝑥 − ℎ)) ∧ (abs‘(𝑥 − ℎ)) ≤ 𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
285	239, 245, 231, 242, 283, 284	syl32anc 1379	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
286	46	nnge1d 11764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ≤ 𝑀)
287	286	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 1 ≤ 𝑀)
288	219	nn0zd 12166	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℤ)
289	77	nn0zd 12166	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑃 ∈ ℤ)
290		iftrue 4420	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = 0 → if(ℎ = 0, (𝑃 − 1), 𝑃) = (𝑃 − 1))
291	290	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) = (𝑃 − 1))
292	30	nnred 11731	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑃 ∈ ℝ)
293	292	lem1d 11651	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑃 − 1) ≤ 𝑃)
294	293	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ℎ = 0) → (𝑃 − 1) ≤ 𝑃)
295	291, 294	eqbrtrd 5052	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃)
296		iffalse 4423	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ ℎ = 0 → if(ℎ = 0, (𝑃 − 1), 𝑃) = 𝑃)
297	296	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ¬ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) = 𝑃)
298	292	leidd 11284	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑃 ≤ 𝑃)
299	298	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ¬ ℎ = 0) → 𝑃 ≤ 𝑃)
300	297, 299	eqbrtrd 5052	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ¬ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃)
301	295, 300	pm2.61dan 813	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃)
302		eluz2 12330	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ (ℤ_≥‘if(ℎ = 0, (𝑃 − 1), 𝑃)) ↔ (if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃))
303	288, 289, 301, 302	syl3anbrc 1344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑃 ∈ (ℤ_≥‘if(ℎ = 0, (𝑃 − 1), 𝑃)))
304	303	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑃 ∈ (ℤ_≥‘if(ℎ = 0, (𝑃 − 1), 𝑃)))
305	245, 287, 304	leexp2ad 13709	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑𝑃))
306	240, 246, 244, 285, 305	letrd 10875	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑𝑃))
307	235, 236, 240, 243, 244, 306	fprodle 15442	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃))
308	78	recnd 10747	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀↑𝑃) ∈ ℂ)
309		fprodconst 15424	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0...𝑀) ∈ Fin ∧ (𝑀↑𝑃) ∈ ℂ) → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(♯‘(0...𝑀))))
310	7, 308, 309	syl2anc 587	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(♯‘(0...𝑀))))
311		hashfz0 13885	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ ℕ₀ → (♯‘(0...𝑀)) = (𝑀 + 1))
312	47, 311	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (♯‘(0...𝑀)) = (𝑀 + 1))
313	312	oveq2d 7186	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑀↑𝑃)↑(♯‘(0...𝑀))) = ((𝑀↑𝑃)↑(𝑀 + 1)))
314	310, 313	eqtrd 2773	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(𝑀 + 1)))
315	314	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(𝑀 + 1)))
316	307, 315	breqtrd 5056	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
317	234, 316	eqbrtrd 5052	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
318	160, 161, 162, 136, 163, 164, 205, 317	lemul12ad 11660	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((abs‘(e↑_𝑐-𝑥)) · (abs‘(𝐹‘𝑥))) ≤ (1 · ((𝑀↑𝑃)↑(𝑀 + 1))))
319	82	mulid2d 10737	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · ((𝑀↑𝑃)↑(𝑀 + 1))) = ((𝑀↑𝑃)↑(𝑀 + 1)))
320	319	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (1 · ((𝑀↑𝑃)↑(𝑀 + 1))) = ((𝑀↑𝑃)↑(𝑀 + 1)))
321	318, 320	breqtrd 5056	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((abs‘(e↑_𝑐-𝑥)) · (abs‘(𝐹‘𝑥))) ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
322	159, 321	eqbrtrd 5052	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
323	156, 148, 155, 136, 322	itgle 24562	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)(abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) d𝑥 ≤ ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥)
324	153, 157, 149, 158, 323	letrd 10875	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ≤ ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥)
325	153, 149, 109, 154, 324	lemul2ad 11658	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥))
326	152, 325	eqbrtrd 5052	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥))
327	7, 133, 150, 326	fsumle 15247	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥))
328		itgconst 24571	. . . . . . . . . . 11 ⊢ (((0(,)𝑗) ∈ dom vol ∧ (vol‘(0(,)𝑗)) ∈ ℝ ∧ ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 = (((𝑀↑𝑃)↑(𝑀 + 1)) · (vol‘(0(,)𝑗))))
329	138, 145, 146, 328	syl3anc 1372	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 = (((𝑀↑𝑃)↑(𝑀 + 1)) · (vol‘(0(,)𝑗))))
330	47	nn0ge0d 12039	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ≤ 𝑀)
331	76, 77, 330	expge0d 13620	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ (𝑀↑𝑃))
332	78, 80, 331	expge0d 13620	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
333	332	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
334	18	subid1d 11064	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 0) = 𝑗)
335	142, 334	eqtrd 2773	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) = 𝑗)
336	335, 273	eqbrtrd 5052	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) ≤ 𝑀)
337	336	adantl 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (vol‘(0(,)𝑗)) ≤ 𝑀)
338	145, 124, 123, 333, 337	lemul2ad 11658	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀↑𝑃)↑(𝑀 + 1)) · (vol‘(0(,)𝑗))) ≤ (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀))
339	329, 338	eqbrtrd 5052	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 ≤ (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀))
340	149, 125, 109, 154, 339	lemul2ad 11658	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ≤ ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)))
341	7, 150, 126, 340	fsumle 15247	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)))
342	134, 151, 127, 327, 341	letrd 10875	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)))
343	131, 134, 127, 135, 342	letrd 10875	. . . . 5 ⊢ (𝜑 → (abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)))
344	131, 127, 132, 343	lediv1dd 12572	. . . 4 ⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))) ≤ (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))))
345	344, 122	breqtrd 5056	. . 3 ⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))) ≤ (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))))
346		etransclem23.lt1	. . 3 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))) < 1)
347	75, 129, 130, 345, 346	lelttrd 10876	. 2 ⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))) < 1)
348	70, 347	eqbrtrd 5052	1 ⊢ (𝜑 → (abs‘𝐾) < 1)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 = wceq 1542 ∈ wcel 2114 ⊆ wss 3843 ifcif 4414 {cpr 4518 class class class wbr 5030 ↦ cmpt 5110 dom cdm 5525 ran crn 5526 ⟶wf 6335 ‘cfv 6339 (class class class)co 7170 Fincfn 8555 ℂcc 10613 ℝcr 10614 0cc0 10615 1c1 10616 + caddc 10618 · cmul 10620 ℝ^*cxr 10752 < clt 10753 ≤ cle 10754 − cmin 10948 -cneg 10949 / cdiv 11375 ℕcn 11716 2c2 11771 3c3 11772 ℕ₀cn0 11976 ℤcz 12062 ℤ_≥cuz 12324 (,)cioo 12821 ...cfz 12981 ↑cexp 13521 !cfa 13725 ♯chash 13782 abscabs 14683 Σcsu 15135 ∏cprod 15351 eceu 15508 ↾_t crest 16797 TopOpenctopn 16798 topGenctg 16814 ℂ_fldccnfld 20217 volcvol 24215 𝐿¹cibl 24369 ∫citg 24370 ↑_𝑐ccxp 25299

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 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2710 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5232 ax-pr 5296 ax-un 7479 ax-inf2 9177 ax-cc 9935 ax-cnex 10671 ax-resscn 10672 ax-1cn 10673 ax-icn 10674 ax-addcl 10675 ax-addrcl 10676 ax-mulcl 10677 ax-mulrcl 10678 ax-mulcom 10679 ax-addass 10680 ax-mulass 10681 ax-distr 10682 ax-i2m1 10683 ax-1ne0 10684 ax-1rid 10685 ax-rnegex 10686 ax-rrecex 10687 ax-cnre 10688 ax-pre-lttri 10689 ax-pre-lttrn 10690 ax-pre-ltadd 10691 ax-pre-mulgt0 10692 ax-pre-sup 10693 ax-addf 10694 ax-mulf 10695

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-reu 3060 df-rmo 3061 df-rab 3062 df-v 3400 df-sbc 3681 df-csb 3791 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-pss 3862 df-nul 4212 df-if 4415 df-pw 4490 df-sn 4517 df-pr 4519 df-tp 4521 df-op 4523 df-uni 4797 df-int 4837 df-iun 4883 df-iin 4884 df-disj 4996 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5429 df-eprel 5434 df-po 5442 df-so 5443 df-fr 5483 df-se 5484 df-we 5485 df-xp 5531 df-rel 5532 df-cnv 5533 df-co 5534 df-dm 5535 df-rn 5536 df-res 5537 df-ima 5538 df-pred 6129 df-ord 6175 df-on 6176 df-lim 6177 df-suc 6178 df-iota 6297 df-fun 6341 df-fn 6342 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 df-fv 6347 df-isom 6348 df-riota 7127 df-ov 7173 df-oprab 7174 df-mpo 7175 df-of 7425 df-ofr 7426 df-om 7600 df-1st 7714 df-2nd 7715 df-supp 7857 df-wrecs 7976 df-recs 8037 df-rdg 8075 df-1o 8131 df-2o 8132 df-oadd 8135 df-omul 8136 df-er 8320 df-map 8439 df-pm 8440 df-ixp 8508 df-en 8556 df-dom 8557 df-sdom 8558 df-fin 8559 df-fsupp 8907 df-fi 8948 df-sup 8979 df-inf 8980 df-oi 9047 df-dju 9403 df-card 9441 df-acn 9444 df-pnf 10755 df-mnf 10756 df-xr 10757 df-ltxr 10758 df-le 10759 df-sub 10950 df-neg 10951 df-div 11376 df-nn 11717 df-2 11779 df-3 11780 df-4 11781 df-5 11782 df-6 11783 df-7 11784 df-8 11785 df-9 11786 df-n0 11977 df-z 12063 df-dec 12180 df-uz 12325 df-q 12431 df-rp 12473 df-xneg 12590 df-xadd 12591 df-xmul 12592 df-ioo 12825 df-ioc 12826 df-ico 12827 df-icc 12828 df-fz 12982 df-fzo 13125 df-fl 13253 df-mod 13329 df-seq 13461 df-exp 13522 df-fac 13726 df-bc 13755 df-hash 13783 df-shft 14516 df-cj 14548 df-re 14549 df-im 14550 df-sqrt 14684 df-abs 14685 df-limsup 14918 df-clim 14935 df-rlim 14936 df-sum 15136 df-prod 15352 df-ef 15513 df-e 15514 df-sin 15515 df-cos 15516 df-tan 15517 df-pi 15518 df-struct 16588 df-ndx 16589 df-slot 16590 df-base 16592 df-sets 16593 df-ress 16594 df-plusg 16681 df-mulr 16682 df-starv 16683 df-sca 16684 df-vsca 16685 df-ip 16686 df-tset 16687 df-ple 16688 df-ds 16690 df-unif 16691 df-hom 16692 df-cco 16693 df-rest 16799 df-topn 16800 df-0g 16818 df-gsum 16819 df-topgen 16820 df-pt 16821 df-prds 16824 df-xrs 16878 df-qtop 16883 df-imas 16884 df-xps 16886 df-mre 16960 df-mrc 16961 df-acs 16963 df-mgm 17968 df-sgrp 18017 df-mnd 18028 df-submnd 18073 df-mulg 18343 df-cntz 18565 df-cmn 19026 df-psmet 20209 df-xmet 20210 df-met 20211 df-bl 20212 df-mopn 20213 df-fbas 20214 df-fg 20215 df-cnfld 20218 df-top 21645 df-topon 21662 df-topsp 21684 df-bases 21697 df-cld 21770 df-ntr 21771 df-cls 21772 df-nei 21849 df-lp 21887 df-perf 21888 df-cn 21978 df-cnp 21979 df-haus 22066 df-cmp 22138 df-tx 22313 df-hmeo 22506 df-fil 22597 df-fm 22689 df-flim 22690 df-flf 22691 df-xms 23073 df-ms 23074 df-tms 23075 df-cncf 23630 df-ovol 24216 df-vol 24217 df-mbf 24371 df-itg1 24372 df-itg2 24373 df-ibl 24374 df-itg 24375 df-0p 24422 df-limc 24618 df-dv 24619 df-log 25300 df-cxp 25301

This theorem is referenced by: etransclem47 43364

W3C validator