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 40266
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 6658 . . . . . . . . . . . . 13 (ℝ D 𝑂) = (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥))))
54a1i 11 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) = (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))))
6 etransclem46.s . . . . . . . . . . . . . 14 (𝜑 → ℝ ∈ {ℝ, ℂ})
76adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → ℝ ∈ {ℝ, ℂ})
8 ere 14813 . . . . . . . . . . . . . . . . . . . 20 e ∈ ℝ
98recni 10049 . . . . . . . . . . . . . . . . . . 19 e ∈ ℂ
109a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → e ∈ ℂ)
11 recn 10023 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
1211negcld 10376 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → -𝑥 ∈ ℂ)
1310, 12cxpcld 24448 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (e↑𝑐-𝑥) ∈ ℂ)
1413adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → (e↑𝑐-𝑥) ∈ ℂ)
15 simpr 477 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
16 fzfid 12767 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → (0...𝑅) ∈ Fin)
17 elfznn0 12429 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (0...𝑅) → 𝑖 ∈ ℕ0)
186adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → ℝ ∈ {ℝ, ℂ})
19 etransclem46.x . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))
2019adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))
21 etransclem46.p . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑃 ∈ ℕ)
2221adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → 𝑃 ∈ ℕ)
23 etransclem46.m . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑀 = (deg‘𝑄)
24 etransclem46.q . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝}))
2524eldifad 3584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑄 ∈ (Poly‘ℤ))
26 dgrcl 23983 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑄 ∈ (Poly‘ℤ) → (deg‘𝑄) ∈ ℕ0)
2725, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (deg‘𝑄) ∈ ℕ0)
2823, 27syl5eqel 2704 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑀 ∈ ℕ0)
2928adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → 𝑀 ∈ ℕ0)
30 etransclem46.f . . . . . . . . . . . . . . . . . . . . . . 23 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃)))
31 simpr 477 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → 𝑖 ∈ ℕ0)
3218, 20, 22, 29, 30, 31etransclem33 40253 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
3317, 32sylan2 491 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
3433adantlr 751 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
35 simplr 792 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → 𝑥 ∈ ℝ)
3634, 35ffvelrnd 6358 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ)
3716, 36fsumcl 14458 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ)
38 etransclem46.g . . . . . . . . . . . . . . . . . . 19 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))
3938fvmpt2 6289 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ) → (𝐺𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))
4015, 37, 39syl2anc 693 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → (𝐺𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))
4140, 37eqeltrd 2700 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → (𝐺𝑥) ∈ ℂ)
4214, 41mulcld 10057 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · (𝐺𝑥)) ∈ ℂ)
4342negcld 10376 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → -((e↑𝑐-𝑥) · (𝐺𝑥)) ∈ ℂ)
4443adantlr 751 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ ℝ) → -((e↑𝑐-𝑥) · (𝐺𝑥)) ∈ ℂ)
456, 19dvdmsscn 39920 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ℝ ⊆ ℂ)
4645, 21, 30etransclem8 40228 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:ℝ⟶ℂ)
4746ffvelrnda 6357 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℂ)
4814, 47mulcld 10057 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
4948negcld 10376 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ) → -((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
5049negcld 10376 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → --((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
5150adantlr 751 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ ℝ) → --((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
528a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → e ∈ ℝ)
53 0re 10037 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℝ
54 epos 14929 . . . . . . . . . . . . . . . . . . . . . 22 0 < e
5553, 8, 54ltleii 10157 . . . . . . . . . . . . . . . . . . . . 21 0 ≤ e
5655a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → 0 ≤ e)
57 renegcl 10341 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → -𝑥 ∈ ℝ)
5852, 56, 57recxpcld 24463 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → (e↑𝑐-𝑥) ∈ ℝ)
5958renegcld 10454 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → -(e↑𝑐-𝑥) ∈ ℝ)
6059adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → -(e↑𝑐-𝑥) ∈ ℝ)
61 reelprrecn 10025 . . . . . . . . . . . . . . . . . . . . . 22 ℝ ∈ {ℝ, ℂ}
6261a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → ℝ ∈ {ℝ, ℂ})
63 cnelprrecn 10026 . . . . . . . . . . . . . . . . . . . . . 22 ℂ ∈ {ℝ, ℂ}
6463a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → ℂ ∈ {ℝ, ℂ})
6512adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑥 ∈ ℝ) → -𝑥 ∈ ℂ)
66 neg1rr 11122 . . . . . . . . . . . . . . . . . . . . . 22 -1 ∈ ℝ
6766a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑥 ∈ ℝ) → -1 ∈ ℝ)
689a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℂ → e ∈ ℂ)
69 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
7068, 69cxpcld 24448 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℂ → (e↑𝑐𝑦) ∈ ℂ)
7170adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑦 ∈ ℂ) → (e↑𝑐𝑦) ∈ ℂ)
7211adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
73 1red 10052 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
7462dvmptid 23714 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
7562, 72, 73, 74dvmptneg 23723 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ -𝑥)) = (𝑥 ∈ ℝ ↦ -1))
76 epr 14930 . . . . . . . . . . . . . . . . . . . . . . . 24 e ∈ ℝ+
77 dvcxp2 24476 . . . . . . . . . . . . . . . . . . . . . . . 24 (e ∈ ℝ+ → (ℂ D (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑𝑐𝑦))))
7876, 77ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (ℂ D (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑𝑐𝑦)))
79 loge 24327 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (log‘e) = 1
8079oveq1i 6657 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((log‘e) · (e↑𝑐𝑦)) = (1 · (e↑𝑐𝑦))
8170mulid2d 10055 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ℂ → (1 · (e↑𝑐𝑦)) = (e↑𝑐𝑦))
8280, 81syl5eq 2667 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ℂ → ((log‘e) · (e↑𝑐𝑦)) = (e↑𝑐𝑦))
8382mpteq2ia 4738 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))
8478, 83eqtri 2643 . . . . . . . . . . . . . . . . . . . . . 22 (ℂ D (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))
8584a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)))
86 oveq2 6655 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = -𝑥 → (e↑𝑐𝑦) = (e↑𝑐-𝑥))
8762, 64, 65, 67, 71, 71, 75, 85, 86, 86dvmptco 23729 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ (e↑𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -1)))
8887trud 1492 . . . . . . . . . . . . . . . . . . 19 (ℝ D (𝑥 ∈ ℝ ↦ (e↑𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -1))
8966a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → -1 ∈ ℝ)
9089recnd 10065 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → -1 ∈ ℂ)
9113, 90mulcomd 10058 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → ((e↑𝑐-𝑥) · -1) = (-1 · (e↑𝑐-𝑥)))
9213mulm1d 10479 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → (-1 · (e↑𝑐-𝑥)) = -(e↑𝑐-𝑥))
9391, 92eqtrd 2655 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → ((e↑𝑐-𝑥) · -1) = -(e↑𝑐-𝑥))
9493mpteq2ia 4738 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -1)) = (𝑥 ∈ ℝ ↦ -(e↑𝑐-𝑥))
9588, 94eqtri 2643 . . . . . . . . . . . . . . . . . 18 (ℝ D (𝑥 ∈ ℝ ↦ (e↑𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ -(e↑𝑐-𝑥))
9695a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (e↑𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ -(e↑𝑐-𝑥)))
9717adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0...𝑅)) → 𝑖 ∈ ℕ0)
98 peano2nn0 11330 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℕ0)
9997, 98syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0...𝑅)) → (𝑖 + 1) ∈ ℕ0)
100 ovex 6675 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 + 1) ∈ V
101 eleq1 2688 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = (𝑖 + 1) → (𝑗 ∈ ℕ0 ↔ (𝑖 + 1) ∈ ℕ0))
102101anbi2d 740 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = (𝑖 + 1) → ((𝜑𝑗 ∈ ℕ0) ↔ (𝜑 ∧ (𝑖 + 1) ∈ ℕ0)))
103 fveq2 6189 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = (𝑖 + 1) → ((ℝ D𝑛 𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘(𝑖 + 1)))
104103feq1d 6028 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = (𝑖 + 1) → (((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ ↔ ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ))
105102, 104imbi12d 334 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑖 + 1) → (((𝜑𝑗 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ) ↔ ((𝜑 ∧ (𝑖 + 1) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)))
106 eleq1 2688 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑗 → (𝑖 ∈ ℕ0𝑗 ∈ ℕ0))
107106anbi2d 740 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑗 → ((𝜑𝑖 ∈ ℕ0) ↔ (𝜑𝑗 ∈ ℕ0)))
108 fveq2 6189 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑗 → ((ℝ D𝑛 𝐹)‘𝑖) = ((ℝ D𝑛 𝐹)‘𝑗))
109108feq1d 6028 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑗 → (((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ ↔ ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ))
110107, 109imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = 𝑗 → (((𝜑𝑖 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ) ↔ ((𝜑𝑗 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)))
111110, 32chvarv 2262 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
112100, 105, 111vtocl 3257 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑖 + 1) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
11399, 112syldan 487 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
114113adantlr 751 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
115114, 35ffvelrnd 6358 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ)
11616, 115fsumcl 14458 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ)
11721, 28, 30, 38etransclem39 40259 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐺:ℝ⟶ℂ)
118117feqmptd 6247 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺 = (𝑥 ∈ ℝ ↦ (𝐺𝑥)))
119118eqcomd 2627 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑥 ∈ ℝ ↦ (𝐺𝑥)) = 𝐺)
120119oveq2d 6663 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝐺𝑥))) = (ℝ D 𝐺))
121 nfcv 2763 . . . . . . . . . . . . . . . . . . 19 𝑥𝐹
122 elfznn0 12429 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (0...(𝑅 + 1)) → 𝑖 ∈ ℕ0)
123122, 32sylan2 491 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0...(𝑅 + 1))) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
124121, 46, 123, 38etransclem2 40222 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℝ D 𝐺) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
125120, 124eqtrd 2655 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝐺𝑥))) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
1266, 14, 60, 96, 41, 116, 125dvmptmul 23718 . . . . . . . . . . . . . . . 16 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ ℝ ↦ ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥)))))
127116, 14mulcomd 10058 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥)) = ((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
128127oveq2d 6663 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥))) = ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + ((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))))
12914negcld 10376 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → -(e↑𝑐-𝑥) ∈ ℂ)
130129, 41mulcld 10057 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → (-(e↑𝑐-𝑥) · (𝐺𝑥)) ∈ ℂ)
13114, 116mulcld 10057 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) ∈ ℂ)
132130, 131addcomd 10235 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + ((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) = (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑𝑐-𝑥) · (𝐺𝑥))))
133131, 42negsubd 10395 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + -((e↑𝑐-𝑥) · (𝐺𝑥))) = (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) − ((e↑𝑐-𝑥) · (𝐺𝑥))))
13414, 41mulneg1d 10480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (-(e↑𝑐-𝑥) · (𝐺𝑥)) = -((e↑𝑐-𝑥) · (𝐺𝑥)))
135134oveq2d 6663 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑𝑐-𝑥) · (𝐺𝑥))) = (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + -((e↑𝑐-𝑥) · (𝐺𝑥))))
136116, 41, 14subdir2d 10485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥))) = (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) − ((e↑𝑐-𝑥) · (𝐺𝑥))))
137133, 135, 1363eqtr4d 2665 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑𝑐-𝑥) · (𝐺𝑥))) = ((e↑𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥))))
13840oveq2d 6663 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥)) = (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)))
13916, 115, 36fsumsub 14514 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)((((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)) = (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)))
140 fveq2 6189 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑖 → ((ℝ D𝑛 𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘𝑖))
141140fveq1d 6191 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑖 → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))
142103fveq1d 6191 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑖 + 1) → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))
143 fveq2 6189 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 0 → ((ℝ D𝑛 𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘0))
144143fveq1d 6191 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 0 → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D𝑛 𝐹)‘0)‘𝑥))
145 fveq2 6189 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = (𝑅 + 1) → ((ℝ D𝑛 𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘(𝑅 + 1)))
146145fveq1d 6191 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑅 + 1) → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥))
147 etransclem46.r . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑅 = ((𝑀 · 𝑃) + (𝑃 − 1))
14821nnnn0d 11348 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑃 ∈ ℕ0)
14928, 148nn0mulcld 11353 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑀 · 𝑃) ∈ ℕ0)
150 nnm1nn0 11331 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ0)
15121, 150syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑃 − 1) ∈ ℕ0)
152149, 151nn0addcld 11352 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) ∈ ℕ0)
153147, 152syl5eqel 2704 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑅 ∈ ℕ0)
154153adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → 𝑅 ∈ ℕ0)
155154nn0zd 11477 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → 𝑅 ∈ ℤ)
156 peano2nn0 11330 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑅 ∈ ℕ0 → (𝑅 + 1) ∈ ℕ0)
157153, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑅 + 1) ∈ ℕ0)
158 nn0uz 11719 . . . . . . . . . . . . . . . . . . . . . . . 24 0 = (ℤ‘0)
159157, 158syl6eleq 2710 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑅 + 1) ∈ (ℤ‘0))
160159adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (𝑅 + 1) ∈ (ℤ‘0))
161 elfznn0 12429 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 ∈ (0...(𝑅 + 1)) → 𝑗 ∈ ℕ0)
162161, 111sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
163162adantlr 751 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
164 simplr 792 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → 𝑥 ∈ ℝ)
165163, 164ffvelrnd 6358 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) ∈ ℂ)
166141, 142, 144, 146, 155, 160, 165telfsum2 14531 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)((((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)) = ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥)))
167138, 139, 1663eqtr2d 2661 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥)) = ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥)))
168167oveq2d 6663 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥))) = ((e↑𝑐-𝑥) · ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥))))
169153nn0red 11349 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑅 ∈ ℝ)
170169ltp1d 10951 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑅 < (𝑅 + 1))
171147, 170syl5eqbrr 4687 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) < (𝑅 + 1))
172 etransclem5 40225 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))
1736, 19, 21, 28, 30, 157, 171, 172etransclem32 40252 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑅 + 1)) = (𝑥 ∈ ℝ ↦ 0))
174173fveq1d 6191 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) = ((𝑥 ∈ ℝ ↦ 0)‘𝑥))
175 eqid 2621 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℝ ↦ 0) = (𝑥 ∈ ℝ ↦ 0)
176175fvmpt2 6289 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ ℝ ∧ 0 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ 0)‘𝑥) = 0)
17753, 176mpan2 707 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → ((𝑥 ∈ ℝ ↦ 0)‘𝑥) = 0)
178174, 177sylan9eq 2675 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) = 0)
179 cnex 10014 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℂ ∈ V
180179a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ℂ ∈ V)
181 etransclem46.rex . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ℝ ⊆ ℝ)
1826, 181ssexd 4803 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ℝ ∈ V)
183 elpm2r 7872 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:ℝ⟶ℂ ∧ ℝ ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑pm ℝ))
184180, 182, 46, 181, 183syl22anc 1326 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹 ∈ (ℂ ↑pm ℝ))
185 dvn0 23681 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℝ ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm ℝ)) → ((ℝ D𝑛 𝐹)‘0) = 𝐹)
18645, 184, 185syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((ℝ D𝑛 𝐹)‘0) = 𝐹)
187186fveq1d 6191 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((ℝ D𝑛 𝐹)‘0)‘𝑥) = (𝐹𝑥))
188187adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (((ℝ D𝑛 𝐹)‘0)‘𝑥) = (𝐹𝑥))
189178, 188oveq12d 6665 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥)) = (0 − (𝐹𝑥)))
190 df-neg 10266 . . . . . . . . . . . . . . . . . . . . 21 -(𝐹𝑥) = (0 − (𝐹𝑥))
191189, 190syl6eqr 2673 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥)) = -(𝐹𝑥))
192191oveq2d 6663 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥))) = ((e↑𝑐-𝑥) · -(𝐹𝑥)))
193137, 168, 1923eqtrd 2659 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑𝑐-𝑥) · (𝐺𝑥))) = ((e↑𝑐-𝑥) · -(𝐹𝑥)))
194128, 132, 1933eqtrd 2659 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥))) = ((e↑𝑐-𝑥) · -(𝐹𝑥)))
195194mpteq2dva 4742 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ ℝ ↦ ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥)))) = (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -(𝐹𝑥))))
19614, 47mulneg2d 10481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · -(𝐹𝑥)) = -((e↑𝑐-𝑥) · (𝐹𝑥)))
197196mpteq2dva 4742 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -(𝐹𝑥))) = (𝑥 ∈ ℝ ↦ -((e↑𝑐-𝑥) · (𝐹𝑥))))
198126, 195, 1973eqtrd 2659 . . . . . . . . . . . . . . 15 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ ℝ ↦ -((e↑𝑐-𝑥) · (𝐹𝑥))))
1996, 42, 49, 198dvmptneg 23723 . . . . . . . . . . . . . 14 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ ℝ ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))))
200199adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D (𝑥 ∈ ℝ ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ ℝ ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))))
201 0red 10038 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ)
202 elfzelz 12339 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
203202zred 11479 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
204203adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ)
205201, 204iccssred 39536 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℝ)
206 eqid 2621 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
207206tgioo2 22600 . . . . . . . . . . . . 13 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
208 0red 10038 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 0 ∈ ℝ)
209 iccntr 22618 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ 𝑗 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
210208, 203, 209syl2anc 693 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
211210adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
2127, 44, 51, 200, 205, 207, 206, 211dvmptres2 23719 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ (0(,)𝑗) ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))))
2139a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0(,)𝑗)) → e ∈ ℂ)
214 elioore 12202 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℝ)
215214recnd 10065 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℂ)
216215adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℂ)
217216negcld 10376 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℂ)
218213, 217cxpcld 24448 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0(,)𝑗)) → (e↑𝑐-𝑥) ∈ ℂ)
21946adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0(,)𝑗)) → 𝐹:ℝ⟶ℂ)
220214adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
221219, 220ffvelrnd 6358 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0(,)𝑗)) → (𝐹𝑥) ∈ ℂ)
222218, 221mulcld 10057 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (0(,)𝑗)) → ((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
223222negnegd 10380 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0(,)𝑗)) → --((e↑𝑐-𝑥) · (𝐹𝑥)) = ((e↑𝑐-𝑥) · (𝐹𝑥)))
224223mpteq2dva 4742 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (0(,)𝑗) ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))))
225224adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))))
2265, 212, 2253eqtrd 2659 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))))
227226fveq1d 6191 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ((ℝ D 𝑂)‘𝑥) = ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥))
228227adantr 481 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((ℝ D 𝑂)‘𝑥) = ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥))
229 simpr 477 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ (0(,)𝑗))
230 eqid 2621 . . . . . . . . . . . 12 (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))
231230fvmpt2 6289 . . . . . . . . . . 11 ((𝑥 ∈ (0(,)𝑗) ∧ ((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥) = ((e↑𝑐-𝑥) · (𝐹𝑥)))
232229, 222, 231syl2anc 693 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0(,)𝑗)) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥) = ((e↑𝑐-𝑥) · (𝐹𝑥)))
233232adantlr 751 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥) = ((e↑𝑐-𝑥) · (𝐹𝑥)))
234228, 233eqtr2d 2656 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑𝑐-𝑥) · (𝐹𝑥)) = ((ℝ D 𝑂)‘𝑥))
235234itgeq2d 39968 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥 = ∫(0(,)𝑗)((ℝ D 𝑂)‘𝑥) d𝑥)
236 elfzle1 12341 . . . . . . . . 9 (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
237236adantl 482 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ≤ 𝑗)
238 eqid 2621 . . . . . . . . . 10 (𝑥 ∈ (0[,]𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) = (𝑥 ∈ (0[,]𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))
239 eqidd 2622 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)) = (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)))
24086adantl 482 . . . . . . . . . . . . . . . 16 (((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) ∧ 𝑦 = -𝑥) → (e↑𝑐𝑦) = (e↑𝑐-𝑥))
241208, 203iccssred 39536 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → (0[,]𝑗) ⊆ ℝ)
242 ax-resscn 9990 . . . . . . . . . . . . . . . . . . 19 ℝ ⊆ ℂ
243241, 242syl6ss 3613 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → (0[,]𝑗) ⊆ ℂ)
244243sselda 3601 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℂ)
245244negcld 10376 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → -𝑥 ∈ ℂ)
2469a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → e ∈ ℂ)
247 negcl 10278 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → -𝑥 ∈ ℂ)
248246, 247cxpcld 24448 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → (e↑𝑐-𝑥) ∈ ℂ)
249244, 248syl 17 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑𝑐-𝑥) ∈ ℂ)
250239, 240, 245, 249fvmptd 6286 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥) = (e↑𝑐-𝑥))
251250eqcomd 2627 . . . . . . . . . . . . . 14 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑𝑐-𝑥) = ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥))
252251adantll 750 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑𝑐-𝑥) = ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥))
253252mpteq2dva 4742 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (e↑𝑐-𝑥)) = (𝑥 ∈ (0[,]𝑗) ↦ ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥)))
254 mnfxr 10093 . . . . . . . . . . . . . . . . . 18 -∞ ∈ ℝ*
255254a1i 11 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → -∞ ∈ ℝ*)
256 0red 10038 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → 0 ∈ ℝ)
257 rpxr 11837 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → e ∈ ℝ*)
258 rpgt0 11841 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → 0 < e)
259255, 256, 257, 258gtnelioc 39521 . . . . . . . . . . . . . . . 16 (e ∈ ℝ+ → ¬ e ∈ (-∞(,]0))
26076, 259ax-mp 5 . . . . . . . . . . . . . . 15 ¬ e ∈ (-∞(,]0)
261 eldif 3582 . . . . . . . . . . . . . . 15 (e ∈ (ℂ ∖ (-∞(,]0)) ↔ (e ∈ ℂ ∧ ¬ e ∈ (-∞(,]0)))
2629, 260, 261mpbir2an 955 . . . . . . . . . . . . . 14 e ∈ (ℂ ∖ (-∞(,]0))
263 cxpcncf2 39882 . . . . . . . . . . . . . 14 (e ∈ (ℂ ∖ (-∞(,]0)) → (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)) ∈ (ℂ–cn→ℂ))
264262, 263mp1i 13 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)) ∈ (ℂ–cn→ℂ))
265 eqid 2621 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) = (𝑥 ∈ (0[,]𝑗) ↦ -𝑥)
266265negcncf 22715 . . . . . . . . . . . . . . 15 ((0[,]𝑗) ⊆ ℂ → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
267243, 266syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
268267adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
269264, 268cncfmpt1f 22710 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
270253, 269eqeltrd 2700 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (e↑𝑐-𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
271242a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → ℝ ⊆ ℂ)
27221ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ)
27328ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑀 ∈ ℕ0)
274 etransclem6 40226 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦𝑘)↑𝑃)))
27530, 274eqtri 2643 . . . . . . . . . . . . . 14 𝐹 = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦𝑘)↑𝑃)))
276241sselda 3601 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℝ)
277276adantll 750 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℝ)
278271, 272, 273, 275, 277etransclem13 40233 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝐹𝑥) = ∏𝑘 ∈ (0...𝑀)((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))
279278mpteq2dva 4742 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐹𝑥)) = (𝑥 ∈ (0[,]𝑗) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))))
280243adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℂ)
281 fzfid 12767 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (0...𝑀) ∈ Fin)
282277recnd 10065 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℂ)
2832823adant3 1080 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → 𝑥 ∈ ℂ)
284 elfzelz 12339 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ)
285284zcnd 11480 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ)
2862853ad2ant3 1083 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
287283, 286subcld 10389 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥𝑘) ∈ ℂ)
28821adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ)
289288, 150syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0[,]𝑗)) → (𝑃 − 1) ∈ ℕ0)
290148adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ0)
291289, 290ifcld 4129 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0[,]𝑗)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0)
2922913adant3 1080 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0)
2932923adant1r 1318 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0)
294287, 293expcld 13003 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) ∈ ℂ)
295 nfv 1842 . . . . . . . . . . . . . 14 𝑥((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀))
296243adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℂ)
297 ssid 3622 . . . . . . . . . . . . . . . . . 18 ℂ ⊆ ℂ
298297a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
299296, 298idcncfg 39854 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ 𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
300285adantl 482 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
301296, 300, 298constcncfg 39853 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ 𝑘) ∈ ((0[,]𝑗)–cn→ℂ))
302299, 301subcncf 39851 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝑥𝑘)) ∈ ((0[,]𝑗)–cn→ℂ))
303302adantll 750 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝑥𝑘)) ∈ ((0[,]𝑗)–cn→ℂ))
304151, 148ifcld 4129 . . . . . . . . . . . . . . . 16 (𝜑 → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0)
305 expcncf 22719 . . . . . . . . . . . . . . . 16 (if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0 → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
306304, 305syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
307306ad2antrr 762 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
308297a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
309 oveq1 6654 . . . . . . . . . . . . . 14 (𝑦 = (𝑥𝑘) → (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) = ((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))
310295, 303, 307, 308, 309cncfcompt2 39881 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((0[,]𝑗)–cn→ℂ))
311280, 281, 294, 310fprodcncf 39883 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((0[,]𝑗)–cn→ℂ))
312279, 311eqeltrd 2700 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐹𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
313270, 312mulcncf 23209 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
314 ioossicc 12256 . . . . . . . . . . 11 (0(,)𝑗) ⊆ (0[,]𝑗)
315314a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (0(,)𝑗) ⊆ (0[,]𝑗))
316297a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
317222adantlr 751 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
318238, 313, 315, 316, 317cncfmptssg 39852 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) ∈ ((0(,)𝑗)–cn→ℂ))
319226, 318eqeltrd 2700 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) ∈ ((0(,)𝑗)–cn→ℂ))
32019adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))
32121adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑃 ∈ ℕ)
32228adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℕ0)
323 oveq2 6655 . . . . . . . . . . . . . . 15 (𝑗 = 𝑘 → (𝑥𝑗) = (𝑥𝑘))
324323oveq1d 6662 . . . . . . . . . . . . . 14 (𝑗 = 𝑘 → ((𝑥𝑗)↑𝑃) = ((𝑥𝑘)↑𝑃))
325324cbvprodv 14640 . . . . . . . . . . . . 13 𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃) = ∏𝑘 ∈ (1...𝑀)((𝑥𝑘)↑𝑃)
326325oveq2i 6658 . . . . . . . . . . . 12 ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃)) = ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥𝑘)↑𝑃))
327326mpteq2i 4739 . . . . . . . . . . 11 (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥𝑘)↑𝑃)))
32830, 327eqtri 2643 . . . . . . . . . 10 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥𝑘)↑𝑃)))
3297, 320, 321, 322, 328, 201, 204etransclem18 40238 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) ∈ 𝐿1)
330226, 329eqeltrd 2700 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) ∈ 𝐿1)
331 eqid 2621 . . . . . . . . . . . 12 (𝑥 ∈ ℝ ↦ (𝐺𝑥)) = (𝑥 ∈ ℝ ↦ (𝐺𝑥))
3326, 19, 21, 28, 30, 38etransclem43 40263 . . . . . . . . . . . . . 14 (𝜑𝐺 ∈ (ℝ–cn→ℂ))
333119, 332eqeltrd 2700 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℝ ↦ (𝐺𝑥)) ∈ (ℝ–cn→ℂ))
334333adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ ℝ ↦ (𝐺𝑥)) ∈ (ℝ–cn→ℂ))
335117ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝐺:ℝ⟶ℂ)
336335, 277ffvelrnd 6358 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝐺𝑥) ∈ ℂ)
337331, 334, 205, 316, 336cncfmptssg 39852 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐺𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
338270, 337mulcncf 23209 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((e↑𝑐-𝑥) · (𝐺𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
339338negcncfg 39863 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
3403, 339syl5eqel 2704 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑂 ∈ ((0[,]𝑗)–cn→ℂ))
341201, 204, 237, 319, 330, 340ftc2 23801 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((ℝ D 𝑂)‘𝑥) d𝑥 = ((𝑂𝑗) − (𝑂‘0)))
3423a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑂 = (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥))))
343 negeq 10270 . . . . . . . . . . . . . 14 (𝑥 = 𝑗 → -𝑥 = -𝑗)
344343oveq2d 6663 . . . . . . . . . . . . 13 (𝑥 = 𝑗 → (e↑𝑐-𝑥) = (e↑𝑐-𝑗))
345 fveq2 6189 . . . . . . . . . . . . 13 (𝑥 = 𝑗 → (𝐺𝑥) = (𝐺𝑗))
346344, 345oveq12d 6665 . . . . . . . . . . . 12 (𝑥 = 𝑗 → ((e↑𝑐-𝑥) · (𝐺𝑥)) = ((e↑𝑐-𝑗) · (𝐺𝑗)))
347346negeqd 10272 . . . . . . . . . . 11 (𝑥 = 𝑗 → -((e↑𝑐-𝑥) · (𝐺𝑥)) = -((e↑𝑐-𝑗) · (𝐺𝑗)))
348347adantl 482 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 = 𝑗) → -((e↑𝑐-𝑥) · (𝐺𝑥)) = -((e↑𝑐-𝑗) · (𝐺𝑗)))
349201rexrd 10086 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ*)
350204rexrd 10086 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ*)
351 ubicc2 12286 . . . . . . . . . . 11 ((0 ∈ ℝ*𝑗 ∈ ℝ* ∧ 0 ≤ 𝑗) → 𝑗 ∈ (0[,]𝑗))
352349, 350, 237, 351syl3anc 1325 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0[,]𝑗))
3539a1i 11 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → e ∈ ℂ)
354203recnd 10065 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
355354negcld 10376 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → -𝑗 ∈ ℂ)
356353, 355cxpcld 24448 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (e↑𝑐-𝑗) ∈ ℂ)
357356adantl 482 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (e↑𝑐-𝑗) ∈ ℂ)
358117adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → 𝐺:ℝ⟶ℂ)
359358, 204ffvelrnd 6358 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐺𝑗) ∈ ℂ)
360357, 359mulcld 10057 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → ((e↑𝑐-𝑗) · (𝐺𝑗)) ∈ ℂ)
361360negcld 10376 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → -((e↑𝑐-𝑗) · (𝐺𝑗)) ∈ ℂ)
362342, 348, 352, 361fvmptd 6286 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑂𝑗) = -((e↑𝑐-𝑗) · (𝐺𝑗)))
363 negeq 10270 . . . . . . . . . . . . . . . 16 (𝑥 = 0 → -𝑥 = -0)
364363oveq2d 6663 . . . . . . . . . . . . . . 15 (𝑥 = 0 → (e↑𝑐-𝑥) = (e↑𝑐-0))
365 neg0 10324 . . . . . . . . . . . . . . . . 17 -0 = 0
366365oveq2i 6658 . . . . . . . . . . . . . . . 16 (e↑𝑐-0) = (e↑𝑐0)
367 cxp0 24410 . . . . . . . . . . . . . . . . 17 (e ∈ ℂ → (e↑𝑐0) = 1)
3689, 367ax-mp 5 . . . . . . . . . . . . . . . 16 (e↑𝑐0) = 1
369366, 368eqtri 2643 . . . . . . . . . . . . . . 15 (e↑𝑐-0) = 1
370364, 369syl6eq 2671 . . . . . . . . . . . . . 14 (𝑥 = 0 → (e↑𝑐-𝑥) = 1)
371 fveq2 6189 . . . . . . . . . . . . . 14 (𝑥 = 0 → (𝐺𝑥) = (𝐺‘0))
372370, 371oveq12d 6665 . . . . . . . . . . . . 13 (𝑥 = 0 → ((e↑𝑐-𝑥) · (𝐺𝑥)) = (1 · (𝐺‘0)))
373 0red 10038 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ ℝ)
374117, 373ffvelrnd 6358 . . . . . . . . . . . . . 14 (𝜑 → (𝐺‘0) ∈ ℂ)
375374mulid2d 10055 . . . . . . . . . . . . 13 (𝜑 → (1 · (𝐺‘0)) = (𝐺‘0))
376372, 375sylan9eqr 2677 . . . . . . . . . . . 12 ((𝜑𝑥 = 0) → ((e↑𝑐-𝑥) · (𝐺𝑥)) = (𝐺‘0))
377376negeqd 10272 . . . . . . . . . . 11 ((𝜑𝑥 = 0) → -((e↑𝑐-𝑥) · (𝐺𝑥)) = -(𝐺‘0))
378377adantlr 751 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 = 0) → -((e↑𝑐-𝑥) · (𝐺𝑥)) = -(𝐺‘0))
379 lbicc2 12285 . . . . . . . . . . 11 ((0 ∈ ℝ*𝑗 ∈ ℝ* ∧ 0 ≤ 𝑗) → 0 ∈ (0[,]𝑗))
380349, 350, 237, 379syl3anc 1325 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ (0[,]𝑗))
381374negcld 10376 . . . . . . . . . . 11 (𝜑 → -(𝐺‘0) ∈ ℂ)
382381adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → -(𝐺‘0) ∈ ℂ)
383342, 378, 380, 382fvmptd 6286 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑂‘0) = -(𝐺‘0))
384362, 383oveq12d 6665 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑂𝑗) − (𝑂‘0)) = (-((e↑𝑐-𝑗) · (𝐺𝑗)) − -(𝐺‘0)))
385374adantr 481 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐺‘0) ∈ ℂ)
386361, 385subnegd 10396 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (-((e↑𝑐-𝑗) · (𝐺𝑗)) − -(𝐺‘0)) = (-((e↑𝑐-𝑗) · (𝐺𝑗)) + (𝐺‘0)))
387361, 385addcomd 10235 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (-((e↑𝑐-𝑗) · (𝐺𝑗)) + (𝐺‘0)) = ((𝐺‘0) + -((e↑𝑐-𝑗) · (𝐺𝑗))))
388385, 360negsubd 10395 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐺‘0) + -((e↑𝑐-𝑗) · (𝐺𝑗))) = ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗))))
389387, 388eqtrd 2655 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (-((e↑𝑐-𝑗) · (𝐺𝑗)) + (𝐺‘0)) = ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗))))
390384, 386, 3893eqtrd 2659 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑂𝑗) − (𝑂‘0)) = ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗))))
391235, 341, 3903eqtrd 2659 . . . . . 6 ((𝜑𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥 = ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗))))
392391oveq2d 6663 . . . . 5 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥) = (((𝐴𝑗) · (e↑𝑐𝑗)) · ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗)))))
39325adantr 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑄 ∈ (Poly‘ℤ))
394 0zd 11386 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ ℤ)
395 etransclem46.a . . . . . . . . . . 11 𝐴 = (coeff‘𝑄)
396395coef2 23981 . . . . . . . . . 10 ((𝑄 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → 𝐴:ℕ0⟶ℤ)
397393, 394, 396syl2anc 693 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → 𝐴:ℕ0⟶ℤ)
398 elfznn0 12429 . . . . . . . . . 10 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0)
399398adantl 482 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ0)
400397, 399ffvelrnd 6358 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐴𝑗) ∈ ℤ)
401400zcnd 11480 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐴𝑗) ∈ ℂ)
402353, 354cxpcld 24448 . . . . . . . 8 (𝑗 ∈ (0...𝑀) → (e↑𝑐𝑗) ∈ ℂ)
403402adantl 482 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → (e↑𝑐𝑗) ∈ ℂ)
404401, 403mulcld 10057 . . . . . 6 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · (e↑𝑐𝑗)) ∈ ℂ)
405404, 385, 360subdid 10483 . . . . 5 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗)))) = ((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))))
406392, 405eqtrd 2655 . . . 4 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥) = ((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))))
407406sumeq2dv 14427 . . 3 (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥) = Σ𝑗 ∈ (0...𝑀)((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))))
408 fzfid 12767 . . . . 5 (𝜑 → (0...𝑀) ∈ Fin)
409404, 385mulcld 10057 . . . . 5 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) ∈ ℂ)
410404, 360mulcld 10057 . . . . 5 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) ∈ ℂ)
411408, 409, 410fsumsub 14514 . . . 4 (𝜑 → Σ𝑗 ∈ (0...𝑀)((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))) = (Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))))
412 etransclem46.qe0 . . . . . . . . 9 (𝜑 → (𝑄‘e) = 0)
413412eqcomd 2627 . . . . . . . 8 (𝜑 → 0 = (𝑄‘e))
414395, 23coeid2 23989 . . . . . . . . 9 ((𝑄 ∈ (Poly‘ℤ) ∧ e ∈ ℂ) → (𝑄‘e) = Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑗)))
41525, 9, 414sylancl 694 . . . . . . . 8 (𝜑 → (𝑄‘e) = Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑗)))
416 cxpexp 24408 . . . . . . . . . . . . 13 ((e ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (e↑𝑐𝑗) = (e↑𝑗))
417353, 398, 416syl2anc 693 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (e↑𝑐𝑗) = (e↑𝑗))
418417eqcomd 2627 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑀) → (e↑𝑗) = (e↑𝑐𝑗))
419418oveq2d 6663 . . . . . . . . . 10 (𝑗 ∈ (0...𝑀) → ((𝐴𝑗) · (e↑𝑗)) = ((𝐴𝑗) · (e↑𝑐𝑗)))
420419adantl 482 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · (e↑𝑗)) = ((𝐴𝑗) · (e↑𝑐𝑗)))
421420sumeq2dv 14427 . . . . . . . 8 (𝜑 → Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑗)) = Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑐𝑗)))
422413, 415, 4213eqtrd 2659 . . . . . . 7 (𝜑 → 0 = Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑐𝑗)))
423422oveq1d 6662 . . . . . 6 (𝜑 → (0 · (𝐺‘0)) = (Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)))
424374mul02d 10231 . . . . . 6 (𝜑 → (0 · (𝐺‘0)) = 0)
425408, 374, 404fsummulc1 14511 . . . . . 6 (𝜑 → (Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) = Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)))
426423, 424, 4253eqtr3rd 2664 . . . . 5 (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) = 0)
42738a1i 11 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)))
428 fveq2 6189 . . . . . . . . . . . . 13 (𝑥 = 𝑗 → (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) = (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
429428sumeq2sdv 14429 . . . . . . . . . . . 12 (𝑥 = 𝑗 → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
430429adantl 482 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 = 𝑗) → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
431 fzfid 12767 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (0...𝑅) ∈ Fin)
43233adantlr 751 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
433204adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → 𝑗 ∈ ℝ)
434432, 433ffvelrnd 6358 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
435431, 434fsumcl 14458 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
436427, 430, 204, 435fvmptd 6286 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐺𝑗) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
437436oveq2d 6663 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((e↑𝑐-𝑗) · (𝐺𝑗)) = ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
438437oveq2d 6663 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) = (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))))
439357, 435mulcld 10057 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) ∈ ℂ)
440401, 403, 439mulassd 10060 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))) = ((𝐴𝑗) · ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))))
441368eqcomi 2630 . . . . . . . . . . . . . . 15 1 = (e↑𝑐0)
442441a1i 11 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → 1 = (e↑𝑐0))
443354negidd 10379 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → (𝑗 + -𝑗) = 0)
444443eqcomd 2627 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 0 = (𝑗 + -𝑗))
445444oveq2d 6663 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (e↑𝑐0) = (e↑𝑐(𝑗 + -𝑗)))
44653, 54gtneii 10146 . . . . . . . . . . . . . . . 16 e ≠ 0
447446a1i 11 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → e ≠ 0)
448353, 447, 354, 355cxpaddd 24457 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (e↑𝑐(𝑗 + -𝑗)) = ((e↑𝑐𝑗) · (e↑𝑐-𝑗)))
449442, 445, 4483eqtrd 2659 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 1 = ((e↑𝑐𝑗) · (e↑𝑐-𝑗)))
450449oveq1d 6662 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = (((e↑𝑐𝑗) · (e↑𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
451450adantl 482 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = (((e↑𝑐𝑗) · (e↑𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
452435mulid2d 10055 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
453403, 357, 435mulassd 10060 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (((e↑𝑐𝑗) · (e↑𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))))
454451, 452, 4533eqtr3rd 2664 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
455454oveq2d 6663 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))) = ((𝐴𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
456431, 401, 434fsummulc2 14510 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
457455, 456eqtrd 2655 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))) = Σ𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
458438, 440, 4573eqtrd 2659 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) = Σ𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
459458sumeq2dv 14427 . . . . . 6 (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) = Σ𝑗 ∈ (0...𝑀𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
460 vex 3201 . . . . . . . . . 10 𝑗 ∈ V
461 vex 3201 . . . . . . . . . 10 𝑖 ∈ V
462460, 461op1std 7175 . . . . . . . . 9 (𝑘 = ⟨𝑗, 𝑖⟩ → (1st𝑘) = 𝑗)
463462fveq2d 6193 . . . . . . . 8 (𝑘 = ⟨𝑗, 𝑖⟩ → (𝐴‘(1st𝑘)) = (𝐴𝑗))
464460, 461op2ndd 7176 . . . . . . . . . 10 (𝑘 = ⟨𝑗, 𝑖⟩ → (2nd𝑘) = 𝑖)
465464fveq2d 6193 . . . . . . . . 9 (𝑘 = ⟨𝑗, 𝑖⟩ → ((ℝ D𝑛 𝐹)‘(2nd𝑘)) = ((ℝ D𝑛 𝐹)‘𝑖))
466465, 462fveq12d 6195 . . . . . . . 8 (𝑘 = ⟨𝑗, 𝑖⟩ → (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) = (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
467463, 466oveq12d 6665 . . . . . . 7 (𝑘 = ⟨𝑗, 𝑖⟩ → ((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) = ((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
468 fzfid 12767 . . . . . . 7 (𝜑 → (0...𝑅) ∈ Fin)
469401adantrr 753 . . . . . . . 8 ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → (𝐴𝑗) ∈ ℂ)
470434anasss 679 . . . . . . . 8 ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
471469, 470mulcld 10057 . . . . . . 7 ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → ((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) ∈ ℂ)
472467, 408, 468, 471fsumxp 14497 . . . . . 6 (𝜑 → Σ𝑗 ∈ (0...𝑀𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
473459, 472eqtrd 2655 . . . . 5 (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) = Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
474426, 473oveq12d 6665 . . . 4 (𝜑 → (Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))) = (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)))))
475 df-neg 10266 . . . . . 6 𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) = (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
476475eqcomi 2630 . . . . 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 2659 . . 3 (𝜑 → Σ𝑗 ∈ (0...𝑀)((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))) = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
4792, 407, 4783eqtrd 2659 . 2 (𝜑𝐿 = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
480479oveq1d 6662 1 (𝜑 → (𝐿 / (!‘(𝑃 − 1))) = (-Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  w3a 1037   = wceq 1482  wtru 1483  wcel 1989  wne 2793  Vcvv 3198  cdif 3569  wss 3572  ifcif 4084  {csn 4175  {cpr 4177  cop 4181   class class class wbr 4651  cmpt 4727   × cxp 5110  ran crn 5113  wf 5882  cfv 5886  (class class class)co 6647  1st c1st 7163  2nd c2nd 7164  pm cpm 7855  cc 9931  cr 9932  0cc0 9933  1c1 9934   + caddc 9936   · cmul 9938  -∞cmnf 10069  *cxr 10070   < clt 10071  cle 10072  cmin 10263  -cneg 10264   / cdiv 10681  cn 11017  0cn0 11289  cz 11374  cuz 11684  +crp 11829  (,)cioo 12172  (,]cioc 12173  [,]cicc 12175  ...cfz 12323  cexp 12855  !cfa 13055  Σcsu 14410  cprod 14629  eceu 14787  t crest 16075  TopOpenctopn 16076  topGenctg 16092  fldccnfld 19740  intcnt 20815  cnccncf 22673  𝐿1cibl 23380  citg 23381  0𝑝c0p 23430   D cdv 23621   D𝑛 cdvn 23622  Polycply 23934  coeffccoe 23936  degcdgr 23937  logclog 24295  𝑐ccxp 24296
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-inf2 8535  ax-cc 9254  ax-cnex 9989  ax-resscn 9990  ax-1cn 9991  ax-icn 9992  ax-addcl 9993  ax-addrcl 9994  ax-mulcl 9995  ax-mulrcl 9996  ax-mulcom 9997  ax-addass 9998  ax-mulass 9999  ax-distr 10000  ax-i2m1 10001  ax-1ne0 10002  ax-1rid 10003  ax-rnegex 10004  ax-rrecex 10005  ax-cnre 10006  ax-pre-lttri 10007  ax-pre-lttrn 10008  ax-pre-ltadd 10009  ax-pre-mulgt0 10010  ax-pre-sup 10011  ax-addf 10012  ax-mulf 10013
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-fal 1488  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-nel 2897  df-ral 2916  df-rex 2917  df-reu 2918  df-rmo 2919  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-int 4474  df-iun 4520  df-iin 4521  df-disj 4619  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-se 5072  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-isom 5895  df-riota 6608  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-of 6894  df-ofr 6895  df-om 7063  df-1st 7165  df-2nd 7166  df-supp 7293  df-wrecs 7404  df-recs 7465  df-rdg 7503  df-1o 7557  df-2o 7558  df-oadd 7561  df-omul 7562  df-er 7739  df-map 7856  df-pm 7857  df-ixp 7906  df-en 7953  df-dom 7954  df-sdom 7955  df-fin 7956  df-fsupp 8273  df-fi 8314  df-sup 8345  df-inf 8346  df-oi 8412  df-card 8762  df-acn 8765  df-cda 8987  df-pnf 10073  df-mnf 10074  df-xr 10075  df-ltxr 10076  df-le 10077  df-sub 10265  df-neg 10266  df-div 10682  df-nn 11018  df-2 11076  df-3 11077  df-4 11078  df-5 11079  df-6 11080  df-7 11081  df-8 11082  df-9 11083  df-n0 11290  df-z 11375  df-dec 11491  df-uz 11685  df-q 11786  df-rp 11830  df-xneg 11943  df-xadd 11944  df-xmul 11945  df-ioo 12176  df-ioc 12177  df-ico 12178  df-icc 12179  df-fz 12324  df-fzo 12462  df-fl 12588  df-mod 12664  df-seq 12797  df-exp 12856  df-fac 13056  df-bc 13085  df-hash 13113  df-shft 13801  df-cj 13833  df-re 13834  df-im 13835  df-sqrt 13969  df-abs 13970  df-limsup 14196  df-clim 14213  df-rlim 14214  df-sum 14411  df-prod 14630  df-ef 14792  df-e 14793  df-sin 14794  df-cos 14795  df-tan 14796  df-pi 14797  df-struct 15853  df-ndx 15854  df-slot 15855  df-base 15857  df-sets 15858  df-ress 15859  df-plusg 15948  df-mulr 15949  df-starv 15950  df-sca 15951  df-vsca 15952  df-ip 15953  df-tset 15954  df-ple 15955  df-ds 15958  df-unif 15959  df-hom 15960  df-cco 15961  df-rest 16077  df-topn 16078  df-0g 16096  df-gsum 16097  df-topgen 16098  df-pt 16099  df-prds 16102  df-xrs 16156  df-qtop 16161  df-imas 16162  df-xps 16164  df-mre 16240  df-mrc 16241  df-acs 16243  df-mgm 17236  df-sgrp 17278  df-mnd 17289  df-submnd 17330  df-mulg 17535  df-cntz 17744  df-cmn 18189  df-psmet 19732  df-xmet 19733  df-met 19734  df-bl 19735  df-mopn 19736  df-fbas 19737  df-fg 19738  df-cnfld 19741  df-top 20693  df-topon 20710  df-topsp 20731  df-bases 20744  df-cld 20817  df-ntr 20818  df-cls 20819  df-nei 20896  df-lp 20934  df-perf 20935  df-cn 21025  df-cnp 21026  df-haus 21113  df-cmp 21184  df-tx 21359  df-hmeo 21552  df-fil 21644  df-fm 21736  df-flim 21737  df-flf 21738  df-xms 22119  df-ms 22120  df-tms 22121  df-cncf 22675  df-ovol 23227  df-vol 23228  df-mbf 23382  df-itg1 23383  df-itg2 23384  df-ibl 23385  df-itg 23386  df-0p 23431  df-limc 23624  df-dv 23625  df-dvn 23626  df-ply 23938  df-coe 23940  df-dgr 23941  df-log 24297  df-cxp 24298
This theorem is referenced by:  etransclem47  40267
  Copyright terms: Public domain W3C validator