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 41008
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 6803 . . . . . . . . . . . . 13 (ℝ D 𝑂) = (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥))))
54a1i 11 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) = (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))))
6 etransclem46.s . . . . . . . . . . . . . 14 (𝜑 → ℝ ∈ {ℝ, ℂ})
76adantr 466 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → ℝ ∈ {ℝ, ℂ})
8 ere 15024 . . . . . . . . . . . . . . . . . . . 20 e ∈ ℝ
98recni 10253 . . . . . . . . . . . . . . . . . . 19 e ∈ ℂ
109a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → e ∈ ℂ)
11 recn 10227 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
1211negcld 10580 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → -𝑥 ∈ ℂ)
1310, 12cxpcld 24674 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (e↑𝑐-𝑥) ∈ ℂ)
1413adantl 467 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → (e↑𝑐-𝑥) ∈ ℂ)
15 simpr 471 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
16 fzfid 12979 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → (0...𝑅) ∈ Fin)
17 elfznn0 12639 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (0...𝑅) → 𝑖 ∈ ℕ0)
186adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → ℝ ∈ {ℝ, ℂ})
19 etransclem46.x . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))
2019adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))
21 etransclem46.p . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑃 ∈ ℕ)
2221adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → 𝑃 ∈ ℕ)
23 etransclem46.m . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑀 = (deg‘𝑄)
24 etransclem46.q . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝}))
2524eldifad 3733 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑄 ∈ (Poly‘ℤ))
26 dgrcl 24208 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑄 ∈ (Poly‘ℤ) → (deg‘𝑄) ∈ ℕ0)
2725, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (deg‘𝑄) ∈ ℕ0)
2823, 27syl5eqel 2853 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑀 ∈ ℕ0)
2928adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → 𝑀 ∈ ℕ0)
30 etransclem46.f . . . . . . . . . . . . . . . . . . . . . . 23 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃)))
31 simpr 471 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → 𝑖 ∈ ℕ0)
3218, 20, 22, 29, 30, 31etransclem33 40995 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
3317, 32sylan2 572 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
3433adantlr 686 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
35 simplr 744 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → 𝑥 ∈ ℝ)
3634, 35ffvelrnd 6503 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ)
3716, 36fsumcl 14671 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ)
38 etransclem46.g . . . . . . . . . . . . . . . . . . 19 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))
3938fvmpt2 6433 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ) → (𝐺𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))
4015, 37, 39syl2anc 565 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → (𝐺𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))
4140, 37eqeltrd 2849 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → (𝐺𝑥) ∈ ℂ)
4214, 41mulcld 10261 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · (𝐺𝑥)) ∈ ℂ)
4342negcld 10580 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → -((e↑𝑐-𝑥) · (𝐺𝑥)) ∈ ℂ)
4443adantlr 686 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ ℝ) → -((e↑𝑐-𝑥) · (𝐺𝑥)) ∈ ℂ)
456, 19dvdmsscn 40663 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ℝ ⊆ ℂ)
4645, 21, 30etransclem8 40970 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:ℝ⟶ℂ)
4746ffvelrnda 6502 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℂ)
4814, 47mulcld 10261 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
4948negcld 10580 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ) → -((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
5049negcld 10580 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → --((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
5150adantlr 686 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ ℝ) → --((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
528a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → e ∈ ℝ)
53 0re 10241 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℝ
54 epos 15140 . . . . . . . . . . . . . . . . . . . . . 22 0 < e
5553, 8, 54ltleii 10361 . . . . . . . . . . . . . . . . . . . . 21 0 ≤ e
5655a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → 0 ≤ e)
57 renegcl 10545 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → -𝑥 ∈ ℝ)
5852, 56, 57recxpcld 24689 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → (e↑𝑐-𝑥) ∈ ℝ)
5958renegcld 10658 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → -(e↑𝑐-𝑥) ∈ ℝ)
6059adantl 467 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → -(e↑𝑐-𝑥) ∈ ℝ)
61 reelprrecn 10229 . . . . . . . . . . . . . . . . . . . . . 22 ℝ ∈ {ℝ, ℂ}
6261a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → ℝ ∈ {ℝ, ℂ})
63 cnelprrecn 10230 . . . . . . . . . . . . . . . . . . . . . 22 ℂ ∈ {ℝ, ℂ}
6463a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → ℂ ∈ {ℝ, ℂ})
6512adantl 467 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑥 ∈ ℝ) → -𝑥 ∈ ℂ)
66 neg1rr 11326 . . . . . . . . . . . . . . . . . . . . . 22 -1 ∈ ℝ
6766a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑥 ∈ ℝ) → -1 ∈ ℝ)
689a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℂ → e ∈ ℂ)
69 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
7068, 69cxpcld 24674 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℂ → (e↑𝑐𝑦) ∈ ℂ)
7170adantl 467 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑦 ∈ ℂ) → (e↑𝑐𝑦) ∈ ℂ)
7211adantl 467 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
73 1red 10256 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
7462dvmptid 23939 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
7562, 72, 73, 74dvmptneg 23948 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ -𝑥)) = (𝑥 ∈ ℝ ↦ -1))
76 epr 15141 . . . . . . . . . . . . . . . . . . . . . . . 24 e ∈ ℝ+
77 dvcxp2 24702 . . . . . . . . . . . . . . . . . . . . . . . 24 (e ∈ ℝ+ → (ℂ D (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑𝑐𝑦))))
7876, 77ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (ℂ D (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑𝑐𝑦)))
79 loge 24553 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (log‘e) = 1
8079oveq1i 6802 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((log‘e) · (e↑𝑐𝑦)) = (1 · (e↑𝑐𝑦))
8170mulid2d 10259 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ℂ → (1 · (e↑𝑐𝑦)) = (e↑𝑐𝑦))
8280, 81syl5eq 2816 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ℂ → ((log‘e) · (e↑𝑐𝑦)) = (e↑𝑐𝑦))
8382mpteq2ia 4872 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))
8478, 83eqtri 2792 . . . . . . . . . . . . . . . . . . . . . 22 (ℂ D (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))
8584a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)))
86 oveq2 6800 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = -𝑥 → (e↑𝑐𝑦) = (e↑𝑐-𝑥))
8762, 64, 65, 67, 71, 71, 75, 85, 86, 86dvmptco 23954 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ (e↑𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -1)))
8887trud 1640 . . . . . . . . . . . . . . . . . . 19 (ℝ D (𝑥 ∈ ℝ ↦ (e↑𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -1))
8966a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → -1 ∈ ℝ)
9089recnd 10269 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → -1 ∈ ℂ)
9113, 90mulcomd 10262 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → ((e↑𝑐-𝑥) · -1) = (-1 · (e↑𝑐-𝑥)))
9213mulm1d 10683 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → (-1 · (e↑𝑐-𝑥)) = -(e↑𝑐-𝑥))
9391, 92eqtrd 2804 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → ((e↑𝑐-𝑥) · -1) = -(e↑𝑐-𝑥))
9493mpteq2ia 4872 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -1)) = (𝑥 ∈ ℝ ↦ -(e↑𝑐-𝑥))
9588, 94eqtri 2792 . . . . . . . . . . . . . . . . . 18 (ℝ D (𝑥 ∈ ℝ ↦ (e↑𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ -(e↑𝑐-𝑥))
9695a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (e↑𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ -(e↑𝑐-𝑥)))
9717adantl 467 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0...𝑅)) → 𝑖 ∈ ℕ0)
98 peano2nn0 11534 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℕ0)
9997, 98syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0...𝑅)) → (𝑖 + 1) ∈ ℕ0)
100 ovex 6822 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 + 1) ∈ V
101 eleq1 2837 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = (𝑖 + 1) → (𝑗 ∈ ℕ0 ↔ (𝑖 + 1) ∈ ℕ0))
102101anbi2d 606 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = (𝑖 + 1) → ((𝜑𝑗 ∈ ℕ0) ↔ (𝜑 ∧ (𝑖 + 1) ∈ ℕ0)))
103 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = (𝑖 + 1) → ((ℝ D𝑛 𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘(𝑖 + 1)))
104103feq1d 6170 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = (𝑖 + 1) → (((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ ↔ ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ))
105102, 104imbi12d 333 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑖 + 1) → (((𝜑𝑗 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ) ↔ ((𝜑 ∧ (𝑖 + 1) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)))
106 eleq1 2837 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑗 → (𝑖 ∈ ℕ0𝑗 ∈ ℕ0))
107106anbi2d 606 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑗 → ((𝜑𝑖 ∈ ℕ0) ↔ (𝜑𝑗 ∈ ℕ0)))
108 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑗 → ((ℝ D𝑛 𝐹)‘𝑖) = ((ℝ D𝑛 𝐹)‘𝑗))
109108feq1d 6170 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑗 → (((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ ↔ ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ))
110107, 109imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = 𝑗 → (((𝜑𝑖 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ) ↔ ((𝜑𝑗 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)))
111110, 32chvarv 2424 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
112100, 105, 111vtocl 3408 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑖 + 1) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
11399, 112syldan 571 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
114113adantlr 686 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
115114, 35ffvelrnd 6503 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ)
11616, 115fsumcl 14671 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ)
11721, 28, 30, 38etransclem39 41001 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐺:ℝ⟶ℂ)
118117feqmptd 6391 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺 = (𝑥 ∈ ℝ ↦ (𝐺𝑥)))
119118eqcomd 2776 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑥 ∈ ℝ ↦ (𝐺𝑥)) = 𝐺)
120119oveq2d 6808 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝐺𝑥))) = (ℝ D 𝐺))
121 nfcv 2912 . . . . . . . . . . . . . . . . . . 19 𝑥𝐹
122 elfznn0 12639 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (0...(𝑅 + 1)) → 𝑖 ∈ ℕ0)
123122, 32sylan2 572 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0...(𝑅 + 1))) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
124121, 46, 123, 38etransclem2 40964 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℝ D 𝐺) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
125120, 124eqtrd 2804 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝐺𝑥))) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
1266, 14, 60, 96, 41, 116, 125dvmptmul 23943 . . . . . . . . . . . . . . . 16 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ ℝ ↦ ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥)))))
127116, 14mulcomd 10262 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥)) = ((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
128127oveq2d 6808 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥))) = ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + ((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))))
12914negcld 10580 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → -(e↑𝑐-𝑥) ∈ ℂ)
130129, 41mulcld 10261 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → (-(e↑𝑐-𝑥) · (𝐺𝑥)) ∈ ℂ)
13114, 116mulcld 10261 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) ∈ ℂ)
132130, 131addcomd 10439 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + ((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) = (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑𝑐-𝑥) · (𝐺𝑥))))
133131, 42negsubd 10599 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + -((e↑𝑐-𝑥) · (𝐺𝑥))) = (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) − ((e↑𝑐-𝑥) · (𝐺𝑥))))
13414, 41mulneg1d 10684 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (-(e↑𝑐-𝑥) · (𝐺𝑥)) = -((e↑𝑐-𝑥) · (𝐺𝑥)))
135134oveq2d 6808 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑𝑐-𝑥) · (𝐺𝑥))) = (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + -((e↑𝑐-𝑥) · (𝐺𝑥))))
136116, 41, 14subdir2d 10689 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥))) = (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) − ((e↑𝑐-𝑥) · (𝐺𝑥))))
137133, 135, 1363eqtr4d 2814 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑𝑐-𝑥) · (𝐺𝑥))) = ((e↑𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥))))
13840oveq2d 6808 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥)) = (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)))
13916, 115, 36fsumsub 14726 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)((((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)) = (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)))
140 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑖 → ((ℝ D𝑛 𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘𝑖))
141140fveq1d 6334 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑖 → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))
142103fveq1d 6334 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑖 + 1) → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))
143 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 0 → ((ℝ D𝑛 𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘0))
144143fveq1d 6334 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 0 → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D𝑛 𝐹)‘0)‘𝑥))
145 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = (𝑅 + 1) → ((ℝ D𝑛 𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘(𝑅 + 1)))
146145fveq1d 6334 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑅 + 1) → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥))
147 etransclem46.r . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑅 = ((𝑀 · 𝑃) + (𝑃 − 1))
14821nnnn0d 11552 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑃 ∈ ℕ0)
14928, 148nn0mulcld 11557 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑀 · 𝑃) ∈ ℕ0)
150 nnm1nn0 11535 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ0)
15121, 150syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑃 − 1) ∈ ℕ0)
152149, 151nn0addcld 11556 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) ∈ ℕ0)
153147, 152syl5eqel 2853 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑅 ∈ ℕ0)
154153adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → 𝑅 ∈ ℕ0)
155154nn0zd 11681 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → 𝑅 ∈ ℤ)
156 peano2nn0 11534 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑅 ∈ ℕ0 → (𝑅 + 1) ∈ ℕ0)
157153, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑅 + 1) ∈ ℕ0)
158 nn0uz 11923 . . . . . . . . . . . . . . . . . . . . . . . 24 0 = (ℤ‘0)
159157, 158syl6eleq 2859 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑅 + 1) ∈ (ℤ‘0))
160159adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (𝑅 + 1) ∈ (ℤ‘0))
161 elfznn0 12639 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 ∈ (0...(𝑅 + 1)) → 𝑗 ∈ ℕ0)
162161, 111sylan2 572 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
163162adantlr 686 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
164 simplr 744 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → 𝑥 ∈ ℝ)
165163, 164ffvelrnd 6503 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) ∈ ℂ)
166141, 142, 144, 146, 155, 160, 165telfsum2 14743 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)((((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)) = ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥)))
167138, 139, 1663eqtr2d 2810 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥)) = ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥)))
168167oveq2d 6808 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥))) = ((e↑𝑐-𝑥) · ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥))))
169153nn0red 11553 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑅 ∈ ℝ)
170169ltp1d 11155 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑅 < (𝑅 + 1))
171147, 170syl5eqbrr 4820 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) < (𝑅 + 1))
172 etransclem5 40967 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))
1736, 19, 21, 28, 30, 157, 171, 172etransclem32 40994 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑅 + 1)) = (𝑥 ∈ ℝ ↦ 0))
174173fveq1d 6334 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) = ((𝑥 ∈ ℝ ↦ 0)‘𝑥))
175 eqid 2770 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℝ ↦ 0) = (𝑥 ∈ ℝ ↦ 0)
176175fvmpt2 6433 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ ℝ ∧ 0 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ 0)‘𝑥) = 0)
17753, 176mpan2 663 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → ((𝑥 ∈ ℝ ↦ 0)‘𝑥) = 0)
178174, 177sylan9eq 2824 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) = 0)
179 cnex 10218 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℂ ∈ V
180179a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ℂ ∈ V)
181 etransclem46.rex . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ℝ ⊆ ℝ)
1826, 181ssexd 4936 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ℝ ∈ V)
183 elpm2r 8026 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:ℝ⟶ℂ ∧ ℝ ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑pm ℝ))
184180, 182, 46, 181, 183syl22anc 1476 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹 ∈ (ℂ ↑pm ℝ))
185 dvn0 23906 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℝ ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm ℝ)) → ((ℝ D𝑛 𝐹)‘0) = 𝐹)
18645, 184, 185syl2anc 565 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((ℝ D𝑛 𝐹)‘0) = 𝐹)
187186fveq1d 6334 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((ℝ D𝑛 𝐹)‘0)‘𝑥) = (𝐹𝑥))
188187adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (((ℝ D𝑛 𝐹)‘0)‘𝑥) = (𝐹𝑥))
189178, 188oveq12d 6810 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥)) = (0 − (𝐹𝑥)))
190 df-neg 10470 . . . . . . . . . . . . . . . . . . . . 21 -(𝐹𝑥) = (0 − (𝐹𝑥))
191189, 190syl6eqr 2822 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥)) = -(𝐹𝑥))
192191oveq2d 6808 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥))) = ((e↑𝑐-𝑥) · -(𝐹𝑥)))
193137, 168, 1923eqtrd 2808 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑𝑐-𝑥) · (𝐺𝑥))) = ((e↑𝑐-𝑥) · -(𝐹𝑥)))
194128, 132, 1933eqtrd 2808 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥))) = ((e↑𝑐-𝑥) · -(𝐹𝑥)))
195194mpteq2dva 4876 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ ℝ ↦ ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥)))) = (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -(𝐹𝑥))))
19614, 47mulneg2d 10685 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · -(𝐹𝑥)) = -((e↑𝑐-𝑥) · (𝐹𝑥)))
197196mpteq2dva 4876 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -(𝐹𝑥))) = (𝑥 ∈ ℝ ↦ -((e↑𝑐-𝑥) · (𝐹𝑥))))
198126, 195, 1973eqtrd 2808 . . . . . . . . . . . . . . 15 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ ℝ ↦ -((e↑𝑐-𝑥) · (𝐹𝑥))))
1996, 42, 49, 198dvmptneg 23948 . . . . . . . . . . . . . 14 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ ℝ ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))))
200199adantr 466 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D (𝑥 ∈ ℝ ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ ℝ ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))))
201 0red 10242 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ)
202 elfzelz 12548 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
203202zred 11683 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
204203adantl 467 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ)
205201, 204iccssred 40242 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℝ)
206 eqid 2770 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
207206tgioo2 22825 . . . . . . . . . . . . 13 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
208 0red 10242 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 0 ∈ ℝ)
209 iccntr 22843 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ 𝑗 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
210208, 203, 209syl2anc 565 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
211210adantl 467 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
2127, 44, 51, 200, 205, 207, 206, 211dvmptres2 23944 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ (0(,)𝑗) ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))))
2139a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0(,)𝑗)) → e ∈ ℂ)
214 elioore 12409 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℝ)
215214recnd 10269 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℂ)
216215adantl 467 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℂ)
217216negcld 10580 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℂ)
218213, 217cxpcld 24674 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0(,)𝑗)) → (e↑𝑐-𝑥) ∈ ℂ)
21946adantr 466 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0(,)𝑗)) → 𝐹:ℝ⟶ℂ)
220214adantl 467 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
221219, 220ffvelrnd 6503 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0(,)𝑗)) → (𝐹𝑥) ∈ ℂ)
222218, 221mulcld 10261 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (0(,)𝑗)) → ((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
223222negnegd 10584 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0(,)𝑗)) → --((e↑𝑐-𝑥) · (𝐹𝑥)) = ((e↑𝑐-𝑥) · (𝐹𝑥)))
224223mpteq2dva 4876 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (0(,)𝑗) ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))))
225224adantr 466 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))))
2265, 212, 2253eqtrd 2808 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))))
227226fveq1d 6334 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ((ℝ D 𝑂)‘𝑥) = ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥))
228227adantr 466 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((ℝ D 𝑂)‘𝑥) = ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥))
229 simpr 471 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ (0(,)𝑗))
230 eqid 2770 . . . . . . . . . . . 12 (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))
231230fvmpt2 6433 . . . . . . . . . . 11 ((𝑥 ∈ (0(,)𝑗) ∧ ((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥) = ((e↑𝑐-𝑥) · (𝐹𝑥)))
232229, 222, 231syl2anc 565 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0(,)𝑗)) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥) = ((e↑𝑐-𝑥) · (𝐹𝑥)))
233232adantlr 686 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥) = ((e↑𝑐-𝑥) · (𝐹𝑥)))
234228, 233eqtr2d 2805 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑𝑐-𝑥) · (𝐹𝑥)) = ((ℝ D 𝑂)‘𝑥))
235234itgeq2d 40710 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥 = ∫(0(,)𝑗)((ℝ D 𝑂)‘𝑥) d𝑥)
236 elfzle1 12550 . . . . . . . . 9 (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
237236adantl 467 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ≤ 𝑗)
238 eqid 2770 . . . . . . . . . 10 (𝑥 ∈ (0[,]𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) = (𝑥 ∈ (0[,]𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))
239 eqidd 2771 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)) = (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)))
24086adantl 467 . . . . . . . . . . . . . . . 16 (((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) ∧ 𝑦 = -𝑥) → (e↑𝑐𝑦) = (e↑𝑐-𝑥))
241208, 203iccssred 40242 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → (0[,]𝑗) ⊆ ℝ)
242 ax-resscn 10194 . . . . . . . . . . . . . . . . . . 19 ℝ ⊆ ℂ
243241, 242syl6ss 3762 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → (0[,]𝑗) ⊆ ℂ)
244243sselda 3750 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℂ)
245244negcld 10580 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → -𝑥 ∈ ℂ)
2469a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → e ∈ ℂ)
247 negcl 10482 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → -𝑥 ∈ ℂ)
248246, 247cxpcld 24674 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → (e↑𝑐-𝑥) ∈ ℂ)
249244, 248syl 17 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑𝑐-𝑥) ∈ ℂ)
250239, 240, 245, 249fvmptd 6430 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥) = (e↑𝑐-𝑥))
251250eqcomd 2776 . . . . . . . . . . . . . 14 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑𝑐-𝑥) = ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥))
252251adantll 685 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑𝑐-𝑥) = ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥))
253252mpteq2dva 4876 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (e↑𝑐-𝑥)) = (𝑥 ∈ (0[,]𝑗) ↦ ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥)))
254 mnfxr 10297 . . . . . . . . . . . . . . . . . 18 -∞ ∈ ℝ*
255254a1i 11 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → -∞ ∈ ℝ*)
256 0red 10242 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → 0 ∈ ℝ)
257 rpxr 12042 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → e ∈ ℝ*)
258 rpgt0 12046 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → 0 < e)
259255, 256, 257, 258gtnelioc 40227 . . . . . . . . . . . . . . . 16 (e ∈ ℝ+ → ¬ e ∈ (-∞(,]0))
26076, 259ax-mp 5 . . . . . . . . . . . . . . 15 ¬ e ∈ (-∞(,]0)
261 eldif 3731 . . . . . . . . . . . . . . 15 (e ∈ (ℂ ∖ (-∞(,]0)) ↔ (e ∈ ℂ ∧ ¬ e ∈ (-∞(,]0)))
2629, 260, 261mpbir2an 682 . . . . . . . . . . . . . 14 e ∈ (ℂ ∖ (-∞(,]0))
263 cxpcncf2 40625 . . . . . . . . . . . . . 14 (e ∈ (ℂ ∖ (-∞(,]0)) → (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)) ∈ (ℂ–cn→ℂ))
264262, 263mp1i 13 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)) ∈ (ℂ–cn→ℂ))
265 eqid 2770 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) = (𝑥 ∈ (0[,]𝑗) ↦ -𝑥)
266265negcncf 22940 . . . . . . . . . . . . . . 15 ((0[,]𝑗) ⊆ ℂ → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
267243, 266syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
268267adantl 467 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
269264, 268cncfmpt1f 22935 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
270253, 269eqeltrd 2849 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (e↑𝑐-𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
271242a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → ℝ ⊆ ℂ)
27221ad2antrr 697 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ)
27328ad2antrr 697 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑀 ∈ ℕ0)
274 etransclem6 40968 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦𝑘)↑𝑃)))
27530, 274eqtri 2792 . . . . . . . . . . . . . 14 𝐹 = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦𝑘)↑𝑃)))
276241sselda 3750 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℝ)
277276adantll 685 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℝ)
278271, 272, 273, 275, 277etransclem13 40975 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝐹𝑥) = ∏𝑘 ∈ (0...𝑀)((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))
279278mpteq2dva 4876 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐹𝑥)) = (𝑥 ∈ (0[,]𝑗) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))))
280243adantl 467 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℂ)
281 fzfid 12979 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (0...𝑀) ∈ Fin)
282277recnd 10269 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℂ)
2832823adant3 1125 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → 𝑥 ∈ ℂ)
284 elfzelz 12548 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ)
285284zcnd 11684 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ)
2862853ad2ant3 1128 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
287283, 286subcld 10593 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥𝑘) ∈ ℂ)
28821adantr 466 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ)
289288, 150syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0[,]𝑗)) → (𝑃 − 1) ∈ ℕ0)
290148adantr 466 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ0)
291289, 290ifcld 4268 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0[,]𝑗)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0)
2922913adant3 1125 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0)
2932923adant1r 1186 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0)
294287, 293expcld 13214 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) ∈ ℂ)
295 nfv 1994 . . . . . . . . . . . . . 14 𝑥((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀))
296243adantr 466 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℂ)
297 ssid 3771 . . . . . . . . . . . . . . . . . 18 ℂ ⊆ ℂ
298297a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
299296, 298idcncfg 40597 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ 𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
300285adantl 467 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
301296, 300, 298constcncfg 40596 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ 𝑘) ∈ ((0[,]𝑗)–cn→ℂ))
302299, 301subcncf 40594 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝑥𝑘)) ∈ ((0[,]𝑗)–cn→ℂ))
303302adantll 685 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝑥𝑘)) ∈ ((0[,]𝑗)–cn→ℂ))
304151, 148ifcld 4268 . . . . . . . . . . . . . . . 16 (𝜑 → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0)
305 expcncf 22944 . . . . . . . . . . . . . . . 16 (if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0 → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
306304, 305syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
307306ad2antrr 697 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
308297a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
309 oveq1 6799 . . . . . . . . . . . . . 14 (𝑦 = (𝑥𝑘) → (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) = ((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))
310295, 303, 307, 308, 309cncfcompt2 40624 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((0[,]𝑗)–cn→ℂ))
311280, 281, 294, 310fprodcncf 40626 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((0[,]𝑗)–cn→ℂ))
312279, 311eqeltrd 2849 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐹𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
313270, 312mulcncf 23433 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
314 ioossicc 12463 . . . . . . . . . . 11 (0(,)𝑗) ⊆ (0[,]𝑗)
315314a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (0(,)𝑗) ⊆ (0[,]𝑗))
316297a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
317222adantlr 686 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
318238, 313, 315, 316, 317cncfmptssg 40595 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) ∈ ((0(,)𝑗)–cn→ℂ))
319226, 318eqeltrd 2849 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) ∈ ((0(,)𝑗)–cn→ℂ))
32019adantr 466 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))
32121adantr 466 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑃 ∈ ℕ)
32228adantr 466 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℕ0)
323 oveq2 6800 . . . . . . . . . . . . . . 15 (𝑗 = 𝑘 → (𝑥𝑗) = (𝑥𝑘))
324323oveq1d 6807 . . . . . . . . . . . . . 14 (𝑗 = 𝑘 → ((𝑥𝑗)↑𝑃) = ((𝑥𝑘)↑𝑃))
325324cbvprodv 14852 . . . . . . . . . . . . 13 𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃) = ∏𝑘 ∈ (1...𝑀)((𝑥𝑘)↑𝑃)
326325oveq2i 6803 . . . . . . . . . . . 12 ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃)) = ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥𝑘)↑𝑃))
327326mpteq2i 4873 . . . . . . . . . . 11 (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥𝑘)↑𝑃)))
32830, 327eqtri 2792 . . . . . . . . . 10 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥𝑘)↑𝑃)))
3297, 320, 321, 322, 328, 201, 204etransclem18 40980 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) ∈ 𝐿1)
330226, 329eqeltrd 2849 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) ∈ 𝐿1)
331 eqid 2770 . . . . . . . . . . . 12 (𝑥 ∈ ℝ ↦ (𝐺𝑥)) = (𝑥 ∈ ℝ ↦ (𝐺𝑥))
3326, 19, 21, 28, 30, 38etransclem43 41005 . . . . . . . . . . . . . 14 (𝜑𝐺 ∈ (ℝ–cn→ℂ))
333119, 332eqeltrd 2849 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℝ ↦ (𝐺𝑥)) ∈ (ℝ–cn→ℂ))
334333adantr 466 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ ℝ ↦ (𝐺𝑥)) ∈ (ℝ–cn→ℂ))
335117ad2antrr 697 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝐺:ℝ⟶ℂ)
336335, 277ffvelrnd 6503 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝐺𝑥) ∈ ℂ)
337331, 334, 205, 316, 336cncfmptssg 40595 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐺𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
338270, 337mulcncf 23433 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((e↑𝑐-𝑥) · (𝐺𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
339338negcncfg 40606 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
3403, 339syl5eqel 2853 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑂 ∈ ((0[,]𝑗)–cn→ℂ))
341201, 204, 237, 319, 330, 340ftc2 24026 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((ℝ D 𝑂)‘𝑥) d𝑥 = ((𝑂𝑗) − (𝑂‘0)))
3423a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑂 = (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥))))
343 negeq 10474 . . . . . . . . . . . . . 14 (𝑥 = 𝑗 → -𝑥 = -𝑗)
344343oveq2d 6808 . . . . . . . . . . . . 13 (𝑥 = 𝑗 → (e↑𝑐-𝑥) = (e↑𝑐-𝑗))
345 fveq2 6332 . . . . . . . . . . . . 13 (𝑥 = 𝑗 → (𝐺𝑥) = (𝐺𝑗))
346344, 345oveq12d 6810 . . . . . . . . . . . 12 (𝑥 = 𝑗 → ((e↑𝑐-𝑥) · (𝐺𝑥)) = ((e↑𝑐-𝑗) · (𝐺𝑗)))
347346negeqd 10476 . . . . . . . . . . 11 (𝑥 = 𝑗 → -((e↑𝑐-𝑥) · (𝐺𝑥)) = -((e↑𝑐-𝑗) · (𝐺𝑗)))
348347adantl 467 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 = 𝑗) → -((e↑𝑐-𝑥) · (𝐺𝑥)) = -((e↑𝑐-𝑗) · (𝐺𝑗)))
349201rexrd 10290 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ*)
350204rexrd 10290 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ*)
351 ubicc2 12495 . . . . . . . . . . 11 ((0 ∈ ℝ*𝑗 ∈ ℝ* ∧ 0 ≤ 𝑗) → 𝑗 ∈ (0[,]𝑗))
352349, 350, 237, 351syl3anc 1475 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0[,]𝑗))
3539a1i 11 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → e ∈ ℂ)
354203recnd 10269 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
355354negcld 10580 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → -𝑗 ∈ ℂ)
356353, 355cxpcld 24674 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (e↑𝑐-𝑗) ∈ ℂ)
357356adantl 467 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (e↑𝑐-𝑗) ∈ ℂ)
358117adantr 466 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → 𝐺:ℝ⟶ℂ)
359358, 204ffvelrnd 6503 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐺𝑗) ∈ ℂ)
360357, 359mulcld 10261 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → ((e↑𝑐-𝑗) · (𝐺𝑗)) ∈ ℂ)
361360negcld 10580 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → -((e↑𝑐-𝑗) · (𝐺𝑗)) ∈ ℂ)
362342, 348, 352, 361fvmptd 6430 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑂𝑗) = -((e↑𝑐-𝑗) · (𝐺𝑗)))
363 negeq 10474 . . . . . . . . . . . . . . . 16 (𝑥 = 0 → -𝑥 = -0)
364363oveq2d 6808 . . . . . . . . . . . . . . 15 (𝑥 = 0 → (e↑𝑐-𝑥) = (e↑𝑐-0))
365 neg0 10528 . . . . . . . . . . . . . . . . 17 -0 = 0
366365oveq2i 6803 . . . . . . . . . . . . . . . 16 (e↑𝑐-0) = (e↑𝑐0)
367 cxp0 24636 . . . . . . . . . . . . . . . . 17 (e ∈ ℂ → (e↑𝑐0) = 1)
3689, 367ax-mp 5 . . . . . . . . . . . . . . . 16 (e↑𝑐0) = 1
369366, 368eqtri 2792 . . . . . . . . . . . . . . 15 (e↑𝑐-0) = 1
370364, 369syl6eq 2820 . . . . . . . . . . . . . 14 (𝑥 = 0 → (e↑𝑐-𝑥) = 1)
371 fveq2 6332 . . . . . . . . . . . . . 14 (𝑥 = 0 → (𝐺𝑥) = (𝐺‘0))
372370, 371oveq12d 6810 . . . . . . . . . . . . 13 (𝑥 = 0 → ((e↑𝑐-𝑥) · (𝐺𝑥)) = (1 · (𝐺‘0)))
373 0red 10242 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ ℝ)
374117, 373ffvelrnd 6503 . . . . . . . . . . . . . 14 (𝜑 → (𝐺‘0) ∈ ℂ)
375374mulid2d 10259 . . . . . . . . . . . . 13 (𝜑 → (1 · (𝐺‘0)) = (𝐺‘0))
376372, 375sylan9eqr 2826 . . . . . . . . . . . 12 ((𝜑𝑥 = 0) → ((e↑𝑐-𝑥) · (𝐺𝑥)) = (𝐺‘0))
377376negeqd 10476 . . . . . . . . . . 11 ((𝜑𝑥 = 0) → -((e↑𝑐-𝑥) · (𝐺𝑥)) = -(𝐺‘0))
378377adantlr 686 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 = 0) → -((e↑𝑐-𝑥) · (𝐺𝑥)) = -(𝐺‘0))
379 lbicc2 12494 . . . . . . . . . . 11 ((0 ∈ ℝ*𝑗 ∈ ℝ* ∧ 0 ≤ 𝑗) → 0 ∈ (0[,]𝑗))
380349, 350, 237, 379syl3anc 1475 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ (0[,]𝑗))
381374negcld 10580 . . . . . . . . . . 11 (𝜑 → -(𝐺‘0) ∈ ℂ)
382381adantr 466 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → -(𝐺‘0) ∈ ℂ)
383342, 378, 380, 382fvmptd 6430 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑂‘0) = -(𝐺‘0))
384362, 383oveq12d 6810 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑂𝑗) − (𝑂‘0)) = (-((e↑𝑐-𝑗) · (𝐺𝑗)) − -(𝐺‘0)))
385374adantr 466 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐺‘0) ∈ ℂ)
386361, 385subnegd 10600 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (-((e↑𝑐-𝑗) · (𝐺𝑗)) − -(𝐺‘0)) = (-((e↑𝑐-𝑗) · (𝐺𝑗)) + (𝐺‘0)))
387361, 385addcomd 10439 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (-((e↑𝑐-𝑗) · (𝐺𝑗)) + (𝐺‘0)) = ((𝐺‘0) + -((e↑𝑐-𝑗) · (𝐺𝑗))))
388385, 360negsubd 10599 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐺‘0) + -((e↑𝑐-𝑗) · (𝐺𝑗))) = ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗))))
389387, 388eqtrd 2804 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (-((e↑𝑐-𝑗) · (𝐺𝑗)) + (𝐺‘0)) = ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗))))
390384, 386, 3893eqtrd 2808 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑂𝑗) − (𝑂‘0)) = ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗))))
391235, 341, 3903eqtrd 2808 . . . . . 6 ((𝜑𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥 = ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗))))
392391oveq2d 6808 . . . . 5 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥) = (((𝐴𝑗) · (e↑𝑐𝑗)) · ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗)))))
39325adantr 466 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑄 ∈ (Poly‘ℤ))
394 0zd 11590 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ ℤ)
395 etransclem46.a . . . . . . . . . . 11 𝐴 = (coeff‘𝑄)
396395coef2 24206 . . . . . . . . . 10 ((𝑄 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → 𝐴:ℕ0⟶ℤ)
397393, 394, 396syl2anc 565 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → 𝐴:ℕ0⟶ℤ)
398 elfznn0 12639 . . . . . . . . . 10 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0)
399398adantl 467 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ0)
400397, 399ffvelrnd 6503 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐴𝑗) ∈ ℤ)
401400zcnd 11684 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐴𝑗) ∈ ℂ)
402353, 354cxpcld 24674 . . . . . . . 8 (𝑗 ∈ (0...𝑀) → (e↑𝑐𝑗) ∈ ℂ)
403402adantl 467 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → (e↑𝑐𝑗) ∈ ℂ)
404401, 403mulcld 10261 . . . . . 6 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · (e↑𝑐𝑗)) ∈ ℂ)
405404, 385, 360subdid 10687 . . . . 5 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗)))) = ((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))))
406392, 405eqtrd 2804 . . . 4 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥) = ((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))))
407406sumeq2dv 14640 . . 3 (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥) = Σ𝑗 ∈ (0...𝑀)((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))))
408 fzfid 12979 . . . . 5 (𝜑 → (0...𝑀) ∈ Fin)
409404, 385mulcld 10261 . . . . 5 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) ∈ ℂ)
410404, 360mulcld 10261 . . . . 5 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) ∈ ℂ)
411408, 409, 410fsumsub 14726 . . . 4 (𝜑 → Σ𝑗 ∈ (0...𝑀)((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))) = (Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))))
412 etransclem46.qe0 . . . . . . . . 9 (𝜑 → (𝑄‘e) = 0)
413412eqcomd 2776 . . . . . . . 8 (𝜑 → 0 = (𝑄‘e))
414395, 23coeid2 24214 . . . . . . . . 9 ((𝑄 ∈ (Poly‘ℤ) ∧ e ∈ ℂ) → (𝑄‘e) = Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑗)))
41525, 9, 414sylancl 566 . . . . . . . 8 (𝜑 → (𝑄‘e) = Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑗)))
416 cxpexp 24634 . . . . . . . . . . . . 13 ((e ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (e↑𝑐𝑗) = (e↑𝑗))
417353, 398, 416syl2anc 565 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (e↑𝑐𝑗) = (e↑𝑗))
418417eqcomd 2776 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑀) → (e↑𝑗) = (e↑𝑐𝑗))
419418oveq2d 6808 . . . . . . . . . 10 (𝑗 ∈ (0...𝑀) → ((𝐴𝑗) · (e↑𝑗)) = ((𝐴𝑗) · (e↑𝑐𝑗)))
420419adantl 467 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · (e↑𝑗)) = ((𝐴𝑗) · (e↑𝑐𝑗)))
421420sumeq2dv 14640 . . . . . . . 8 (𝜑 → Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑗)) = Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑐𝑗)))
422413, 415, 4213eqtrd 2808 . . . . . . 7 (𝜑 → 0 = Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑐𝑗)))
423422oveq1d 6807 . . . . . 6 (𝜑 → (0 · (𝐺‘0)) = (Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)))
424374mul02d 10435 . . . . . 6 (𝜑 → (0 · (𝐺‘0)) = 0)
425408, 374, 404fsummulc1 14723 . . . . . 6 (𝜑 → (Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) = Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)))
426423, 424, 4253eqtr3rd 2813 . . . . 5 (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) = 0)
42738a1i 11 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)))
428 fveq2 6332 . . . . . . . . . . . . 13 (𝑥 = 𝑗 → (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) = (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
429428sumeq2sdv 14642 . . . . . . . . . . . 12 (𝑥 = 𝑗 → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
430429adantl 467 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 = 𝑗) → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
431 fzfid 12979 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (0...𝑅) ∈ Fin)
43233adantlr 686 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
433204adantr 466 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → 𝑗 ∈ ℝ)
434432, 433ffvelrnd 6503 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
435431, 434fsumcl 14671 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
436427, 430, 204, 435fvmptd 6430 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐺𝑗) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
437436oveq2d 6808 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((e↑𝑐-𝑗) · (𝐺𝑗)) = ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
438437oveq2d 6808 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) = (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))))
439357, 435mulcld 10261 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) ∈ ℂ)
440401, 403, 439mulassd 10264 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))) = ((𝐴𝑗) · ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))))
441368eqcomi 2779 . . . . . . . . . . . . . . 15 1 = (e↑𝑐0)
442441a1i 11 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → 1 = (e↑𝑐0))
443354negidd 10583 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → (𝑗 + -𝑗) = 0)
444443eqcomd 2776 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 0 = (𝑗 + -𝑗))
445444oveq2d 6808 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (e↑𝑐0) = (e↑𝑐(𝑗 + -𝑗)))
44653, 54gtneii 10350 . . . . . . . . . . . . . . . 16 e ≠ 0
447446a1i 11 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → e ≠ 0)
448353, 447, 354, 355cxpaddd 24683 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (e↑𝑐(𝑗 + -𝑗)) = ((e↑𝑐𝑗) · (e↑𝑐-𝑗)))
449442, 445, 4483eqtrd 2808 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 1 = ((e↑𝑐𝑗) · (e↑𝑐-𝑗)))
450449oveq1d 6807 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = (((e↑𝑐𝑗) · (e↑𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
451450adantl 467 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = (((e↑𝑐𝑗) · (e↑𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
452435mulid2d 10259 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
453403, 357, 435mulassd 10264 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (((e↑𝑐𝑗) · (e↑𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))))
454451, 452, 4533eqtr3rd 2813 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
455454oveq2d 6808 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))) = ((𝐴𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
456431, 401, 434fsummulc2 14722 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
457455, 456eqtrd 2804 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))) = Σ𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
458438, 440, 4573eqtrd 2808 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) = Σ𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
459458sumeq2dv 14640 . . . . . 6 (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) = Σ𝑗 ∈ (0...𝑀𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
460 vex 3352 . . . . . . . . . 10 𝑗 ∈ V
461 vex 3352 . . . . . . . . . 10 𝑖 ∈ V
462460, 461op1std 7324 . . . . . . . . 9 (𝑘 = ⟨𝑗, 𝑖⟩ → (1st𝑘) = 𝑗)
463462fveq2d 6336 . . . . . . . 8 (𝑘 = ⟨𝑗, 𝑖⟩ → (𝐴‘(1st𝑘)) = (𝐴𝑗))
464460, 461op2ndd 7325 . . . . . . . . . 10 (𝑘 = ⟨𝑗, 𝑖⟩ → (2nd𝑘) = 𝑖)
465464fveq2d 6336 . . . . . . . . 9 (𝑘 = ⟨𝑗, 𝑖⟩ → ((ℝ D𝑛 𝐹)‘(2nd𝑘)) = ((ℝ D𝑛 𝐹)‘𝑖))
466465, 462fveq12d 6338 . . . . . . . 8 (𝑘 = ⟨𝑗, 𝑖⟩ → (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) = (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
467463, 466oveq12d 6810 . . . . . . 7 (𝑘 = ⟨𝑗, 𝑖⟩ → ((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) = ((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
468 fzfid 12979 . . . . . . 7 (𝜑 → (0...𝑅) ∈ Fin)
469401adantrr 688 . . . . . . . 8 ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → (𝐴𝑗) ∈ ℂ)
470434anasss 457 . . . . . . . 8 ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
471469, 470mulcld 10261 . . . . . . 7 ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → ((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) ∈ ℂ)
472467, 408, 468, 471fsumxp 14710 . . . . . 6 (𝜑 → Σ𝑗 ∈ (0...𝑀𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
473459, 472eqtrd 2804 . . . . 5 (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) = Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
474426, 473oveq12d 6810 . . . 4 (𝜑 → (Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))) = (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)))))
475 df-neg 10470 . . . . . 6 𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) = (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
476475eqcomi 2779 . . . . 5 (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)))) = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)))
477476a1i 11 . . . 4 (𝜑 → (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)))) = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
478411, 474, 4773eqtrd 2808 . . 3 (𝜑 → Σ𝑗 ∈ (0...𝑀)((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))) = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
4792, 407, 4783eqtrd 2808 . 2 (𝜑𝐿 = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
480479oveq1d 6807 1 (𝜑 → (𝐿 / (!‘(𝑃 − 1))) = (-Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382  w3a 1070   = wceq 1630  wtru 1631  wcel 2144  wne 2942  Vcvv 3349  cdif 3718  wss 3721  ifcif 4223  {csn 4314  {cpr 4316  cop 4320   class class class wbr 4784  cmpt 4861   × cxp 5247  ran crn 5250  wf 6027  cfv 6031  (class class class)co 6792  1st c1st 7312  2nd c2nd 7313  pm cpm 8009  cc 10135  cr 10136  0cc0 10137  1c1 10138   + caddc 10140   · cmul 10142  -∞cmnf 10273  *cxr 10274   < clt 10275  cle 10276  cmin 10467  -cneg 10468   / cdiv 10885  cn 11221  0cn0 11493  cz 11578  cuz 11887  +crp 12034  (,)cioo 12379  (,]cioc 12380  [,]cicc 12382  ...cfz 12532  cexp 13066  !cfa 13263  Σcsu 14623  cprod 14841  eceu 14998  t crest 16288  TopOpenctopn 16289  topGenctg 16305  fldccnfld 19960  intcnt 21041  cnccncf 22898  𝐿1cibl 23604  citg 23605  0𝑝c0p 23655   D cdv 23846   D𝑛 cdvn 23847  Polycply 24159  coeffccoe 24161  degcdgr 24162  logclog 24521  𝑐ccxp 24522
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-rep 4902  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095  ax-inf2 8701  ax-cc 9458  ax-cnex 10193  ax-resscn 10194  ax-1cn 10195  ax-icn 10196  ax-addcl 10197  ax-addrcl 10198  ax-mulcl 10199  ax-mulrcl 10200  ax-mulcom 10201  ax-addass 10202  ax-mulass 10203  ax-distr 10204  ax-i2m1 10205  ax-1ne0 10206  ax-1rid 10207  ax-rnegex 10208  ax-rrecex 10209  ax-cnre 10210  ax-pre-lttri 10211  ax-pre-lttrn 10212  ax-pre-ltadd 10213  ax-pre-mulgt0 10214  ax-pre-sup 10215  ax-addf 10216  ax-mulf 10217
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1071  df-3an 1072  df-tru 1633  df-fal 1636  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-nel 3046  df-ral 3065  df-rex 3066  df-reu 3067  df-rmo 3068  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-pss 3737  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-tp 4319  df-op 4321  df-uni 4573  df-int 4610  df-iun 4654  df-iin 4655  df-disj 4753  df-br 4785  df-opab 4845  df-mpt 4862  df-tr 4885  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6753  df-ov 6795  df-oprab 6796  df-mpt2 6797  df-of 7043  df-ofr 7044  df-om 7212  df-1st 7314  df-2nd 7315  df-supp 7446  df-wrecs 7558  df-recs 7620  df-rdg 7658  df-1o 7712  df-2o 7713  df-oadd 7716  df-omul 7717  df-er 7895  df-map 8010  df-pm 8011  df-ixp 8062  df-en 8109  df-dom 8110  df-sdom 8111  df-fin 8112  df-fsupp 8431  df-fi 8472  df-sup 8503  df-inf 8504  df-oi 8570  df-card 8964  df-acn 8967  df-cda 9191  df-pnf 10277  df-mnf 10278  df-xr 10279  df-ltxr 10280  df-le 10281  df-sub 10469  df-neg 10470  df-div 10886  df-nn 11222  df-2 11280  df-3 11281  df-4 11282  df-5 11283  df-6 11284  df-7 11285  df-8 11286  df-9 11287  df-n0 11494  df-z 11579  df-dec 11695  df-uz 11888  df-q 11991  df-rp 12035  df-xneg 12150  df-xadd 12151  df-xmul 12152  df-ioo 12383  df-ioc 12384  df-ico 12385  df-icc 12386  df-fz 12533  df-fzo 12673  df-fl 12800  df-mod 12876  df-seq 13008  df-exp 13067  df-fac 13264  df-bc 13293  df-hash 13321  df-shft 14014  df-cj 14046  df-re 14047  df-im 14048  df-sqrt 14182  df-abs 14183  df-limsup 14409  df-clim 14426  df-rlim 14427  df-sum 14624  df-prod 14842  df-ef 15003  df-e 15004  df-sin 15005  df-cos 15006  df-tan 15007  df-pi 15008  df-struct 16065  df-ndx 16066  df-slot 16067  df-base 16069  df-sets 16070  df-ress 16071  df-plusg 16161  df-mulr 16162  df-starv 16163  df-sca 16164  df-vsca 16165  df-ip 16166  df-tset 16167  df-ple 16168  df-ds 16171  df-unif 16172  df-hom 16173  df-cco 16174  df-rest 16290  df-topn 16291  df-0g 16309  df-gsum 16310  df-topgen 16311  df-pt 16312  df-prds 16315  df-xrs 16369  df-qtop 16374  df-imas 16375  df-xps 16377  df-mre 16453  df-mrc 16454  df-acs 16456  df-mgm 17449  df-sgrp 17491  df-mnd 17502  df-submnd 17543  df-mulg 17748  df-cntz 17956  df-cmn 18401  df-psmet 19952  df-xmet 19953  df-met 19954  df-bl 19955  df-mopn 19956  df-fbas 19957  df-fg 19958  df-cnfld 19961  df-top 20918  df-topon 20935  df-topsp 20957  df-bases 20970  df-cld 21043  df-ntr 21044  df-cls 21045  df-nei 21122  df-lp 21160  df-perf 21161  df-cn 21251  df-cnp 21252  df-haus 21339  df-cmp 21410  df-tx 21585  df-hmeo 21778  df-fil 21869  df-fm 21961  df-flim 21962  df-flf 21963  df-xms 22344  df-ms 22345  df-tms 22346  df-cncf 22900  df-ovol 23451  df-vol 23452  df-mbf 23606  df-itg1 23607  df-itg2 23608  df-ibl 23609  df-itg 23610  df-0p 23656  df-limc 23849  df-dv 23850  df-dvn 23851  df-ply 24163  df-coe 24165  df-dgr 24166  df-log 24523  df-cxp 24524
This theorem is referenced by:  etransclem47  41009
  Copyright terms: Public domain W3C validator