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 45273

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 7422	. . . . . 6 ⊢ (𝐿 / (!‘(𝑃 − 1))) = (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))
4	1, 3	eqtri 2759	. . . . 5 ⊢ 𝐾 = (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))
5	4	fveq2i 6895	. . . 4 ⊢ (abs‘𝐾) = (abs‘(Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1))))
6	5	a1i 11	. . 3 ⊢ (𝜑 → (abs‘𝐾) = (abs‘(Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))))
7		fzfid 13943	. . . . 5 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
8		etransclem23.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℤ)
9	8	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐴:ℕ₀⟶ℤ)
10		elfznn0 13599	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ₀)
11	10	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ₀)
12	9, 11	ffvelcdmd 7088	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℤ)
13	12	zcnd 12672	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℂ)
14		ere 16037	. . . . . . . . . 10 ⊢ e ∈ ℝ
15	14	recni 11233	. . . . . . . . 9 ⊢ e ∈ ℂ
16	15	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → e ∈ ℂ)
17		elfzelz 13506	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
18	17	zcnd 12672	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
19	18	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ)
20	16, 19	cxpcld 26449	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑_𝑐𝑗) ∈ ℂ)
21	13, 20	mulcld 11239	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑_𝑐𝑗)) ∈ ℂ)
22	15	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → e ∈ ℂ)
23		elioore 13359	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℝ)
24	23	recnd 11247	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℂ)
25	24	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℂ)
26	25	negcld 11563	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℂ)
27	22, 26	cxpcld 26449	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) ∈ ℂ)
28		ax-resscn 11170	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
29	28	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ ⊆ ℂ)
30		etransclem23.p	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℕ)
31		etransclem23.f	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))
32	29, 30, 31	etransclem8 45258	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
33	32	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝐹:ℝ⟶ℂ)
34	23	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
35	33, 34	ffvelcdmd 7088	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) ∈ ℂ)
36	35	adantlr 712	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) ∈ ℂ)
37	27, 36	mulcld 11239	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
38		reelprrecn 11205	. . . . . . . . 9 ⊢ ℝ ∈ {ℝ, ℂ}
39	38	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℝ ∈ {ℝ, ℂ})
40		reopn 44299	. . . . . . . . . 10 ⊢ ℝ ∈ (topGen‘ran (,))
41		eqid 2731	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
42	41	tgioo2 24540	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
43	40, 42	eleqtri 2830	. . . . . . . . 9 ⊢ ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ)
44	43	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
45	30	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑃 ∈ ℕ)
46		etransclem23.m	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℕ)
47	46	nnnn0d 12537	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
48	47	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℕ₀)
49		etransclem6 45256	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏ℎ ∈ (1...𝑀)((𝑦 − ℎ)↑𝑃)))
50		etransclem6 45256	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏ℎ ∈ (1...𝑀)((𝑦 − ℎ)↑𝑃))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))
51	31, 49, 50	3eqtri 2763	. . . . . . . 8 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))
52		0red 11222	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ)
53	17	zred 12671	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
54	53	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ)
55	39, 44, 45, 48, 51, 52, 54	etransclem18 45268	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ 𝐿¹)
56	37, 55	itgcl 25534	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥 ∈ ℂ)
57	21, 56	mulcld 11239	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ∈ ℂ)
58	7, 57	fsumcl 15684	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ∈ ℂ)
59		nnm1nn0 12518	. . . . . . 7 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
60	30, 59	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑃 − 1) ∈ ℕ₀)
61	60	faccld 14249	. . . . 5 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℕ)
62	61	nncnd 12233	. . . 4 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℂ)
63	61	nnne0d 12267	. . . 4 ⊢ (𝜑 → (!‘(𝑃 − 1)) ≠ 0)
64	58, 62, 63	absdivd 15407	. . 3 ⊢ (𝜑 → (abs‘(Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))) = ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (abs‘(!‘(𝑃 − 1)))))
65	61	nnred 12232	. . . . 5 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℝ)
66	61	nnnn0d 12537	. . . . . 6 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℕ₀)
67	66	nn0ge0d 12540	. . . . 5 ⊢ (𝜑 → 0 ≤ (!‘(𝑃 − 1)))
68	65, 67	absidd 15374	. . . 4 ⊢ (𝜑 → (abs‘(!‘(𝑃 − 1))) = (!‘(𝑃 − 1)))
69	68	oveq2d 7428	. . 3 ⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (abs‘(!‘(𝑃 − 1)))) = ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))))
70	6, 64, 69	3eqtrd 2775	. 2 ⊢ (𝜑 → (abs‘𝐾) = ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))))
71	2, 58	eqeltrid 2836	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ℂ)
72	71, 62, 63	divcld 11995	. . . . . 6 ⊢ (𝜑 → (𝐿 / (!‘(𝑃 − 1))) ∈ ℂ)
73	1, 72	eqeltrid 2836	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℂ)
74	73	abscld 15388	. . . 4 ⊢ (𝜑 → (abs‘𝐾) ∈ ℝ)
75	70, 74	eqeltrrd 2833	. . 3 ⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))) ∈ ℝ)
76	46	nnred 12232	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℝ)
77	30	nnnn0d 12537	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
78	76, 77	reexpcld 14133	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑𝑃) ∈ ℝ)
79		peano2nn0 12517	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ₀ → (𝑀 + 1) ∈ ℕ₀)
80	47, 79	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ₀)
81	78, 80	reexpcld 14133	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℝ)
82	81	recnd 11247	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ)
83	46	nncnd 12233	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℂ)
84	82, 83	mulcomd 11240	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) = (𝑀 · ((𝑀↑𝑃)↑(𝑀 + 1))))
85	30	nncnd 12233	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ ℂ)
86		1cnd 11214	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℂ)
87	85, 86	npcand 11580	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑃 − 1) + 1) = 𝑃)
88	87	eqcomd 2737	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 = ((𝑃 − 1) + 1))
89	88	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑𝑃) = ((𝑀↑(𝑀 + 1))↑((𝑃 − 1) + 1)))
90	80	nn0cnd 12539	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 + 1) ∈ ℂ)
91	90, 85	mulcomd 11240	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀 + 1) · 𝑃) = (𝑃 · (𝑀 + 1)))
92	91	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑((𝑀 + 1) · 𝑃)) = (𝑀↑(𝑃 · (𝑀 + 1))))
93	83, 77, 80	expmuld 14119	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑((𝑀 + 1) · 𝑃)) = ((𝑀↑(𝑀 + 1))↑𝑃))
94	83, 80, 77	expmuld 14119	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑(𝑃 · (𝑀 + 1))) = ((𝑀↑𝑃)↑(𝑀 + 1)))
95	92, 93, 94	3eqtr3d 2779	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑𝑃) = ((𝑀↑𝑃)↑(𝑀 + 1)))
96	76, 80	reexpcld 14133	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℝ)
97	96	recnd 11247	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℂ)
98	97, 60	expp1d 14117	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑((𝑃 − 1) + 1)) = (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1))))
99	89, 95, 98	3eqtr3d 2779	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀↑𝑃)↑(𝑀 + 1)) = (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1))))
100	99	oveq2d 7428	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 · ((𝑀↑𝑃)↑(𝑀 + 1))) = (𝑀 · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1)))))
101	97, 60	expcld 14116	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) ∈ ℂ)
102	83, 101, 97	mul12d 11428	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀 · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1)))) = (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀 · (𝑀↑(𝑀 + 1)))))
103	83, 97	mulcld 11239	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ)
104	101, 103	mulcomd 11240	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀 · (𝑀↑(𝑀 + 1)))) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
105	102, 104	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1)))) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
106	84, 100, 105	3eqtrd 2775	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
107	106	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
108	107	oveq2d 7428	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)))))
109	21	abscld 15388	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) ∈ ℝ)
110	109	recnd 11247	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) ∈ ℂ)
111	103	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ)
112	101	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) ∈ ℂ)
113	110, 111, 112	mulassd 11242	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) = ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)))))
114	108, 113	eqtr4d 2774	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = (((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
115	114	sumeq2dv 15654	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = Σ𝑗 ∈ (0...𝑀)(((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
116	110, 111	mulcld 11239	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
117	7, 101, 116	fsummulc1 15736	. . . . . . 7 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) = Σ𝑗 ∈ (0...𝑀)(((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
118	115, 117	eqtr4d 2774	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
119	118	oveq1d 7427	. . . . 5 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))) = ((Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) / (!‘(𝑃 − 1))))
120	7, 116	fsumcl 15684	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
121	120, 101, 62, 63	divassd 12030	. . . . 5 ⊢ (𝜑 → ((Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) / (!‘(𝑃 − 1))) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))))
122	119, 121	eqtrd 2771	. . . 4 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))))
123	81	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℝ)
124	76	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℝ)
125	123, 124	remulcld 11249	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) ∈ ℝ)
126	109, 125	remulcld 11249	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) ∈ ℝ)
127	7, 126	fsumrecl 15685	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) ∈ ℝ)
128	127, 61	nndivred 12271	. . . 4 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))) ∈ ℝ)
129	122, 128	eqeltrrd 2833	. . 3 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))) ∈ ℝ)
130		1red 11220	. . 3 ⊢ (𝜑 → 1 ∈ ℝ)
131	58	abscld 15388	. . . . 5 ⊢ (𝜑 → (abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ∈ ℝ)
132	61	nnrpd 13019	. . . . 5 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℝ⁺)
133	57	abscld 15388	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ∈ ℝ)
134	7, 133	fsumrecl 15685	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ∈ ℝ)
135	7, 57	fsumabs 15752	. . . . . 6 ⊢ (𝜑 → (abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)))
136	81	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℝ)
137		ioombl 25315	. . . . . . . . . . . 12 ⊢ (0(,)𝑗) ∈ dom vol
138	137	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0(,)𝑗) ∈ dom vol)
139		0red 11222	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → 0 ∈ ℝ)
140		elfzle1 13509	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
141		volioo 25319	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ 𝑗 ∈ ℝ ∧ 0 ≤ 𝑗) → (vol‘(0(,)𝑗)) = (𝑗 − 0))
142	139, 53, 140, 141	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) = (𝑗 − 0))
143	53, 139	resubcld 11647	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 0) ∈ ℝ)
144	142, 143	eqeltrd 2832	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) ∈ ℝ)
145	144	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (vol‘(0(,)𝑗)) ∈ ℝ)
146	82	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ)
147		iblconstmpt 44972	. . . . . . . . . . 11 ⊢ (((0(,)𝑗) ∈ dom vol ∧ (vol‘(0(,)𝑗)) ∈ ℝ ∧ ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ) → (𝑥 ∈ (0(,)𝑗) ↦ ((𝑀↑𝑃)↑(𝑀 + 1))) ∈ 𝐿¹)
148	138, 145, 146, 147	syl3anc 1370	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((𝑀↑𝑃)↑(𝑀 + 1))) ∈ 𝐿¹)
149	136, 148	itgrecl 25548	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 ∈ ℝ)
150	109, 149	remulcld 11249	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ∈ ℝ)
151	7, 150	fsumrecl 15685	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ∈ ℝ)
152	21, 56	absmuld 15406	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) = ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)))
153	56	abscld 15388	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ∈ ℝ)
154	21	absge0d 15396	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ (abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))))
155	37	abscld 15388	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ ℝ)
156	37, 55	iblabs 25579	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ (abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥)))) ∈ 𝐿¹)
157	155, 156	itgrecl 25548	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)(abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) d𝑥 ∈ ℝ)
158	37, 55	itgabs 25585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ≤ ∫(0(,)𝑗)(abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) d𝑥)
159	27, 36	absmuld 15406	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = ((abs‘(e↑_𝑐-𝑥)) · (abs‘(𝐹‘𝑥))))
160	27	abscld 15388	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(e↑_𝑐-𝑥)) ∈ ℝ)
161		1red 11220	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 1 ∈ ℝ)
162	36	abscld 15388	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) ∈ ℝ)
163	27	absge0d 15396	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ (abs‘(e↑_𝑐-𝑥)))
164	36	absge0d 15396	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ (abs‘(𝐹‘𝑥)))
165	14	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0(,)𝑗) → e ∈ ℝ)
166		0re 11221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℝ
167		epos 16155	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < e
168	166, 14, 167	ltleii 11342	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ≤ e
169	168	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0(,)𝑗) → 0 ≤ e)
170	23	renegcld 11646	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0(,)𝑗) → -𝑥 ∈ ℝ)
171	165, 169, 170	recxpcld 26464	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0(,)𝑗) → (e↑_𝑐-𝑥) ∈ ℝ)
172	165, 169, 170	cxpge0d 26465	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0(,)𝑗) → 0 ≤ (e↑_𝑐-𝑥))
173	171, 172	absidd 15374	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (0(,)𝑗) → (abs‘(e↑_𝑐-𝑥)) = (e↑_𝑐-𝑥))
174	173	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(e↑_𝑐-𝑥)) = (e↑_𝑐-𝑥))
175	171	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) ∈ ℝ)
176		1red 11220	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 1 ∈ ℝ)
177		0xr 11266	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℝ^*
178	177	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ∈ ℝ^*)
179	53	rexrd 11269	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ^*)
180	179	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑗 ∈ ℝ^*)
181		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ (0(,)𝑗))
182		ioogtlb 44508	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ∈ ℝ^* ∧ 𝑗 ∈ ℝ^* ∧ 𝑥 ∈ (0(,)𝑗)) → 0 < 𝑥)
183	178, 180, 181, 182	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 < 𝑥)
184	23	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
185	184	lt0neg2d 11789	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (0 < 𝑥 ↔ -𝑥 < 0))
186	183, 185	mpbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 < 0)
187	14	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → e ∈ ℝ)
188		1lt2 12388	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 < 2
189		egt2lt3 16154	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2 < e ∧ e < 3)
190	189	simpli 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 < e
191		1re 11219	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℝ
192		2re 12291	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℝ
193	191, 192, 14	lttri 11345	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 < 2 ∧ 2 < e) → 1 < e)
194	188, 190, 193	mp2an 689	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 < e
195	194	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 1 < e)
196	170	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℝ)
197		0red 11222	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ∈ ℝ)
198	187, 195, 196, 197	cxpltd 26460	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (-𝑥 < 0 ↔ (e↑_𝑐-𝑥) < (e↑_𝑐0)))
199	186, 198	mpbid 231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) < (e↑_𝑐0))
200		cxp0 26411	. . . . . . . . . . . . . . . . . . . 20 ⊢ (e ∈ ℂ → (e↑_𝑐0) = 1)
201	15, 200	mp1i 13	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐0) = 1)
202	199, 201	breqtrd 5175	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) < 1)
203	175, 176, 202	ltled 11367	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) ≤ 1)
204	174, 203	eqbrtrd 5171	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(e↑_𝑐-𝑥)) ≤ 1)
205	204	adantll 711	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(e↑_𝑐-𝑥)) ≤ 1)
206	28	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ℝ ⊆ ℂ)
207	30	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑃 ∈ ℕ)
208	47	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑀 ∈ ℕ₀)
209	31, 49	eqtri 2759	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏ℎ ∈ (1...𝑀)((𝑦 − ℎ)↑𝑃)))
210	23	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
211	206, 207, 208, 209, 210	etransclem13 45263	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) = ∏ℎ ∈ (0...𝑀)((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
212	211	fveq2d 6896	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) = (abs‘∏ℎ ∈ (0...𝑀)((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))))
213		nn0uz 12869	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ₀ = (ℤ_≥‘0)
214	23	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → 𝑥 ∈ ℝ)
215		nn0re 12486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ ∈ ℕ₀ → ℎ ∈ ℝ)
216	215	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → ℎ ∈ ℝ)
217	214, 216	resubcld 11647	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → (𝑥 − ℎ) ∈ ℝ)
218	217	adantll 711	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → (𝑥 − ℎ) ∈ ℝ)
219	60, 77	ifcld 4575	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
220	219	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
221	218, 220	reexpcld 14133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → ((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℝ)
222	221	recnd 11247	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → ((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℂ)
223	213, 208, 222	fprodabs 15923	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘∏ℎ ∈ (0...𝑀)((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))) = ∏ℎ ∈ (0...𝑀)(abs‘((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))))
224		elfznn0 13599	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ ∈ (0...𝑀) → ℎ ∈ ℕ₀)
225	24	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → 𝑥 ∈ ℂ)
226		nn0cn 12487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ ∈ ℕ₀ → ℎ ∈ ℂ)
227	226	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → ℎ ∈ ℂ)
228	225, 227	subcld 11576	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → (𝑥 − ℎ) ∈ ℂ)
229	228	adantll 711	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → (𝑥 − ℎ) ∈ ℂ)
230	224, 229	sylan2 592	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ∈ ℂ)
231	219	ad3antrrr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
232	230, 231	absexpd 15404	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (abs‘((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))) = ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
233	232	prodeq2dv 15872	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)(abs‘((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))) = ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
234	212, 223, 233	3eqtrd 2775	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) = ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
235		nfv 1916	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎℎ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗))
236		fzfid 13943	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (0...𝑀) ∈ Fin)
237	224, 228	sylan2 592	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ∈ ℂ)
238	237	abscld 15388	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → (abs‘(𝑥 − ℎ)) ∈ ℝ)
239	238	adantll 711	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (abs‘(𝑥 − ℎ)) ∈ ℝ)
240	239, 231	reexpcld 14133	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℝ)
241	237	absge0d 15396	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ (abs‘(𝑥 − ℎ)))
242	241	adantll 711	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ (abs‘(𝑥 − ℎ)))
243	239, 231, 242	expge0d 14134	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
244	78	ad3antrrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀↑𝑃) ∈ ℝ)
245	76	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑀 ∈ ℝ)
246	245, 231	reexpcld 14133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℝ)
247	224, 218	sylan2 592	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ∈ ℝ)
248	24	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → 𝑥 ∈ ℂ)
249	224, 227	sylan2 592	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → ℎ ∈ ℂ)
250	248, 249	negsubdi2d 11592	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → -(𝑥 − ℎ) = (ℎ − 𝑥))
251	250	adantll 711	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → -(𝑥 − ℎ) = (ℎ − 𝑥))
252	224	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ℎ ∈ ℕ₀)
253	252	nn0red 12538	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ℎ ∈ ℝ)
254		0red 11222	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ∈ ℝ)
255	210	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑥 ∈ ℝ)
256		elfzle2 13510	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ ∈ (0...𝑀) → ℎ ≤ 𝑀)
257	256	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ℎ ≤ 𝑀)
258	197, 184, 183	ltled 11367	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ 𝑥)
259	258	adantll 711	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ 𝑥)
260	259	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ 𝑥)
261	253, 254, 245, 255, 257, 260	le2subd 11839	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (ℎ − 𝑥) ≤ (𝑀 − 0))
262	83	subid1d 11565	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑀 − 0) = 𝑀)
263	262	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀 − 0) = 𝑀)
264	261, 263	breqtrd 5175	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (ℎ − 𝑥) ≤ 𝑀)
265	251, 264	eqbrtrd 5171	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → -(𝑥 − ℎ) ≤ 𝑀)
266	247, 245, 265	lenegcon1d 11801	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → -𝑀 ≤ (𝑥 − ℎ))
267		elfzel2 13504	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
268	267	zred 12671	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
269	268	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑀 ∈ ℝ)
270	53	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑗 ∈ ℝ)
271		iooltub 44523	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0 ∈ ℝ^* ∧ 𝑗 ∈ ℝ^* ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 < 𝑗)
272	178, 180, 181, 271	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 < 𝑗)
273		elfzle2 13510	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀)
274	273	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑗 ≤ 𝑀)
275	184, 270, 269, 272, 274	ltletrd 11379	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 < 𝑀)
276	184, 269, 275	ltled 11367	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ≤ 𝑀)
277	276	adantll 711	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ≤ 𝑀)
278	277	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑥 ≤ 𝑀)
279	252	nn0ge0d 12540	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ ℎ)
280	255, 254, 245, 253, 278, 279	le2subd 11839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ≤ (𝑀 − 0))
281	280, 263	breqtrd 5175	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ≤ 𝑀)
282	247, 245	absled 15382	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ)) ≤ 𝑀 ↔ (-𝑀 ≤ (𝑥 − ℎ) ∧ (𝑥 − ℎ) ≤ 𝑀)))
283	266, 281, 282	mpbir2and 710	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (abs‘(𝑥 − ℎ)) ≤ 𝑀)
284		leexp1a 14145	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((abs‘(𝑥 − ℎ)) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀) ∧ (0 ≤ (abs‘(𝑥 − ℎ)) ∧ (abs‘(𝑥 − ℎ)) ≤ 𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
285	239, 245, 231, 242, 283, 284	syl32anc 1377	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
286	46	nnge1d 12265	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ≤ 𝑀)
287	286	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 1 ≤ 𝑀)
288	219	nn0zd 12589	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℤ)
289	77	nn0zd 12589	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑃 ∈ ℤ)
290		iftrue 4535	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = 0 → if(ℎ = 0, (𝑃 − 1), 𝑃) = (𝑃 − 1))
291	290	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) = (𝑃 − 1))
292	30	nnred 12232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑃 ∈ ℝ)
293	292	lem1d 12152	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑃 − 1) ≤ 𝑃)
294	293	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ℎ = 0) → (𝑃 − 1) ≤ 𝑃)
295	291, 294	eqbrtrd 5171	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃)
296		iffalse 4538	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ ℎ = 0 → if(ℎ = 0, (𝑃 − 1), 𝑃) = 𝑃)
297	296	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ¬ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) = 𝑃)
298	292	leidd 11785	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑃 ≤ 𝑃)
299	298	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ¬ ℎ = 0) → 𝑃 ≤ 𝑃)
300	297, 299	eqbrtrd 5171	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ¬ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃)
301	295, 300	pm2.61dan 810	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃)
302		eluz2 12833	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ (ℤ_≥‘if(ℎ = 0, (𝑃 − 1), 𝑃)) ↔ (if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃))
303	288, 289, 301, 302	syl3anbrc 1342	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑃 ∈ (ℤ_≥‘if(ℎ = 0, (𝑃 − 1), 𝑃)))
304	303	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑃 ∈ (ℤ_≥‘if(ℎ = 0, (𝑃 − 1), 𝑃)))
305	245, 287, 304	leexp2ad 14222	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑𝑃))
306	240, 246, 244, 285, 305	letrd 11376	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑𝑃))
307	235, 236, 240, 243, 244, 306	fprodle 15945	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃))
308	78	recnd 11247	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀↑𝑃) ∈ ℂ)
309		fprodconst 15927	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0...𝑀) ∈ Fin ∧ (𝑀↑𝑃) ∈ ℂ) → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(♯‘(0...𝑀))))
310	7, 308, 309	syl2anc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(♯‘(0...𝑀))))
311		hashfz0 14397	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ ℕ₀ → (♯‘(0...𝑀)) = (𝑀 + 1))
312	47, 311	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (♯‘(0...𝑀)) = (𝑀 + 1))
313	312	oveq2d 7428	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑀↑𝑃)↑(♯‘(0...𝑀))) = ((𝑀↑𝑃)↑(𝑀 + 1)))
314	310, 313	eqtrd 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(𝑀 + 1)))
315	314	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(𝑀 + 1)))
316	307, 315	breqtrd 5175	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
317	234, 316	eqbrtrd 5171	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
318	160, 161, 162, 136, 163, 164, 205, 317	lemul12ad 12161	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((abs‘(e↑_𝑐-𝑥)) · (abs‘(𝐹‘𝑥))) ≤ (1 · ((𝑀↑𝑃)↑(𝑀 + 1))))
319	82	mullidd 11237	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · ((𝑀↑𝑃)↑(𝑀 + 1))) = ((𝑀↑𝑃)↑(𝑀 + 1)))
320	319	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (1 · ((𝑀↑𝑃)↑(𝑀 + 1))) = ((𝑀↑𝑃)↑(𝑀 + 1)))
321	318, 320	breqtrd 5175	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((abs‘(e↑_𝑐-𝑥)) · (abs‘(𝐹‘𝑥))) ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
322	159, 321	eqbrtrd 5171	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
323	156, 148, 155, 136, 322	itgle 25560	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)(abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) d𝑥 ≤ ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥)
324	153, 157, 149, 158, 323	letrd 11376	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ≤ ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥)
325	153, 149, 109, 154, 324	lemul2ad 12159	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥))
326	152, 325	eqbrtrd 5171	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥))
327	7, 133, 150, 326	fsumle 15750	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥))
328		itgconst 25569	. . . . . . . . . . 11 ⊢ (((0(,)𝑗) ∈ dom vol ∧ (vol‘(0(,)𝑗)) ∈ ℝ ∧ ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 = (((𝑀↑𝑃)↑(𝑀 + 1)) · (vol‘(0(,)𝑗))))
329	138, 145, 146, 328	syl3anc 1370	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 = (((𝑀↑𝑃)↑(𝑀 + 1)) · (vol‘(0(,)𝑗))))
330	47	nn0ge0d 12540	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ≤ 𝑀)
331	76, 77, 330	expge0d 14134	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ (𝑀↑𝑃))
332	78, 80, 331	expge0d 14134	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
333	332	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
334	18	subid1d 11565	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 0) = 𝑗)
335	142, 334	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) = 𝑗)
336	335, 273	eqbrtrd 5171	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) ≤ 𝑀)
337	336	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (vol‘(0(,)𝑗)) ≤ 𝑀)
338	145, 124, 123, 333, 337	lemul2ad 12159	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀↑𝑃)↑(𝑀 + 1)) · (vol‘(0(,)𝑗))) ≤ (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀))
339	329, 338	eqbrtrd 5171	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 ≤ (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀))
340	149, 125, 109, 154, 339	lemul2ad 12159	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ≤ ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)))
341	7, 150, 126, 340	fsumle 15750	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)))
342	134, 151, 127, 327, 341	letrd 11376	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)))
343	131, 134, 127, 135, 342	letrd 11376	. . . . 5 ⊢ (𝜑 → (abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)))
344	131, 127, 132, 343	lediv1dd 13079	. . . 4 ⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))) ≤ (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))))
345	344, 122	breqtrd 5175	. . 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 11377	. 2 ⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))) < 1)
348	70, 347	eqbrtrd 5171	1 ⊢ (𝜑 → (abs‘𝐾) < 1)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2105 ⊆ wss 3949 ifcif 4529 {cpr 4631 class class class wbr 5149 ↦ cmpt 5232 dom cdm 5677 ran crn 5678 ⟶wf 6540 ‘cfv 6544 (class class class)co 7412 Fincfn 8942 ℂcc 11111 ℝcr 11112 0cc0 11113 1c1 11114 + caddc 11116 · cmul 11118 ℝ^*cxr 11252 < clt 11253 ≤ cle 11254 − cmin 11449 -cneg 11450 / cdiv 11876 ℕcn 12217 2c2 12272 3c3 12273 ℕ₀cn0 12477 ℤcz 12563 ℤ_≥cuz 12827 (,)cioo 13329 ...cfz 13489 ↑cexp 14032 !cfa 14238 ♯chash 14295 abscabs 15186 Σcsu 15637 ∏cprod 15854 eceu 16011 ↾_t crest 17371 TopOpenctopn 17372 topGenctg 17388 ℂ_fldccnfld 21145 volcvol 25213 𝐿¹cibl 25367 ∫citg 25368 ↑_𝑐ccxp 26297

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7728 ax-inf2 9639 ax-cc 10433 ax-cnex 11169 ax-resscn 11170 ax-1cn 11171 ax-icn 11172 ax-addcl 11173 ax-addrcl 11174 ax-mulcl 11175 ax-mulrcl 11176 ax-mulcom 11177 ax-addass 11178 ax-mulass 11179 ax-distr 11180 ax-i2m1 11181 ax-1ne0 11182 ax-1rid 11183 ax-rnegex 11184 ax-rrecex 11185 ax-cnre 11186 ax-pre-lttri 11187 ax-pre-lttrn 11188 ax-pre-ltadd 11189 ax-pre-mulgt0 11190 ax-pre-sup 11191 ax-addf 11192 ax-mulf 11193

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-uni 4910 df-int 4952 df-iun 5000 df-iin 5001 df-disj 5115 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-se 5633 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-isom 6553 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7673 df-ofr 7674 df-om 7859 df-1st 7978 df-2nd 7979 df-supp 8150 df-frecs 8269 df-wrecs 8300 df-recs 8374 df-rdg 8413 df-1o 8469 df-2o 8470 df-oadd 8473 df-omul 8474 df-er 8706 df-map 8825 df-pm 8826 df-ixp 8895 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-fsupp 9365 df-fi 9409 df-sup 9440 df-inf 9441 df-oi 9508 df-dju 9899 df-card 9937 df-acn 9940 df-pnf 11255 df-mnf 11256 df-xr 11257 df-ltxr 11258 df-le 11259 df-sub 11451 df-neg 11452 df-div 11877 df-nn 12218 df-2 12280 df-3 12281 df-4 12282 df-5 12283 df-6 12284 df-7 12285 df-8 12286 df-9 12287 df-n0 12478 df-z 12564 df-dec 12683 df-uz 12828 df-q 12938 df-rp 12980 df-xneg 13097 df-xadd 13098 df-xmul 13099 df-ioo 13333 df-ioc 13334 df-ico 13335 df-icc 13336 df-fz 13490 df-fzo 13633 df-fl 13762 df-mod 13840 df-seq 13972 df-exp 14033 df-fac 14239 df-bc 14268 df-hash 14296 df-shft 15019 df-cj 15051 df-re 15052 df-im 15053 df-sqrt 15187 df-abs 15188 df-limsup 15420 df-clim 15437 df-rlim 15438 df-sum 15638 df-prod 15855 df-ef 16016 df-e 16017 df-sin 16018 df-cos 16019 df-tan 16020 df-pi 16021 df-struct 17085 df-sets 17102 df-slot 17120 df-ndx 17132 df-base 17150 df-ress 17179 df-plusg 17215 df-mulr 17216 df-starv 17217 df-sca 17218 df-vsca 17219 df-ip 17220 df-tset 17221 df-ple 17222 df-ds 17224 df-unif 17225 df-hom 17226 df-cco 17227 df-rest 17373 df-topn 17374 df-0g 17392 df-gsum 17393 df-topgen 17394 df-pt 17395 df-prds 17398 df-xrs 17453 df-qtop 17458 df-imas 17459 df-xps 17461 df-mre 17535 df-mrc 17536 df-acs 17538 df-mgm 18566 df-sgrp 18645 df-mnd 18661 df-submnd 18707 df-mulg 18988 df-cntz 19223 df-cmn 19692 df-psmet 21137 df-xmet 21138 df-met 21139 df-bl 21140 df-mopn 21141 df-fbas 21142 df-fg 21143 df-cnfld 21146 df-top 22617 df-topon 22634 df-topsp 22656 df-bases 22670 df-cld 22744 df-ntr 22745 df-cls 22746 df-nei 22823 df-lp 22861 df-perf 22862 df-cn 22952 df-cnp 22953 df-haus 23040 df-cmp 23112 df-tx 23287 df-hmeo 23480 df-fil 23571 df-fm 23663 df-flim 23664 df-flf 23665 df-xms 24047 df-ms 24048 df-tms 24049 df-cncf 24619 df-ovol 25214 df-vol 25215 df-mbf 25369 df-itg1 25370 df-itg2 25371 df-ibl 25372 df-itg 25373 df-0p 25420 df-limc 25616 df-dv 25617 df-log 26298 df-cxp 26299

This theorem is referenced by: etransclem47 45297

W3C validator