Metamath Proof Explorer

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 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ( 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 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
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 mulid2d ⊢ ( 𝑦 ∈ ℂ → ( 1 · ( e ↑𝑐 𝑦 ) ) = ( e ↑𝑐 𝑦 ) )
86 84 85 syl5eq ⊢ ( 𝑦 ∈ ℂ → ( ( 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 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑖 ∈ ( 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 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ ( 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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 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 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 ffvelrnd ⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) ∈ ℂ )
376 375 mulid2d ⊢ ( 𝜑 → ( 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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 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 mulid2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 ) ) ) )