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

Metamath Proof Explorer

Theorem etransclem23

Proof