Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  etransclem46 Structured version   Visualization version   GIF version

Theorem etransclem46 44071
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 𝑃, but the right-hand side is a nonzero integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
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
Ref Expression
etransclem46 (𝜑 → (𝐿 / (!‘(𝑃 − 1))) = (-Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))))
Distinct variable groups:   𝐴,𝑖,𝑗,𝑘   𝑖,𝐹,𝑗,𝑘,𝑥   𝑗,𝐺,𝑥   𝑖,𝑀,𝑗,𝑘,𝑥   𝑥,𝑂   𝑃,𝑗,𝑘,𝑥   𝑄,𝑗   𝑅,𝑖,𝑗,𝑘,𝑥   𝜑,𝑖,𝑗,𝑘,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝑃(𝑖)   𝑄(𝑥,𝑖,𝑘)   𝐺(𝑖,𝑘)   𝐿(𝑥,𝑖,𝑗,𝑘)   𝑂(𝑖,𝑗,𝑘)

Proof of Theorem etransclem46
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 etransclem46.l . . . 4 𝐿 = Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥)
21a1i 11 . . 3 (𝜑𝐿 = Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥))
3 etransclem46.h . . . . . . . . . . . . . 14 𝑂 = (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))
43oveq2i 7328 . . . . . . . . . . . . 13 (ℝ D 𝑂) = (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥))))
54a1i 11 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) = (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))))
6 etransclem46.s . . . . . . . . . . . . . 14 (𝜑 → ℝ ∈ {ℝ, ℂ})
76adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → ℝ ∈ {ℝ, ℂ})
8 ere 15877 . . . . . . . . . . . . . . . . . . . 20 e ∈ ℝ
98recni 11069 . . . . . . . . . . . . . . . . . . 19 e ∈ ℂ
109a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → e ∈ ℂ)
11 recn 11041 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
1211negcld 11399 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → -𝑥 ∈ ℂ)
1310, 12cxpcld 25946 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (e↑𝑐-𝑥) ∈ ℂ)
1413adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → (e↑𝑐-𝑥) ∈ ℂ)
15 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
16 fzfid 13773 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → (0...𝑅) ∈ Fin)
17 elfznn0 13429 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (0...𝑅) → 𝑖 ∈ ℕ0)
186adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → ℝ ∈ {ℝ, ℂ})
19 etransclem46.x . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))
2019adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))
21 etransclem46.p . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑃 ∈ ℕ)
2221adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → 𝑃 ∈ ℕ)
23 etransclem46.m . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑀 = (deg‘𝑄)
24 etransclem46.q . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝}))
2524eldifad 3909 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑄 ∈ (Poly‘ℤ))
26 dgrcl 25477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑄 ∈ (Poly‘ℤ) → (deg‘𝑄) ∈ ℕ0)
2725, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (deg‘𝑄) ∈ ℕ0)
2823, 27eqeltrid 2842 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑀 ∈ ℕ0)
2928adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → 𝑀 ∈ ℕ0)
30 etransclem46.f . . . . . . . . . . . . . . . . . . . . . . 23 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃)))
31 simpr 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → 𝑖 ∈ ℕ0)
3218, 20, 22, 29, 30, 31etransclem33 44058 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
3317, 32sylan2 593 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
3433adantlr 712 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
35 simplr 766 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → 𝑥 ∈ ℝ)
3634, 35ffvelcdmd 7002 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ)
3716, 36fsumcl 15524 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ)
38 etransclem46.g . . . . . . . . . . . . . . . . . . 19 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))
3938fvmpt2 6926 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ) → (𝐺𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))
4015, 37, 39syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → (𝐺𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))
4140, 37eqeltrd 2838 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → (𝐺𝑥) ∈ ℂ)
4214, 41mulcld 11075 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · (𝐺𝑥)) ∈ ℂ)
4342negcld 11399 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → -((e↑𝑐-𝑥) · (𝐺𝑥)) ∈ ℂ)
4443adantlr 712 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ ℝ) → -((e↑𝑐-𝑥) · (𝐺𝑥)) ∈ ℂ)
456, 19dvdmsscn 43727 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ℝ ⊆ ℂ)
4645, 21, 30etransclem8 44033 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:ℝ⟶ℂ)
4746ffvelcdmda 7001 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℂ)
4814, 47mulcld 11075 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
4948negcld 11399 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ) → -((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
5049negcld 11399 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → --((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
5150adantlr 712 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ ℝ) → --((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
528a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → e ∈ ℝ)
53 0re 11057 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℝ
54 epos 15995 . . . . . . . . . . . . . . . . . . . . . 22 0 < e
5553, 8, 54ltleii 11178 . . . . . . . . . . . . . . . . . . . . 21 0 ≤ e
5655a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → 0 ≤ e)
57 renegcl 11364 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → -𝑥 ∈ ℝ)
5852, 56, 57recxpcld 25961 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → (e↑𝑐-𝑥) ∈ ℝ)
5958renegcld 11482 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → -(e↑𝑐-𝑥) ∈ ℝ)
6059adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → -(e↑𝑐-𝑥) ∈ ℝ)
61 reelprrecn 11043 . . . . . . . . . . . . . . . . . . . . . 22 ℝ ∈ {ℝ, ℂ}
6261a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → ℝ ∈ {ℝ, ℂ})
63 cnelprrecn 11044 . . . . . . . . . . . . . . . . . . . . . 22 ℂ ∈ {ℝ, ℂ}
6463a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → ℂ ∈ {ℝ, ℂ})
6512adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑥 ∈ ℝ) → -𝑥 ∈ ℂ)
66 neg1rr 12168 . . . . . . . . . . . . . . . . . . . . . 22 -1 ∈ ℝ
6766a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑥 ∈ ℝ) → -1 ∈ ℝ)
689a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℂ → e ∈ ℂ)
69 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
7068, 69cxpcld 25946 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℂ → (e↑𝑐𝑦) ∈ ℂ)
7170adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑦 ∈ ℂ) → (e↑𝑐𝑦) ∈ ℂ)
7211adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
73 1red 11056 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
7462dvmptid 25204 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
7562, 72, 73, 74dvmptneg 25213 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ -𝑥)) = (𝑥 ∈ ℝ ↦ -1))
76 epr 15996 . . . . . . . . . . . . . . . . . . . . . . . 24 e ∈ ℝ+
77 dvcxp2 25977 . . . . . . . . . . . . . . . . . . . . . . . 24 (e ∈ ℝ+ → (ℂ D (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑𝑐𝑦))))
7876, 77ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (ℂ D (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑𝑐𝑦)))
79 loge 25825 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (log‘e) = 1
8079oveq1i 7327 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((log‘e) · (e↑𝑐𝑦)) = (1 · (e↑𝑐𝑦))
8170mulid2d 11073 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ℂ → (1 · (e↑𝑐𝑦)) = (e↑𝑐𝑦))
8280, 81eqtrid 2789 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ℂ → ((log‘e) · (e↑𝑐𝑦)) = (e↑𝑐𝑦))
8382mpteq2ia 5190 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))
8478, 83eqtri 2765 . . . . . . . . . . . . . . . . . . . . . 22 (ℂ D (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))
8584a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)))
86 oveq2 7325 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = -𝑥 → (e↑𝑐𝑦) = (e↑𝑐-𝑥))
8762, 64, 65, 67, 71, 71, 75, 85, 86, 86dvmptco 25219 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ (e↑𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -1)))
8887mptru 1547 . . . . . . . . . . . . . . . . . . 19 (ℝ D (𝑥 ∈ ℝ ↦ (e↑𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -1))
8966a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → -1 ∈ ℝ)
9089recnd 11083 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → -1 ∈ ℂ)
9113, 90mulcomd 11076 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → ((e↑𝑐-𝑥) · -1) = (-1 · (e↑𝑐-𝑥)))
9213mulm1d 11507 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → (-1 · (e↑𝑐-𝑥)) = -(e↑𝑐-𝑥))
9391, 92eqtrd 2777 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → ((e↑𝑐-𝑥) · -1) = -(e↑𝑐-𝑥))
9493mpteq2ia 5190 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -1)) = (𝑥 ∈ ℝ ↦ -(e↑𝑐-𝑥))
9588, 94eqtri 2765 . . . . . . . . . . . . . . . . . 18 (ℝ D (𝑥 ∈ ℝ ↦ (e↑𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ -(e↑𝑐-𝑥))
9695a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (e↑𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ -(e↑𝑐-𝑥)))
9717adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0...𝑅)) → 𝑖 ∈ ℕ0)
98 peano2nn0 12353 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℕ0)
9997, 98syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0...𝑅)) → (𝑖 + 1) ∈ ℕ0)
100 ovex 7350 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 + 1) ∈ V
101 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = (𝑖 + 1) → (𝑗 ∈ ℕ0 ↔ (𝑖 + 1) ∈ ℕ0))
102101anbi2d 629 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = (𝑖 + 1) → ((𝜑𝑗 ∈ ℕ0) ↔ (𝜑 ∧ (𝑖 + 1) ∈ ℕ0)))
103 fveq2 6812 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = (𝑖 + 1) → ((ℝ D𝑛 𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘(𝑖 + 1)))
104103feq1d 6623 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = (𝑖 + 1) → (((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ ↔ ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ))
105102, 104imbi12d 344 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑖 + 1) → (((𝜑𝑗 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ) ↔ ((𝜑 ∧ (𝑖 + 1) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)))
106 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑗 → (𝑖 ∈ ℕ0𝑗 ∈ ℕ0))
107106anbi2d 629 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑗 → ((𝜑𝑖 ∈ ℕ0) ↔ (𝜑𝑗 ∈ ℕ0)))
108 fveq2 6812 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑗 → ((ℝ D𝑛 𝐹)‘𝑖) = ((ℝ D𝑛 𝐹)‘𝑗))
109108feq1d 6623 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑗 → (((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ ↔ ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ))
110107, 109imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = 𝑗 → (((𝜑𝑖 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ) ↔ ((𝜑𝑗 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)))
111110, 32chvarvv 2001 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
112100, 105, 111vtocl 3507 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑖 + 1) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
11399, 112syldan 591 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
114113adantlr 712 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
115114, 35ffvelcdmd 7002 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ)
11616, 115fsumcl 15524 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ)
11721, 28, 30, 38etransclem39 44064 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐺:ℝ⟶ℂ)
118117feqmptd 6877 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺 = (𝑥 ∈ ℝ ↦ (𝐺𝑥)))
119118eqcomd 2743 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑥 ∈ ℝ ↦ (𝐺𝑥)) = 𝐺)
120119oveq2d 7333 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝐺𝑥))) = (ℝ D 𝐺))
121 nfcv 2905 . . . . . . . . . . . . . . . . . . 19 𝑥𝐹
122 elfznn0 13429 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (0...(𝑅 + 1)) → 𝑖 ∈ ℕ0)
123122, 32sylan2 593 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0...(𝑅 + 1))) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
124121, 46, 123, 38etransclem2 44027 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℝ D 𝐺) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
125120, 124eqtrd 2777 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝐺𝑥))) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
1266, 14, 60, 96, 41, 116, 125dvmptmul 25208 . . . . . . . . . . . . . . . 16 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ ℝ ↦ ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥)))))
127116, 14mulcomd 11076 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥)) = ((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
128127oveq2d 7333 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥))) = ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + ((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))))
12914negcld 11399 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → -(e↑𝑐-𝑥) ∈ ℂ)
130129, 41mulcld 11075 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → (-(e↑𝑐-𝑥) · (𝐺𝑥)) ∈ ℂ)
13114, 116mulcld 11075 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) ∈ ℂ)
132130, 131addcomd 11257 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + ((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) = (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑𝑐-𝑥) · (𝐺𝑥))))
133131, 42negsubd 11418 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + -((e↑𝑐-𝑥) · (𝐺𝑥))) = (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) − ((e↑𝑐-𝑥) · (𝐺𝑥))))
13414, 41mulneg1d 11508 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (-(e↑𝑐-𝑥) · (𝐺𝑥)) = -((e↑𝑐-𝑥) · (𝐺𝑥)))
135134oveq2d 7333 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑𝑐-𝑥) · (𝐺𝑥))) = (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + -((e↑𝑐-𝑥) · (𝐺𝑥))))
13614, 116, 41subdid 11511 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥))) = (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) − ((e↑𝑐-𝑥) · (𝐺𝑥))))
137133, 135, 1363eqtr4d 2787 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑𝑐-𝑥) · (𝐺𝑥))) = ((e↑𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥))))
13840oveq2d 7333 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥)) = (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)))
13916, 115, 36fsumsub 15579 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)((((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)) = (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)))
140 fveq2 6812 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑖 → ((ℝ D𝑛 𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘𝑖))
141140fveq1d 6814 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑖 → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))
142103fveq1d 6814 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑖 + 1) → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))
143 fveq2 6812 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 0 → ((ℝ D𝑛 𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘0))
144143fveq1d 6814 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 0 → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D𝑛 𝐹)‘0)‘𝑥))
145 fveq2 6812 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = (𝑅 + 1) → ((ℝ D𝑛 𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘(𝑅 + 1)))
146145fveq1d 6814 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑅 + 1) → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥))
147 etransclem46.r . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑅 = ((𝑀 · 𝑃) + (𝑃 − 1))
14821nnnn0d 12373 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑃 ∈ ℕ0)
14928, 148nn0mulcld 12378 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑀 · 𝑃) ∈ ℕ0)
150 nnm1nn0 12354 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ0)
15121, 150syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑃 − 1) ∈ ℕ0)
152149, 151nn0addcld 12377 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) ∈ ℕ0)
153147, 152eqeltrid 2842 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑅 ∈ ℕ0)
154153adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → 𝑅 ∈ ℕ0)
155154nn0zd 12504 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → 𝑅 ∈ ℤ)
156 peano2nn0 12353 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑅 ∈ ℕ0 → (𝑅 + 1) ∈ ℕ0)
157153, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑅 + 1) ∈ ℕ0)
158 nn0uz 12700 . . . . . . . . . . . . . . . . . . . . . . . 24 0 = (ℤ‘0)
159157, 158eleqtrdi 2848 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑅 + 1) ∈ (ℤ‘0))
160159adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (𝑅 + 1) ∈ (ℤ‘0))
161 elfznn0 13429 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 ∈ (0...(𝑅 + 1)) → 𝑗 ∈ ℕ0)
162161, 111sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
163162adantlr 712 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
164 simplr 766 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → 𝑥 ∈ ℝ)
165163, 164ffvelcdmd 7002 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) ∈ ℂ)
166141, 142, 144, 146, 155, 160, 165telfsum2 15596 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)((((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)) = ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥)))
167138, 139, 1663eqtr2d 2783 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥)) = ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥)))
168167oveq2d 7333 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥))) = ((e↑𝑐-𝑥) · ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥))))
169153nn0red 12374 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑅 ∈ ℝ)
170169ltp1d 11985 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑅 < (𝑅 + 1))
171147, 170eqbrtrrid 5123 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) < (𝑅 + 1))
172 etransclem5 44030 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))
1736, 19, 21, 28, 30, 157, 171, 172etransclem32 44057 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑅 + 1)) = (𝑥 ∈ ℝ ↦ 0))
174173fveq1d 6814 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) = ((𝑥 ∈ ℝ ↦ 0)‘𝑥))
175 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℝ ↦ 0) = (𝑥 ∈ ℝ ↦ 0)
176175fvmpt2 6926 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ ℝ ∧ 0 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ 0)‘𝑥) = 0)
17753, 176mpan2 688 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → ((𝑥 ∈ ℝ ↦ 0)‘𝑥) = 0)
178174, 177sylan9eq 2797 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) = 0)
179 cnex 11032 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℂ ∈ V
180179a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ℂ ∈ V)
181 etransclem46.rex . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ℝ ⊆ ℝ)
1826, 181ssexd 5263 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ℝ ∈ V)
183 elpm2r 8683 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:ℝ⟶ℂ ∧ ℝ ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑pm ℝ))
184180, 182, 46, 181, 183syl22anc 836 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹 ∈ (ℂ ↑pm ℝ))
185 dvn0 25171 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℝ ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm ℝ)) → ((ℝ D𝑛 𝐹)‘0) = 𝐹)
18645, 184, 185syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((ℝ D𝑛 𝐹)‘0) = 𝐹)
187186fveq1d 6814 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((ℝ D𝑛 𝐹)‘0)‘𝑥) = (𝐹𝑥))
188187adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (((ℝ D𝑛 𝐹)‘0)‘𝑥) = (𝐹𝑥))
189178, 188oveq12d 7335 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥)) = (0 − (𝐹𝑥)))
190 df-neg 11288 . . . . . . . . . . . . . . . . . . . . 21 -(𝐹𝑥) = (0 − (𝐹𝑥))
191189, 190eqtr4di 2795 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥)) = -(𝐹𝑥))
192191oveq2d 7333 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥))) = ((e↑𝑐-𝑥) · -(𝐹𝑥)))
193137, 168, 1923eqtrd 2781 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑𝑐-𝑥) · (𝐺𝑥))) = ((e↑𝑐-𝑥) · -(𝐹𝑥)))
194128, 132, 1933eqtrd 2781 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥))) = ((e↑𝑐-𝑥) · -(𝐹𝑥)))
195194mpteq2dva 5187 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ ℝ ↦ ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥)))) = (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -(𝐹𝑥))))
19614, 47mulneg2d 11509 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · -(𝐹𝑥)) = -((e↑𝑐-𝑥) · (𝐹𝑥)))
197196mpteq2dva 5187 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -(𝐹𝑥))) = (𝑥 ∈ ℝ ↦ -((e↑𝑐-𝑥) · (𝐹𝑥))))
198126, 195, 1973eqtrd 2781 . . . . . . . . . . . . . . 15 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ ℝ ↦ -((e↑𝑐-𝑥) · (𝐹𝑥))))
1996, 42, 49, 198dvmptneg 25213 . . . . . . . . . . . . . 14 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ ℝ ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))))
200199adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D (𝑥 ∈ ℝ ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ ℝ ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))))
201 0red 11058 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ)
202 elfzelz 13336 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
203202zred 12506 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
204203adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ)
205201, 204iccssred 13246 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℝ)
206 eqid 2737 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
207206tgioo2 24049 . . . . . . . . . . . . 13 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
208 0red 11058 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 0 ∈ ℝ)
209 iccntr 24067 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ 𝑗 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
210208, 203, 209syl2anc 584 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
211210adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
2127, 44, 51, 200, 205, 207, 206, 211dvmptres2 25209 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ (0(,)𝑗) ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))))
2139a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0(,)𝑗)) → e ∈ ℂ)
214 elioore 13189 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℝ)
215214recnd 11083 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℂ)
216215adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℂ)
217216negcld 11399 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℂ)
218213, 217cxpcld 25946 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0(,)𝑗)) → (e↑𝑐-𝑥) ∈ ℂ)
21946adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0(,)𝑗)) → 𝐹:ℝ⟶ℂ)
220214adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
221219, 220ffvelcdmd 7002 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0(,)𝑗)) → (𝐹𝑥) ∈ ℂ)
222218, 221mulcld 11075 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (0(,)𝑗)) → ((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
223222negnegd 11403 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0(,)𝑗)) → --((e↑𝑐-𝑥) · (𝐹𝑥)) = ((e↑𝑐-𝑥) · (𝐹𝑥)))
224223mpteq2dva 5187 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (0(,)𝑗) ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))))
225224adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))))
2265, 212, 2253eqtrd 2781 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))))
227226fveq1d 6814 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ((ℝ D 𝑂)‘𝑥) = ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥))
228227adantr 481 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((ℝ D 𝑂)‘𝑥) = ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥))
229 simpr 485 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ (0(,)𝑗))
230 eqid 2737 . . . . . . . . . . . 12 (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))
231230fvmpt2 6926 . . . . . . . . . . 11 ((𝑥 ∈ (0(,)𝑗) ∧ ((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥) = ((e↑𝑐-𝑥) · (𝐹𝑥)))
232229, 222, 231syl2anc 584 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0(,)𝑗)) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥) = ((e↑𝑐-𝑥) · (𝐹𝑥)))
233232adantlr 712 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥) = ((e↑𝑐-𝑥) · (𝐹𝑥)))
234228, 233eqtr2d 2778 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑𝑐-𝑥) · (𝐹𝑥)) = ((ℝ D 𝑂)‘𝑥))
235234itgeq2dv 25029 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥 = ∫(0(,)𝑗)((ℝ D 𝑂)‘𝑥) d𝑥)
236 elfzle1 13339 . . . . . . . . 9 (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
237236adantl 482 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ≤ 𝑗)
238 eqid 2737 . . . . . . . . . 10 (𝑥 ∈ (0[,]𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) = (𝑥 ∈ (0[,]𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))
239 eqidd 2738 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)) = (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)))
24086adantl 482 . . . . . . . . . . . . . . . 16 (((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) ∧ 𝑦 = -𝑥) → (e↑𝑐𝑦) = (e↑𝑐-𝑥))
241208, 203iccssred 13246 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → (0[,]𝑗) ⊆ ℝ)
242 ax-resscn 11008 . . . . . . . . . . . . . . . . . . 19 ℝ ⊆ ℂ
243241, 242sstrdi 3943 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → (0[,]𝑗) ⊆ ℂ)
244243sselda 3931 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℂ)
245244negcld 11399 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → -𝑥 ∈ ℂ)
2469a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → e ∈ ℂ)
247 negcl 11301 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → -𝑥 ∈ ℂ)
248246, 247cxpcld 25946 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → (e↑𝑐-𝑥) ∈ ℂ)
249244, 248syl 17 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑𝑐-𝑥) ∈ ℂ)
250239, 240, 245, 249fvmptd 6922 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥) = (e↑𝑐-𝑥))
251250eqcomd 2743 . . . . . . . . . . . . . 14 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑𝑐-𝑥) = ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥))
252251adantll 711 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑𝑐-𝑥) = ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥))
253252mpteq2dva 5187 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (e↑𝑐-𝑥)) = (𝑥 ∈ (0[,]𝑗) ↦ ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥)))
254 mnfxr 11112 . . . . . . . . . . . . . . . . . 18 -∞ ∈ ℝ*
255254a1i 11 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → -∞ ∈ ℝ*)
256 0red 11058 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → 0 ∈ ℝ)
257 rpxr 12819 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → e ∈ ℝ*)
258 rpgt0 12822 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → 0 < e)
259255, 256, 257, 258gtnelioc 43279 . . . . . . . . . . . . . . . 16 (e ∈ ℝ+ → ¬ e ∈ (-∞(,]0))
26076, 259ax-mp 5 . . . . . . . . . . . . . . 15 ¬ e ∈ (-∞(,]0)
261 eldif 3907 . . . . . . . . . . . . . . 15 (e ∈ (ℂ ∖ (-∞(,]0)) ↔ (e ∈ ℂ ∧ ¬ e ∈ (-∞(,]0)))
2629, 260, 261mpbir2an 708 . . . . . . . . . . . . . 14 e ∈ (ℂ ∖ (-∞(,]0))
263 cxpcncf2 43690 . . . . . . . . . . . . . 14 (e ∈ (ℂ ∖ (-∞(,]0)) → (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)) ∈ (ℂ–cn→ℂ))
264262, 263mp1i 13 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)) ∈ (ℂ–cn→ℂ))
265 eqid 2737 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) = (𝑥 ∈ (0[,]𝑗) ↦ -𝑥)
266265negcncf 24168 . . . . . . . . . . . . . . 15 ((0[,]𝑗) ⊆ ℂ → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
267243, 266syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
268267adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
269264, 268cncfmpt1f 24160 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
270253, 269eqeltrd 2838 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (e↑𝑐-𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
271242a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → ℝ ⊆ ℂ)
27221ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ)
27328ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑀 ∈ ℕ0)
274 etransclem6 44031 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦𝑘)↑𝑃)))
27530, 274eqtri 2765 . . . . . . . . . . . . . 14 𝐹 = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦𝑘)↑𝑃)))
276241sselda 3931 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℝ)
277276adantll 711 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℝ)
278271, 272, 273, 275, 277etransclem13 44038 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝐹𝑥) = ∏𝑘 ∈ (0...𝑀)((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))
279278mpteq2dva 5187 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐹𝑥)) = (𝑥 ∈ (0[,]𝑗) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))))
280243adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℂ)
281 fzfid 13773 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (0...𝑀) ∈ Fin)
282277recnd 11083 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℂ)
2832823adant3 1131 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → 𝑥 ∈ ℂ)
284 elfzelz 13336 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ)
285284zcnd 12507 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ)
2862853ad2ant3 1134 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
287283, 286subcld 11412 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥𝑘) ∈ ℂ)
28821adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ)
289288, 150syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0[,]𝑗)) → (𝑃 − 1) ∈ ℕ0)
290148adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ0)
291289, 290ifcld 4517 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0[,]𝑗)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0)
2922913adant3 1131 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0)
2932923adant1r 1176 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0)
294287, 293expcld 13944 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) ∈ ℂ)
295 nfv 1916 . . . . . . . . . . . . . 14 𝑥((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀))
296243adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℂ)
297 ssid 3953 . . . . . . . . . . . . . . . . . 18 ℂ ⊆ ℂ
298297a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
299296, 298idcncfg 43664 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ 𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
300285adantl 482 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
301296, 300, 298constcncfg 43663 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ 𝑘) ∈ ((0[,]𝑗)–cn→ℂ))
302299, 301subcncf 24692 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝑥𝑘)) ∈ ((0[,]𝑗)–cn→ℂ))
303302adantll 711 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝑥𝑘)) ∈ ((0[,]𝑗)–cn→ℂ))
304151, 148ifcld 4517 . . . . . . . . . . . . . . . 16 (𝜑 → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0)
305 expcncf 24172 . . . . . . . . . . . . . . . 16 (if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0 → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
306304, 305syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
307306ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
308297a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
309 oveq1 7324 . . . . . . . . . . . . . 14 (𝑦 = (𝑥𝑘) → (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) = ((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))
310295, 303, 307, 308, 309cncfcompt2 24154 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((0[,]𝑗)–cn→ℂ))
311280, 281, 294, 310fprodcncf 43691 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((0[,]𝑗)–cn→ℂ))
312279, 311eqeltrd 2838 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐹𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
313270, 312mulcncf 24693 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
314 ioossicc 13245 . . . . . . . . . . 11 (0(,)𝑗) ⊆ (0[,]𝑗)
315314a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (0(,)𝑗) ⊆ (0[,]𝑗))
316297a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
317222adantlr 712 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
318238, 313, 315, 316, 317cncfmptssg 43662 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) ∈ ((0(,)𝑗)–cn→ℂ))
319226, 318eqeltrd 2838 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) ∈ ((0(,)𝑗)–cn→ℂ))
32019adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))
32121adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑃 ∈ ℕ)
32228adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℕ0)
323 oveq2 7325 . . . . . . . . . . . . . . 15 (𝑗 = 𝑘 → (𝑥𝑗) = (𝑥𝑘))
324323oveq1d 7332 . . . . . . . . . . . . . 14 (𝑗 = 𝑘 → ((𝑥𝑗)↑𝑃) = ((𝑥𝑘)↑𝑃))
325324cbvprodv 15705 . . . . . . . . . . . . 13 𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃) = ∏𝑘 ∈ (1...𝑀)((𝑥𝑘)↑𝑃)
326325oveq2i 7328 . . . . . . . . . . . 12 ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃)) = ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥𝑘)↑𝑃))
327326mpteq2i 5192 . . . . . . . . . . 11 (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥𝑘)↑𝑃)))
32830, 327eqtri 2765 . . . . . . . . . 10 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥𝑘)↑𝑃)))
3297, 320, 321, 322, 328, 201, 204etransclem18 44043 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) ∈ 𝐿1)
330226, 329eqeltrd 2838 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) ∈ 𝐿1)
331 eqid 2737 . . . . . . . . . . . 12 (𝑥 ∈ ℝ ↦ (𝐺𝑥)) = (𝑥 ∈ ℝ ↦ (𝐺𝑥))
3326, 19, 21, 28, 30, 38etransclem43 44068 . . . . . . . . . . . . . 14 (𝜑𝐺 ∈ (ℝ–cn→ℂ))
333119, 332eqeltrd 2838 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℝ ↦ (𝐺𝑥)) ∈ (ℝ–cn→ℂ))
334333adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ ℝ ↦ (𝐺𝑥)) ∈ (ℝ–cn→ℂ))
335117ad2antrr 723 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝐺:ℝ⟶ℂ)
336335, 277ffvelcdmd 7002 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝐺𝑥) ∈ ℂ)
337331, 334, 205, 316, 336cncfmptssg 43662 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐺𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
338270, 337mulcncf 24693 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((e↑𝑐-𝑥) · (𝐺𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
339338negcncfg 43672 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
3403, 339eqeltrid 2842 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑂 ∈ ((0[,]𝑗)–cn→ℂ))
341201, 204, 237, 319, 330, 340ftc2 25291 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((ℝ D 𝑂)‘𝑥) d𝑥 = ((𝑂𝑗) − (𝑂‘0)))
342 negeq 11293 . . . . . . . . . . . . 13 (𝑥 = 𝑗 → -𝑥 = -𝑗)
343342oveq2d 7333 . . . . . . . . . . . 12 (𝑥 = 𝑗 → (e↑𝑐-𝑥) = (e↑𝑐-𝑗))
344 fveq2 6812 . . . . . . . . . . . 12 (𝑥 = 𝑗 → (𝐺𝑥) = (𝐺𝑗))
345343, 344oveq12d 7335 . . . . . . . . . . 11 (𝑥 = 𝑗 → ((e↑𝑐-𝑥) · (𝐺𝑥)) = ((e↑𝑐-𝑗) · (𝐺𝑗)))
346345negeqd 11295 . . . . . . . . . 10 (𝑥 = 𝑗 → -((e↑𝑐-𝑥) · (𝐺𝑥)) = -((e↑𝑐-𝑗) · (𝐺𝑗)))
347201rexrd 11105 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ*)
348204rexrd 11105 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ*)
349 ubicc2 13277 . . . . . . . . . . 11 ((0 ∈ ℝ*𝑗 ∈ ℝ* ∧ 0 ≤ 𝑗) → 𝑗 ∈ (0[,]𝑗))
350347, 348, 237, 349syl3anc 1370 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0[,]𝑗))
3519a1i 11 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → e ∈ ℂ)
352203recnd 11083 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
353352negcld 11399 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → -𝑗 ∈ ℂ)
354351, 353cxpcld 25946 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (e↑𝑐-𝑗) ∈ ℂ)
355354adantl 482 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (e↑𝑐-𝑗) ∈ ℂ)
356117adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → 𝐺:ℝ⟶ℂ)
357356, 204ffvelcdmd 7002 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐺𝑗) ∈ ℂ)
358355, 357mulcld 11075 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → ((e↑𝑐-𝑗) · (𝐺𝑗)) ∈ ℂ)
359358negcld 11399 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → -((e↑𝑐-𝑗) · (𝐺𝑗)) ∈ ℂ)
3603, 346, 350, 359fvmptd3 6938 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑂𝑗) = -((e↑𝑐-𝑗) · (𝐺𝑗)))
3613a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑂 = (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥))))
362 negeq 11293 . . . . . . . . . . . . . . . 16 (𝑥 = 0 → -𝑥 = -0)
363362oveq2d 7333 . . . . . . . . . . . . . . 15 (𝑥 = 0 → (e↑𝑐-𝑥) = (e↑𝑐-0))
364 neg0 11347 . . . . . . . . . . . . . . . . 17 -0 = 0
365364oveq2i 7328 . . . . . . . . . . . . . . . 16 (e↑𝑐-0) = (e↑𝑐0)
366 cxp0 25908 . . . . . . . . . . . . . . . . 17 (e ∈ ℂ → (e↑𝑐0) = 1)
3679, 366ax-mp 5 . . . . . . . . . . . . . . . 16 (e↑𝑐0) = 1
368365, 367eqtri 2765 . . . . . . . . . . . . . . 15 (e↑𝑐-0) = 1
369363, 368eqtrdi 2793 . . . . . . . . . . . . . 14 (𝑥 = 0 → (e↑𝑐-𝑥) = 1)
370 fveq2 6812 . . . . . . . . . . . . . 14 (𝑥 = 0 → (𝐺𝑥) = (𝐺‘0))
371369, 370oveq12d 7335 . . . . . . . . . . . . 13 (𝑥 = 0 → ((e↑𝑐-𝑥) · (𝐺𝑥)) = (1 · (𝐺‘0)))
372 0red 11058 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ ℝ)
373117, 372ffvelcdmd 7002 . . . . . . . . . . . . . 14 (𝜑 → (𝐺‘0) ∈ ℂ)
374373mulid2d 11073 . . . . . . . . . . . . 13 (𝜑 → (1 · (𝐺‘0)) = (𝐺‘0))
375371, 374sylan9eqr 2799 . . . . . . . . . . . 12 ((𝜑𝑥 = 0) → ((e↑𝑐-𝑥) · (𝐺𝑥)) = (𝐺‘0))
376375negeqd 11295 . . . . . . . . . . 11 ((𝜑𝑥 = 0) → -((e↑𝑐-𝑥) · (𝐺𝑥)) = -(𝐺‘0))
377376adantlr 712 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 = 0) → -((e↑𝑐-𝑥) · (𝐺𝑥)) = -(𝐺‘0))
378 lbicc2 13276 . . . . . . . . . . 11 ((0 ∈ ℝ*𝑗 ∈ ℝ* ∧ 0 ≤ 𝑗) → 0 ∈ (0[,]𝑗))
379347, 348, 237, 378syl3anc 1370 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ (0[,]𝑗))
380373negcld 11399 . . . . . . . . . . 11 (𝜑 → -(𝐺‘0) ∈ ℂ)
381380adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → -(𝐺‘0) ∈ ℂ)
382361, 377, 379, 381fvmptd 6922 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑂‘0) = -(𝐺‘0))
383360, 382oveq12d 7335 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑂𝑗) − (𝑂‘0)) = (-((e↑𝑐-𝑗) · (𝐺𝑗)) − -(𝐺‘0)))
384373adantr 481 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐺‘0) ∈ ℂ)
385359, 384subnegd 11419 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (-((e↑𝑐-𝑗) · (𝐺𝑗)) − -(𝐺‘0)) = (-((e↑𝑐-𝑗) · (𝐺𝑗)) + (𝐺‘0)))
386359, 384addcomd 11257 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (-((e↑𝑐-𝑗) · (𝐺𝑗)) + (𝐺‘0)) = ((𝐺‘0) + -((e↑𝑐-𝑗) · (𝐺𝑗))))
387384, 358negsubd 11418 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐺‘0) + -((e↑𝑐-𝑗) · (𝐺𝑗))) = ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗))))
388386, 387eqtrd 2777 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (-((e↑𝑐-𝑗) · (𝐺𝑗)) + (𝐺‘0)) = ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗))))
389383, 385, 3883eqtrd 2781 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑂𝑗) − (𝑂‘0)) = ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗))))
390235, 341, 3893eqtrd 2781 . . . . . 6 ((𝜑𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥 = ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗))))
391390oveq2d 7333 . . . . 5 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥) = (((𝐴𝑗) · (e↑𝑐𝑗)) · ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗)))))
39225adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑄 ∈ (Poly‘ℤ))
393 0zd 12411 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ ℤ)
394 etransclem46.a . . . . . . . . . . 11 𝐴 = (coeff‘𝑄)
395394coef2 25475 . . . . . . . . . 10 ((𝑄 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → 𝐴:ℕ0⟶ℤ)
396392, 393, 395syl2anc 584 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → 𝐴:ℕ0⟶ℤ)
397 elfznn0 13429 . . . . . . . . . 10 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0)
398397adantl 482 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ0)
399396, 398ffvelcdmd 7002 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐴𝑗) ∈ ℤ)
400399zcnd 12507 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐴𝑗) ∈ ℂ)
401351, 352cxpcld 25946 . . . . . . . 8 (𝑗 ∈ (0...𝑀) → (e↑𝑐𝑗) ∈ ℂ)
402401adantl 482 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → (e↑𝑐𝑗) ∈ ℂ)
403400, 402mulcld 11075 . . . . . 6 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · (e↑𝑐𝑗)) ∈ ℂ)
404403, 384, 358subdid 11511 . . . . 5 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗)))) = ((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))))
405391, 404eqtrd 2777 . . . 4 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥) = ((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))))
406405sumeq2dv 15494 . . 3 (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥) = Σ𝑗 ∈ (0...𝑀)((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))))
407 fzfid 13773 . . . . 5 (𝜑 → (0...𝑀) ∈ Fin)
408403, 384mulcld 11075 . . . . 5 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) ∈ ℂ)
409403, 358mulcld 11075 . . . . 5 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) ∈ ℂ)
410407, 408, 409fsumsub 15579 . . . 4 (𝜑 → Σ𝑗 ∈ (0...𝑀)((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))) = (Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))))
411 etransclem46.qe0 . . . . . . . . 9 (𝜑 → (𝑄‘e) = 0)
412411eqcomd 2743 . . . . . . . 8 (𝜑 → 0 = (𝑄‘e))
413394, 23coeid2 25483 . . . . . . . . 9 ((𝑄 ∈ (Poly‘ℤ) ∧ e ∈ ℂ) → (𝑄‘e) = Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑗)))
41425, 9, 413sylancl 586 . . . . . . . 8 (𝜑 → (𝑄‘e) = Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑗)))
415 cxpexp 25906 . . . . . . . . . . . . 13 ((e ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (e↑𝑐𝑗) = (e↑𝑗))
416351, 397, 415syl2anc 584 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (e↑𝑐𝑗) = (e↑𝑗))
417416eqcomd 2743 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑀) → (e↑𝑗) = (e↑𝑐𝑗))
418417oveq2d 7333 . . . . . . . . . 10 (𝑗 ∈ (0...𝑀) → ((𝐴𝑗) · (e↑𝑗)) = ((𝐴𝑗) · (e↑𝑐𝑗)))
419418adantl 482 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · (e↑𝑗)) = ((𝐴𝑗) · (e↑𝑐𝑗)))
420419sumeq2dv 15494 . . . . . . . 8 (𝜑 → Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑗)) = Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑐𝑗)))
421412, 414, 4203eqtrd 2781 . . . . . . 7 (𝜑 → 0 = Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑐𝑗)))
422421oveq1d 7332 . . . . . 6 (𝜑 → (0 · (𝐺‘0)) = (Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)))
423373mul02d 11253 . . . . . 6 (𝜑 → (0 · (𝐺‘0)) = 0)
424407, 373, 403fsummulc1 15576 . . . . . 6 (𝜑 → (Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) = Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)))
425422, 423, 4243eqtr3rd 2786 . . . . 5 (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) = 0)
426 fveq2 6812 . . . . . . . . . . . 12 (𝑥 = 𝑗 → (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) = (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
427426sumeq2sdv 15495 . . . . . . . . . . 11 (𝑥 = 𝑗 → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
428 fzfid 13773 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (0...𝑅) ∈ Fin)
42933adantlr 712 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
430204adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → 𝑗 ∈ ℝ)
431429, 430ffvelcdmd 7002 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
432428, 431fsumcl 15524 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
43338, 427, 204, 432fvmptd3 6938 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐺𝑗) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
434433oveq2d 7333 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((e↑𝑐-𝑗) · (𝐺𝑗)) = ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
435434oveq2d 7333 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) = (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))))
436355, 432mulcld 11075 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) ∈ ℂ)
437400, 402, 436mulassd 11078 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))) = ((𝐴𝑗) · ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))))
438367eqcomi 2746 . . . . . . . . . . . . . . 15 1 = (e↑𝑐0)
439438a1i 11 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → 1 = (e↑𝑐0))
440352negidd 11402 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → (𝑗 + -𝑗) = 0)
441440eqcomd 2743 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 0 = (𝑗 + -𝑗))
442441oveq2d 7333 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (e↑𝑐0) = (e↑𝑐(𝑗 + -𝑗)))
44353, 54gtneii 11167 . . . . . . . . . . . . . . . 16 e ≠ 0
444443a1i 11 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → e ≠ 0)
445351, 444, 352, 353cxpaddd 25955 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (e↑𝑐(𝑗 + -𝑗)) = ((e↑𝑐𝑗) · (e↑𝑐-𝑗)))
446439, 442, 4453eqtrd 2781 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 1 = ((e↑𝑐𝑗) · (e↑𝑐-𝑗)))
447446oveq1d 7332 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = (((e↑𝑐𝑗) · (e↑𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
448447adantl 482 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = (((e↑𝑐𝑗) · (e↑𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
449432mulid2d 11073 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
450402, 355, 432mulassd 11078 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (((e↑𝑐𝑗) · (e↑𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))))
451448, 449, 4503eqtr3rd 2786 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
452451oveq2d 7333 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))) = ((𝐴𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
453428, 400, 431fsummulc2 15575 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
454452, 453eqtrd 2777 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))) = Σ𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
455435, 437, 4543eqtrd 2781 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) = Σ𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
456455sumeq2dv 15494 . . . . . 6 (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) = Σ𝑗 ∈ (0...𝑀𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
457 vex 3445 . . . . . . . . . 10 𝑗 ∈ V
458 vex 3445 . . . . . . . . . 10 𝑖 ∈ V
459457, 458op1std 7888 . . . . . . . . 9 (𝑘 = ⟨𝑗, 𝑖⟩ → (1st𝑘) = 𝑗)
460459fveq2d 6816 . . . . . . . 8 (𝑘 = ⟨𝑗, 𝑖⟩ → (𝐴‘(1st𝑘)) = (𝐴𝑗))
461457, 458op2ndd 7889 . . . . . . . . . 10 (𝑘 = ⟨𝑗, 𝑖⟩ → (2nd𝑘) = 𝑖)
462461fveq2d 6816 . . . . . . . . 9 (𝑘 = ⟨𝑗, 𝑖⟩ → ((ℝ D𝑛 𝐹)‘(2nd𝑘)) = ((ℝ D𝑛 𝐹)‘𝑖))
463462, 459fveq12d 6819 . . . . . . . 8 (𝑘 = ⟨𝑗, 𝑖⟩ → (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) = (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
464460, 463oveq12d 7335 . . . . . . 7 (𝑘 = ⟨𝑗, 𝑖⟩ → ((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) = ((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
465 fzfid 13773 . . . . . . 7 (𝜑 → (0...𝑅) ∈ Fin)
466400adantrr 714 . . . . . . . 8 ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → (𝐴𝑗) ∈ ℂ)
467431anasss 467 . . . . . . . 8 ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
468466, 467mulcld 11075 . . . . . . 7 ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → ((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) ∈ ℂ)
469464, 407, 465, 468fsumxp 15563 . . . . . 6 (𝜑 → Σ𝑗 ∈ (0...𝑀𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
470456, 469eqtrd 2777 . . . . 5 (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) = Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
471425, 470oveq12d 7335 . . . 4 (𝜑 → (Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))) = (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)))))
472 df-neg 11288 . . . . . 6 𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) = (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
473472eqcomi 2746 . . . . 5 (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)))) = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)))
474473a1i 11 . . . 4 (𝜑 → (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)))) = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
475410, 471, 4743eqtrd 2781 . . 3 (𝜑 → Σ𝑗 ∈ (0...𝑀)((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))) = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
4762, 406, 4753eqtrd 2781 . 2 (𝜑𝐿 = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
477476oveq1d 7332 1 (𝜑 → (𝐿 / (!‘(𝑃 − 1))) = (-Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1086   = wceq 1540  wtru 1541  wcel 2105  wne 2941  Vcvv 3441  cdif 3894  wss 3897  ifcif 4471  {csn 4571  {cpr 4573  cop 4577   class class class wbr 5087  cmpt 5170   × cxp 5606  ran crn 5609  wf 6462  cfv 6466  (class class class)co 7317  1st c1st 7876  2nd c2nd 7877  pm cpm 8666  cc 10949  cr 10950  0cc0 10951  1c1 10952   + caddc 10954   · cmul 10956  -∞cmnf 11087  *cxr 11088   < clt 11089  cle 11090  cmin 11285  -cneg 11286   / cdiv 11712  cn 12053  0cn0 12313  cz 12399  cuz 12662  +crp 12810  (,)cioo 13159  (,]cioc 13160  [,]cicc 13162  ...cfz 13319  cexp 13862  !cfa 14067  Σcsu 15476  cprod 15694  eceu 15851  t crest 17208  TopOpenctopn 17209  topGenctg 17225  fldccnfld 20680  intcnt 22251  cnccncf 24122  𝐿1cibl 24864  citg 24865  0𝑝c0p 24916   D cdv 25110   D𝑛 cdvn 25111  Polycply 25428  coeffccoe 25430  degcdgr 25431  logclog 25793  𝑐ccxp 25794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7630  ax-inf2 9477  ax-cc 10271  ax-cnex 11007  ax-resscn 11008  ax-1cn 11009  ax-icn 11010  ax-addcl 11011  ax-addrcl 11012  ax-mulcl 11013  ax-mulrcl 11014  ax-mulcom 11015  ax-addass 11016  ax-mulass 11017  ax-distr 11018  ax-i2m1 11019  ax-1ne0 11020  ax-1rid 11021  ax-rnegex 11022  ax-rrecex 11023  ax-cnre 11024  ax-pre-lttri 11025  ax-pre-lttrn 11026  ax-pre-ltadd 11027  ax-pre-mulgt0 11028  ax-pre-sup 11029  ax-addf 11030  ax-mulf 11031
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-symdif 4187  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-tp 4576  df-op 4578  df-uni 4851  df-int 4893  df-iun 4939  df-iin 4940  df-disj 5053  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5563  df-se 5564  df-we 5565  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-pred 6225  df-ord 6292  df-on 6293  df-lim 6294  df-suc 6295  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-fv 6474  df-isom 6475  df-riota 7274  df-ov 7320  df-oprab 7321  df-mpo 7322  df-of 7575  df-ofr 7576  df-om 7760  df-1st 7878  df-2nd 7879  df-supp 8027  df-frecs 8146  df-wrecs 8177  df-recs 8251  df-rdg 8290  df-1o 8346  df-2o 8347  df-oadd 8350  df-omul 8351  df-er 8548  df-map 8667  df-pm 8668  df-ixp 8736  df-en 8784  df-dom 8785  df-sdom 8786  df-fin 8787  df-fsupp 9206  df-fi 9247  df-sup 9278  df-inf 9279  df-oi 9346  df-dju 9737  df-card 9775  df-acn 9778  df-pnf 11091  df-mnf 11092  df-xr 11093  df-ltxr 11094  df-le 11095  df-sub 11287  df-neg 11288  df-div 11713  df-nn 12054  df-2 12116  df-3 12117  df-4 12118  df-5 12119  df-6 12120  df-7 12121  df-8 12122  df-9 12123  df-n0 12314  df-z 12400  df-dec 12518  df-uz 12663  df-q 12769  df-rp 12811  df-xneg 12928  df-xadd 12929  df-xmul 12930  df-ioo 13163  df-ioc 13164  df-ico 13165  df-icc 13166  df-fz 13320  df-fzo 13463  df-fl 13592  df-mod 13670  df-seq 13802  df-exp 13863  df-fac 14068  df-bc 14097  df-hash 14125  df-shft 14857  df-cj 14889  df-re 14890  df-im 14891  df-sqrt 15025  df-abs 15026  df-limsup 15259  df-clim 15276  df-rlim 15277  df-sum 15477  df-prod 15695  df-ef 15856  df-e 15857  df-sin 15858  df-cos 15859  df-tan 15860  df-pi 15861  df-struct 16925  df-sets 16942  df-slot 16960  df-ndx 16972  df-base 16990  df-ress 17019  df-plusg 17052  df-mulr 17053  df-starv 17054  df-sca 17055  df-vsca 17056  df-ip 17057  df-tset 17058  df-ple 17059  df-ds 17061  df-unif 17062  df-hom 17063  df-cco 17064  df-rest 17210  df-topn 17211  df-0g 17229  df-gsum 17230  df-topgen 17231  df-pt 17232  df-prds 17235  df-xrs 17290  df-qtop 17295  df-imas 17296  df-xps 17298  df-mre 17372  df-mrc 17373  df-acs 17375  df-mgm 18403  df-sgrp 18452  df-mnd 18463  df-submnd 18508  df-mulg 18777  df-cntz 18999  df-cmn 19463  df-psmet 20672  df-xmet 20673  df-met 20674  df-bl 20675  df-mopn 20676  df-fbas 20677  df-fg 20678  df-cnfld 20681  df-top 22126  df-topon 22143  df-topsp 22165  df-bases 22179  df-cld 22253  df-ntr 22254  df-cls 22255  df-nei 22332  df-lp 22370  df-perf 22371  df-cn 22461  df-cnp 22462  df-haus 22549  df-cmp 22621  df-tx 22796  df-hmeo 22989  df-fil 23080  df-fm 23172  df-flim 23173  df-flf 23174  df-xms 23556  df-ms 23557  df-tms 23558  df-cncf 24124  df-ovol 24711  df-vol 24712  df-mbf 24866  df-itg1 24867  df-itg2 24868  df-ibl 24869  df-itg 24870  df-0p 24917  df-limc 25113  df-dv 25114  df-dvn 25115  df-ply 25432  df-coe 25434  df-dgr 25435  df-log 25795  df-cxp 25796
This theorem is referenced by:  etransclem47  44072
  Copyright terms: Public domain W3C validator