Theorem 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	⊢ ( 𝜑 → 𝑄 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) )
	etransclem46.qe0	⊢ ( 𝜑 → ( 𝑄 ‘ e ) = 0 )
	etransclem46.a	⊢ 𝐴 = ( coeff ‘ 𝑄 )
	etransclem46.m	⊢ 𝑀 = ( deg ‘ 𝑄 )
	etransclem46.rex	⊢ ( 𝜑 → ℝ ⊆ ℝ )
	etransclem46.s	⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
	etransclem46.x	⊢ ( 𝜑 → ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
	etransclem46.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
	etransclem46.f	⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
	etransclem46.l	⊢ 𝐿 = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐴 ‘ 𝑗 ) · ( e ↑𝑐 𝑗 ) ) · ∫ ( 0 (,) 𝑗 ) ( ( e ↑𝑐 - 𝑥 ) · ( 𝐹 ‘ 𝑥 ) ) d 𝑥 )
	etransclem46.r	⊢ 𝑅 = ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) )
	etransclem46.g	⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... 𝑅 ) ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) )
	etransclem46.h	⊢ 𝑂 = ( 𝑥 ∈ ( 0 [,] 𝑗 ) ↦ - ( ( e ↑𝑐 - 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) )
Assertion	etransclem46	⊢ ( 𝜑 → ( 𝐿 / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( - Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )

Proof

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