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 45808
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 7430 . . . . . . . . . . . . 13 (ℝ D 𝑂) = (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥))))
54a1i 11 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) = (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))))
6 etransclem46.s . . . . . . . . . . . . . 14 (𝜑 → ℝ ∈ {ℝ, ℂ})
76adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → ℝ ∈ {ℝ, ℂ})
8 ere 16074 . . . . . . . . . . . . . . . . . . . 20 e ∈ ℝ
98recni 11265 . . . . . . . . . . . . . . . . . . 19 e ∈ ℂ
109a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → e ∈ ℂ)
11 recn 11235 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
1211negcld 11595 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → -𝑥 ∈ ℂ)
1310, 12cxpcld 26692 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (e↑𝑐-𝑥) ∈ ℂ)
1413adantl 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → (e↑𝑐-𝑥) ∈ ℂ)
15 simpr 483 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
16 fzfid 13979 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → (0...𝑅) ∈ Fin)
17 elfznn0 13634 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (0...𝑅) → 𝑖 ∈ ℕ0)
186adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → ℝ ∈ {ℝ, ℂ})
19 etransclem46.x . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))
2019adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))
21 etransclem46.p . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑃 ∈ ℕ)
2221adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → 𝑃 ∈ ℕ)
23 etransclem46.m . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑀 = (deg‘𝑄)
24 etransclem46.q . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝}))
2524eldifad 3956 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑄 ∈ (Poly‘ℤ))
26 dgrcl 26217 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑄 ∈ (Poly‘ℤ) → (deg‘𝑄) ∈ ℕ0)
2725, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (deg‘𝑄) ∈ ℕ0)
2823, 27eqeltrid 2829 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑀 ∈ ℕ0)
2928adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → 𝑀 ∈ ℕ0)
30 etransclem46.f . . . . . . . . . . . . . . . . . . . . . . 23 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃)))
31 simpr 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → 𝑖 ∈ ℕ0)
3218, 20, 22, 29, 30, 31etransclem33 45795 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
3317, 32sylan2 591 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
3433adantlr 713 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
35 simplr 767 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → 𝑥 ∈ ℝ)
3634, 35ffvelcdmd 7094 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ)
3716, 36fsumcl 15720 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ)
38 etransclem46.g . . . . . . . . . . . . . . . . . . 19 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))
3938fvmpt2 7015 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ) → (𝐺𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))
4015, 37, 39syl2anc 582 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → (𝐺𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))
4140, 37eqeltrd 2825 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → (𝐺𝑥) ∈ ℂ)
4214, 41mulcld 11271 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · (𝐺𝑥)) ∈ ℂ)
4342negcld 11595 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → -((e↑𝑐-𝑥) · (𝐺𝑥)) ∈ ℂ)
4443adantlr 713 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ ℝ) → -((e↑𝑐-𝑥) · (𝐺𝑥)) ∈ ℂ)
456, 19dvdmsscn 45464 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ℝ ⊆ ℂ)
4645, 21, 30etransclem8 45770 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:ℝ⟶ℂ)
4746ffvelcdmda 7093 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℂ)
4814, 47mulcld 11271 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
4948negcld 11595 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ) → -((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
5049negcld 11595 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → --((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
5150adantlr 713 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ ℝ) → --((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
528a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → e ∈ ℝ)
53 0re 11253 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℝ
54 epos 16192 . . . . . . . . . . . . . . . . . . . . . 22 0 < e
5553, 8, 54ltleii 11374 . . . . . . . . . . . . . . . . . . . . 21 0 ≤ e
5655a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → 0 ≤ e)
57 renegcl 11560 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → -𝑥 ∈ ℝ)
5852, 56, 57recxpcld 26707 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → (e↑𝑐-𝑥) ∈ ℝ)
5958renegcld 11678 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → -(e↑𝑐-𝑥) ∈ ℝ)
6059adantl 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → -(e↑𝑐-𝑥) ∈ ℝ)
61 reelprrecn 11237 . . . . . . . . . . . . . . . . . . . . . 22 ℝ ∈ {ℝ, ℂ}
6261a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → ℝ ∈ {ℝ, ℂ})
63 cnelprrecn 11238 . . . . . . . . . . . . . . . . . . . . . 22 ℂ ∈ {ℝ, ℂ}
6463a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → ℂ ∈ {ℝ, ℂ})
6512adantl 480 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑥 ∈ ℝ) → -𝑥 ∈ ℂ)
66 neg1rr 12365 . . . . . . . . . . . . . . . . . . . . . 22 -1 ∈ ℝ
6766a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑥 ∈ ℝ) → -1 ∈ ℝ)
689a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℂ → e ∈ ℂ)
69 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
7068, 69cxpcld 26692 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℂ → (e↑𝑐𝑦) ∈ ℂ)
7170adantl 480 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑦 ∈ ℂ) → (e↑𝑐𝑦) ∈ ℂ)
7211adantl 480 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
73 1red 11252 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
7462dvmptid 25938 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
7562, 72, 73, 74dvmptneg 25947 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ -𝑥)) = (𝑥 ∈ ℝ ↦ -1))
76 epr 16193 . . . . . . . . . . . . . . . . . . . . . . . 24 e ∈ ℝ+
77 dvcxp2 26725 . . . . . . . . . . . . . . . . . . . . . . . 24 (e ∈ ℝ+ → (ℂ D (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑𝑐𝑦))))
7876, 77ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (ℂ D (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑𝑐𝑦)))
79 loge 26570 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (log‘e) = 1
8079oveq1i 7429 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((log‘e) · (e↑𝑐𝑦)) = (1 · (e↑𝑐𝑦))
8170mullidd 11269 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ℂ → (1 · (e↑𝑐𝑦)) = (e↑𝑐𝑦))
8280, 81eqtrid 2777 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ℂ → ((log‘e) · (e↑𝑐𝑦)) = (e↑𝑐𝑦))
8382mpteq2ia 5252 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))
8478, 83eqtri 2753 . . . . . . . . . . . . . . . . . . . . . 22 (ℂ D (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))
8584a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)))
86 oveq2 7427 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = -𝑥 → (e↑𝑐𝑦) = (e↑𝑐-𝑥))
8762, 64, 65, 67, 71, 71, 75, 85, 86, 86dvmptco 25953 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ (e↑𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -1)))
8887mptru 1540 . . . . . . . . . . . . . . . . . . 19 (ℝ D (𝑥 ∈ ℝ ↦ (e↑𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -1))
8966a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → -1 ∈ ℝ)
9089recnd 11279 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → -1 ∈ ℂ)
9113, 90mulcomd 11272 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → ((e↑𝑐-𝑥) · -1) = (-1 · (e↑𝑐-𝑥)))
9213mulm1d 11703 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → (-1 · (e↑𝑐-𝑥)) = -(e↑𝑐-𝑥))
9391, 92eqtrd 2765 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → ((e↑𝑐-𝑥) · -1) = -(e↑𝑐-𝑥))
9493mpteq2ia 5252 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -1)) = (𝑥 ∈ ℝ ↦ -(e↑𝑐-𝑥))
9588, 94eqtri 2753 . . . . . . . . . . . . . . . . . 18 (ℝ D (𝑥 ∈ ℝ ↦ (e↑𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ -(e↑𝑐-𝑥))
9695a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (e↑𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ -(e↑𝑐-𝑥)))
9717adantl 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0...𝑅)) → 𝑖 ∈ ℕ0)
98 peano2nn0 12550 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℕ0)
9997, 98syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0...𝑅)) → (𝑖 + 1) ∈ ℕ0)
100 ovex 7452 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 + 1) ∈ V
101 eleq1 2813 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = (𝑖 + 1) → (𝑗 ∈ ℕ0 ↔ (𝑖 + 1) ∈ ℕ0))
102101anbi2d 628 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = (𝑖 + 1) → ((𝜑𝑗 ∈ ℕ0) ↔ (𝜑 ∧ (𝑖 + 1) ∈ ℕ0)))
103 fveq2 6896 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = (𝑖 + 1) → ((ℝ D𝑛 𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘(𝑖 + 1)))
104103feq1d 6708 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = (𝑖 + 1) → (((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ ↔ ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ))
105102, 104imbi12d 343 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑖 + 1) → (((𝜑𝑗 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ) ↔ ((𝜑 ∧ (𝑖 + 1) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)))
106 eleq1 2813 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑗 → (𝑖 ∈ ℕ0𝑗 ∈ ℕ0))
107106anbi2d 628 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑗 → ((𝜑𝑖 ∈ ℕ0) ↔ (𝜑𝑗 ∈ ℕ0)))
108 fveq2 6896 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑗 → ((ℝ D𝑛 𝐹)‘𝑖) = ((ℝ D𝑛 𝐹)‘𝑗))
109108feq1d 6708 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑗 → (((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ ↔ ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ))
110107, 109imbi12d 343 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = 𝑗 → (((𝜑𝑖 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ) ↔ ((𝜑𝑗 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)))
111110, 32chvarvv 1994 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
112100, 105, 111vtocl 3536 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑖 + 1) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
11399, 112syldan 589 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
114113adantlr 713 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
115114, 35ffvelcdmd 7094 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ)
11616, 115fsumcl 15720 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ)
11721, 28, 30, 38etransclem39 45801 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐺:ℝ⟶ℂ)
118117feqmptd 6966 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺 = (𝑥 ∈ ℝ ↦ (𝐺𝑥)))
119118eqcomd 2731 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑥 ∈ ℝ ↦ (𝐺𝑥)) = 𝐺)
120119oveq2d 7435 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝐺𝑥))) = (ℝ D 𝐺))
121 nfcv 2891 . . . . . . . . . . . . . . . . . . 19 𝑥𝐹
122 elfznn0 13634 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (0...(𝑅 + 1)) → 𝑖 ∈ ℕ0)
123122, 32sylan2 591 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0...(𝑅 + 1))) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
124121, 46, 123, 38etransclem2 45764 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℝ D 𝐺) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
125120, 124eqtrd 2765 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝐺𝑥))) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
1266, 14, 60, 96, 41, 116, 125dvmptmul 25942 . . . . . . . . . . . . . . . 16 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ ℝ ↦ ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥)))))
127116, 14mulcomd 11272 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥)) = ((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
128127oveq2d 7435 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥))) = ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + ((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))))
12914negcld 11595 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → -(e↑𝑐-𝑥) ∈ ℂ)
130129, 41mulcld 11271 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → (-(e↑𝑐-𝑥) · (𝐺𝑥)) ∈ ℂ)
13114, 116mulcld 11271 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) ∈ ℂ)
132130, 131addcomd 11453 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + ((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) = (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑𝑐-𝑥) · (𝐺𝑥))))
133131, 42negsubd 11614 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + -((e↑𝑐-𝑥) · (𝐺𝑥))) = (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) − ((e↑𝑐-𝑥) · (𝐺𝑥))))
13414, 41mulneg1d 11704 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (-(e↑𝑐-𝑥) · (𝐺𝑥)) = -((e↑𝑐-𝑥) · (𝐺𝑥)))
135134oveq2d 7435 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑𝑐-𝑥) · (𝐺𝑥))) = (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + -((e↑𝑐-𝑥) · (𝐺𝑥))))
13614, 116, 41subdid 11707 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥))) = (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) − ((e↑𝑐-𝑥) · (𝐺𝑥))))
137133, 135, 1363eqtr4d 2775 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑𝑐-𝑥) · (𝐺𝑥))) = ((e↑𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥))))
13840oveq2d 7435 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥)) = (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)))
13916, 115, 36fsumsub 15775 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)((((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)) = (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)))
140 fveq2 6896 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑖 → ((ℝ D𝑛 𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘𝑖))
141140fveq1d 6898 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑖 → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))
142103fveq1d 6898 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑖 + 1) → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))
143 fveq2 6896 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 0 → ((ℝ D𝑛 𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘0))
144143fveq1d 6898 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 0 → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D𝑛 𝐹)‘0)‘𝑥))
145 fveq2 6896 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = (𝑅 + 1) → ((ℝ D𝑛 𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘(𝑅 + 1)))
146145fveq1d 6898 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑅 + 1) → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥))
147 etransclem46.r . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑅 = ((𝑀 · 𝑃) + (𝑃 − 1))
14821nnnn0d 12570 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑃 ∈ ℕ0)
14928, 148nn0mulcld 12575 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑀 · 𝑃) ∈ ℕ0)
150 nnm1nn0 12551 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ0)
15121, 150syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑃 − 1) ∈ ℕ0)
152149, 151nn0addcld 12574 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) ∈ ℕ0)
153147, 152eqeltrid 2829 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑅 ∈ ℕ0)
154153adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → 𝑅 ∈ ℕ0)
155154nn0zd 12622 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → 𝑅 ∈ ℤ)
156 peano2nn0 12550 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑅 ∈ ℕ0 → (𝑅 + 1) ∈ ℕ0)
157153, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑅 + 1) ∈ ℕ0)
158 nn0uz 12902 . . . . . . . . . . . . . . . . . . . . . . . 24 0 = (ℤ‘0)
159157, 158eleqtrdi 2835 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑅 + 1) ∈ (ℤ‘0))
160159adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (𝑅 + 1) ∈ (ℤ‘0))
161 elfznn0 13634 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 ∈ (0...(𝑅 + 1)) → 𝑗 ∈ ℕ0)
162161, 111sylan2 591 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
163162adantlr 713 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
164 simplr 767 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → 𝑥 ∈ ℝ)
165163, 164ffvelcdmd 7094 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) ∈ ℂ)
166141, 142, 144, 146, 155, 160, 165telfsum2 15792 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)((((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)) = ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥)))
167138, 139, 1663eqtr2d 2771 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥)) = ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥)))
168167oveq2d 7435 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥))) = ((e↑𝑐-𝑥) · ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥))))
169153nn0red 12571 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑅 ∈ ℝ)
170169ltp1d 12182 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑅 < (𝑅 + 1))
171147, 170eqbrtrrid 5185 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) < (𝑅 + 1))
172 etransclem5 45767 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))
1736, 19, 21, 28, 30, 157, 171, 172etransclem32 45794 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑅 + 1)) = (𝑥 ∈ ℝ ↦ 0))
174173fveq1d 6898 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) = ((𝑥 ∈ ℝ ↦ 0)‘𝑥))
175 eqid 2725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℝ ↦ 0) = (𝑥 ∈ ℝ ↦ 0)
176175fvmpt2 7015 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ ℝ ∧ 0 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ 0)‘𝑥) = 0)
17753, 176mpan2 689 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → ((𝑥 ∈ ℝ ↦ 0)‘𝑥) = 0)
178174, 177sylan9eq 2785 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) = 0)
179 cnex 11226 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℂ ∈ V
180179a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ℂ ∈ V)
181 etransclem46.rex . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ℝ ⊆ ℝ)
1826, 181ssexd 5325 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ℝ ∈ V)
183 elpm2r 8864 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:ℝ⟶ℂ ∧ ℝ ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑pm ℝ))
184180, 182, 46, 181, 183syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹 ∈ (ℂ ↑pm ℝ))
185 dvn0 25903 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℝ ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm ℝ)) → ((ℝ D𝑛 𝐹)‘0) = 𝐹)
18645, 184, 185syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((ℝ D𝑛 𝐹)‘0) = 𝐹)
187186fveq1d 6898 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((ℝ D𝑛 𝐹)‘0)‘𝑥) = (𝐹𝑥))
188187adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (((ℝ D𝑛 𝐹)‘0)‘𝑥) = (𝐹𝑥))
189178, 188oveq12d 7437 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥)) = (0 − (𝐹𝑥)))
190 df-neg 11484 . . . . . . . . . . . . . . . . . . . . 21 -(𝐹𝑥) = (0 − (𝐹𝑥))
191189, 190eqtr4di 2783 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥)) = -(𝐹𝑥))
192191oveq2d 7435 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥))) = ((e↑𝑐-𝑥) · -(𝐹𝑥)))
193137, 168, 1923eqtrd 2769 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑𝑐-𝑥) · (𝐺𝑥))) = ((e↑𝑐-𝑥) · -(𝐹𝑥)))
194128, 132, 1933eqtrd 2769 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥))) = ((e↑𝑐-𝑥) · -(𝐹𝑥)))
195194mpteq2dva 5249 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ ℝ ↦ ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥)))) = (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -(𝐹𝑥))))
19614, 47mulneg2d 11705 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · -(𝐹𝑥)) = -((e↑𝑐-𝑥) · (𝐹𝑥)))
197196mpteq2dva 5249 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -(𝐹𝑥))) = (𝑥 ∈ ℝ ↦ -((e↑𝑐-𝑥) · (𝐹𝑥))))
198126, 195, 1973eqtrd 2769 . . . . . . . . . . . . . . 15 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ ℝ ↦ -((e↑𝑐-𝑥) · (𝐹𝑥))))
1996, 42, 49, 198dvmptneg 25947 . . . . . . . . . . . . . 14 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ ℝ ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))))
200199adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D (𝑥 ∈ ℝ ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ ℝ ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))))
201 0red 11254 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ)
202 elfzelz 13541 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
203202zred 12704 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
204203adantl 480 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ)
205201, 204iccssred 13451 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℝ)
206 eqid 2725 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
207206tgioo2 24768 . . . . . . . . . . . . 13 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
208 0red 11254 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 0 ∈ ℝ)
209 iccntr 24786 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ 𝑗 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
210208, 203, 209syl2anc 582 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
211210adantl 480 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
2127, 44, 51, 200, 205, 207, 206, 211dvmptres2 25943 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ (0(,)𝑗) ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))))
2139a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0(,)𝑗)) → e ∈ ℂ)
214 elioore 13394 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℝ)
215214recnd 11279 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℂ)
216215adantl 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℂ)
217216negcld 11595 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℂ)
218213, 217cxpcld 26692 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0(,)𝑗)) → (e↑𝑐-𝑥) ∈ ℂ)
21946adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0(,)𝑗)) → 𝐹:ℝ⟶ℂ)
220214adantl 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
221219, 220ffvelcdmd 7094 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0(,)𝑗)) → (𝐹𝑥) ∈ ℂ)
222218, 221mulcld 11271 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (0(,)𝑗)) → ((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
223222negnegd 11599 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0(,)𝑗)) → --((e↑𝑐-𝑥) · (𝐹𝑥)) = ((e↑𝑐-𝑥) · (𝐹𝑥)))
224223mpteq2dva 5249 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (0(,)𝑗) ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))))
225224adantr 479 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))))
2265, 212, 2253eqtrd 2769 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))))
227226fveq1d 6898 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ((ℝ D 𝑂)‘𝑥) = ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥))
228227adantr 479 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((ℝ D 𝑂)‘𝑥) = ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥))
229 simpr 483 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ (0(,)𝑗))
230 eqid 2725 . . . . . . . . . . . 12 (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))
231230fvmpt2 7015 . . . . . . . . . . 11 ((𝑥 ∈ (0(,)𝑗) ∧ ((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥) = ((e↑𝑐-𝑥) · (𝐹𝑥)))
232229, 222, 231syl2anc 582 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0(,)𝑗)) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥) = ((e↑𝑐-𝑥) · (𝐹𝑥)))
233232adantlr 713 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥) = ((e↑𝑐-𝑥) · (𝐹𝑥)))
234228, 233eqtr2d 2766 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑𝑐-𝑥) · (𝐹𝑥)) = ((ℝ D 𝑂)‘𝑥))
235234itgeq2dv 25760 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥 = ∫(0(,)𝑗)((ℝ D 𝑂)‘𝑥) d𝑥)
236 elfzle1 13544 . . . . . . . . 9 (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
237236adantl 480 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ≤ 𝑗)
238 eqid 2725 . . . . . . . . . 10 (𝑥 ∈ (0[,]𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) = (𝑥 ∈ (0[,]𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))
239 eqidd 2726 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)) = (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)))
24086adantl 480 . . . . . . . . . . . . . . . 16 (((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) ∧ 𝑦 = -𝑥) → (e↑𝑐𝑦) = (e↑𝑐-𝑥))
241208, 203iccssred 13451 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → (0[,]𝑗) ⊆ ℝ)
242 ax-resscn 11202 . . . . . . . . . . . . . . . . . . 19 ℝ ⊆ ℂ
243241, 242sstrdi 3989 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → (0[,]𝑗) ⊆ ℂ)
244243sselda 3976 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℂ)
245244negcld 11595 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → -𝑥 ∈ ℂ)
2469a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → e ∈ ℂ)
247 negcl 11497 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → -𝑥 ∈ ℂ)
248246, 247cxpcld 26692 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → (e↑𝑐-𝑥) ∈ ℂ)
249244, 248syl 17 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑𝑐-𝑥) ∈ ℂ)
250239, 240, 245, 249fvmptd 7011 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥) = (e↑𝑐-𝑥))
251250eqcomd 2731 . . . . . . . . . . . . . 14 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑𝑐-𝑥) = ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥))
252251adantll 712 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑𝑐-𝑥) = ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥))
253252mpteq2dva 5249 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (e↑𝑐-𝑥)) = (𝑥 ∈ (0[,]𝑗) ↦ ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥)))
254 mnfxr 11308 . . . . . . . . . . . . . . . . . 18 -∞ ∈ ℝ*
255254a1i 11 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → -∞ ∈ ℝ*)
256 0red 11254 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → 0 ∈ ℝ)
257 rpxr 13023 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → e ∈ ℝ*)
258 rpgt0 13026 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → 0 < e)
259255, 256, 257, 258gtnelioc 45016 . . . . . . . . . . . . . . . 16 (e ∈ ℝ+ → ¬ e ∈ (-∞(,]0))
26076, 259ax-mp 5 . . . . . . . . . . . . . . 15 ¬ e ∈ (-∞(,]0)
261 eldif 3954 . . . . . . . . . . . . . . 15 (e ∈ (ℂ ∖ (-∞(,]0)) ↔ (e ∈ ℂ ∧ ¬ e ∈ (-∞(,]0)))
2629, 260, 261mpbir2an 709 . . . . . . . . . . . . . 14 e ∈ (ℂ ∖ (-∞(,]0))
263 cxpcncf2 45427 . . . . . . . . . . . . . 14 (e ∈ (ℂ ∖ (-∞(,]0)) → (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)) ∈ (ℂ–cn→ℂ))
264262, 263mp1i 13 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)) ∈ (ℂ–cn→ℂ))
265 eqid 2725 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) = (𝑥 ∈ (0[,]𝑗) ↦ -𝑥)
266265negcncf 24891 . . . . . . . . . . . . . . 15 ((0[,]𝑗) ⊆ ℂ → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
267243, 266syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
268267adantl 480 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
269264, 268cncfmpt1f 24883 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
270253, 269eqeltrd 2825 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (e↑𝑐-𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
271242a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → ℝ ⊆ ℂ)
27221ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ)
27328ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑀 ∈ ℕ0)
274 etransclem6 45768 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦𝑘)↑𝑃)))
27530, 274eqtri 2753 . . . . . . . . . . . . . 14 𝐹 = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦𝑘)↑𝑃)))
276241sselda 3976 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℝ)
277276adantll 712 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℝ)
278271, 272, 273, 275, 277etransclem13 45775 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝐹𝑥) = ∏𝑘 ∈ (0...𝑀)((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))
279278mpteq2dva 5249 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐹𝑥)) = (𝑥 ∈ (0[,]𝑗) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))))
280243adantl 480 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℂ)
281 fzfid 13979 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (0...𝑀) ∈ Fin)
282277recnd 11279 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℂ)
2832823adant3 1129 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → 𝑥 ∈ ℂ)
284 elfzelz 13541 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ)
285284zcnd 12705 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ)
2862853ad2ant3 1132 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
287283, 286subcld 11608 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥𝑘) ∈ ℂ)
28821adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ)
289288, 150syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0[,]𝑗)) → (𝑃 − 1) ∈ ℕ0)
290148adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ0)
291289, 290ifcld 4576 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0[,]𝑗)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0)
2922913adant3 1129 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0)
2932923adant1r 1174 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0)
294287, 293expcld 14151 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) ∈ ℂ)
295 nfv 1909 . . . . . . . . . . . . . 14 𝑥((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀))
296243adantr 479 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℂ)
297 ssid 3999 . . . . . . . . . . . . . . . . . 18 ℂ ⊆ ℂ
298297a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
299296, 298idcncfg 45401 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ 𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
300285adantl 480 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
301296, 300, 298constcncfg 45400 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ 𝑘) ∈ ((0[,]𝑗)–cn→ℂ))
302299, 301subcncf 25422 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝑥𝑘)) ∈ ((0[,]𝑗)–cn→ℂ))
303302adantll 712 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝑥𝑘)) ∈ ((0[,]𝑗)–cn→ℂ))
304151, 148ifcld 4576 . . . . . . . . . . . . . . . 16 (𝜑 → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0)
305 expcncf 24896 . . . . . . . . . . . . . . . 16 (if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0 → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
306304, 305syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
307306ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
308297a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
309 oveq1 7426 . . . . . . . . . . . . . 14 (𝑦 = (𝑥𝑘) → (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) = ((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))
310295, 303, 307, 308, 309cncfcompt2 24877 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((0[,]𝑗)–cn→ℂ))
311280, 281, 294, 310fprodcncf 45428 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((0[,]𝑗)–cn→ℂ))
312279, 311eqeltrd 2825 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐹𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
313270, 312mulcncf 25423 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
314 ioossicc 13450 . . . . . . . . . . 11 (0(,)𝑗) ⊆ (0[,]𝑗)
315314a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (0(,)𝑗) ⊆ (0[,]𝑗))
316297a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
317222adantlr 713 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
318238, 313, 315, 316, 317cncfmptssg 45399 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) ∈ ((0(,)𝑗)–cn→ℂ))
319226, 318eqeltrd 2825 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) ∈ ((0(,)𝑗)–cn→ℂ))
32019adantr 479 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))
32121adantr 479 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑃 ∈ ℕ)
32228adantr 479 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℕ0)
323 oveq2 7427 . . . . . . . . . . . . . . 15 (𝑗 = 𝑘 → (𝑥𝑗) = (𝑥𝑘))
324323oveq1d 7434 . . . . . . . . . . . . . 14 (𝑗 = 𝑘 → ((𝑥𝑗)↑𝑃) = ((𝑥𝑘)↑𝑃))
325324cbvprodv 15901 . . . . . . . . . . . . 13 𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃) = ∏𝑘 ∈ (1...𝑀)((𝑥𝑘)↑𝑃)
326325oveq2i 7430 . . . . . . . . . . . 12 ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃)) = ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥𝑘)↑𝑃))
327326mpteq2i 5254 . . . . . . . . . . 11 (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥𝑘)↑𝑃)))
32830, 327eqtri 2753 . . . . . . . . . 10 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥𝑘)↑𝑃)))
3297, 320, 321, 322, 328, 201, 204etransclem18 45780 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) ∈ 𝐿1)
330226, 329eqeltrd 2825 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) ∈ 𝐿1)
331 eqid 2725 . . . . . . . . . . . 12 (𝑥 ∈ ℝ ↦ (𝐺𝑥)) = (𝑥 ∈ ℝ ↦ (𝐺𝑥))
3326, 19, 21, 28, 30, 38etransclem43 45805 . . . . . . . . . . . . . 14 (𝜑𝐺 ∈ (ℝ–cn→ℂ))
333119, 332eqeltrd 2825 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℝ ↦ (𝐺𝑥)) ∈ (ℝ–cn→ℂ))
334333adantr 479 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ ℝ ↦ (𝐺𝑥)) ∈ (ℝ–cn→ℂ))
335117ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝐺:ℝ⟶ℂ)
336335, 277ffvelcdmd 7094 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝐺𝑥) ∈ ℂ)
337331, 334, 205, 316, 336cncfmptssg 45399 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐺𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
338270, 337mulcncf 25423 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((e↑𝑐-𝑥) · (𝐺𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
339338negcncfg 45409 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
3403, 339eqeltrid 2829 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑂 ∈ ((0[,]𝑗)–cn→ℂ))
341201, 204, 237, 319, 330, 340ftc2 26028 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((ℝ D 𝑂)‘𝑥) d𝑥 = ((𝑂𝑗) − (𝑂‘0)))
342 negeq 11489 . . . . . . . . . . . . 13 (𝑥 = 𝑗 → -𝑥 = -𝑗)
343342oveq2d 7435 . . . . . . . . . . . 12 (𝑥 = 𝑗 → (e↑𝑐-𝑥) = (e↑𝑐-𝑗))
344 fveq2 6896 . . . . . . . . . . . 12 (𝑥 = 𝑗 → (𝐺𝑥) = (𝐺𝑗))
345343, 344oveq12d 7437 . . . . . . . . . . 11 (𝑥 = 𝑗 → ((e↑𝑐-𝑥) · (𝐺𝑥)) = ((e↑𝑐-𝑗) · (𝐺𝑗)))
346345negeqd 11491 . . . . . . . . . 10 (𝑥 = 𝑗 → -((e↑𝑐-𝑥) · (𝐺𝑥)) = -((e↑𝑐-𝑗) · (𝐺𝑗)))
347201rexrd 11301 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ*)
348204rexrd 11301 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ*)
349 ubicc2 13482 . . . . . . . . . . 11 ((0 ∈ ℝ*𝑗 ∈ ℝ* ∧ 0 ≤ 𝑗) → 𝑗 ∈ (0[,]𝑗))
350347, 348, 237, 349syl3anc 1368 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0[,]𝑗))
3519a1i 11 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → e ∈ ℂ)
352203recnd 11279 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
353352negcld 11595 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → -𝑗 ∈ ℂ)
354351, 353cxpcld 26692 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (e↑𝑐-𝑗) ∈ ℂ)
355354adantl 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (e↑𝑐-𝑗) ∈ ℂ)
356117adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → 𝐺:ℝ⟶ℂ)
357356, 204ffvelcdmd 7094 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐺𝑗) ∈ ℂ)
358355, 357mulcld 11271 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → ((e↑𝑐-𝑗) · (𝐺𝑗)) ∈ ℂ)
359358negcld 11595 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → -((e↑𝑐-𝑗) · (𝐺𝑗)) ∈ ℂ)
3603, 346, 350, 359fvmptd3 7027 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑂𝑗) = -((e↑𝑐-𝑗) · (𝐺𝑗)))
3613a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑂 = (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥))))
362 negeq 11489 . . . . . . . . . . . . . . . 16 (𝑥 = 0 → -𝑥 = -0)
363362oveq2d 7435 . . . . . . . . . . . . . . 15 (𝑥 = 0 → (e↑𝑐-𝑥) = (e↑𝑐-0))
364 neg0 11543 . . . . . . . . . . . . . . . . 17 -0 = 0
365364oveq2i 7430 . . . . . . . . . . . . . . . 16 (e↑𝑐-0) = (e↑𝑐0)
366 cxp0 26654 . . . . . . . . . . . . . . . . 17 (e ∈ ℂ → (e↑𝑐0) = 1)
3679, 366ax-mp 5 . . . . . . . . . . . . . . . 16 (e↑𝑐0) = 1
368365, 367eqtri 2753 . . . . . . . . . . . . . . 15 (e↑𝑐-0) = 1
369363, 368eqtrdi 2781 . . . . . . . . . . . . . 14 (𝑥 = 0 → (e↑𝑐-𝑥) = 1)
370 fveq2 6896 . . . . . . . . . . . . . 14 (𝑥 = 0 → (𝐺𝑥) = (𝐺‘0))
371369, 370oveq12d 7437 . . . . . . . . . . . . 13 (𝑥 = 0 → ((e↑𝑐-𝑥) · (𝐺𝑥)) = (1 · (𝐺‘0)))
372 0red 11254 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ ℝ)
373117, 372ffvelcdmd 7094 . . . . . . . . . . . . . 14 (𝜑 → (𝐺‘0) ∈ ℂ)
374373mullidd 11269 . . . . . . . . . . . . 13 (𝜑 → (1 · (𝐺‘0)) = (𝐺‘0))
375371, 374sylan9eqr 2787 . . . . . . . . . . . 12 ((𝜑𝑥 = 0) → ((e↑𝑐-𝑥) · (𝐺𝑥)) = (𝐺‘0))
376375negeqd 11491 . . . . . . . . . . 11 ((𝜑𝑥 = 0) → -((e↑𝑐-𝑥) · (𝐺𝑥)) = -(𝐺‘0))
377376adantlr 713 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 = 0) → -((e↑𝑐-𝑥) · (𝐺𝑥)) = -(𝐺‘0))
378 lbicc2 13481 . . . . . . . . . . 11 ((0 ∈ ℝ*𝑗 ∈ ℝ* ∧ 0 ≤ 𝑗) → 0 ∈ (0[,]𝑗))
379347, 348, 237, 378syl3anc 1368 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ (0[,]𝑗))
380373negcld 11595 . . . . . . . . . . 11 (𝜑 → -(𝐺‘0) ∈ ℂ)
381380adantr 479 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → -(𝐺‘0) ∈ ℂ)
382361, 377, 379, 381fvmptd 7011 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑂‘0) = -(𝐺‘0))
383360, 382oveq12d 7437 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑂𝑗) − (𝑂‘0)) = (-((e↑𝑐-𝑗) · (𝐺𝑗)) − -(𝐺‘0)))
384373adantr 479 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐺‘0) ∈ ℂ)
385359, 384subnegd 11615 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (-((e↑𝑐-𝑗) · (𝐺𝑗)) − -(𝐺‘0)) = (-((e↑𝑐-𝑗) · (𝐺𝑗)) + (𝐺‘0)))
386359, 384addcomd 11453 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (-((e↑𝑐-𝑗) · (𝐺𝑗)) + (𝐺‘0)) = ((𝐺‘0) + -((e↑𝑐-𝑗) · (𝐺𝑗))))
387384, 358negsubd 11614 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐺‘0) + -((e↑𝑐-𝑗) · (𝐺𝑗))) = ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗))))
388386, 387eqtrd 2765 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (-((e↑𝑐-𝑗) · (𝐺𝑗)) + (𝐺‘0)) = ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗))))
389383, 385, 3883eqtrd 2769 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑂𝑗) − (𝑂‘0)) = ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗))))
390235, 341, 3893eqtrd 2769 . . . . . 6 ((𝜑𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥 = ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗))))
391390oveq2d 7435 . . . . 5 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥) = (((𝐴𝑗) · (e↑𝑐𝑗)) · ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗)))))
39225adantr 479 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑄 ∈ (Poly‘ℤ))
393 0zd 12608 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ ℤ)
394 etransclem46.a . . . . . . . . . . 11 𝐴 = (coeff‘𝑄)
395394coef2 26215 . . . . . . . . . 10 ((𝑄 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → 𝐴:ℕ0⟶ℤ)
396392, 393, 395syl2anc 582 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → 𝐴:ℕ0⟶ℤ)
397 elfznn0 13634 . . . . . . . . . 10 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0)
398397adantl 480 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ0)
399396, 398ffvelcdmd 7094 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐴𝑗) ∈ ℤ)
400399zcnd 12705 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐴𝑗) ∈ ℂ)
401351, 352cxpcld 26692 . . . . . . . 8 (𝑗 ∈ (0...𝑀) → (e↑𝑐𝑗) ∈ ℂ)
402401adantl 480 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → (e↑𝑐𝑗) ∈ ℂ)
403400, 402mulcld 11271 . . . . . 6 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · (e↑𝑐𝑗)) ∈ ℂ)
404403, 384, 358subdid 11707 . . . . 5 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗)))) = ((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))))
405391, 404eqtrd 2765 . . . 4 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥) = ((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))))
406405sumeq2dv 15690 . . 3 (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥) = Σ𝑗 ∈ (0...𝑀)((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))))
407 fzfid 13979 . . . . 5 (𝜑 → (0...𝑀) ∈ Fin)
408403, 384mulcld 11271 . . . . 5 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) ∈ ℂ)
409403, 358mulcld 11271 . . . . 5 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) ∈ ℂ)
410407, 408, 409fsumsub 15775 . . . 4 (𝜑 → Σ𝑗 ∈ (0...𝑀)((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))) = (Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))))
411 etransclem46.qe0 . . . . . . . . 9 (𝜑 → (𝑄‘e) = 0)
412411eqcomd 2731 . . . . . . . 8 (𝜑 → 0 = (𝑄‘e))
413394, 23coeid2 26223 . . . . . . . . 9 ((𝑄 ∈ (Poly‘ℤ) ∧ e ∈ ℂ) → (𝑄‘e) = Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑗)))
41425, 9, 413sylancl 584 . . . . . . . 8 (𝜑 → (𝑄‘e) = Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑗)))
415 cxpexp 26652 . . . . . . . . . . . . 13 ((e ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (e↑𝑐𝑗) = (e↑𝑗))
416351, 397, 415syl2anc 582 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (e↑𝑐𝑗) = (e↑𝑗))
417416eqcomd 2731 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑀) → (e↑𝑗) = (e↑𝑐𝑗))
418417oveq2d 7435 . . . . . . . . . 10 (𝑗 ∈ (0...𝑀) → ((𝐴𝑗) · (e↑𝑗)) = ((𝐴𝑗) · (e↑𝑐𝑗)))
419418adantl 480 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · (e↑𝑗)) = ((𝐴𝑗) · (e↑𝑐𝑗)))
420419sumeq2dv 15690 . . . . . . . 8 (𝜑 → Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑗)) = Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑐𝑗)))
421412, 414, 4203eqtrd 2769 . . . . . . 7 (𝜑 → 0 = Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑐𝑗)))
422421oveq1d 7434 . . . . . 6 (𝜑 → (0 · (𝐺‘0)) = (Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)))
423373mul02d 11449 . . . . . 6 (𝜑 → (0 · (𝐺‘0)) = 0)
424407, 373, 403fsummulc1 15772 . . . . . 6 (𝜑 → (Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) = Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)))
425422, 423, 4243eqtr3rd 2774 . . . . 5 (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) = 0)
426 fveq2 6896 . . . . . . . . . . . 12 (𝑥 = 𝑗 → (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) = (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
427426sumeq2sdv 15691 . . . . . . . . . . 11 (𝑥 = 𝑗 → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
428 fzfid 13979 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (0...𝑅) ∈ Fin)
42933adantlr 713 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
430204adantr 479 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → 𝑗 ∈ ℝ)
431429, 430ffvelcdmd 7094 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
432428, 431fsumcl 15720 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
43338, 427, 204, 432fvmptd3 7027 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐺𝑗) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
434433oveq2d 7435 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((e↑𝑐-𝑗) · (𝐺𝑗)) = ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
435434oveq2d 7435 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) = (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))))
436355, 432mulcld 11271 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) ∈ ℂ)
437400, 402, 436mulassd 11274 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))) = ((𝐴𝑗) · ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))))
438367eqcomi 2734 . . . . . . . . . . . . . . 15 1 = (e↑𝑐0)
439438a1i 11 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → 1 = (e↑𝑐0))
440352negidd 11598 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → (𝑗 + -𝑗) = 0)
441440eqcomd 2731 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 0 = (𝑗 + -𝑗))
442441oveq2d 7435 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (e↑𝑐0) = (e↑𝑐(𝑗 + -𝑗)))
44353, 54gtneii 11363 . . . . . . . . . . . . . . . 16 e ≠ 0
444443a1i 11 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → e ≠ 0)
445351, 444, 352, 353cxpaddd 26701 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (e↑𝑐(𝑗 + -𝑗)) = ((e↑𝑐𝑗) · (e↑𝑐-𝑗)))
446439, 442, 4453eqtrd 2769 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 1 = ((e↑𝑐𝑗) · (e↑𝑐-𝑗)))
447446oveq1d 7434 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = (((e↑𝑐𝑗) · (e↑𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
448447adantl 480 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = (((e↑𝑐𝑗) · (e↑𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
449432mullidd 11269 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
450402, 355, 432mulassd 11274 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (((e↑𝑐𝑗) · (e↑𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))))
451448, 449, 4503eqtr3rd 2774 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
452451oveq2d 7435 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))) = ((𝐴𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
453428, 400, 431fsummulc2 15771 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
454452, 453eqtrd 2765 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))) = Σ𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
455435, 437, 4543eqtrd 2769 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) = Σ𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
456455sumeq2dv 15690 . . . . . 6 (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) = Σ𝑗 ∈ (0...𝑀𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
457 vex 3465 . . . . . . . . . 10 𝑗 ∈ V
458 vex 3465 . . . . . . . . . 10 𝑖 ∈ V
459457, 458op1std 8004 . . . . . . . . 9 (𝑘 = ⟨𝑗, 𝑖⟩ → (1st𝑘) = 𝑗)
460459fveq2d 6900 . . . . . . . 8 (𝑘 = ⟨𝑗, 𝑖⟩ → (𝐴‘(1st𝑘)) = (𝐴𝑗))
461457, 458op2ndd 8005 . . . . . . . . . 10 (𝑘 = ⟨𝑗, 𝑖⟩ → (2nd𝑘) = 𝑖)
462461fveq2d 6900 . . . . . . . . 9 (𝑘 = ⟨𝑗, 𝑖⟩ → ((ℝ D𝑛 𝐹)‘(2nd𝑘)) = ((ℝ D𝑛 𝐹)‘𝑖))
463462, 459fveq12d 6903 . . . . . . . 8 (𝑘 = ⟨𝑗, 𝑖⟩ → (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) = (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
464460, 463oveq12d 7437 . . . . . . 7 (𝑘 = ⟨𝑗, 𝑖⟩ → ((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) = ((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
465 fzfid 13979 . . . . . . 7 (𝜑 → (0...𝑅) ∈ Fin)
466400adantrr 715 . . . . . . . 8 ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → (𝐴𝑗) ∈ ℂ)
467431anasss 465 . . . . . . . 8 ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
468466, 467mulcld 11271 . . . . . . 7 ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → ((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) ∈ ℂ)
469464, 407, 465, 468fsumxp 15759 . . . . . 6 (𝜑 → Σ𝑗 ∈ (0...𝑀𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
470456, 469eqtrd 2765 . . . . 5 (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) = Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
471425, 470oveq12d 7437 . . . 4 (𝜑 → (Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))) = (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)))))
472 df-neg 11484 . . . . . 6 𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) = (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
473472eqcomi 2734 . . . . 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 2769 . . 3 (𝜑 → Σ𝑗 ∈ (0...𝑀)((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))) = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
4762, 406, 4753eqtrd 2769 . 2 (𝜑𝐿 = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
477476oveq1d 7434 1 (𝜑 → (𝐿 / (!‘(𝑃 − 1))) = (-Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394  w3a 1084   = wceq 1533  wtru 1534  wcel 2098  wne 2929  Vcvv 3461  cdif 3941  wss 3944  ifcif 4530  {csn 4630  {cpr 4632  cop 4636   class class class wbr 5149  cmpt 5232   × cxp 5676  ran crn 5679  wf 6545  cfv 6549  (class class class)co 7419  1st c1st 7992  2nd c2nd 7993  pm cpm 8846  cc 11143  cr 11144  0cc0 11145  1c1 11146   + caddc 11148   · cmul 11150  -∞cmnf 11283  *cxr 11284   < clt 11285  cle 11286  cmin 11481  -cneg 11482   / cdiv 11908  cn 12250  0cn0 12510  cz 12596  cuz 12860  +crp 13014  (,)cioo 13364  (,]cioc 13365  [,]cicc 13367  ...cfz 13524  cexp 14067  !cfa 14273  Σcsu 15673  cprod 15890  eceu 16047  t crest 17410  TopOpenctopn 17411  topGenctg 17427  fldccnfld 21301  intcnt 22970  cnccncf 24845  𝐿1cibl 25595  citg 25596  0𝑝c0p 25647   D cdv 25841   D𝑛 cdvn 25842  Polycply 26168  coeffccoe 26170  degcdgr 26171  logclog 26538  𝑐ccxp 26539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-inf2 9671  ax-cc 10465  ax-cnex 11201  ax-resscn 11202  ax-1cn 11203  ax-icn 11204  ax-addcl 11205  ax-addrcl 11206  ax-mulcl 11207  ax-mulrcl 11208  ax-mulcom 11209  ax-addass 11210  ax-mulass 11211  ax-distr 11212  ax-i2m1 11213  ax-1ne0 11214  ax-1rid 11215  ax-rnegex 11216  ax-rrecex 11217  ax-cnre 11218  ax-pre-lttri 11219  ax-pre-lttrn 11220  ax-pre-ltadd 11221  ax-pre-mulgt0 11222  ax-pre-sup 11223  ax-addf 11224
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-symdif 4241  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-iin 5000  df-disj 5115  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-of 7685  df-ofr 7686  df-om 7872  df-1st 7994  df-2nd 7995  df-supp 8166  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-oadd 8491  df-omul 8492  df-er 8725  df-map 8847  df-pm 8848  df-ixp 8917  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fsupp 9393  df-fi 9441  df-sup 9472  df-inf 9473  df-oi 9540  df-dju 9931  df-card 9969  df-acn 9972  df-pnf 11287  df-mnf 11288  df-xr 11289  df-ltxr 11290  df-le 11291  df-sub 11483  df-neg 11484  df-div 11909  df-nn 12251  df-2 12313  df-3 12314  df-4 12315  df-5 12316  df-6 12317  df-7 12318  df-8 12319  df-9 12320  df-n0 12511  df-z 12597  df-dec 12716  df-uz 12861  df-q 12971  df-rp 13015  df-xneg 13132  df-xadd 13133  df-xmul 13134  df-ioo 13368  df-ioc 13369  df-ico 13370  df-icc 13371  df-fz 13525  df-fzo 13668  df-fl 13798  df-mod 13876  df-seq 14008  df-exp 14068  df-fac 14274  df-bc 14303  df-hash 14331  df-shft 15055  df-cj 15087  df-re 15088  df-im 15089  df-sqrt 15223  df-abs 15224  df-limsup 15456  df-clim 15473  df-rlim 15474  df-sum 15674  df-prod 15891  df-ef 16052  df-e 16053  df-sin 16054  df-cos 16055  df-tan 16056  df-pi 16057  df-struct 17124  df-sets 17141  df-slot 17159  df-ndx 17171  df-base 17189  df-ress 17218  df-plusg 17254  df-mulr 17255  df-starv 17256  df-sca 17257  df-vsca 17258  df-ip 17259  df-tset 17260  df-ple 17261  df-ds 17263  df-unif 17264  df-hom 17265  df-cco 17266  df-rest 17412  df-topn 17413  df-0g 17431  df-gsum 17432  df-topgen 17433  df-pt 17434  df-prds 17437  df-xrs 17492  df-qtop 17497  df-imas 17498  df-xps 17500  df-mre 17574  df-mrc 17575  df-acs 17577  df-mgm 18608  df-sgrp 18687  df-mnd 18703  df-submnd 18749  df-mulg 19037  df-cntz 19285  df-cmn 19754  df-psmet 21293  df-xmet 21294  df-met 21295  df-bl 21296  df-mopn 21297  df-fbas 21298  df-fg 21299  df-cnfld 21302  df-top 22845  df-topon 22862  df-topsp 22884  df-bases 22898  df-cld 22972  df-ntr 22973  df-cls 22974  df-nei 23051  df-lp 23089  df-perf 23090  df-cn 23180  df-cnp 23181  df-haus 23268  df-cmp 23340  df-tx 23515  df-hmeo 23708  df-fil 23799  df-fm 23891  df-flim 23892  df-flf 23893  df-xms 24275  df-ms 24276  df-tms 24277  df-cncf 24847  df-ovol 25442  df-vol 25443  df-mbf 25597  df-itg1 25598  df-itg2 25599  df-ibl 25600  df-itg 25601  df-0p 25648  df-limc 25844  df-dv 25845  df-dvn 25846  df-ply 26172  df-coe 26174  df-dgr 26175  df-log 26540  df-cxp 26541
This theorem is referenced by:  etransclem47  45809
  Copyright terms: Public domain W3C validator