etransclem23

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)

	Ref	Expression
Hypotheses	etransclem23.a	$⊢ φ \to A : ℕ_{0} ⟶ ℤ$
	etransclem23.l	$⊢ L = \sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x$
	etransclem23.k	$⊢ K = \frac{L}{(P - 1)!}$
	etransclem23.p	$⊢ φ \to P \in ℕ$
	etransclem23.m	$⊢ φ \to M \in ℕ$
	etransclem23.f	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
	etransclem23.lt1	$⊢ φ \to \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} (\frac{{(M^{M + 1})}^{P - 1}}{(P - 1)!}) < 1$
Assertion	etransclem23	$⊢ φ \to \|K\| < 1$

Proof

Step	Hyp	Ref	Expression
1		etransclem23.a	$⊢ φ \to A : ℕ_{0} ⟶ ℤ$
2		etransclem23.l	$⊢ L = \sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x$
3		etransclem23.k	$⊢ K = \frac{L}{(P - 1)!}$
4		etransclem23.p	$⊢ φ \to P \in ℕ$
5		etransclem23.m	$⊢ φ \to M \in ℕ$
6		etransclem23.f	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
7		etransclem23.lt1	$⊢ φ \to \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} (\frac{{(M^{M + 1})}^{P - 1}}{(P - 1)!}) < 1$
8	2	oveq1i	$⊢ \frac{L}{(P - 1)!} = \frac{\sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x}{(P - 1)!}$
9	3 8	eqtri	$⊢ K = \frac{\sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x}{(P - 1)!}$
10	9	fveq2i	$⊢ \|K\| = \|\frac{\sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x}{(P - 1)!}\|$
11	10	a1i	$⊢ φ \to \|K\| = \|\frac{\sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x}{(P - 1)!}\|$
12		fzfid	$⊢ φ \to (0 \dots M) \in Fin$
13	1	adantr	$⊢ (φ \land j \in (0 \dots M)) \to A : ℕ_{0} ⟶ ℤ$
14		elfznn0	$⊢ j \in (0 \dots M) \to j \in ℕ_{0}$
15	14	adantl	$⊢ (φ \land j \in (0 \dots M)) \to j \in ℕ_{0}$
16	13 15	ffvelcdmd	$⊢ (φ \land j \in (0 \dots M)) \to A (j) \in ℤ$
17	16	zcnd	$⊢ (φ \land j \in (0 \dots M)) \to A (j) \in ℂ$
18		ere	$⊢ e \in ℝ$
19	18	recni	$⊢ e \in ℂ$
20	19	a1i	$⊢ (φ \land j \in (0 \dots M)) \to e \in ℂ$
21		elfzelz	$⊢ j \in (0 \dots M) \to j \in ℤ$
22	21	zcnd	$⊢ j \in (0 \dots M) \to j \in ℂ$
23	22	adantl	$⊢ (φ \land j \in (0 \dots M)) \to j \in ℂ$
24	20 23	cxpcld	$⊢ (φ \land j \in (0 \dots M)) \to e^{j} \in ℂ$
25	17 24	mulcld	$⊢ (φ \land j \in (0 \dots M)) \to A (j) e^{j} \in ℂ$
26	19	a1i	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to e \in ℂ$
27		elioore	$⊢ x \in (0, j) \to x \in ℝ$
28	27	recnd	$⊢ x \in (0, j) \to x \in ℂ$
29	28	adantl	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to x \in ℂ$
30	29	negcld	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to - x \in ℂ$
31	26 30	cxpcld	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to e^{- x} \in ℂ$
32		ax-resscn	$⊢ ℝ \subseteq ℂ$
33	32	a1i	$⊢ φ \to ℝ \subseteq ℂ$
34	33 4 6	etransclem8	$⊢ φ \to F : ℝ ⟶ ℂ$
35	34	adantr	$⊢ (φ \land x \in (0, j)) \to F : ℝ ⟶ ℂ$
36	27	adantl	$⊢ (φ \land x \in (0, j)) \to x \in ℝ$
37	35 36	ffvelcdmd	$⊢ (φ \land x \in (0, j)) \to F (x) \in ℂ$
38	37	adantlr	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to F (x) \in ℂ$
39	31 38	mulcld	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to e^{- x} F (x) \in ℂ$
40		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
41	40	a1i	$⊢ (φ \land j \in (0 \dots M)) \to ℝ \in \{ℝ, ℂ\}$
42		reopn	$⊢ ℝ \in topGen (ran (.))$
43		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
44	42 43	eleqtri	$⊢ ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
45	44	a1i	$⊢ (φ \land j \in (0 \dots M)) \to ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
46	4	adantr	$⊢ (φ \land j \in (0 \dots M)) \to P \in ℕ$
47	5	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
48	47	adantr	$⊢ (φ \land j \in (0 \dots M)) \to M \in ℕ_{0}$
49		etransclem6	$⊢ (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P}) = (y \in ℝ ⟼ y^{P - 1} \prod_{h = 1}^{M} {(y - h)}^{P})$
50		etransclem6	$⊢ (y \in ℝ ⟼ y^{P - 1} \prod_{h = 1}^{M} {(y - h)}^{P}) = (x \in ℝ ⟼ x^{P - 1} \prod_{k = 1}^{M} {(x - k)}^{P})$
51	6 49 50	3eqtri	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{k = 1}^{M} {(x - k)}^{P})$
52		0red	$⊢ (φ \land j \in (0 \dots M)) \to 0 \in ℝ$
53	21	zred	$⊢ j \in (0 \dots M) \to j \in ℝ$
54	53	adantl	$⊢ (φ \land j \in (0 \dots M)) \to j \in ℝ$
55	41 45 46 48 51 52 54	etransclem18	$⊢ (φ \land j \in (0 \dots M)) \to (x \in (0, j) ⟼ e^{- x} F (x)) \in 𝐿^{1}$
56	39 55	itgcl	$⊢ (φ \land j \in (0 \dots M)) \to \int_{(0, j)} e^{- x} F (x) d x \in ℂ$
57	25 56	mulcld	$⊢ (φ \land j \in (0 \dots M)) \to A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x \in ℂ$
58	12 57	fsumcl	$⊢ φ \to \sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x \in ℂ$
59		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
60	4 59	syl	$⊢ φ \to P - 1 \in ℕ_{0}$
61	60	faccld	$⊢ φ \to (P - 1)! \in ℕ$
62	61	nncnd	$⊢ φ \to (P - 1)! \in ℂ$
63	61	nnne0d	$⊢ φ \to (P - 1)! \neq 0$
64	58 62 63	absdivd	$⊢ φ \to \|\frac{\sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x}{(P - 1)!}\| = \frac{\|\sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x\|}{\|(P - 1)!\|}$
65	61	nnred	$⊢ φ \to (P - 1)! \in ℝ$
66	61	nnnn0d	$⊢ φ \to (P - 1)! \in ℕ_{0}$
67	66	nn0ge0d	$⊢ φ \to 0 \leq (P - 1)!$
68	65 67	absidd	$⊢ φ \to \|(P - 1)!\| = (P - 1)!$
69	68	oveq2d	$⊢ φ \to \frac{\|\sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x\|}{\|(P - 1)!\|} = \frac{\|\sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x\|}{(P - 1)!}$
70	11 64 69	3eqtrd	$⊢ φ \to \|K\| = \frac{\|\sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x\|}{(P - 1)!}$
71	2 58	eqeltrid	$⊢ φ \to L \in ℂ$
72	71 62 63	divcld	$⊢ φ \to \frac{L}{(P - 1)!} \in ℂ$
73	3 72	eqeltrid	$⊢ φ \to K \in ℂ$
74	73	abscld	$⊢ φ \to \|K\| \in ℝ$
75	70 74	eqeltrrd	$⊢ φ \to \frac{\|\sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x\|}{(P - 1)!} \in ℝ$
76	5	nnred	$⊢ φ \to M \in ℝ$
77	4	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
78	76 77	reexpcld	$⊢ φ \to M^{P} \in ℝ$
79		peano2nn0	$⊢ M \in ℕ_{0} \to M + 1 \in ℕ_{0}$
80	47 79	syl	$⊢ φ \to M + 1 \in ℕ_{0}$
81	78 80	reexpcld	$⊢ φ \to {(M^{P})}^{M + 1} \in ℝ$
82	81	recnd	$⊢ φ \to {(M^{P})}^{M + 1} \in ℂ$
83	5	nncnd	$⊢ φ \to M \in ℂ$
84	82 83	mulcomd	$⊢ φ \to {(M^{P})}^{M + 1} \cdot M = M {(M^{P})}^{M + 1}$
85	4	nncnd	$⊢ φ \to P \in ℂ$
86		1cnd	$⊢ φ \to 1 \in ℂ$
87	85 86	npcand	$⊢ φ \to P - 1 + 1 = P$
88	87	eqcomd	$⊢ φ \to P = P - 1 + 1$
89	88	oveq2d	$⊢ φ \to {(M^{M + 1})}^{P} = {(M^{M + 1})}^{P - 1 + 1}$
90	80	nn0cnd	$⊢ φ \to M + 1 \in ℂ$
91	90 85	mulcomd	$⊢ φ \to (M + 1) P = P (M + 1)$
92	91	oveq2d	$⊢ φ \to M^{(M + 1) P} = M^{P (M + 1)}$
93	83 77 80	expmuld	$⊢ φ \to M^{(M + 1) P} = {(M^{M + 1})}^{P}$
94	83 80 77	expmuld	$⊢ φ \to M^{P (M + 1)} = {(M^{P})}^{M + 1}$
95	92 93 94	3eqtr3d	$⊢ φ \to {(M^{M + 1})}^{P} = {(M^{P})}^{M + 1}$
96	76 80	reexpcld	$⊢ φ \to M^{M + 1} \in ℝ$
97	96	recnd	$⊢ φ \to M^{M + 1} \in ℂ$
98	97 60	expp1d	$⊢ φ \to {(M^{M + 1})}^{P - 1 + 1} = {(M^{M + 1})}^{P - 1} M^{M + 1}$
99	89 95 98	3eqtr3d	$⊢ φ \to {(M^{P})}^{M + 1} = {(M^{M + 1})}^{P - 1} M^{M + 1}$
100	99	oveq2d	$⊢ φ \to M {(M^{P})}^{M + 1} = M {(M^{M + 1})}^{P - 1} M^{M + 1}$
101	97 60	expcld	$⊢ φ \to {(M^{M + 1})}^{P - 1} \in ℂ$
102	83 101 97	mul12d	$⊢ φ \to M {(M^{M + 1})}^{P - 1} M^{M + 1} = {(M^{M + 1})}^{P - 1} M M^{M + 1}$
103	83 97	mulcld	$⊢ φ \to M M^{M + 1} \in ℂ$
104	101 103	mulcomd	$⊢ φ \to {(M^{M + 1})}^{P - 1} M M^{M + 1} = M M^{M + 1} {(M^{M + 1})}^{P - 1}$
105	102 104	eqtrd	$⊢ φ \to M {(M^{M + 1})}^{P - 1} M^{M + 1} = M M^{M + 1} {(M^{M + 1})}^{P - 1}$
106	84 100 105	3eqtrd	$⊢ φ \to {(M^{P})}^{M + 1} \cdot M = M M^{M + 1} {(M^{M + 1})}^{P - 1}$
107	106	adantr	$⊢ (φ \land j \in (0 \dots M)) \to {(M^{P})}^{M + 1} \cdot M = M M^{M + 1} {(M^{M + 1})}^{P - 1}$
108	107	oveq2d	$⊢ (φ \land j \in (0 \dots M)) \to \|A (j) e^{j}\| {(M^{P})}^{M + 1} \cdot M = \|A (j) e^{j}\| M M^{M + 1} {(M^{M + 1})}^{P - 1}$
109	25	abscld	$⊢ (φ \land j \in (0 \dots M)) \to \|A (j) e^{j}\| \in ℝ$
110	109	recnd	$⊢ (φ \land j \in (0 \dots M)) \to \|A (j) e^{j}\| \in ℂ$
111	103	adantr	$⊢ (φ \land j \in (0 \dots M)) \to M M^{M + 1} \in ℂ$
112	101	adantr	$⊢ (φ \land j \in (0 \dots M)) \to {(M^{M + 1})}^{P - 1} \in ℂ$
113	110 111 112	mulassd	$⊢ (φ \land j \in (0 \dots M)) \to \|A (j) e^{j}\| M M^{M + 1} {(M^{M + 1})}^{P - 1} = \|A (j) e^{j}\| M M^{M + 1} {(M^{M + 1})}^{P - 1}$
114	108 113	eqtr4d	$⊢ (φ \land j \in (0 \dots M)) \to \|A (j) e^{j}\| {(M^{P})}^{M + 1} \cdot M = \|A (j) e^{j}\| M M^{M + 1} {(M^{M + 1})}^{P - 1}$
115	114	sumeq2dv	$⊢ φ \to \sum_{j = 0}^{M} \|A (j) e^{j}\| {(M^{P})}^{M + 1} \cdot M = \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} {(M^{M + 1})}^{P - 1}$
116	110 111	mulcld	$⊢ (φ \land j \in (0 \dots M)) \to \|A (j) e^{j}\| M M^{M + 1} \in ℂ$
117	12 101 116	fsummulc1	$⊢ φ \to \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} {(M^{M + 1})}^{P - 1} = \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} {(M^{M + 1})}^{P - 1}$
118	115 117	eqtr4d	$⊢ φ \to \sum_{j = 0}^{M} \|A (j) e^{j}\| {(M^{P})}^{M + 1} \cdot M = \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} {(M^{M + 1})}^{P - 1}$
119	118	oveq1d	$⊢ φ \to \frac{\sum_{j = 0}^{M} \|A (j) e^{j}\| {(M^{P})}^{M + 1} \cdot M}{(P - 1)!} = \frac{\sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} {(M^{M + 1})}^{P - 1}}{(P - 1)!}$
120	12 116	fsumcl	$⊢ φ \to \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} \in ℂ$
121	120 101 62 63	divassd	$⊢ φ \to \frac{\sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} {(M^{M + 1})}^{P - 1}}{(P - 1)!} = \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} (\frac{{(M^{M + 1})}^{P - 1}}{(P - 1)!})$
122	119 121	eqtrd	$⊢ φ \to \frac{\sum_{j = 0}^{M} \|A (j) e^{j}\| {(M^{P})}^{M + 1} \cdot M}{(P - 1)!} = \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} (\frac{{(M^{M + 1})}^{P - 1}}{(P - 1)!})$
123	81	adantr	$⊢ (φ \land j \in (0 \dots M)) \to {(M^{P})}^{M + 1} \in ℝ$
124	76	adantr	$⊢ (φ \land j \in (0 \dots M)) \to M \in ℝ$
125	123 124	remulcld	$⊢ (φ \land j \in (0 \dots M)) \to {(M^{P})}^{M + 1} \cdot M \in ℝ$
126	109 125	remulcld	$⊢ (φ \land j \in (0 \dots M)) \to \|A (j) e^{j}\| {(M^{P})}^{M + 1} \cdot M \in ℝ$
127	12 126	fsumrecl	$⊢ φ \to \sum_{j = 0}^{M} \|A (j) e^{j}\| {(M^{P})}^{M + 1} \cdot M \in ℝ$
128	127 61	nndivred	$⊢ φ \to \frac{\sum_{j = 0}^{M} \|A (j) e^{j}\| {(M^{P})}^{M + 1} \cdot M}{(P - 1)!} \in ℝ$
129	122 128	eqeltrrd	$⊢ φ \to \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} (\frac{{(M^{M + 1})}^{P - 1}}{(P - 1)!}) \in ℝ$
130		1red	$⊢ φ \to 1 \in ℝ$
131	58	abscld	$⊢ φ \to \|\sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x\| \in ℝ$
132	61	nnrpd	$⊢ φ \to (P - 1)! \in ℝ^{+}$
133	57	abscld	$⊢ (φ \land j \in (0 \dots M)) \to \|A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x\| \in ℝ$
134	12 133	fsumrecl	$⊢ φ \to \sum_{j = 0}^{M} \|A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x\| \in ℝ$
135	12 57	fsumabs	$⊢ φ \to \|\sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x\| \leq \sum_{j = 0}^{M} \|A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x\|$
136	81	ad2antrr	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to {(M^{P})}^{M + 1} \in ℝ$
137		ioombl	$⊢ (0, j) \in dom vol$
138	137	a1i	$⊢ (φ \land j \in (0 \dots M)) \to (0, j) \in dom vol$
139		0red	$⊢ j \in (0 \dots M) \to 0 \in ℝ$
140		elfzle1	$⊢ j \in (0 \dots M) \to 0 \leq j$
141		volioo	$⊢ (0 \in ℝ \land j \in ℝ \land 0 \leq j) \to vol ((0, j)) = j - 0$
142	139 53 140 141	syl3anc	$⊢ j \in (0 \dots M) \to vol ((0, j)) = j - 0$
143	53 139	resubcld	$⊢ j \in (0 \dots M) \to j - 0 \in ℝ$
144	142 143	eqeltrd	$⊢ j \in (0 \dots M) \to vol ((0, j)) \in ℝ$
145	144	adantl	$⊢ (φ \land j \in (0 \dots M)) \to vol ((0, j)) \in ℝ$
146	82	adantr	$⊢ (φ \land j \in (0 \dots M)) \to {(M^{P})}^{M + 1} \in ℂ$
147		iblconstmpt	$⊢ ((0, j) \in dom vol \land vol ((0, j)) \in ℝ \land {(M^{P})}^{M + 1} \in ℂ) \to (x \in (0, j) ⟼ {(M^{P})}^{M + 1}) \in 𝐿^{1}$
148	138 145 146 147	syl3anc	$⊢ (φ \land j \in (0 \dots M)) \to (x \in (0, j) ⟼ {(M^{P})}^{M + 1}) \in 𝐿^{1}$
149	136 148	itgrecl	$⊢ (φ \land j \in (0 \dots M)) \to \int_{(0, j)} {(M^{P})}^{M + 1} d x \in ℝ$
150	109 149	remulcld	$⊢ (φ \land j \in (0 \dots M)) \to \|A (j) e^{j}\| \int_{(0, j)} {(M^{P})}^{M + 1} d x \in ℝ$
151	12 150	fsumrecl	$⊢ φ \to \sum_{j = 0}^{M} \|A (j) e^{j}\| \int_{(0, j)} {(M^{P})}^{M + 1} d x \in ℝ$
152	25 56	absmuld	$⊢ (φ \land j \in (0 \dots M)) \to \|A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x\| = \|A (j) e^{j}\| \|\int_{(0, j)} e^{- x} F (x) d x\|$
153	56	abscld	$⊢ (φ \land j \in (0 \dots M)) \to \|\int_{(0, j)} e^{- x} F (x) d x\| \in ℝ$
154	25	absge0d	$⊢ (φ \land j \in (0 \dots M)) \to 0 \leq \|A (j) e^{j}\|$
155	39	abscld	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to \|e^{- x} F (x)\| \in ℝ$
156	39 55	iblabs	$⊢ (φ \land j \in (0 \dots M)) \to (x \in (0, j) ⟼ \|e^{- x} F (x)\|) \in 𝐿^{1}$
157	155 156	itgrecl	$⊢ (φ \land j \in (0 \dots M)) \to \int_{(0, j)} \|e^{- x} F (x)\| d x \in ℝ$
158	39 55	itgabs	$⊢ (φ \land j \in (0 \dots M)) \to \|\int_{(0, j)} e^{- x} F (x) d x\| \leq \int_{(0, j)} \|e^{- x} F (x)\| d x$
159	31 38	absmuld	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to \|e^{- x} F (x)\| = \|e^{- x}\| \|F (x)\|$
160	31	abscld	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to \|e^{- x}\| \in ℝ$
161		1red	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to 1 \in ℝ$
162	38	abscld	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to \|F (x)\| \in ℝ$
163	31	absge0d	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to 0 \leq \|e^{- x}\|$
164	38	absge0d	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to 0 \leq \|F (x)\|$
165	18	a1i	$⊢ x \in (0, j) \to e \in ℝ$
166		0re	$⊢ 0 \in ℝ$
167		epos	$⊢ 0 < e$
168	166 18 167	ltleii	$⊢ 0 \leq e$
169	168	a1i	$⊢ x \in (0, j) \to 0 \leq e$
170	27	renegcld	$⊢ x \in (0, j) \to - x \in ℝ$
171	165 169 170	recxpcld	$⊢ x \in (0, j) \to e^{- x} \in ℝ$
172	165 169 170	cxpge0d	$⊢ x \in (0, j) \to 0 \leq e^{- x}$
173	171 172	absidd	$⊢ x \in (0, j) \to \|e^{- x}\| = e^{- x}$
174	173	adantl	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to \|e^{- x}\| = e^{- x}$
175	171	adantl	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to e^{- x} \in ℝ$
176		1red	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to 1 \in ℝ$
177		0xr	$⊢ 0 \in ℝ^{*}$
178	177	a1i	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to 0 \in ℝ^{*}$
179	53	rexrd	$⊢ j \in (0 \dots M) \to j \in ℝ^{*}$
180	179	adantr	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to j \in ℝ^{*}$
181		simpr	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to x \in (0, j)$
182		ioogtlb	$⊢ (0 \in ℝ^{} \land j \in ℝ^{} \land x \in (0, j)) \to 0 < x$
183	178 180 181 182	syl3anc	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to 0 < x$
184	27	adantl	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to x \in ℝ$
185	184	lt0neg2d	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to (0 < x \leftrightarrow - x < 0)$
186	183 185	mpbid	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to - x < 0$
187	18	a1i	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to e \in ℝ$
188		1lt2	$⊢ 1 < 2$
189		egt2lt3	$⊢ (2 < e \land e < 3)$
190	189	simpli	$⊢ 2 < e$
191		1re	$⊢ 1 \in ℝ$
192		2re	$⊢ 2 \in ℝ$
193	191 192 18	lttri	$⊢ (1 < 2 \land 2 < e) \to 1 < e$
194	188 190 193	mp2an	$⊢ 1 < e$
195	194	a1i	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to 1 < e$
196	170	adantl	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to - x \in ℝ$
197		0red	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to 0 \in ℝ$
198	187 195 196 197	cxpltd	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to (- x < 0 \leftrightarrow e^{- x} < e^{0})$
199	186 198	mpbid	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to e^{- x} < e^{0}$
200		cxp0	$⊢ e \in ℂ \to e^{0} = 1$
201	19 200	mp1i	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to e^{0} = 1$
202	199 201	breqtrd	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to e^{- x} < 1$
203	175 176 202	ltled	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to e^{- x} \leq 1$
204	174 203	eqbrtrd	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to \|e^{- x}\| \leq 1$
205	204	adantll	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to \|e^{- x}\| \leq 1$
206	32	a1i	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to ℝ \subseteq ℂ$
207	4	ad2antrr	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to P \in ℕ$
208	47	ad2antrr	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to M \in ℕ_{0}$
209	6 49	eqtri	$⊢ F = (y \in ℝ ⟼ y^{P - 1} \prod_{h = 1}^{M} {(y - h)}^{P})$
210	27	adantl	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to x \in ℝ$
211	206 207 208 209 210	etransclem13	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to F (x) = \prod_{h = 0}^{M} {(x - h)}^{if (h = 0, P - 1, P)}$
212	211	fveq2d	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to \|F (x)\| = \|\prod_{h = 0}^{M} {(x - h)}^{if (h = 0, P - 1, P)}\|$
213		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
214	27	adantr	$⊢ (x \in (0, j) \land h \in ℕ_{0}) \to x \in ℝ$
215		nn0re	$⊢ h \in ℕ_{0} \to h \in ℝ$
216	215	adantl	$⊢ (x \in (0, j) \land h \in ℕ_{0}) \to h \in ℝ$
217	214 216	resubcld	$⊢ (x \in (0, j) \land h \in ℕ_{0}) \to x - h \in ℝ$
218	217	adantll	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in ℕ_{0}) \to x - h \in ℝ$
219	60 77	ifcld	$⊢ φ \to if (h = 0, P - 1, P) \in ℕ_{0}$
220	219	ad3antrrr	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in ℕ_{0}) \to if (h = 0, P - 1, P) \in ℕ_{0}$
221	218 220	reexpcld	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in ℕ_{0}) \to {(x - h)}^{if (h = 0, P - 1, P)} \in ℝ$
222	221	recnd	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in ℕ_{0}) \to {(x - h)}^{if (h = 0, P - 1, P)} \in ℂ$
223	213 208 222	fprodabs	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to \|\prod_{h = 0}^{M} {(x - h)}^{if (h = 0, P - 1, P)}\| = \prod_{h = 0}^{M} \|{(x - h)}^{if (h = 0, P - 1, P)}\|$
224		elfznn0	$⊢ h \in (0 \dots M) \to h \in ℕ_{0}$
225	28	adantr	$⊢ (x \in (0, j) \land h \in ℕ_{0}) \to x \in ℂ$
226		nn0cn	$⊢ h \in ℕ_{0} \to h \in ℂ$
227	226	adantl	$⊢ (x \in (0, j) \land h \in ℕ_{0}) \to h \in ℂ$
228	225 227	subcld	$⊢ (x \in (0, j) \land h \in ℕ_{0}) \to x - h \in ℂ$
229	228	adantll	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in ℕ_{0}) \to x - h \in ℂ$
230	224 229	sylan2	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to x - h \in ℂ$
231	219	ad3antrrr	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to if (h = 0, P - 1, P) \in ℕ_{0}$
232	230 231	absexpd	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to \|{(x - h)}^{if (h = 0, P - 1, P)}\| = {\|x - h\|}^{if (h = 0, P - 1, P)}$
233	232	prodeq2dv	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to \prod_{h = 0}^{M} \|{(x - h)}^{if (h = 0, P - 1, P)}\| = \prod_{h = 0}^{M} {\|x - h\|}^{if (h = 0, P - 1, P)}$
234	212 223 233	3eqtrd	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to \|F (x)\| = \prod_{h = 0}^{M} {\|x - h\|}^{if (h = 0, P - 1, P)}$
235		nfv	$⊢ Ⅎ h ((φ \land j \in (0 \dots M)) \land x \in (0, j))$
236		fzfid	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to (0 \dots M) \in Fin$
237	224 228	sylan2	$⊢ (x \in (0, j) \land h \in (0 \dots M)) \to x - h \in ℂ$
238	237	abscld	$⊢ (x \in (0, j) \land h \in (0 \dots M)) \to \|x - h\| \in ℝ$
239	238	adantll	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to \|x - h\| \in ℝ$
240	239 231	reexpcld	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to {\|x - h\|}^{if (h = 0, P - 1, P)} \in ℝ$
241	237	absge0d	$⊢ (x \in (0, j) \land h \in (0 \dots M)) \to 0 \leq \|x - h\|$
242	241	adantll	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to 0 \leq \|x - h\|$
243	239 231 242	expge0d	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to 0 \leq {\|x - h\|}^{if (h = 0, P - 1, P)}$
244	78	ad3antrrr	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to M^{P} \in ℝ$
245	76	ad3antrrr	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to M \in ℝ$
246	245 231	reexpcld	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to M^{if (h = 0, P - 1, P)} \in ℝ$
247	224 218	sylan2	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to x - h \in ℝ$
248	28	adantr	$⊢ (x \in (0, j) \land h \in (0 \dots M)) \to x \in ℂ$
249	224 227	sylan2	$⊢ (x \in (0, j) \land h \in (0 \dots M)) \to h \in ℂ$
250	248 249	negsubdi2d	$⊢ (x \in (0, j) \land h \in (0 \dots M)) \to - (x - h) = h - x$
251	250	adantll	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to - (x - h) = h - x$
252	224	adantl	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to h \in ℕ_{0}$
253	252	nn0red	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to h \in ℝ$
254		0red	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to 0 \in ℝ$
255	210	adantr	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to x \in ℝ$
256		elfzle2	$⊢ h \in (0 \dots M) \to h \leq M$
257	256	adantl	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to h \leq M$
258	197 184 183	ltled	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to 0 \leq x$
259	258	adantll	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to 0 \leq x$
260	259	adantr	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to 0 \leq x$
261	253 254 245 255 257 260	le2subd	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to h - x \leq M - 0$
262	83	subid1d	$⊢ φ \to M - 0 = M$
263	262	ad3antrrr	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to M - 0 = M$
264	261 263	breqtrd	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to h - x \leq M$
265	251 264	eqbrtrd	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to - (x - h) \leq M$
266	247 245 265	lenegcon1d	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to - M \leq x - h$
267		elfzel2	$⊢ j \in (0 \dots M) \to M \in ℤ$
268	267	zred	$⊢ j \in (0 \dots M) \to M \in ℝ$
269	268	adantr	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to M \in ℝ$
270	53	adantr	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to j \in ℝ$
271		iooltub	$⊢ (0 \in ℝ^{} \land j \in ℝ^{} \land x \in (0, j)) \to x < j$
272	178 180 181 271	syl3anc	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to x < j$
273		elfzle2	$⊢ j \in (0 \dots M) \to j \leq M$
274	273	adantr	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to j \leq M$
275	184 270 269 272 274	ltletrd	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to x < M$
276	184 269 275	ltled	$⊢ (j \in (0 \dots M) \land x \in (0, j)) \to x \leq M$
277	276	adantll	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to x \leq M$
278	277	adantr	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to x \leq M$
279	252	nn0ge0d	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to 0 \leq h$
280	255 254 245 253 278 279	le2subd	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to x - h \leq M - 0$
281	280 263	breqtrd	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to x - h \leq M$
282	247 245	absled	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to (\|x - h\| \leq M \leftrightarrow (- M \leq x - h \land x - h \leq M))$
283	266 281 282	mpbir2and	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to \|x - h\| \leq M$
284		leexp1a	$⊢ ((\|x - h\| \in ℝ \land M \in ℝ \land if (h = 0, P - 1, P) \in ℕ_{0}) \land (0 \leq \|x - h\| \land \|x - h\| \leq M)) \to {\|x - h\|}^{if (h = 0, P - 1, P)} \leq M^{if (h = 0, P - 1, P)}$
285	239 245 231 242 283 284	syl32anc	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to {\|x - h\|}^{if (h = 0, P - 1, P)} \leq M^{if (h = 0, P - 1, P)}$
286	5	nnge1d	$⊢ φ \to 1 \leq M$
287	286	ad3antrrr	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to 1 \leq M$
288	219	nn0zd	$⊢ φ \to if (h = 0, P - 1, P) \in ℤ$
289	77	nn0zd	$⊢ φ \to P \in ℤ$
290		iftrue	$⊢ h = 0 \to if (h = 0, P - 1, P) = P - 1$
291	290	adantl	$⊢ (φ \land h = 0) \to if (h = 0, P - 1, P) = P - 1$
292	4	nnred	$⊢ φ \to P \in ℝ$
293	292	lem1d	$⊢ φ \to P - 1 \leq P$
294	293	adantr	$⊢ (φ \land h = 0) \to P - 1 \leq P$
295	291 294	eqbrtrd	$⊢ (φ \land h = 0) \to if (h = 0, P - 1, P) \leq P$
296		iffalse	$⊢ \neg h = 0 \to if (h = 0, P - 1, P) = P$
297	296	adantl	$⊢ (φ \land \neg h = 0) \to if (h = 0, P - 1, P) = P$
298	292	leidd	$⊢ φ \to P \leq P$
299	298	adantr	$⊢ (φ \land \neg h = 0) \to P \leq P$
300	297 299	eqbrtrd	$⊢ (φ \land \neg h = 0) \to if (h = 0, P - 1, P) \leq P$
301	295 300	pm2.61dan	$⊢ φ \to if (h = 0, P - 1, P) \leq P$
302		eluz2	$⊢ P \in ℤ_{\geq if (h = 0, P - 1, P)} \leftrightarrow (if (h = 0, P - 1, P) \in ℤ \land P \in ℤ \land if (h = 0, P - 1, P) \leq P)$
303	288 289 301 302	syl3anbrc	$⊢ φ \to P \in ℤ_{\geq if (h = 0, P - 1, P)}$
304	303	ad3antrrr	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to P \in ℤ_{\geq if (h = 0, P - 1, P)}$
305	245 287 304	leexp2ad	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to M^{if (h = 0, P - 1, P)} \leq M^{P}$
306	240 246 244 285 305	letrd	$⊢ (((φ \land j \in (0 \dots M)) \land x \in (0, j)) \land h \in (0 \dots M)) \to {\|x - h\|}^{if (h = 0, P - 1, P)} \leq M^{P}$
307	235 236 240 243 244 306	fprodle	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to \prod_{h = 0}^{M} {\|x - h\|}^{if (h = 0, P - 1, P)} \leq \prod_{h = 0}^{M} M^{P}$
308	78	recnd	$⊢ φ \to M^{P} \in ℂ$
309		fprodconst	$⊢ ((0 \dots M) \in Fin \land M^{P} \in ℂ) \to \prod_{h = 0}^{M} M^{P} = {(M^{P})}^{\|(0 \dots M)\|}$
310	12 308 309	syl2anc	$⊢ φ \to \prod_{h = 0}^{M} M^{P} = {(M^{P})}^{\|(0 \dots M)\|}$
311		hashfz0	$⊢ M \in ℕ_{0} \to \|(0 \dots M)\| = M + 1$
312	47 311	syl	$⊢ φ \to \|(0 \dots M)\| = M + 1$
313	312	oveq2d	$⊢ φ \to {(M^{P})}^{\|(0 \dots M)\|} = {(M^{P})}^{M + 1}$
314	310 313	eqtrd	$⊢ φ \to \prod_{h = 0}^{M} M^{P} = {(M^{P})}^{M + 1}$
315	314	ad2antrr	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to \prod_{h = 0}^{M} M^{P} = {(M^{P})}^{M + 1}$
316	307 315	breqtrd	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to \prod_{h = 0}^{M} {\|x - h\|}^{if (h = 0, P - 1, P)} \leq {(M^{P})}^{M + 1}$
317	234 316	eqbrtrd	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to \|F (x)\| \leq {(M^{P})}^{M + 1}$
318	160 161 162 136 163 164 205 317	lemul12ad	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to \|e^{- x}\| \|F (x)\| \leq 1 {(M^{P})}^{M + 1}$
319	82	mullidd	$⊢ φ \to 1 {(M^{P})}^{M + 1} = {(M^{P})}^{M + 1}$
320	319	ad2antrr	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to 1 {(M^{P})}^{M + 1} = {(M^{P})}^{M + 1}$
321	318 320	breqtrd	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to \|e^{- x}\| \|F (x)\| \leq {(M^{P})}^{M + 1}$
322	159 321	eqbrtrd	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to \|e^{- x} F (x)\| \leq {(M^{P})}^{M + 1}$
323	156 148 155 136 322	itgle	$⊢ (φ \land j \in (0 \dots M)) \to \int_{(0, j)} \|e^{- x} F (x)\| d x \leq \int_{(0, j)} {(M^{P})}^{M + 1} d x$
324	153 157 149 158 323	letrd	$⊢ (φ \land j \in (0 \dots M)) \to \|\int_{(0, j)} e^{- x} F (x) d x\| \leq \int_{(0, j)} {(M^{P})}^{M + 1} d x$
325	153 149 109 154 324	lemul2ad	$⊢ (φ \land j \in (0 \dots M)) \to \|A (j) e^{j}\| \|\int_{(0, j)} e^{- x} F (x) d x\| \leq \|A (j) e^{j}\| \int_{(0, j)} {(M^{P})}^{M + 1} d x$
326	152 325	eqbrtrd	$⊢ (φ \land j \in (0 \dots M)) \to \|A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x\| \leq \|A (j) e^{j}\| \int_{(0, j)} {(M^{P})}^{M + 1} d x$
327	12 133 150 326	fsumle	$⊢ φ \to \sum_{j = 0}^{M} \|A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x\| \leq \sum_{j = 0}^{M} \|A (j) e^{j}\| \int_{(0, j)} {(M^{P})}^{M + 1} d x$
328		itgconst	$⊢ ((0, j) \in dom vol \land vol ((0, j)) \in ℝ \land {(M^{P})}^{M + 1} \in ℂ) \to \int_{(0, j)} {(M^{P})}^{M + 1} d x = {(M^{P})}^{M + 1} vol ((0, j))$
329	138 145 146 328	syl3anc	$⊢ (φ \land j \in (0 \dots M)) \to \int_{(0, j)} {(M^{P})}^{M + 1} d x = {(M^{P})}^{M + 1} vol ((0, j))$
330	47	nn0ge0d	$⊢ φ \to 0 \leq M$
331	76 77 330	expge0d	$⊢ φ \to 0 \leq M^{P}$
332	78 80 331	expge0d	$⊢ φ \to 0 \leq {(M^{P})}^{M + 1}$
333	332	adantr	$⊢ (φ \land j \in (0 \dots M)) \to 0 \leq {(M^{P})}^{M + 1}$
334	22	subid1d	$⊢ j \in (0 \dots M) \to j - 0 = j$
335	142 334	eqtrd	$⊢ j \in (0 \dots M) \to vol ((0, j)) = j$
336	335 273	eqbrtrd	$⊢ j \in (0 \dots M) \to vol ((0, j)) \leq M$
337	336	adantl	$⊢ (φ \land j \in (0 \dots M)) \to vol ((0, j)) \leq M$
338	145 124 123 333 337	lemul2ad	$⊢ (φ \land j \in (0 \dots M)) \to {(M^{P})}^{M + 1} vol ((0, j)) \leq {(M^{P})}^{M + 1} \cdot M$
339	329 338	eqbrtrd	$⊢ (φ \land j \in (0 \dots M)) \to \int_{(0, j)} {(M^{P})}^{M + 1} d x \leq {(M^{P})}^{M + 1} \cdot M$
340	149 125 109 154 339	lemul2ad	$⊢ (φ \land j \in (0 \dots M)) \to \|A (j) e^{j}\| \int_{(0, j)} {(M^{P})}^{M + 1} d x \leq \|A (j) e^{j}\| {(M^{P})}^{M + 1} \cdot M$
341	12 150 126 340	fsumle	$⊢ φ \to \sum_{j = 0}^{M} \|A (j) e^{j}\| \int_{(0, j)} {(M^{P})}^{M + 1} d x \leq \sum_{j = 0}^{M} \|A (j) e^{j}\| {(M^{P})}^{M + 1} \cdot M$
342	134 151 127 327 341	letrd	$⊢ φ \to \sum_{j = 0}^{M} \|A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x\| \leq \sum_{j = 0}^{M} \|A (j) e^{j}\| {(M^{P})}^{M + 1} \cdot M$
343	131 134 127 135 342	letrd	$⊢ φ \to \|\sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x\| \leq \sum_{j = 0}^{M} \|A (j) e^{j}\| {(M^{P})}^{M + 1} \cdot M$
344	131 127 132 343	lediv1dd	$⊢ φ \to \frac{\|\sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x\|}{(P - 1)!} \leq \frac{\sum_{j = 0}^{M} \|A (j) e^{j}\| {(M^{P})}^{M + 1} \cdot M}{(P - 1)!}$
345	344 122	breqtrd	$⊢ φ \to \frac{\|\sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x\|}{(P - 1)!} \leq \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} (\frac{{(M^{M + 1})}^{P - 1}}{(P - 1)!})$
346	75 129 130 345 7	lelttrd	$⊢ φ \to \frac{\|\sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x\|}{(P - 1)!} < 1$
347	70 346	eqbrtrd	$⊢ φ \to \|K\| < 1$

Metamath Proof Explorer

Theorem etransclem23

Proof