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 45783

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 7429	. . . . . 6 ⊢ (𝐿 / (!‘(𝑃 − 1))) = (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))
4	1, 3	eqtri 2753	. . . . 5 ⊢ 𝐾 = (Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))
5	4	fveq2i 6899	. . . 4 ⊢ (abs‘𝐾) = (abs‘(Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1))))
6	5	a1i 11	. . 3 ⊢ (𝜑 → (abs‘𝐾) = (abs‘(Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))))
7		fzfid 13974	. . . . 5 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
8		etransclem23.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℤ)
9	8	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝐴:ℕ₀⟶ℤ)
10		elfznn0 13629	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ₀)
11	10	adantl 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ₀)
12	9, 11	ffvelcdmd 7094	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℤ)
13	12	zcnd 12700	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝐴‘𝑗) ∈ ℂ)
14		ere 16069	. . . . . . . . . 10 ⊢ e ∈ ℝ
15	14	recni 11260	. . . . . . . . 9 ⊢ e ∈ ℂ
16	15	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → e ∈ ℂ)
17		elfzelz 13536	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
18	17	zcnd 12700	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
19	18	adantl 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℂ)
20	16, 19	cxpcld 26687	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (e↑_𝑐𝑗) ∈ ℂ)
21	13, 20	mulcld 11266	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝐴‘𝑗) · (e↑_𝑐𝑗)) ∈ ℂ)
22	15	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → e ∈ ℂ)
23		elioore 13389	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℝ)
24	23	recnd 11274	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℂ)
25	24	adantl 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℂ)
26	25	negcld 11590	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℂ)
27	22, 26	cxpcld 26687	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) ∈ ℂ)
28		ax-resscn 11197	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
29	28	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ ⊆ ℂ)
30		etransclem23.p	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℕ)
31		etransclem23.f	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃)))
32	29, 30, 31	etransclem8 45768	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
33	32	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝐹:ℝ⟶ℂ)
34	23	adantl 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
35	33, 34	ffvelcdmd 7094	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) ∈ ℂ)
36	35	adantlr 713	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) ∈ ℂ)
37	27, 36	mulcld 11266	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑_𝑐-𝑥) · (𝐹‘𝑥)) ∈ ℂ)
38		reelprrecn 11232	. . . . . . . . 9 ⊢ ℝ ∈ {ℝ, ℂ}
39	38	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℝ ∈ {ℝ, ℂ})
40		reopn 44809	. . . . . . . . . 10 ⊢ ℝ ∈ (topGen‘ran (,))
41		eqid 2725	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
42	41	tgioo2 24763	. . . . . . . . . 10 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
43	40, 42	eleqtri 2823	. . . . . . . . 9 ⊢ ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ)
44	43	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ℝ ∈ ((TopOpen‘ℂ_fld) ↾_t ℝ))
45	30	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑃 ∈ ℕ)
46		etransclem23.m	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℕ)
47	46	nnnn0d 12565	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
48	47	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℕ₀)
49		etransclem6 45766	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏ℎ ∈ (1...𝑀)((𝑦 − ℎ)↑𝑃)))
50		etransclem6 45766	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏ℎ ∈ (1...𝑀)((𝑦 − ℎ)↑𝑃))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))
51	31, 49, 50	3eqtri 2757	. . . . . . . 8 ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥 − 𝑘)↑𝑃)))
52		0red 11249	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ)
53	17	zred 12699	. . . . . . . . 9 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
54	53	adantl 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ)
55	39, 44, 45, 48, 51, 52, 54	etransclem18 45778	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ 𝐿¹)
56	37, 55	itgcl 25757	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥 ∈ ℂ)
57	21, 56	mulcld 11266	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ∈ ℂ)
58	7, 57	fsumcl 15715	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ∈ ℂ)
59		nnm1nn0 12546	. . . . . . 7 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
60	30, 59	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑃 − 1) ∈ ℕ₀)
61	60	faccld 14279	. . . . 5 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℕ)
62	61	nncnd 12261	. . . 4 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℂ)
63	61	nnne0d 12295	. . . 4 ⊢ (𝜑 → (!‘(𝑃 − 1)) ≠ 0)
64	58, 62, 63	absdivd 15438	. . 3 ⊢ (𝜑 → (abs‘(Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) / (!‘(𝑃 − 1)))) = ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (abs‘(!‘(𝑃 − 1)))))
65	61	nnred 12260	. . . . 5 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℝ)
66	61	nnnn0d 12565	. . . . . 6 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℕ₀)
67	66	nn0ge0d 12568	. . . . 5 ⊢ (𝜑 → 0 ≤ (!‘(𝑃 − 1)))
68	65, 67	absidd 15405	. . . 4 ⊢ (𝜑 → (abs‘(!‘(𝑃 − 1))) = (!‘(𝑃 − 1)))
69	68	oveq2d 7435	. . 3 ⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (abs‘(!‘(𝑃 − 1)))) = ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))))
70	6, 64, 69	3eqtrd 2769	. 2 ⊢ (𝜑 → (abs‘𝐾) = ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))))
71	2, 58	eqeltrid 2829	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ ℂ)
72	71, 62, 63	divcld 12023	. . . . . 6 ⊢ (𝜑 → (𝐿 / (!‘(𝑃 − 1))) ∈ ℂ)
73	1, 72	eqeltrid 2829	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℂ)
74	73	abscld 15419	. . . 4 ⊢ (𝜑 → (abs‘𝐾) ∈ ℝ)
75	70, 74	eqeltrrd 2826	. . 3 ⊢ (𝜑 → ((abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) / (!‘(𝑃 − 1))) ∈ ℝ)
76	46	nnred 12260	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℝ)
77	30	nnnn0d 12565	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ ℕ₀)
78	76, 77	reexpcld 14163	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑𝑃) ∈ ℝ)
79		peano2nn0 12545	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ ℕ₀ → (𝑀 + 1) ∈ ℕ₀)
80	47, 79	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ₀)
81	78, 80	reexpcld 14163	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℝ)
82	81	recnd 11274	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ)
83	46	nncnd 12261	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℂ)
84	82, 83	mulcomd 11267	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) = (𝑀 · ((𝑀↑𝑃)↑(𝑀 + 1))))
85	30	nncnd 12261	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ ℂ)
86		1cnd 11241	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℂ)
87	85, 86	npcand 11607	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑃 − 1) + 1) = 𝑃)
88	87	eqcomd 2731	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 = ((𝑃 − 1) + 1))
89	88	oveq2d 7435	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑𝑃) = ((𝑀↑(𝑀 + 1))↑((𝑃 − 1) + 1)))
90	80	nn0cnd 12567	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 + 1) ∈ ℂ)
91	90, 85	mulcomd 11267	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑀 + 1) · 𝑃) = (𝑃 · (𝑀 + 1)))
92	91	oveq2d 7435	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑((𝑀 + 1) · 𝑃)) = (𝑀↑(𝑃 · (𝑀 + 1))))
93	83, 77, 80	expmuld 14149	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑((𝑀 + 1) · 𝑃)) = ((𝑀↑(𝑀 + 1))↑𝑃))
94	83, 80, 77	expmuld 14149	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑(𝑃 · (𝑀 + 1))) = ((𝑀↑𝑃)↑(𝑀 + 1)))
95	92, 93, 94	3eqtr3d 2773	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑𝑃) = ((𝑀↑𝑃)↑(𝑀 + 1)))
96	76, 80	reexpcld 14163	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℝ)
97	96	recnd 11274	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀↑(𝑀 + 1)) ∈ ℂ)
98	97, 60	expp1d 14147	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑((𝑃 − 1) + 1)) = (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1))))
99	89, 95, 98	3eqtr3d 2773	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑀↑𝑃)↑(𝑀 + 1)) = (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1))))
100	99	oveq2d 7435	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 · ((𝑀↑𝑃)↑(𝑀 + 1))) = (𝑀 · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1)))))
101	97, 60	expcld 14146	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) ∈ ℂ)
102	83, 101, 97	mul12d 11455	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀 · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1)))) = (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀 · (𝑀↑(𝑀 + 1)))))
103	83, 97	mulcld 11266	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ)
104	101, 103	mulcomd 11267	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀 · (𝑀↑(𝑀 + 1)))) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
105	102, 104	eqtrd 2765	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) · (𝑀↑(𝑀 + 1)))) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
106	84, 100, 105	3eqtrd 2769	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
107	106	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) = ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
108	107	oveq2d 7435	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)))))
109	21	abscld 15419	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) ∈ ℝ)
110	109	recnd 11274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) ∈ ℂ)
111	103	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑀 · (𝑀↑(𝑀 + 1))) ∈ ℂ)
112	101	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) ∈ ℂ)
113	110, 111, 112	mulassd 11269	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) = ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ((𝑀 · (𝑀↑(𝑀 + 1))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1)))))
114	108, 113	eqtr4d 2768	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = (((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
115	114	sumeq2dv 15685	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = Σ𝑗 ∈ (0...𝑀)(((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
116	110, 111	mulcld 11266	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
117	7, 101, 116	fsummulc1 15767	. . . . . . 7 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) = Σ𝑗 ∈ (0...𝑀)(((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
118	115, 117	eqtr4d 2768	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))))
119	118	oveq1d 7434	. . . . 5 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))) = ((Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) / (!‘(𝑃 − 1))))
120	7, 116	fsumcl 15715	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) ∈ ℂ)
121	120, 101, 62, 63	divassd 12058	. . . . 5 ⊢ (𝜑 → ((Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · ((𝑀↑(𝑀 + 1))↑(𝑃 − 1))) / (!‘(𝑃 − 1))) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))))
122	119, 121	eqtrd 2765	. . . 4 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))) = (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))))
123	81	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℝ)
124	76	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℝ)
125	123, 124	remulcld 11276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀) ∈ ℝ)
126	109, 125	remulcld 11276	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) ∈ ℝ)
127	7, 126	fsumrecl 15716	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) ∈ ℝ)
128	127, 61	nndivred 12299	. . . 4 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)) / (!‘(𝑃 − 1))) ∈ ℝ)
129	122, 128	eqeltrrd 2826	. . 3 ⊢ (𝜑 → (Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (𝑀 · (𝑀↑(𝑀 + 1)))) · (((𝑀↑(𝑀 + 1))↑(𝑃 − 1)) / (!‘(𝑃 − 1)))) ∈ ℝ)
130		1red 11247	. . 3 ⊢ (𝜑 → 1 ∈ ℝ)
131	58	abscld 15419	. . . . 5 ⊢ (𝜑 → (abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ∈ ℝ)
132	61	nnrpd 13049	. . . . 5 ⊢ (𝜑 → (!‘(𝑃 − 1)) ∈ ℝ⁺)
133	57	abscld 15419	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ∈ ℝ)
134	7, 133	fsumrecl 15716	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ∈ ℝ)
135	7, 57	fsumabs 15783	. . . . . 6 ⊢ (𝜑 → (abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)))
136	81	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℝ)
137		ioombl 25538	. . . . . . . . . . . 12 ⊢ (0(,)𝑗) ∈ dom vol
138	137	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (0(,)𝑗) ∈ dom vol)
139		0red 11249	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → 0 ∈ ℝ)
140		elfzle1 13539	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
141		volioo 25542	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ 𝑗 ∈ ℝ ∧ 0 ≤ 𝑗) → (vol‘(0(,)𝑗)) = (𝑗 − 0))
142	139, 53, 140, 141	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) = (𝑗 − 0))
143	53, 139	resubcld 11674	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 0) ∈ ℝ)
144	142, 143	eqeltrd 2825	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) ∈ ℝ)
145	144	adantl 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (vol‘(0(,)𝑗)) ∈ ℝ)
146	82	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ)
147		iblconstmpt 45482	. . . . . . . . . . 11 ⊢ (((0(,)𝑗) ∈ dom vol ∧ (vol‘(0(,)𝑗)) ∈ ℝ ∧ ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ) → (𝑥 ∈ (0(,)𝑗) ↦ ((𝑀↑𝑃)↑(𝑀 + 1))) ∈ 𝐿¹)
148	138, 145, 146, 147	syl3anc 1368	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((𝑀↑𝑃)↑(𝑀 + 1))) ∈ 𝐿¹)
149	136, 148	itgrecl 25771	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 ∈ ℝ)
150	109, 149	remulcld 11276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ∈ ℝ)
151	7, 150	fsumrecl 15716	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ∈ ℝ)
152	21, 56	absmuld 15437	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) = ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)))
153	56	abscld 15419	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ∈ ℝ)
154	21	absge0d 15427	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ (abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))))
155	37	abscld 15419	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) ∈ ℝ)
156	37, 55	iblabs 25802	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ (abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥)))) ∈ 𝐿¹)
157	155, 156	itgrecl 25771	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)(abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) d𝑥 ∈ ℝ)
158	37, 55	itgabs 25808	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ≤ ∫(0(,)𝑗)(abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) d𝑥)
159	27, 36	absmuld 15437	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) = ((abs‘(e↑_𝑐-𝑥)) · (abs‘(𝐹‘𝑥))))
160	27	abscld 15419	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(e↑_𝑐-𝑥)) ∈ ℝ)
161		1red 11247	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 1 ∈ ℝ)
162	36	abscld 15419	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) ∈ ℝ)
163	27	absge0d 15427	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ (abs‘(e↑_𝑐-𝑥)))
164	36	absge0d 15427	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ (abs‘(𝐹‘𝑥)))
165	14	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0(,)𝑗) → e ∈ ℝ)
166		0re 11248	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℝ
167		epos 16187	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 < e
168	166, 14, 167	ltleii 11369	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ≤ e
169	168	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0(,)𝑗) → 0 ≤ e)
170	23	renegcld 11673	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (0(,)𝑗) → -𝑥 ∈ ℝ)
171	165, 169, 170	recxpcld 26702	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0(,)𝑗) → (e↑_𝑐-𝑥) ∈ ℝ)
172	165, 169, 170	cxpge0d 26703	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (0(,)𝑗) → 0 ≤ (e↑_𝑐-𝑥))
173	171, 172	absidd 15405	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (0(,)𝑗) → (abs‘(e↑_𝑐-𝑥)) = (e↑_𝑐-𝑥))
174	173	adantl 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(e↑_𝑐-𝑥)) = (e↑_𝑐-𝑥))
175	171	adantl 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) ∈ ℝ)
176		1red 11247	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 1 ∈ ℝ)
177		0xr 11293	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℝ^*
178	177	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ∈ ℝ^*)
179	53	rexrd 11296	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ^*)
180	179	adantr 479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑗 ∈ ℝ^*)
181		simpr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ (0(,)𝑗))
182		ioogtlb 45018	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ∈ ℝ^* ∧ 𝑗 ∈ ℝ^* ∧ 𝑥 ∈ (0(,)𝑗)) → 0 < 𝑥)
183	178, 180, 181, 182	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 < 𝑥)
184	23	adantl 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
185	184	lt0neg2d 11816	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (0 < 𝑥 ↔ -𝑥 < 0))
186	183, 185	mpbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 < 0)
187	14	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → e ∈ ℝ)
188		1lt2 12416	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 < 2
189		egt2lt3 16186	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2 < e ∧ e < 3)
190	189	simpli 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 < e
191		1re 11246	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℝ
192		2re 12319	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℝ
193	191, 192, 14	lttri 11372	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 < 2 ∧ 2 < e) → 1 < e)
194	188, 190, 193	mp2an 690	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 < e
195	194	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 1 < e)
196	170	adantl 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℝ)
197		0red 11249	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ∈ ℝ)
198	187, 195, 196, 197	cxpltd 26698	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (-𝑥 < 0 ↔ (e↑_𝑐-𝑥) < (e↑_𝑐0)))
199	186, 198	mpbid 231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) < (e↑_𝑐0))
200		cxp0 26649	. . . . . . . . . . . . . . . . . . . 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 11394	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (e↑_𝑐-𝑥) ≤ 1)
204	174, 203	eqbrtrd 5171	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(e↑_𝑐-𝑥)) ≤ 1)
205	204	adantll 712	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(e↑_𝑐-𝑥)) ≤ 1)
206	28	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ℝ ⊆ ℂ)
207	30	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑃 ∈ ℕ)
208	47	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑀 ∈ ℕ₀)
209	31, 49	eqtri 2753	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐹 = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏ℎ ∈ (1...𝑀)((𝑦 − ℎ)↑𝑃)))
210	23	adantl 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
211	206, 207, 208, 209, 210	etransclem13 45773	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (𝐹‘𝑥) = ∏ℎ ∈ (0...𝑀)((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
212	211	fveq2d 6900	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) = (abs‘∏ℎ ∈ (0...𝑀)((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))))
213		nn0uz 12897	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ₀ = (ℤ_≥‘0)
214	23	adantr 479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → 𝑥 ∈ ℝ)
215		nn0re 12514	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ ∈ ℕ₀ → ℎ ∈ ℝ)
216	215	adantl 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → ℎ ∈ ℝ)
217	214, 216	resubcld 11674	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → (𝑥 − ℎ) ∈ ℝ)
218	217	adantll 712	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → (𝑥 − ℎ) ∈ ℝ)
219	60, 77	ifcld 4576	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
220	219	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
221	218, 220	reexpcld 14163	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → ((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℝ)
222	221	recnd 11274	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → ((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℂ)
223	213, 208, 222	fprodabs 15954	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘∏ℎ ∈ (0...𝑀)((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))) = ∏ℎ ∈ (0...𝑀)(abs‘((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))))
224		elfznn0 13629	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ ∈ (0...𝑀) → ℎ ∈ ℕ₀)
225	24	adantr 479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → 𝑥 ∈ ℂ)
226		nn0cn 12515	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ ∈ ℕ₀ → ℎ ∈ ℂ)
227	226	adantl 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → ℎ ∈ ℂ)
228	225, 227	subcld 11603	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ ℕ₀) → (𝑥 − ℎ) ∈ ℂ)
229	228	adantll 712	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ ℕ₀) → (𝑥 − ℎ) ∈ ℂ)
230	224, 229	sylan2 591	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ∈ ℂ)
231	219	ad3antrrr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀)
232	230, 231	absexpd 15435	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (abs‘((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))) = ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
233	232	prodeq2dv 15903	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)(abs‘((𝑥 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃))) = ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
234	212, 223, 233	3eqtrd 2769	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (abs‘(𝐹‘𝑥)) = ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
235		nfv 1909	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎℎ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗))
236		fzfid 13974	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → (0...𝑀) ∈ Fin)
237	224, 228	sylan2 591	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ∈ ℂ)
238	237	abscld 15419	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → (abs‘(𝑥 − ℎ)) ∈ ℝ)
239	238	adantll 712	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (abs‘(𝑥 − ℎ)) ∈ ℝ)
240	239, 231	reexpcld 14163	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℝ)
241	237	absge0d 15427	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ (abs‘(𝑥 − ℎ)))
242	241	adantll 712	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ (abs‘(𝑥 − ℎ)))
243	239, 231, 242	expge0d 14164	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
244	78	ad3antrrr 728	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀↑𝑃) ∈ ℝ)
245	76	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑀 ∈ ℝ)
246	245, 231	reexpcld 14163	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ∈ ℝ)
247	224, 218	sylan2 591	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ∈ ℝ)
248	24	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → 𝑥 ∈ ℂ)
249	224, 227	sylan2 591	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → ℎ ∈ ℂ)
250	248, 249	negsubdi2d 11619	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑥 ∈ (0(,)𝑗) ∧ ℎ ∈ (0...𝑀)) → -(𝑥 − ℎ) = (ℎ − 𝑥))
251	250	adantll 712	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → -(𝑥 − ℎ) = (ℎ − 𝑥))
252	224	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ℎ ∈ ℕ₀)
253	252	nn0red 12566	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ℎ ∈ ℝ)
254		0red 11249	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ∈ ℝ)
255	210	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑥 ∈ ℝ)
256		elfzle2 13540	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ ∈ (0...𝑀) → ℎ ≤ 𝑀)
257	256	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ℎ ≤ 𝑀)
258	197, 184, 183	ltled 11394	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ 𝑥)
259	258	adantll 712	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 0 ≤ 𝑥)
260	259	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ 𝑥)
261	253, 254, 245, 255, 257, 260	le2subd 11866	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (ℎ − 𝑥) ≤ (𝑀 − 0))
262	83	subid1d 11592	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑀 − 0) = 𝑀)
263	262	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . 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 11828	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → -𝑀 ≤ (𝑥 − ℎ))
267		elfzel2 13534	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
268	267	zred 12699	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
269	268	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑀 ∈ ℝ)
270	53	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑗 ∈ ℝ)
271		iooltub 45033	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((0 ∈ ℝ^* ∧ 𝑗 ∈ ℝ^* ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 < 𝑗)
272	178, 180, 181, 271	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 < 𝑗)
273		elfzle2 13540	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑀) → 𝑗 ≤ 𝑀)
274	273	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑗 ≤ 𝑀)
275	184, 270, 269, 272, 274	ltletrd 11406	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 < 𝑀)
276	184, 269, 275	ltled 11394	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ≤ 𝑀)
277	276	adantll 712	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → 𝑥 ≤ 𝑀)
278	277	adantr 479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑥 ≤ 𝑀)
279	252	nn0ge0d 12568	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 0 ≤ ℎ)
280	255, 254, 245, 253, 278, 279	le2subd 11866	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ≤ (𝑀 − 0))
281	280, 263	breqtrd 5175	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑥 − ℎ) ≤ 𝑀)
282	247, 245	absled 15413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ)) ≤ 𝑀 ↔ (-𝑀 ≤ (𝑥 − ℎ) ∧ (𝑥 − ℎ) ≤ 𝑀)))
283	266, 281, 282	mpbir2and 711	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (abs‘(𝑥 − ℎ)) ≤ 𝑀)
284		leexp1a 14175	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((abs‘(𝑥 − ℎ)) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℕ₀) ∧ (0 ≤ (abs‘(𝑥 − ℎ)) ∧ (abs‘(𝑥 − ℎ)) ≤ 𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
285	239, 245, 231, 242, 283, 284	syl32anc 1375	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)))
286	46	nnge1d 12293	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ≤ 𝑀)
287	286	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 1 ≤ 𝑀)
288	219	nn0zd 12617	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℤ)
289	77	nn0zd 12617	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑃 ∈ ℤ)
290		iftrue 4536	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ = 0 → if(ℎ = 0, (𝑃 − 1), 𝑃) = (𝑃 − 1))
291	290	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) = (𝑃 − 1))
292	30	nnred 12260	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑃 ∈ ℝ)
293	292	lem1d 12180	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑃 − 1) ≤ 𝑃)
294	293	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ℎ = 0) → (𝑃 − 1) ≤ 𝑃)
295	291, 294	eqbrtrd 5171	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃)
296		iffalse 4539	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ ℎ = 0 → if(ℎ = 0, (𝑃 − 1), 𝑃) = 𝑃)
297	296	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ¬ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) = 𝑃)
298	292	leidd 11812	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑃 ≤ 𝑃)
299	298	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ¬ ℎ = 0) → 𝑃 ≤ 𝑃)
300	297, 299	eqbrtrd 5171	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ¬ ℎ = 0) → if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃)
301	295, 300	pm2.61dan 811	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃)
302		eluz2 12861	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ (ℤ_≥‘if(ℎ = 0, (𝑃 − 1), 𝑃)) ↔ (if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ if(ℎ = 0, (𝑃 − 1), 𝑃) ≤ 𝑃))
303	288, 289, 301, 302	syl3anbrc 1340	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑃 ∈ (ℤ_≥‘if(ℎ = 0, (𝑃 − 1), 𝑃)))
304	303	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → 𝑃 ∈ (ℤ_≥‘if(ℎ = 0, (𝑃 − 1), 𝑃)))
305	245, 287, 304	leexp2ad 14252	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → (𝑀↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑𝑃))
306	240, 246, 244, 285, 305	letrd 11403	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) ∧ ℎ ∈ (0...𝑀)) → ((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ (𝑀↑𝑃))
307	235, 236, 240, 243, 244, 306	fprodle 15976	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ∏ℎ ∈ (0...𝑀)((abs‘(𝑥 − ℎ))↑if(ℎ = 0, (𝑃 − 1), 𝑃)) ≤ ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃))
308	78	recnd 11274	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑀↑𝑃) ∈ ℂ)
309		fprodconst 15958	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((0...𝑀) ∈ Fin ∧ (𝑀↑𝑃) ∈ ℂ) → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(♯‘(0...𝑀))))
310	7, 308, 309	syl2anc 582	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(♯‘(0...𝑀))))
311		hashfz0 14427	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ ℕ₀ → (♯‘(0...𝑀)) = (𝑀 + 1))
312	47, 311	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (♯‘(0...𝑀)) = (𝑀 + 1))
313	312	oveq2d 7435	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑀↑𝑃)↑(♯‘(0...𝑀))) = ((𝑀↑𝑃)↑(𝑀 + 1)))
314	310, 313	eqtrd 2765	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∏ℎ ∈ (0...𝑀)(𝑀↑𝑃) = ((𝑀↑𝑃)↑(𝑀 + 1)))
315	314	ad2antrr 724	. . . . . . . . . . . . . . . . 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 12189	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((abs‘(e↑_𝑐-𝑥)) · (abs‘(𝐹‘𝑥))) ≤ (1 · ((𝑀↑𝑃)↑(𝑀 + 1))))
319	82	mullidd 11264	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · ((𝑀↑𝑃)↑(𝑀 + 1))) = ((𝑀↑𝑃)↑(𝑀 + 1)))
320	319	ad2antrr 724	. . . . . . . . . . . . . 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 25783	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)(abs‘((e↑_𝑐-𝑥) · (𝐹‘𝑥))) d𝑥 ≤ ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥)
324	153, 157, 149, 158, 323	letrd 11403	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (abs‘∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥) ≤ ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥)
325	153, 149, 109, 154, 324	lemul2ad 12187	. . . . . . . . 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 15781	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥))
328		itgconst 25792	. . . . . . . . . . 11 ⊢ (((0(,)𝑗) ∈ dom vol ∧ (vol‘(0(,)𝑗)) ∈ ℝ ∧ ((𝑀↑𝑃)↑(𝑀 + 1)) ∈ ℂ) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 = (((𝑀↑𝑃)↑(𝑀 + 1)) · (vol‘(0(,)𝑗))))
329	138, 145, 146, 328	syl3anc 1368	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 = (((𝑀↑𝑃)↑(𝑀 + 1)) · (vol‘(0(,)𝑗))))
330	47	nn0ge0d 12568	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ≤ 𝑀)
331	76, 77, 330	expge0d 14164	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ≤ (𝑀↑𝑃))
332	78, 80, 331	expge0d 14164	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
333	332	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → 0 ≤ ((𝑀↑𝑃)↑(𝑀 + 1)))
334	18	subid1d 11592	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (0...𝑀) → (𝑗 − 0) = 𝑗)
335	142, 334	eqtrd 2765	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) = 𝑗)
336	335, 273	eqbrtrd 5171	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...𝑀) → (vol‘(0(,)𝑗)) ≤ 𝑀)
337	336	adantl 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (vol‘(0(,)𝑗)) ≤ 𝑀)
338	145, 124, 123, 333, 337	lemul2ad 12187	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → (((𝑀↑𝑃)↑(𝑀 + 1)) · (vol‘(0(,)𝑗))) ≤ (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀))
339	329, 338	eqbrtrd 5171	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥 ≤ (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀))
340	149, 125, 109, 154, 339	lemul2ad 12187	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑀)) → ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ≤ ((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)))
341	7, 150, 126, 340	fsumle 15781	. . . . . . 7 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · ∫(0(,)𝑗)((𝑀↑𝑃)↑(𝑀 + 1)) d𝑥) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)))
342	134, 151, 127, 327, 341	letrd 11403	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (0...𝑀)(abs‘(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)))
343	131, 134, 127, 135, 342	letrd 11403	. . . . 5 ⊢ (𝜑 → (abs‘Σ𝑗 ∈ (0...𝑀)(((𝐴‘𝑗) · (e↑_𝑐𝑗)) · ∫(0(,)𝑗)((e↑_𝑐-𝑥) · (𝐹‘𝑥)) d𝑥)) ≤ Σ𝑗 ∈ (0...𝑀)((abs‘((𝐴‘𝑗) · (e↑_𝑐𝑗))) · (((𝑀↑𝑃)↑(𝑀 + 1)) · 𝑀)))
344	131, 127, 132, 343	lediv1dd 13109	. . . 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 11404	. 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 394 = wceq 1533 ∈ wcel 2098 ⊆ wss 3944 ifcif 4530 {cpr 4632 class class class wbr 5149 ↦ cmpt 5232 dom cdm 5678 ran crn 5679 ⟶wf 6545 ‘cfv 6549 (class class class)co 7419 Fincfn 8964 ℂcc 11138 ℝcr 11139 0cc0 11140 1c1 11141 + caddc 11143 · cmul 11145 ℝ^*cxr 11279 < clt 11280 ≤ cle 11281 − cmin 11476 -cneg 11477 / cdiv 11903 ℕcn 12245 2c2 12300 3c3 12301 ℕ₀cn0 12505 ℤcz 12591 ℤ_≥cuz 12855 (,)cioo 13359 ...cfz 13519 ↑cexp 14062 !cfa 14268 ♯chash 14325 abscabs 15217 Σcsu 15668 ∏cprod 15885 eceu 16042 ↾_t crest 17405 TopOpenctopn 17406 topGenctg 17422 ℂ_fldccnfld 21296 volcvol 25436 𝐿¹cibl 25590 ∫citg 25591 ↑_𝑐ccxp 26534

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5365 ax-pr 5429 ax-un 7741 ax-inf2 9666 ax-cc 10460 ax-cnex 11196 ax-resscn 11197 ax-1cn 11198 ax-icn 11199 ax-addcl 11200 ax-addrcl 11201 ax-mulcl 11202 ax-mulrcl 11203 ax-mulcom 11204 ax-addass 11205 ax-mulass 11206 ax-distr 11207 ax-i2m1 11208 ax-1ne0 11209 ax-1rid 11210 ax-rnegex 11211 ax-rrecex 11212 ax-cnre 11213 ax-pre-lttri 11214 ax-pre-lttrn 11215 ax-pre-ltadd 11216 ax-pre-mulgt0 11217 ax-pre-sup 11218 ax-addf 11219

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2930 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3419 df-v 3463 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3964 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-tp 4635 df-op 4637 df-uni 4910 df-int 4951 df-iun 4999 df-iin 5000 df-disj 5115 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5633 df-se 5634 df-we 5635 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-pred 6307 df-ord 6374 df-on 6375 df-lim 6376 df-suc 6377 df-iota 6501 df-fun 6551 df-fn 6552 df-f 6553 df-f1 6554 df-fo 6555 df-f1o 6556 df-fv 6557 df-isom 6558 df-riota 7375 df-ov 7422 df-oprab 7423 df-mpo 7424 df-of 7685 df-ofr 7686 df-om 7872 df-1st 7994 df-2nd 7995 df-supp 8166 df-frecs 8287 df-wrecs 8318 df-recs 8392 df-rdg 8431 df-1o 8487 df-2o 8488 df-oadd 8491 df-omul 8492 df-er 8725 df-map 8847 df-pm 8848 df-ixp 8917 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-fsupp 9388 df-fi 9436 df-sup 9467 df-inf 9468 df-oi 9535 df-dju 9926 df-card 9964 df-acn 9967 df-pnf 11282 df-mnf 11283 df-xr 11284 df-ltxr 11285 df-le 11286 df-sub 11478 df-neg 11479 df-div 11904 df-nn 12246 df-2 12308 df-3 12309 df-4 12310 df-5 12311 df-6 12312 df-7 12313 df-8 12314 df-9 12315 df-n0 12506 df-z 12592 df-dec 12711 df-uz 12856 df-q 12966 df-rp 13010 df-xneg 13127 df-xadd 13128 df-xmul 13129 df-ioo 13363 df-ioc 13364 df-ico 13365 df-icc 13366 df-fz 13520 df-fzo 13663 df-fl 13793 df-mod 13871 df-seq 14003 df-exp 14063 df-fac 14269 df-bc 14298 df-hash 14326 df-shft 15050 df-cj 15082 df-re 15083 df-im 15084 df-sqrt 15218 df-abs 15219 df-limsup 15451 df-clim 15468 df-rlim 15469 df-sum 15669 df-prod 15886 df-ef 16047 df-e 16048 df-sin 16049 df-cos 16050 df-tan 16051 df-pi 16052 df-struct 17119 df-sets 17136 df-slot 17154 df-ndx 17166 df-base 17184 df-ress 17213 df-plusg 17249 df-mulr 17250 df-starv 17251 df-sca 17252 df-vsca 17253 df-ip 17254 df-tset 17255 df-ple 17256 df-ds 17258 df-unif 17259 df-hom 17260 df-cco 17261 df-rest 17407 df-topn 17408 df-0g 17426 df-gsum 17427 df-topgen 17428 df-pt 17429 df-prds 17432 df-xrs 17487 df-qtop 17492 df-imas 17493 df-xps 17495 df-mre 17569 df-mrc 17570 df-acs 17572 df-mgm 18603 df-sgrp 18682 df-mnd 18698 df-submnd 18744 df-mulg 19032 df-cntz 19280 df-cmn 19749 df-psmet 21288 df-xmet 21289 df-met 21290 df-bl 21291 df-mopn 21292 df-fbas 21293 df-fg 21294 df-cnfld 21297 df-top 22840 df-topon 22857 df-topsp 22879 df-bases 22893 df-cld 22967 df-ntr 22968 df-cls 22969 df-nei 23046 df-lp 23084 df-perf 23085 df-cn 23175 df-cnp 23176 df-haus 23263 df-cmp 23335 df-tx 23510 df-hmeo 23703 df-fil 23794 df-fm 23886 df-flim 23887 df-flf 23888 df-xms 24270 df-ms 24271 df-tms 24272 df-cncf 24842 df-ovol 25437 df-vol 25438 df-mbf 25592 df-itg1 25593 df-itg2 25594 df-ibl 25595 df-itg 25596 df-0p 25643 df-limc 25839 df-dv 25840 df-log 26535 df-cxp 26536

This theorem is referenced by: etransclem47 45807

W3C validator