etransclem46

Description: This is the proof for equation *(7) in Juillerat p. 12. The proven equality will lead to a contradiction, because the left-hand side goes to 0 for large P , but the right-hand side is a nonzero integer. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem46.q	$⊢ φ \to Q \in (Poly (ℤ) ∖ \{0_{𝑝}\})$
	etransclem46.qe0	$⊢ φ \to Q (e) = 0$
	etransclem46.a	$⊢ A = coeff (Q)$
	etransclem46.m	$⊢ M = \deg (Q)$
	etransclem46.rex	$⊢ φ \to ℝ \subseteq ℝ$
	etransclem46.s	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
	etransclem46.x	$⊢ φ \to ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
	etransclem46.p	$⊢ φ \to P \in ℕ$
	etransclem46.f	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
	etransclem46.l	$⊢ L = \sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x$
	etransclem46.r	$⊢ R = M P + P - 1$
	etransclem46.g	$⊢ G = (x \in ℝ ⟼ \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (x))$
	etransclem46.h	$⊢ O = (x \in [0, j] ⟼ - e^{- x} G (x))$
Assertion	etransclem46	$⊢ φ \to \frac{L}{(P - 1)!} = \frac{- \sum_{k \in (0 \dots M) \times (0 \dots R)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}$

Proof

Step	Hyp	Ref	Expression
1		etransclem46.q	$⊢ φ \to Q \in (Poly (ℤ) ∖ \{0_{𝑝}\})$
2		etransclem46.qe0	$⊢ φ \to Q (e) = 0$
3		etransclem46.a	$⊢ A = coeff (Q)$
4		etransclem46.m	$⊢ M = \deg (Q)$
5		etransclem46.rex	$⊢ φ \to ℝ \subseteq ℝ$
6		etransclem46.s	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
7		etransclem46.x	$⊢ φ \to ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
8		etransclem46.p	$⊢ φ \to P \in ℕ$
9		etransclem46.f	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
10		etransclem46.l	$⊢ L = \sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x$
11		etransclem46.r	$⊢ R = M P + P - 1$
12		etransclem46.g	$⊢ G = (x \in ℝ ⟼ \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (x))$
13		etransclem46.h	$⊢ O = (x \in [0, j] ⟼ - e^{- x} G (x))$
14	10	a1i	$⊢ φ \to L = \sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x$
15	13	oveq2i	$⊢ ℝ D O = \frac{d (x \in [0, j]⟼ - e^{- x} G (x))}{d_{ℝ} x}$
16	15	a1i	$⊢ (φ \land j \in (0 \dots M)) \to ℝ D O = \frac{d (x \in [0, j]⟼ - e^{- x} G (x))}{d_{ℝ} x}$
17	6	adantr	$⊢ (φ \land j \in (0 \dots M)) \to ℝ \in \{ℝ, ℂ\}$
18		ere	$⊢ e \in ℝ$
19	18	recni	$⊢ e \in ℂ$
20	19	a1i	$⊢ x \in ℝ \to e \in ℂ$
21		recn	$⊢ x \in ℝ \to x \in ℂ$
22	21	negcld	$⊢ x \in ℝ \to - x \in ℂ$
23	20 22	cxpcld	$⊢ x \in ℝ \to e^{- x} \in ℂ$
24	23	adantl	$⊢ (φ \land x \in ℝ) \to e^{- x} \in ℂ$
25		simpr	$⊢ (φ \land x \in ℝ) \to x \in ℝ$
26		fzfid	$⊢ (φ \land x \in ℝ) \to (0 \dots R) \in Fin$
27		elfznn0	$⊢ i \in (0 \dots R) \to i \in ℕ_{0}$
28	6	adantr	$⊢ (φ \land i \in ℕ_{0}) \to ℝ \in \{ℝ, ℂ\}$
29	7	adantr	$⊢ (φ \land i \in ℕ_{0}) \to ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
30	8	adantr	$⊢ (φ \land i \in ℕ_{0}) \to P \in ℕ$
31	1	eldifad	$⊢ φ \to Q \in Poly (ℤ)$
32		dgrcl	$⊢ Q \in Poly (ℤ) \to \deg (Q) \in ℕ_{0}$
33	31 32	syl	$⊢ φ \to \deg (Q) \in ℕ_{0}$
34	4 33	eqeltrid	$⊢ φ \to M \in ℕ_{0}$
35	34	adantr	$⊢ (φ \land i \in ℕ_{0}) \to M \in ℕ_{0}$
36		simpr	$⊢ (φ \land i \in ℕ_{0}) \to i \in ℕ_{0}$
37	28 29 30 35 9 36	etransclem33	$⊢ (φ \land i \in ℕ_{0}) \to (ℝ D^{n} F) (i) : ℝ ⟶ ℂ$
38	27 37	sylan2	$⊢ (φ \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i) : ℝ ⟶ ℂ$
39	38	adantlr	$⊢ ((φ \land x \in ℝ) \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i) : ℝ ⟶ ℂ$
40		simplr	$⊢ ((φ \land x \in ℝ) \land i \in (0 \dots R)) \to x \in ℝ$
41	39 40	ffvelrnd	$⊢ ((φ \land x \in ℝ) \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i) (x) \in ℂ$
42	26 41	fsumcl	$⊢ (φ \land x \in ℝ) \to \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (x) \in ℂ$
43	12	fvmpt2	$⊢ (x \in ℝ \land \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (x) \in ℂ) \to G (x) = \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (x)$
44	25 42 43	syl2anc	$⊢ (φ \land x \in ℝ) \to G (x) = \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (x)$
45	44 42	eqeltrd	$⊢ (φ \land x \in ℝ) \to G (x) \in ℂ$
46	24 45	mulcld	$⊢ (φ \land x \in ℝ) \to e^{- x} G (x) \in ℂ$
47	46	negcld	$⊢ (φ \land x \in ℝ) \to - e^{- x} G (x) \in ℂ$
48	47	adantlr	$⊢ ((φ \land j \in (0 \dots M)) \land x \in ℝ) \to - e^{- x} G (x) \in ℂ$
49	6 7	dvdmsscn	$⊢ φ \to ℝ \subseteq ℂ$
50	49 8 9	etransclem8	$⊢ φ \to F : ℝ ⟶ ℂ$
51	50	ffvelrnda	$⊢ (φ \land x \in ℝ) \to F (x) \in ℂ$
52	24 51	mulcld	$⊢ (φ \land x \in ℝ) \to e^{- x} F (x) \in ℂ$
53	52	negcld	$⊢ (φ \land x \in ℝ) \to - e^{- x} F (x) \in ℂ$
54	53	negcld	$⊢ (φ \land x \in ℝ) \to - (- e^{- x} F (x)) \in ℂ$
55	54	adantlr	$⊢ ((φ \land j \in (0 \dots M)) \land x \in ℝ) \to - (- e^{- x} F (x)) \in ℂ$
56	18	a1i	$⊢ x \in ℝ \to e \in ℝ$
57		0re	$⊢ 0 \in ℝ$
58		epos	$⊢ 0 < e$
59	57 18 58	ltleii	$⊢ 0 \leq e$
60	59	a1i	$⊢ x \in ℝ \to 0 \leq e$
61		renegcl	$⊢ x \in ℝ \to - x \in ℝ$
62	56 60 61	recxpcld	$⊢ x \in ℝ \to e^{- x} \in ℝ$
63	62	renegcld	$⊢ x \in ℝ \to - e^{- x} \in ℝ$
64	63	adantl	$⊢ (φ \land x \in ℝ) \to - e^{- x} \in ℝ$
65		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
66	65	a1i	$⊢ ⊤ \to ℝ \in \{ℝ, ℂ\}$
67		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
68	67	a1i	$⊢ ⊤ \to ℂ \in \{ℝ, ℂ\}$
69	22	adantl	$⊢ (⊤ \land x \in ℝ) \to - x \in ℂ$
70		neg1rr	$⊢ - 1 \in ℝ$
71	70	a1i	$⊢ (⊤ \land x \in ℝ) \to - 1 \in ℝ$
72	19	a1i	$⊢ y \in ℂ \to e \in ℂ$
73		id	$⊢ y \in ℂ \to y \in ℂ$
74	72 73	cxpcld	$⊢ y \in ℂ \to e^{y} \in ℂ$
75	74	adantl	$⊢ (⊤ \land y \in ℂ) \to e^{y} \in ℂ$
76	21	adantl	$⊢ (⊤ \land x \in ℝ) \to x \in ℂ$
77		1red	$⊢ (⊤ \land x \in ℝ) \to 1 \in ℝ$
78	66	dvmptid	$⊢ ⊤ \to \frac{d (x \in ℝ⟼ x)}{d_{ℝ} x} = (x \in ℝ ⟼ 1)$
79	66 76 77 78	dvmptneg	$⊢ ⊤ \to \frac{d (x \in ℝ⟼ - x)}{d_{ℝ} x} = (x \in ℝ ⟼ - 1)$
80		epr	$⊢ e \in ℝ^{+}$
81		dvcxp2	$⊢ e \in ℝ^{+} \to \frac{d (y \in ℂ⟼ e^{y})}{d_{ℂ} y} = (y \in ℂ ⟼ \log e e^{y})$
82	80 81	ax-mp	$⊢ \frac{d (y \in ℂ⟼ e^{y})}{d_{ℂ} y} = (y \in ℂ ⟼ \log e e^{y})$
83		loge	$⊢ \log e = 1$
84	83	oveq1i	$⊢ \log e e^{y} = 1 e^{y}$
85	74	mulid2d	$⊢ y \in ℂ \to 1 e^{y} = e^{y}$
86	84 85	syl5eq	$⊢ y \in ℂ \to \log e e^{y} = e^{y}$
87	86	mpteq2ia	$⊢ (y \in ℂ ⟼ \log e e^{y}) = (y \in ℂ ⟼ e^{y})$
88	82 87	eqtri	$⊢ \frac{d (y \in ℂ⟼ e^{y})}{d_{ℂ} y} = (y \in ℂ ⟼ e^{y})$
89	88	a1i	$⊢ ⊤ \to \frac{d (y \in ℂ⟼ e^{y})}{d_{ℂ} y} = (y \in ℂ ⟼ e^{y})$
90		oveq2	$⊢ y = - x \to e^{y} = e^{- x}$
91	66 68 69 71 75 75 79 89 90 90	dvmptco	$⊢ ⊤ \to \frac{d (x \in ℝ⟼ e^{- x})}{d_{ℝ} x} = (x \in ℝ ⟼ e^{- x} -1)$
92	91	mptru	$⊢ \frac{d (x \in ℝ⟼ e^{- x})}{d_{ℝ} x} = (x \in ℝ ⟼ e^{- x} -1)$
93	70	a1i	$⊢ x \in ℝ \to - 1 \in ℝ$
94	93	recnd	$⊢ x \in ℝ \to - 1 \in ℂ$
95	23 94	mulcomd	$⊢ x \in ℝ \to e^{- x} -1 = -1 e^{- x}$
96	23	mulm1d	$⊢ x \in ℝ \to -1 e^{- x} = - e^{- x}$
97	95 96	eqtrd	$⊢ x \in ℝ \to e^{- x} -1 = - e^{- x}$
98	97	mpteq2ia	$⊢ (x \in ℝ ⟼ e^{- x} -1) = (x \in ℝ ⟼ - e^{- x})$
99	92 98	eqtri	$⊢ \frac{d (x \in ℝ⟼ e^{- x})}{d_{ℝ} x} = (x \in ℝ ⟼ - e^{- x})$
100	99	a1i	$⊢ φ \to \frac{d (x \in ℝ⟼ e^{- x})}{d_{ℝ} x} = (x \in ℝ ⟼ - e^{- x})$
101	27	adantl	$⊢ (φ \land i \in (0 \dots R)) \to i \in ℕ_{0}$
102		peano2nn0	$⊢ i \in ℕ_{0} \to i + 1 \in ℕ_{0}$
103	101 102	syl	$⊢ (φ \land i \in (0 \dots R)) \to i + 1 \in ℕ_{0}$
104		ovex	$⊢ i + 1 \in V$
105		eleq1	$⊢ j = i + 1 \to (j \in ℕ_{0} \leftrightarrow i + 1 \in ℕ_{0})$
106	105	anbi2d	$⊢ j = i + 1 \to ((φ \land j \in ℕ_{0}) \leftrightarrow (φ \land i + 1 \in ℕ_{0}))$
107		fveq2	$⊢ j = i + 1 \to (ℝ D^{n} F) (j) = (ℝ D^{n} F) (i + 1)$
108	107	feq1d	$⊢ j = i + 1 \to ((ℝ D^{n} F) (j) : ℝ ⟶ ℂ \leftrightarrow (ℝ D^{n} F) (i + 1) : ℝ ⟶ ℂ)$
109	106 108	imbi12d	$⊢ j = i + 1 \to (((φ \land j \in ℕ_{0}) \to (ℝ D^{n} F) (j) : ℝ ⟶ ℂ) \leftrightarrow ((φ \land i + 1 \in ℕ_{0}) \to (ℝ D^{n} F) (i + 1) : ℝ ⟶ ℂ))$
110		eleq1	$⊢ i = j \to (i \in ℕ_{0} \leftrightarrow j \in ℕ_{0})$
111	110	anbi2d	$⊢ i = j \to ((φ \land i \in ℕ_{0}) \leftrightarrow (φ \land j \in ℕ_{0}))$
112		fveq2	$⊢ i = j \to (ℝ D^{n} F) (i) = (ℝ D^{n} F) (j)$
113	112	feq1d	$⊢ i = j \to ((ℝ D^{n} F) (i) : ℝ ⟶ ℂ \leftrightarrow (ℝ D^{n} F) (j) : ℝ ⟶ ℂ)$
114	111 113	imbi12d	$⊢ i = j \to (((φ \land i \in ℕ_{0}) \to (ℝ D^{n} F) (i) : ℝ ⟶ ℂ) \leftrightarrow ((φ \land j \in ℕ_{0}) \to (ℝ D^{n} F) (j) : ℝ ⟶ ℂ))$
115	114 37	chvarvv	$⊢ (φ \land j \in ℕ_{0}) \to (ℝ D^{n} F) (j) : ℝ ⟶ ℂ$
116	104 109 115	vtocl	$⊢ (φ \land i + 1 \in ℕ_{0}) \to (ℝ D^{n} F) (i + 1) : ℝ ⟶ ℂ$
117	103 116	syldan	$⊢ (φ \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i + 1) : ℝ ⟶ ℂ$
118	117	adantlr	$⊢ ((φ \land x \in ℝ) \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i + 1) : ℝ ⟶ ℂ$
119	118 40	ffvelrnd	$⊢ ((φ \land x \in ℝ) \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i + 1) (x) \in ℂ$
120	26 119	fsumcl	$⊢ (φ \land x \in ℝ) \to \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) \in ℂ$
121	8 34 9 12	etransclem39	$⊢ φ \to G : ℝ ⟶ ℂ$
122	121	feqmptd	$⊢ φ \to G = (x \in ℝ ⟼ G (x))$
123	122	eqcomd	$⊢ φ \to (x \in ℝ ⟼ G (x)) = G$
124	123	oveq2d	$⊢ φ \to \frac{d (x \in ℝ⟼ G (x))}{d_{ℝ} x} = ℝ D G$
125		nfcv	$⊢ \underline{Ⅎ} x F$
126		elfznn0	$⊢ i \in (0 \dots R + 1) \to i \in ℕ_{0}$
127	126 37	sylan2	$⊢ (φ \land i \in (0 \dots R + 1)) \to (ℝ D^{n} F) (i) : ℝ ⟶ ℂ$
128	125 50 127 12	etransclem2	$⊢ φ \to ℝ D G = (x \in ℝ ⟼ \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x))$
129	124 128	eqtrd	$⊢ φ \to \frac{d (x \in ℝ⟼ G (x))}{d_{ℝ} x} = (x \in ℝ ⟼ \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x))$
130	6 24 64 100 45 120 129	dvmptmul	$⊢ φ \to \frac{d (x \in ℝ⟼ e^{- x} G (x))}{d_{ℝ} x} = (x \in ℝ ⟼ (- e^{- x}) G (x) + \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) e^{- x})$
131	120 24	mulcomd	$⊢ (φ \land x \in ℝ) \to \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) e^{- x} = e^{- x} \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x)$
132	131	oveq2d	$⊢ (φ \land x \in ℝ) \to (- e^{- x}) G (x) + \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) e^{- x} = (- e^{- x}) G (x) + e^{- x} \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x)$
133	24	negcld	$⊢ (φ \land x \in ℝ) \to - e^{- x} \in ℂ$
134	133 45	mulcld	$⊢ (φ \land x \in ℝ) \to (- e^{- x}) G (x) \in ℂ$
135	24 120	mulcld	$⊢ (φ \land x \in ℝ) \to e^{- x} \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) \in ℂ$
136	134 135	addcomd	$⊢ (φ \land x \in ℝ) \to (- e^{- x}) G (x) + e^{- x} \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) = e^{- x} \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) + (- e^{- x}) G (x)$
137	135 46	negsubd	$⊢ (φ \land x \in ℝ) \to e^{- x} \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) + (- e^{- x} G (x)) = e^{- x} \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) - e^{- x} G (x)$
138	24 45	mulneg1d	$⊢ (φ \land x \in ℝ) \to (- e^{- x}) G (x) = - e^{- x} G (x)$
139	138	oveq2d	$⊢ (φ \land x \in ℝ) \to e^{- x} \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) + (- e^{- x}) G (x) = e^{- x} \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) + (- e^{- x} G (x))$
140	24 120 45	subdid	$⊢ (φ \land x \in ℝ) \to e^{- x} (\sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) - G (x)) = e^{- x} \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) - e^{- x} G (x)$
141	137 139 140	3eqtr4d	$⊢ (φ \land x \in ℝ) \to e^{- x} \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) + (- e^{- x}) G (x) = e^{- x} (\sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) - G (x))$
142	44	oveq2d	$⊢ (φ \land x \in ℝ) \to \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) - G (x) = \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) - \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (x)$
143	26 119 41	fsumsub	$⊢ (φ \land x \in ℝ) \to \sum_{i = 0}^{R} ((ℝ D^{n} F) (i + 1) (x) - (ℝ D^{n} F) (i) (x)) = \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) - \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (x)$
144		fveq2	$⊢ j = i \to (ℝ D^{n} F) (j) = (ℝ D^{n} F) (i)$
145	144	fveq1d	$⊢ j = i \to (ℝ D^{n} F) (j) (x) = (ℝ D^{n} F) (i) (x)$
146	107	fveq1d	$⊢ j = i + 1 \to (ℝ D^{n} F) (j) (x) = (ℝ D^{n} F) (i + 1) (x)$
147		fveq2	$⊢ j = 0 \to (ℝ D^{n} F) (j) = (ℝ D^{n} F) (0)$
148	147	fveq1d	$⊢ j = 0 \to (ℝ D^{n} F) (j) (x) = (ℝ D^{n} F) (0) (x)$
149		fveq2	$⊢ j = R + 1 \to (ℝ D^{n} F) (j) = (ℝ D^{n} F) (R + 1)$
150	149	fveq1d	$⊢ j = R + 1 \to (ℝ D^{n} F) (j) (x) = (ℝ D^{n} F) (R + 1) (x)$
151	8	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
152	34 151	nn0mulcld	$⊢ φ \to M P \in ℕ_{0}$
153		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
154	8 153	syl	$⊢ φ \to P - 1 \in ℕ_{0}$
155	152 154	nn0addcld	$⊢ φ \to M P + P - 1 \in ℕ_{0}$
156	11 155	eqeltrid	$⊢ φ \to R \in ℕ_{0}$
157	156	adantr	$⊢ (φ \land x \in ℝ) \to R \in ℕ_{0}$
158	157	nn0zd	$⊢ (φ \land x \in ℝ) \to R \in ℤ$
159		peano2nn0	$⊢ R \in ℕ_{0} \to R + 1 \in ℕ_{0}$
160	156 159	syl	$⊢ φ \to R + 1 \in ℕ_{0}$
161		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
162	160 161	eleqtrdi	$⊢ φ \to R + 1 \in ℤ_{\geq 0}$
163	162	adantr	$⊢ (φ \land x \in ℝ) \to R + 1 \in ℤ_{\geq 0}$
164		elfznn0	$⊢ j \in (0 \dots R + 1) \to j \in ℕ_{0}$
165	164 115	sylan2	$⊢ (φ \land j \in (0 \dots R + 1)) \to (ℝ D^{n} F) (j) : ℝ ⟶ ℂ$
166	165	adantlr	$⊢ ((φ \land x \in ℝ) \land j \in (0 \dots R + 1)) \to (ℝ D^{n} F) (j) : ℝ ⟶ ℂ$
167		simplr	$⊢ ((φ \land x \in ℝ) \land j \in (0 \dots R + 1)) \to x \in ℝ$
168	166 167	ffvelrnd	$⊢ ((φ \land x \in ℝ) \land j \in (0 \dots R + 1)) \to (ℝ D^{n} F) (j) (x) \in ℂ$
169	145 146 148 150 158 163 168	telfsum2	$⊢ (φ \land x \in ℝ) \to \sum_{i = 0}^{R} ((ℝ D^{n} F) (i + 1) (x) - (ℝ D^{n} F) (i) (x)) = (ℝ D^{n} F) (R + 1) (x) - (ℝ D^{n} F) (0) (x)$
170	142 143 169	3eqtr2d	$⊢ (φ \land x \in ℝ) \to \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) - G (x) = (ℝ D^{n} F) (R + 1) (x) - (ℝ D^{n} F) (0) (x)$
171	170	oveq2d	$⊢ (φ \land x \in ℝ) \to e^{- x} (\sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) - G (x)) = e^{- x} ((ℝ D^{n} F) (R + 1) (x) - (ℝ D^{n} F) (0) (x))$
172	156	nn0red	$⊢ φ \to R \in ℝ$
173	172	ltp1d	$⊢ φ \to R < R + 1$
174	11 173	eqbrtrrid	$⊢ φ \to M P + P - 1 < R + 1$
175		etransclem5	$⊢ (k \in (0 \dots M) ⟼ (y \in ℝ ⟼ {(y - k)}^{if (k = 0, P - 1, P)})) = (j \in (0 \dots M) ⟼ (x \in ℝ ⟼ {(x - j)}^{if (j = 0, P - 1, P)}))$
176	6 7 8 34 9 160 174 175	etransclem32	$⊢ φ \to (ℝ D^{n} F) (R + 1) = (x \in ℝ ⟼ 0)$
177	176	fveq1d	$⊢ φ \to (ℝ D^{n} F) (R + 1) (x) = (x \in ℝ ⟼ 0) (x)$
178		eqid	$⊢ (x \in ℝ ⟼ 0) = (x \in ℝ ⟼ 0)$
179	178	fvmpt2	$⊢ (x \in ℝ \land 0 \in ℝ) \to (x \in ℝ ⟼ 0) (x) = 0$
180	57 179	mpan2	$⊢ x \in ℝ \to (x \in ℝ ⟼ 0) (x) = 0$
181	177 180	sylan9eq	$⊢ (φ \land x \in ℝ) \to (ℝ D^{n} F) (R + 1) (x) = 0$
182		cnex	$⊢ ℂ \in V$
183	182	a1i	$⊢ φ \to ℂ \in V$
184	6 5	ssexd	$⊢ φ \to ℝ \in V$
185		elpm2r	$⊢ ((ℂ \in V \land ℝ \in V) \land (F : ℝ ⟶ ℂ \land ℝ \subseteq ℝ)) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
186	183 184 50 5 185	syl22anc	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
187		dvn0	$⊢ (ℝ \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} ℝ)) \to (ℝ D^{n} F) (0) = F$
188	49 186 187	syl2anc	$⊢ φ \to (ℝ D^{n} F) (0) = F$
189	188	fveq1d	$⊢ φ \to (ℝ D^{n} F) (0) (x) = F (x)$
190	189	adantr	$⊢ (φ \land x \in ℝ) \to (ℝ D^{n} F) (0) (x) = F (x)$
191	181 190	oveq12d	$⊢ (φ \land x \in ℝ) \to (ℝ D^{n} F) (R + 1) (x) - (ℝ D^{n} F) (0) (x) = 0 - F (x)$
192		df-neg	$⊢ - F (x) = 0 - F (x)$
193	191 192	syl6eqr	$⊢ (φ \land x \in ℝ) \to (ℝ D^{n} F) (R + 1) (x) - (ℝ D^{n} F) (0) (x) = - F (x)$
194	193	oveq2d	$⊢ (φ \land x \in ℝ) \to e^{- x} ((ℝ D^{n} F) (R + 1) (x) - (ℝ D^{n} F) (0) (x)) = e^{- x} (- F (x))$
195	141 171 194	3eqtrd	$⊢ (φ \land x \in ℝ) \to e^{- x} \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) + (- e^{- x}) G (x) = e^{- x} (- F (x))$
196	132 136 195	3eqtrd	$⊢ (φ \land x \in ℝ) \to (- e^{- x}) G (x) + \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) e^{- x} = e^{- x} (- F (x))$
197	196	mpteq2dva	$⊢ φ \to (x \in ℝ ⟼ (- e^{- x}) G (x) + \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x) e^{- x}) = (x \in ℝ ⟼ e^{- x} (- F (x)))$
198	24 51	mulneg2d	$⊢ (φ \land x \in ℝ) \to e^{- x} (- F (x)) = - e^{- x} F (x)$
199	198	mpteq2dva	$⊢ φ \to (x \in ℝ ⟼ e^{- x} (- F (x))) = (x \in ℝ ⟼ - e^{- x} F (x))$
200	130 197 199	3eqtrd	$⊢ φ \to \frac{d (x \in ℝ⟼ e^{- x} G (x))}{d_{ℝ} x} = (x \in ℝ ⟼ - e^{- x} F (x))$
201	6 46 53 200	dvmptneg	$⊢ φ \to \frac{d (x \in ℝ⟼ - e^{- x} G (x))}{d_{ℝ} x} = (x \in ℝ ⟼ - (- e^{- x} F (x)))$
202	201	adantr	$⊢ (φ \land j \in (0 \dots M)) \to \frac{d (x \in ℝ⟼ - e^{- x} G (x))}{d_{ℝ} x} = (x \in ℝ ⟼ - (- e^{- x} F (x)))$
203		0red	$⊢ (φ \land j \in (0 \dots M)) \to 0 \in ℝ$
204		elfzelz	$⊢ j \in (0 \dots M) \to j \in ℤ$
205	204	zred	$⊢ j \in (0 \dots M) \to j \in ℝ$
206	205	adantl	$⊢ (φ \land j \in (0 \dots M)) \to j \in ℝ$
207	203 206	iccssred	$⊢ (φ \land j \in (0 \dots M)) \to [0, j] \subseteq ℝ$
208		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
209	208	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
210		0red	$⊢ j \in (0 \dots M) \to 0 \in ℝ$
211		iccntr	$⊢ (0 \in ℝ \land j \in ℝ) \to int (topGen (ran (.))) ([0, j]) = (0, j)$
212	210 205 211	syl2anc	$⊢ j \in (0 \dots M) \to int (topGen (ran (.))) ([0, j]) = (0, j)$
213	212	adantl	$⊢ (φ \land j \in (0 \dots M)) \to int (topGen (ran (.))) ([0, j]) = (0, j)$
214	17 48 55 202 207 209 208 213	dvmptres2	$⊢ (φ \land j \in (0 \dots M)) \to \frac{d (x \in [0, j]⟼ - e^{- x} G (x))}{d_{ℝ} x} = (x \in (0, j) ⟼ - (- e^{- x} F (x)))$
215	19	a1i	$⊢ (φ \land x \in (0, j)) \to e \in ℂ$
216		elioore	$⊢ x \in (0, j) \to x \in ℝ$
217	216	recnd	$⊢ x \in (0, j) \to x \in ℂ$
218	217	adantl	$⊢ (φ \land x \in (0, j)) \to x \in ℂ$
219	218	negcld	$⊢ (φ \land x \in (0, j)) \to - x \in ℂ$
220	215 219	cxpcld	$⊢ (φ \land x \in (0, j)) \to e^{- x} \in ℂ$
221	50	adantr	$⊢ (φ \land x \in (0, j)) \to F : ℝ ⟶ ℂ$
222	216	adantl	$⊢ (φ \land x \in (0, j)) \to x \in ℝ$
223	221 222	ffvelrnd	$⊢ (φ \land x \in (0, j)) \to F (x) \in ℂ$
224	220 223	mulcld	$⊢ (φ \land x \in (0, j)) \to e^{- x} F (x) \in ℂ$
225	224	negnegd	$⊢ (φ \land x \in (0, j)) \to - (- e^{- x} F (x)) = e^{- x} F (x)$
226	225	mpteq2dva	$⊢ φ \to (x \in (0, j) ⟼ - (- e^{- x} F (x))) = (x \in (0, j) ⟼ e^{- x} F (x))$
227	226	adantr	$⊢ (φ \land j \in (0 \dots M)) \to (x \in (0, j) ⟼ - (- e^{- x} F (x))) = (x \in (0, j) ⟼ e^{- x} F (x))$
228	16 214 227	3eqtrd	$⊢ (φ \land j \in (0 \dots M)) \to ℝ D O = (x \in (0, j) ⟼ e^{- x} F (x))$
229	228	fveq1d	$⊢ (φ \land j \in (0 \dots M)) \to O_{ℝ}^{'} (x) = (x \in (0, j) ⟼ e^{- x} F (x)) (x)$
230	229	adantr	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to O_{ℝ}^{'} (x) = (x \in (0, j) ⟼ e^{- x} F (x)) (x)$
231		simpr	$⊢ (φ \land x \in (0, j)) \to x \in (0, j)$
232		eqid	$⊢ (x \in (0, j) ⟼ e^{- x} F (x)) = (x \in (0, j) ⟼ e^{- x} F (x))$
233	232	fvmpt2	$⊢ (x \in (0, j) \land e^{- x} F (x) \in ℂ) \to (x \in (0, j) ⟼ e^{- x} F (x)) (x) = e^{- x} F (x)$
234	231 224 233	syl2anc	$⊢ (φ \land x \in (0, j)) \to (x \in (0, j) ⟼ e^{- x} F (x)) (x) = e^{- x} F (x)$
235	234	adantlr	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to (x \in (0, j) ⟼ e^{- x} F (x)) (x) = e^{- x} F (x)$
236	230 235	eqtr2d	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to e^{- x} F (x) = O_{ℝ}^{'} (x)$
237	236	itgeq2dv	$⊢ (φ \land j \in (0 \dots M)) \to \int_{(0, j)} e^{- x} F (x) d x = \int_{(0, j)} O_{ℝ}^{'} (x) d x$
238		elfzle1	$⊢ j \in (0 \dots M) \to 0 \leq j$
239	238	adantl	$⊢ (φ \land j \in (0 \dots M)) \to 0 \leq j$
240		eqid	$⊢ (x \in [0, j] ⟼ e^{- x} F (x)) = (x \in [0, j] ⟼ e^{- x} F (x))$
241		eqidd	$⊢ (j \in (0 \dots M) \land x \in [0, j]) \to (y \in ℂ ⟼ e^{y}) = (y \in ℂ ⟼ e^{y})$
242	90	adantl	$⊢ ((j \in (0 \dots M) \land x \in [0, j]) \land y = - x) \to e^{y} = e^{- x}$
243	210 205	iccssred	$⊢ j \in (0 \dots M) \to [0, j] \subseteq ℝ$
244		ax-resscn	$⊢ ℝ \subseteq ℂ$
245	243 244	sstrdi	$⊢ j \in (0 \dots M) \to [0, j] \subseteq ℂ$
246	245	sselda	$⊢ (j \in (0 \dots M) \land x \in [0, j]) \to x \in ℂ$
247	246	negcld	$⊢ (j \in (0 \dots M) \land x \in [0, j]) \to - x \in ℂ$
248	19	a1i	$⊢ x \in ℂ \to e \in ℂ$
249		negcl	$⊢ x \in ℂ \to - x \in ℂ$
250	248 249	cxpcld	$⊢ x \in ℂ \to e^{- x} \in ℂ$
251	246 250	syl	$⊢ (j \in (0 \dots M) \land x \in [0, j]) \to e^{- x} \in ℂ$
252	241 242 247 251	fvmptd	$⊢ (j \in (0 \dots M) \land x \in [0, j]) \to (y \in ℂ ⟼ e^{y}) (- x) = e^{- x}$
253	252	eqcomd	$⊢ (j \in (0 \dots M) \land x \in [0, j]) \to e^{- x} = (y \in ℂ ⟼ e^{y}) (- x)$
254	253	adantll	$⊢ ((φ \land j \in (0 \dots M)) \land x \in [0, j]) \to e^{- x} = (y \in ℂ ⟼ e^{y}) (- x)$
255	254	mpteq2dva	$⊢ (φ \land j \in (0 \dots M)) \to (x \in [0, j] ⟼ e^{- x}) = (x \in [0, j] ⟼ (y \in ℂ ⟼ e^{y}) (- x))$
256		mnfxr	$⊢ −∞ \in ℝ^{*}$
257	256	a1i	$⊢ e \in ℝ^{+} \to −∞ \in ℝ^{*}$
258		0red	$⊢ e \in ℝ^{+} \to 0 \in ℝ$
259		rpxr	$⊢ e \in ℝ^{+} \to e \in ℝ^{*}$
260		rpgt0	$⊢ e \in ℝ^{+} \to 0 < e$
261	257 258 259 260	gtnelioc	$⊢ e \in ℝ^{+} \to \neg e \in (−∞, 0]$
262	80 261	ax-mp	$⊢ \neg e \in (−∞, 0]$
263		eldif	$⊢ e \in (ℂ ∖ (−∞, 0]) \leftrightarrow (e \in ℂ \land \neg e \in (−∞, 0])$
264	19 262 263	mpbir2an	$⊢ e \in (ℂ ∖ (−∞, 0])$
265		cxpcncf2	$⊢ e \in (ℂ ∖ (−∞, 0]) \to (y \in ℂ ⟼ e^{y}) : ℂ \underset{cn}{⟶} ℂ$
266	264 265	mp1i	$⊢ (φ \land j \in (0 \dots M)) \to (y \in ℂ ⟼ e^{y}) : ℂ \underset{cn}{⟶} ℂ$
267		eqid	$⊢ (x \in [0, j] ⟼ - x) = (x \in [0, j] ⟼ - x)$
268	267	negcncf	$⊢ [0, j] \subseteq ℂ \to (x \in [0, j] ⟼ - x) : [0, j] \underset{cn}{⟶} ℂ$
269	245 268	syl	$⊢ j \in (0 \dots M) \to (x \in [0, j] ⟼ - x) : [0, j] \underset{cn}{⟶} ℂ$
270	269	adantl	$⊢ (φ \land j \in (0 \dots M)) \to (x \in [0, j] ⟼ - x) : [0, j] \underset{cn}{⟶} ℂ$
271	266 270	cncfmpt1f	$⊢ (φ \land j \in (0 \dots M)) \to (x \in [0, j] ⟼ (y \in ℂ ⟼ e^{y}) (- x)) : [0, j] \underset{cn}{⟶} ℂ$
272	255 271	eqeltrd	$⊢ (φ \land j \in (0 \dots M)) \to (x \in [0, j] ⟼ e^{- x}) : [0, j] \underset{cn}{⟶} ℂ$
273	244	a1i	$⊢ ((φ \land j \in (0 \dots M)) \land x \in [0, j]) \to ℝ \subseteq ℂ$
274	8	ad2antrr	$⊢ ((φ \land j \in (0 \dots M)) \land x \in [0, j]) \to P \in ℕ$
275	34	ad2antrr	$⊢ ((φ \land j \in (0 \dots M)) \land x \in [0, j]) \to M \in ℕ_{0}$
276		etransclem6	$⊢ (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P}) = (y \in ℝ ⟼ y^{P - 1} \prod_{k = 1}^{M} {(y - k)}^{P})$
277	9 276	eqtri	$⊢ F = (y \in ℝ ⟼ y^{P - 1} \prod_{k = 1}^{M} {(y - k)}^{P})$
278	243	sselda	$⊢ (j \in (0 \dots M) \land x \in [0, j]) \to x \in ℝ$
279	278	adantll	$⊢ ((φ \land j \in (0 \dots M)) \land x \in [0, j]) \to x \in ℝ$
280	273 274 275 277 279	etransclem13	$⊢ ((φ \land j \in (0 \dots M)) \land x \in [0, j]) \to F (x) = \prod_{k = 0}^{M} {(x - k)}^{if (k = 0, P - 1, P)}$
281	280	mpteq2dva	$⊢ (φ \land j \in (0 \dots M)) \to (x \in [0, j] ⟼ F (x)) = (x \in [0, j] ⟼ \prod_{k = 0}^{M} {(x - k)}^{if (k = 0, P - 1, P)})$
282	245	adantl	$⊢ (φ \land j \in (0 \dots M)) \to [0, j] \subseteq ℂ$
283		fzfid	$⊢ (φ \land j \in (0 \dots M)) \to (0 \dots M) \in Fin$
284	279	recnd	$⊢ ((φ \land j \in (0 \dots M)) \land x \in [0, j]) \to x \in ℂ$
285	284	3adant3	$⊢ ((φ \land j \in (0 \dots M)) \land x \in [0, j] \land k \in (0 \dots M)) \to x \in ℂ$
286		elfzelz	$⊢ k \in (0 \dots M) \to k \in ℤ$
287	286	zcnd	$⊢ k \in (0 \dots M) \to k \in ℂ$
288	287	3ad2ant3	$⊢ ((φ \land j \in (0 \dots M)) \land x \in [0, j] \land k \in (0 \dots M)) \to k \in ℂ$
289	285 288	subcld	$⊢ ((φ \land j \in (0 \dots M)) \land x \in [0, j] \land k \in (0 \dots M)) \to x - k \in ℂ$
290	8	adantr	$⊢ (φ \land x \in [0, j]) \to P \in ℕ$
291	290 153	syl	$⊢ (φ \land x \in [0, j]) \to P - 1 \in ℕ_{0}$
292	151	adantr	$⊢ (φ \land x \in [0, j]) \to P \in ℕ_{0}$
293	291 292	ifcld	$⊢ (φ \land x \in [0, j]) \to if (k = 0, P - 1, P) \in ℕ_{0}$
294	293	3adant3	$⊢ (φ \land x \in [0, j] \land k \in (0 \dots M)) \to if (k = 0, P - 1, P) \in ℕ_{0}$
295	294	3adant1r	$⊢ ((φ \land j \in (0 \dots M)) \land x \in [0, j] \land k \in (0 \dots M)) \to if (k = 0, P - 1, P) \in ℕ_{0}$
296	289 295	expcld	$⊢ ((φ \land j \in (0 \dots M)) \land x \in [0, j] \land k \in (0 \dots M)) \to {(x - k)}^{if (k = 0, P - 1, P)} \in ℂ$
297		nfv	$⊢ Ⅎ x ((φ \land j \in (0 \dots M)) \land k \in (0 \dots M))$
298	245	adantr	$⊢ (j \in (0 \dots M) \land k \in (0 \dots M)) \to [0, j] \subseteq ℂ$
299		ssid	$⊢ ℂ \subseteq ℂ$
300	299	a1i	$⊢ (j \in (0 \dots M) \land k \in (0 \dots M)) \to ℂ \subseteq ℂ$
301	298 300	idcncfg	$⊢ (j \in (0 \dots M) \land k \in (0 \dots M)) \to (x \in [0, j] ⟼ x) : [0, j] \underset{cn}{⟶} ℂ$
302	287	adantl	$⊢ (j \in (0 \dots M) \land k \in (0 \dots M)) \to k \in ℂ$
303	298 302 300	constcncfg	$⊢ (j \in (0 \dots M) \land k \in (0 \dots M)) \to (x \in [0, j] ⟼ k) : [0, j] \underset{cn}{⟶} ℂ$
304	301 303	subcncf	$⊢ (j \in (0 \dots M) \land k \in (0 \dots M)) \to (x \in [0, j] ⟼ x - k) : [0, j] \underset{cn}{⟶} ℂ$
305	304	adantll	$⊢ ((φ \land j \in (0 \dots M)) \land k \in (0 \dots M)) \to (x \in [0, j] ⟼ x - k) : [0, j] \underset{cn}{⟶} ℂ$
306	154 151	ifcld	$⊢ φ \to if (k = 0, P - 1, P) \in ℕ_{0}$
307		expcncf	$⊢ if (k = 0, P - 1, P) \in ℕ_{0} \to (y \in ℂ ⟼ y^{if (k = 0, P - 1, P)}) : ℂ \underset{cn}{⟶} ℂ$
308	306 307	syl	$⊢ φ \to (y \in ℂ ⟼ y^{if (k = 0, P - 1, P)}) : ℂ \underset{cn}{⟶} ℂ$
309	308	ad2antrr	$⊢ ((φ \land j \in (0 \dots M)) \land k \in (0 \dots M)) \to (y \in ℂ ⟼ y^{if (k = 0, P - 1, P)}) : ℂ \underset{cn}{⟶} ℂ$
310	299	a1i	$⊢ ((φ \land j \in (0 \dots M)) \land k \in (0 \dots M)) \to ℂ \subseteq ℂ$
311		oveq1	$⊢ y = x - k \to y^{if (k = 0, P - 1, P)} = {(x - k)}^{if (k = 0, P - 1, P)}$
312	297 305 309 310 311	cncfcompt2	$⊢ ((φ \land j \in (0 \dots M)) \land k \in (0 \dots M)) \to (x \in [0, j] ⟼ {(x - k)}^{if (k = 0, P - 1, P)}) : [0, j] \underset{cn}{⟶} ℂ$
313	282 283 296 312	fprodcncf	$⊢ (φ \land j \in (0 \dots M)) \to (x \in [0, j] ⟼ \prod_{k = 0}^{M} {(x - k)}^{if (k = 0, P - 1, P)}) : [0, j] \underset{cn}{⟶} ℂ$
314	281 313	eqeltrd	$⊢ (φ \land j \in (0 \dots M)) \to (x \in [0, j] ⟼ F (x)) : [0, j] \underset{cn}{⟶} ℂ$
315	272 314	mulcncf	$⊢ (φ \land j \in (0 \dots M)) \to (x \in [0, j] ⟼ e^{- x} F (x)) : [0, j] \underset{cn}{⟶} ℂ$
316		ioossicc	$⊢ (0, j) \subseteq [0, j]$
317	316	a1i	$⊢ (φ \land j \in (0 \dots M)) \to (0, j) \subseteq [0, j]$
318	299	a1i	$⊢ (φ \land j \in (0 \dots M)) \to ℂ \subseteq ℂ$
319	224	adantlr	$⊢ ((φ \land j \in (0 \dots M)) \land x \in (0, j)) \to e^{- x} F (x) \in ℂ$
320	240 315 317 318 319	cncfmptssg	$⊢ (φ \land j \in (0 \dots M)) \to (x \in (0, j) ⟼ e^{- x} F (x)) : (0, j) \underset{cn}{⟶} ℂ$
321	228 320	eqeltrd	$⊢ (φ \land j \in (0 \dots M)) \to O_{ℝ}^{'} : (0, j) \underset{cn}{⟶} ℂ$
322	7	adantr	$⊢ (φ \land j \in (0 \dots M)) \to ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
323	8	adantr	$⊢ (φ \land j \in (0 \dots M)) \to P \in ℕ$
324	34	adantr	$⊢ (φ \land j \in (0 \dots M)) \to M \in ℕ_{0}$
325		oveq2	$⊢ j = k \to x - j = x - k$
326	325	oveq1d	$⊢ j = k \to {(x - j)}^{P} = {(x - k)}^{P}$
327	326	cbvprodv	$⊢ \prod_{j = 1}^{M} {(x - j)}^{P} = \prod_{k = 1}^{M} {(x - k)}^{P}$
328	327	oveq2i	$⊢ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P} = x^{P - 1} \prod_{k = 1}^{M} {(x - k)}^{P}$
329	328	mpteq2i	$⊢ (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P}) = (x \in ℝ ⟼ x^{P - 1} \prod_{k = 1}^{M} {(x - k)}^{P})$
330	9 329	eqtri	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{k = 1}^{M} {(x - k)}^{P})$
331	17 322 323 324 330 203 206	etransclem18	$⊢ (φ \land j \in (0 \dots M)) \to (x \in (0, j) ⟼ e^{- x} F (x)) \in 𝐿^{1}$
332	228 331	eqeltrd	$⊢ (φ \land j \in (0 \dots M)) \to ℝ D O \in 𝐿^{1}$
333		eqid	$⊢ (x \in ℝ ⟼ G (x)) = (x \in ℝ ⟼ G (x))$
334	6 7 8 34 9 12	etransclem43	$⊢ φ \to G : ℝ \underset{cn}{⟶} ℂ$
335	123 334	eqeltrd	$⊢ φ \to (x \in ℝ ⟼ G (x)) : ℝ \underset{cn}{⟶} ℂ$
336	335	adantr	$⊢ (φ \land j \in (0 \dots M)) \to (x \in ℝ ⟼ G (x)) : ℝ \underset{cn}{⟶} ℂ$
337	121	ad2antrr	$⊢ ((φ \land j \in (0 \dots M)) \land x \in [0, j]) \to G : ℝ ⟶ ℂ$
338	337 279	ffvelrnd	$⊢ ((φ \land j \in (0 \dots M)) \land x \in [0, j]) \to G (x) \in ℂ$
339	333 336 207 318 338	cncfmptssg	$⊢ (φ \land j \in (0 \dots M)) \to (x \in [0, j] ⟼ G (x)) : [0, j] \underset{cn}{⟶} ℂ$
340	272 339	mulcncf	$⊢ (φ \land j \in (0 \dots M)) \to (x \in [0, j] ⟼ e^{- x} G (x)) : [0, j] \underset{cn}{⟶} ℂ$
341	340	negcncfg	$⊢ (φ \land j \in (0 \dots M)) \to (x \in [0, j] ⟼ - e^{- x} G (x)) : [0, j] \underset{cn}{⟶} ℂ$
342	13 341	eqeltrid	$⊢ (φ \land j \in (0 \dots M)) \to O : [0, j] \underset{cn}{⟶} ℂ$
343	203 206 239 321 332 342	ftc2	$⊢ (φ \land j \in (0 \dots M)) \to \int_{(0, j)} O_{ℝ}^{'} (x) d x = O (j) - O (0)$
344		negeq	$⊢ x = j \to - x = - j$
345	344	oveq2d	$⊢ x = j \to e^{- x} = e^{- j}$
346		fveq2	$⊢ x = j \to G (x) = G (j)$
347	345 346	oveq12d	$⊢ x = j \to e^{- x} G (x) = e^{- j} G (j)$
348	347	negeqd	$⊢ x = j \to - e^{- x} G (x) = - e^{- j} G (j)$
349	203	rexrd	$⊢ (φ \land j \in (0 \dots M)) \to 0 \in ℝ^{*}$
350	206	rexrd	$⊢ (φ \land j \in (0 \dots M)) \to j \in ℝ^{*}$
351		ubicc2	$⊢ (0 \in ℝ^{} \land j \in ℝ^{} \land 0 \leq j) \to j \in [0, j]$
352	349 350 239 351	syl3anc	$⊢ (φ \land j \in (0 \dots M)) \to j \in [0, j]$
353	19	a1i	$⊢ j \in (0 \dots M) \to e \in ℂ$
354	205	recnd	$⊢ j \in (0 \dots M) \to j \in ℂ$
355	354	negcld	$⊢ j \in (0 \dots M) \to - j \in ℂ$
356	353 355	cxpcld	$⊢ j \in (0 \dots M) \to e^{- j} \in ℂ$
357	356	adantl	$⊢ (φ \land j \in (0 \dots M)) \to e^{- j} \in ℂ$
358	121	adantr	$⊢ (φ \land j \in (0 \dots M)) \to G : ℝ ⟶ ℂ$
359	358 206	ffvelrnd	$⊢ (φ \land j \in (0 \dots M)) \to G (j) \in ℂ$
360	357 359	mulcld	$⊢ (φ \land j \in (0 \dots M)) \to e^{- j} G (j) \in ℂ$
361	360	negcld	$⊢ (φ \land j \in (0 \dots M)) \to - e^{- j} G (j) \in ℂ$
362	13 348 352 361	fvmptd3	$⊢ (φ \land j \in (0 \dots M)) \to O (j) = - e^{- j} G (j)$
363	13	a1i	$⊢ (φ \land j \in (0 \dots M)) \to O = (x \in [0, j] ⟼ - e^{- x} G (x))$
364		negeq	$⊢ x = 0 \to - x = - 0$
365	364	oveq2d	$⊢ x = 0 \to e^{- x} = e^{- 0}$
366		neg0	$⊢ - 0 = 0$
367	366	oveq2i	$⊢ e^{- 0} = e^{0}$
368		cxp0	$⊢ e \in ℂ \to e^{0} = 1$
369	19 368	ax-mp	$⊢ e^{0} = 1$
370	367 369	eqtri	$⊢ e^{- 0} = 1$
371	365 370	syl6eq	$⊢ x = 0 \to e^{- x} = 1$
372		fveq2	$⊢ x = 0 \to G (x) = G (0)$
373	371 372	oveq12d	$⊢ x = 0 \to e^{- x} G (x) = 1 G (0)$
374		0red	$⊢ φ \to 0 \in ℝ$
375	121 374	ffvelrnd	$⊢ φ \to G (0) \in ℂ$
376	375	mulid2d	$⊢ φ \to 1 G (0) = G (0)$
377	373 376	sylan9eqr	$⊢ (φ \land x = 0) \to e^{- x} G (x) = G (0)$
378	377	negeqd	$⊢ (φ \land x = 0) \to - e^{- x} G (x) = - G (0)$
379	378	adantlr	$⊢ ((φ \land j \in (0 \dots M)) \land x = 0) \to - e^{- x} G (x) = - G (0)$
380		lbicc2	$⊢ (0 \in ℝ^{} \land j \in ℝ^{} \land 0 \leq j) \to 0 \in [0, j]$
381	349 350 239 380	syl3anc	$⊢ (φ \land j \in (0 \dots M)) \to 0 \in [0, j]$
382	375	negcld	$⊢ φ \to - G (0) \in ℂ$
383	382	adantr	$⊢ (φ \land j \in (0 \dots M)) \to - G (0) \in ℂ$
384	363 379 381 383	fvmptd	$⊢ (φ \land j \in (0 \dots M)) \to O (0) = - G (0)$
385	362 384	oveq12d	$⊢ (φ \land j \in (0 \dots M)) \to O (j) - O (0) = - e^{- j} G (j) - (- G (0))$
386	375	adantr	$⊢ (φ \land j \in (0 \dots M)) \to G (0) \in ℂ$
387	361 386	subnegd	$⊢ (φ \land j \in (0 \dots M)) \to - e^{- j} G (j) - (- G (0)) = - e^{- j} G (j) + G (0)$
388	361 386	addcomd	$⊢ (φ \land j \in (0 \dots M)) \to - e^{- j} G (j) + G (0) = G (0) + (- e^{- j} G (j))$
389	386 360	negsubd	$⊢ (φ \land j \in (0 \dots M)) \to G (0) + (- e^{- j} G (j)) = G (0) - e^{- j} G (j)$
390	388 389	eqtrd	$⊢ (φ \land j \in (0 \dots M)) \to - e^{- j} G (j) + G (0) = G (0) - e^{- j} G (j)$
391	385 387 390	3eqtrd	$⊢ (φ \land j \in (0 \dots M)) \to O (j) - O (0) = G (0) - e^{- j} G (j)$
392	237 343 391	3eqtrd	$⊢ (φ \land j \in (0 \dots M)) \to \int_{(0, j)} e^{- x} F (x) d x = G (0) - e^{- j} G (j)$
393	392	oveq2d	$⊢ (φ \land j \in (0 \dots M)) \to A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x = A (j) e^{j} (G (0) - e^{- j} G (j))$
394	31	adantr	$⊢ (φ \land j \in (0 \dots M)) \to Q \in Poly (ℤ)$
395		0zd	$⊢ (φ \land j \in (0 \dots M)) \to 0 \in ℤ$
396	3	coef2	$⊢ (Q \in Poly (ℤ) \land 0 \in ℤ) \to A : ℕ_{0} ⟶ ℤ$
397	394 395 396	syl2anc	$⊢ (φ \land j \in (0 \dots M)) \to A : ℕ_{0} ⟶ ℤ$
398		elfznn0	$⊢ j \in (0 \dots M) \to j \in ℕ_{0}$
399	398	adantl	$⊢ (φ \land j \in (0 \dots M)) \to j \in ℕ_{0}$
400	397 399	ffvelrnd	$⊢ (φ \land j \in (0 \dots M)) \to A (j) \in ℤ$
401	400	zcnd	$⊢ (φ \land j \in (0 \dots M)) \to A (j) \in ℂ$
402	353 354	cxpcld	$⊢ j \in (0 \dots M) \to e^{j} \in ℂ$
403	402	adantl	$⊢ (φ \land j \in (0 \dots M)) \to e^{j} \in ℂ$
404	401 403	mulcld	$⊢ (φ \land j \in (0 \dots M)) \to A (j) e^{j} \in ℂ$
405	404 386 360	subdid	$⊢ (φ \land j \in (0 \dots M)) \to A (j) e^{j} (G (0) - e^{- j} G (j)) = A (j) e^{j} G (0) - A (j) e^{j} e^{- j} G (j)$
406	393 405	eqtrd	$⊢ (φ \land j \in (0 \dots M)) \to A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x = A (j) e^{j} G (0) - A (j) e^{j} e^{- j} G (j)$
407	406	sumeq2dv	$⊢ φ \to \sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x = \sum_{j = 0}^{M} (A (j) e^{j} G (0) - A (j) e^{j} e^{- j} G (j))$
408		fzfid	$⊢ φ \to (0 \dots M) \in Fin$
409	404 386	mulcld	$⊢ (φ \land j \in (0 \dots M)) \to A (j) e^{j} G (0) \in ℂ$
410	404 360	mulcld	$⊢ (φ \land j \in (0 \dots M)) \to A (j) e^{j} e^{- j} G (j) \in ℂ$
411	408 409 410	fsumsub	$⊢ φ \to \sum_{j = 0}^{M} (A (j) e^{j} G (0) - A (j) e^{j} e^{- j} G (j)) = \sum_{j = 0}^{M} A (j) e^{j} G (0) - \sum_{j = 0}^{M} A (j) e^{j} e^{- j} G (j)$
412	2	eqcomd	$⊢ φ \to 0 = Q (e)$
413	3 4	coeid2	$⊢ (Q \in Poly (ℤ) \land e \in ℂ) \to Q (e) = \sum_{j = 0}^{M} A (j) e^{j}$
414	31 19 413	sylancl	$⊢ φ \to Q (e) = \sum_{j = 0}^{M} A (j) e^{j}$
415		cxpexp	$⊢ (e \in ℂ \land j \in ℕ_{0}) \to e^{j} = e^{j}$
416	353 398 415	syl2anc	$⊢ j \in (0 \dots M) \to e^{j} = e^{j}$
417	416	eqcomd	$⊢ j \in (0 \dots M) \to e^{j} = e^{j}$
418	417	oveq2d	$⊢ j \in (0 \dots M) \to A (j) e^{j} = A (j) e^{j}$
419	418	adantl	$⊢ (φ \land j \in (0 \dots M)) \to A (j) e^{j} = A (j) e^{j}$
420	419	sumeq2dv	$⊢ φ \to \sum_{j = 0}^{M} A (j) e^{j} = \sum_{j = 0}^{M} A (j) e^{j}$
421	412 414 420	3eqtrd	$⊢ φ \to 0 = \sum_{j = 0}^{M} A (j) e^{j}$
422	421	oveq1d	$⊢ φ \to 0 \cdot G (0) = \sum_{j = 0}^{M} A (j) e^{j} G (0)$
423	375	mul02d	$⊢ φ \to 0 \cdot G (0) = 0$
424	408 375 404	fsummulc1	$⊢ φ \to \sum_{j = 0}^{M} A (j) e^{j} G (0) = \sum_{j = 0}^{M} A (j) e^{j} G (0)$
425	422 423 424	3eqtr3rd	$⊢ φ \to \sum_{j = 0}^{M} A (j) e^{j} G (0) = 0$
426		fveq2	$⊢ x = j \to (ℝ D^{n} F) (i) (x) = (ℝ D^{n} F) (i) (j)$
427	426	sumeq2sdv	$⊢ x = j \to \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (x) = \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j)$
428		fzfid	$⊢ (φ \land j \in (0 \dots M)) \to (0 \dots R) \in Fin$
429	38	adantlr	$⊢ ((φ \land j \in (0 \dots M)) \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i) : ℝ ⟶ ℂ$
430	206	adantr	$⊢ ((φ \land j \in (0 \dots M)) \land i \in (0 \dots R)) \to j \in ℝ$
431	429 430	ffvelrnd	$⊢ ((φ \land j \in (0 \dots M)) \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i) (j) \in ℂ$
432	428 431	fsumcl	$⊢ (φ \land j \in (0 \dots M)) \to \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j) \in ℂ$
433	12 427 206 432	fvmptd3	$⊢ (φ \land j \in (0 \dots M)) \to G (j) = \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j)$
434	433	oveq2d	$⊢ (φ \land j \in (0 \dots M)) \to e^{- j} G (j) = e^{- j} \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j)$
435	434	oveq2d	$⊢ (φ \land j \in (0 \dots M)) \to A (j) e^{j} e^{- j} G (j) = A (j) e^{j} e^{- j} \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j)$
436	357 432	mulcld	$⊢ (φ \land j \in (0 \dots M)) \to e^{- j} \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j) \in ℂ$
437	401 403 436	mulassd	$⊢ (φ \land j \in (0 \dots M)) \to A (j) e^{j} e^{- j} \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j) = A (j) e^{j} e^{- j} \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j)$
438	369	eqcomi	$⊢ 1 = e^{0}$
439	438	a1i	$⊢ j \in (0 \dots M) \to 1 = e^{0}$
440	354	negidd	$⊢ j \in (0 \dots M) \to j + (- j) = 0$
441	440	eqcomd	$⊢ j \in (0 \dots M) \to 0 = j + (- j)$
442	441	oveq2d	$⊢ j \in (0 \dots M) \to e^{0} = e^{j + (- j)}$
443	57 58	gtneii	$⊢ e \neq 0$
444	443	a1i	$⊢ j \in (0 \dots M) \to e \neq 0$
445	353 444 354 355	cxpaddd	$⊢ j \in (0 \dots M) \to e^{j + (- j)} = e^{j} e^{- j}$
446	439 442 445	3eqtrd	$⊢ j \in (0 \dots M) \to 1 = e^{j} e^{- j}$
447	446	oveq1d	$⊢ j \in (0 \dots M) \to 1 \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j) = e^{j} e^{- j} \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j)$
448	447	adantl	$⊢ (φ \land j \in (0 \dots M)) \to 1 \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j) = e^{j} e^{- j} \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j)$
449	432	mulid2d	$⊢ (φ \land j \in (0 \dots M)) \to 1 \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j) = \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j)$
450	403 357 432	mulassd	$⊢ (φ \land j \in (0 \dots M)) \to e^{j} e^{- j} \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j) = e^{j} e^{- j} \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j)$
451	448 449 450	3eqtr3rd	$⊢ (φ \land j \in (0 \dots M)) \to e^{j} e^{- j} \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j) = \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j)$
452	451	oveq2d	$⊢ (φ \land j \in (0 \dots M)) \to A (j) e^{j} e^{- j} \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j) = A (j) \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j)$
453	428 401 431	fsummulc2	$⊢ (φ \land j \in (0 \dots M)) \to A (j) \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j) = \sum_{i = 0}^{R} A (j) (ℝ D^{n} F) (i) (j)$
454	452 453	eqtrd	$⊢ (φ \land j \in (0 \dots M)) \to A (j) e^{j} e^{- j} \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (j) = \sum_{i = 0}^{R} A (j) (ℝ D^{n} F) (i) (j)$
455	435 437 454	3eqtrd	$⊢ (φ \land j \in (0 \dots M)) \to A (j) e^{j} e^{- j} G (j) = \sum_{i = 0}^{R} A (j) (ℝ D^{n} F) (i) (j)$
456	455	sumeq2dv	$⊢ φ \to \sum_{j = 0}^{M} A (j) e^{j} e^{- j} G (j) = \sum_{j = 0}^{M} \sum_{i = 0}^{R} A (j) (ℝ D^{n} F) (i) (j)$
457		vex	$⊢ j \in V$
458		vex	$⊢ i \in V$
459	457 458	op1std	$⊢ k = ⟨j, i⟩ \to 1^{st} (k) = j$
460	459	fveq2d	$⊢ k = ⟨j, i⟩ \to A (1^{st} (k)) = A (j)$
461	457 458	op2ndd	$⊢ k = ⟨j, i⟩ \to 2^{nd} (k) = i$
462	461	fveq2d	$⊢ k = ⟨j, i⟩ \to (ℝ D^{n} F) (2^{nd} (k)) = (ℝ D^{n} F) (i)$
463	462 459	fveq12d	$⊢ k = ⟨j, i⟩ \to (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) = (ℝ D^{n} F) (i) (j)$
464	460 463	oveq12d	$⊢ k = ⟨j, i⟩ \to A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) = A (j) (ℝ D^{n} F) (i) (j)$
465		fzfid	$⊢ φ \to (0 \dots R) \in Fin$
466	401	adantrr	$⊢ (φ \land (j \in (0 \dots M) \land i \in (0 \dots R))) \to A (j) \in ℂ$
467	431	anasss	$⊢ (φ \land (j \in (0 \dots M) \land i \in (0 \dots R))) \to (ℝ D^{n} F) (i) (j) \in ℂ$
468	466 467	mulcld	$⊢ (φ \land (j \in (0 \dots M) \land i \in (0 \dots R))) \to A (j) (ℝ D^{n} F) (i) (j) \in ℂ$
469	464 408 465 468	fsumxp	$⊢ φ \to \sum_{j = 0}^{M} \sum_{i = 0}^{R} A (j) (ℝ D^{n} F) (i) (j) = \sum_{k \in (0 \dots M) \times (0 \dots R)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))$
470	456 469	eqtrd	$⊢ φ \to \sum_{j = 0}^{M} A (j) e^{j} e^{- j} G (j) = \sum_{k \in (0 \dots M) \times (0 \dots R)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))$
471	425 470	oveq12d	$⊢ φ \to \sum_{j = 0}^{M} A (j) e^{j} G (0) - \sum_{j = 0}^{M} A (j) e^{j} e^{- j} G (j) = 0 - \sum_{k \in (0 \dots M) \times (0 \dots R)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))$
472		df-neg	$⊢ - \sum_{k \in (0 \dots M) \times (0 \dots R)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) = 0 - \sum_{k \in (0 \dots M) \times (0 \dots R)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))$
473	472	eqcomi	$⊢ 0 - \sum_{k \in (0 \dots M) \times (0 \dots R)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) = - \sum_{k \in (0 \dots M) \times (0 \dots R)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))$
474	473	a1i	$⊢ φ \to 0 - \sum_{k \in (0 \dots M) \times (0 \dots R)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) = - \sum_{k \in (0 \dots M) \times (0 \dots R)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))$
475	411 471 474	3eqtrd	$⊢ φ \to \sum_{j = 0}^{M} (A (j) e^{j} G (0) - A (j) e^{j} e^{- j} G (j)) = - \sum_{k \in (0 \dots M) \times (0 \dots R)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))$
476	14 407 475	3eqtrd	$⊢ φ \to L = - \sum_{k \in (0 \dots M) \times (0 \dots R)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))$
477	476	oveq1d	$⊢ φ \to \frac{L}{(P - 1)!} = \frac{- \sum_{k \in (0 \dots M) \times (0 \dots R)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}$

Metamath Proof Explorer

Theorem etransclem46

Proof