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 42026
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 6986 . . . . . . . . . . . . 13 (ℝ D 𝑂) = (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥))))
54a1i 11 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) = (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))))
6 etransclem46.s . . . . . . . . . . . . . 14 (𝜑 → ℝ ∈ {ℝ, ℂ})
76adantr 473 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → ℝ ∈ {ℝ, ℂ})
8 ere 15301 . . . . . . . . . . . . . . . . . . . 20 e ∈ ℝ
98recni 10453 . . . . . . . . . . . . . . . . . . 19 e ∈ ℂ
109a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → e ∈ ℂ)
11 recn 10424 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
1211negcld 10784 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → -𝑥 ∈ ℂ)
1310, 12cxpcld 25008 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (e↑𝑐-𝑥) ∈ ℂ)
1413adantl 474 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → (e↑𝑐-𝑥) ∈ ℂ)
15 simpr 477 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
16 fzfid 13155 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → (0...𝑅) ∈ Fin)
17 elfznn0 12815 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (0...𝑅) → 𝑖 ∈ ℕ0)
186adantr 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → ℝ ∈ {ℝ, ℂ})
19 etransclem46.x . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))
2019adantr 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))
21 etransclem46.p . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑃 ∈ ℕ)
2221adantr 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → 𝑃 ∈ ℕ)
23 etransclem46.m . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑀 = (deg‘𝑄)
24 etransclem46.q . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑄 ∈ ((Poly‘ℤ) ∖ {0𝑝}))
2524eldifad 3836 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑄 ∈ (Poly‘ℤ))
26 dgrcl 24542 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑄 ∈ (Poly‘ℤ) → (deg‘𝑄) ∈ ℕ0)
2725, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (deg‘𝑄) ∈ ℕ0)
2823, 27syl5eqel 2865 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑀 ∈ ℕ0)
2928adantr 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → 𝑀 ∈ ℕ0)
30 etransclem46.f . . . . . . . . . . . . . . . . . . . . . . 23 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃)))
31 simpr 477 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ ℕ0) → 𝑖 ∈ ℕ0)
3218, 20, 22, 29, 30, 31etransclem33 42013 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
3317, 32sylan2 584 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
3433adantlr 703 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
35 simplr 757 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → 𝑥 ∈ ℝ)
3634, 35ffvelrnd 6676 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ)
3716, 36fsumcl 14949 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ)
38 etransclem46.g . . . . . . . . . . . . . . . . . . 19 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))
3938fvmpt2 6604 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ) → (𝐺𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))
4015, 37, 39syl2anc 576 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → (𝐺𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))
4140, 37eqeltrd 2861 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → (𝐺𝑥) ∈ ℂ)
4214, 41mulcld 10459 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · (𝐺𝑥)) ∈ ℂ)
4342negcld 10784 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → -((e↑𝑐-𝑥) · (𝐺𝑥)) ∈ ℂ)
4443adantlr 703 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ ℝ) → -((e↑𝑐-𝑥) · (𝐺𝑥)) ∈ ℂ)
456, 19dvdmsscn 41681 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ℝ ⊆ ℂ)
4645, 21, 30etransclem8 41988 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:ℝ⟶ℂ)
4746ffvelrnda 6675 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℂ)
4814, 47mulcld 10459 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
4948negcld 10784 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ) → -((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
5049negcld 10784 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → --((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
5150adantlr 703 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ ℝ) → --((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
528a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → e ∈ ℝ)
53 0re 10440 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℝ
54 epos 15419 . . . . . . . . . . . . . . . . . . . . . 22 0 < e
5553, 8, 54ltleii 10562 . . . . . . . . . . . . . . . . . . . . 21 0 ≤ e
5655a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → 0 ≤ e)
57 renegcl 10749 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → -𝑥 ∈ ℝ)
5852, 56, 57recxpcld 25023 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → (e↑𝑐-𝑥) ∈ ℝ)
5958renegcld 10867 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → -(e↑𝑐-𝑥) ∈ ℝ)
6059adantl 474 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → -(e↑𝑐-𝑥) ∈ ℝ)
61 reelprrecn 10426 . . . . . . . . . . . . . . . . . . . . . 22 ℝ ∈ {ℝ, ℂ}
6261a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → ℝ ∈ {ℝ, ℂ})
63 cnelprrecn 10427 . . . . . . . . . . . . . . . . . . . . . 22 ℂ ∈ {ℝ, ℂ}
6463a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → ℂ ∈ {ℝ, ℂ})
6512adantl 474 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑥 ∈ ℝ) → -𝑥 ∈ ℂ)
66 neg1rr 11561 . . . . . . . . . . . . . . . . . . . . . 22 -1 ∈ ℝ
6766a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑥 ∈ ℝ) → -1 ∈ ℝ)
689a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℂ → e ∈ ℂ)
69 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℂ → 𝑦 ∈ ℂ)
7068, 69cxpcld 25008 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℂ → (e↑𝑐𝑦) ∈ ℂ)
7170adantl 474 . . . . . . . . . . . . . . . . . . . . 21 ((⊤ ∧ 𝑦 ∈ ℂ) → (e↑𝑐𝑦) ∈ ℂ)
7211adantl 474 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
73 1red 10439 . . . . . . . . . . . . . . . . . . . . . 22 ((⊤ ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
7462dvmptid 24273 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ 𝑥)) = (𝑥 ∈ ℝ ↦ 1))
7562, 72, 73, 74dvmptneg 24282 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ -𝑥)) = (𝑥 ∈ ℝ ↦ -1))
76 epr 15420 . . . . . . . . . . . . . . . . . . . . . . . 24 e ∈ ℝ+
77 dvcxp2 25039 . . . . . . . . . . . . . . . . . . . . . . . 24 (e ∈ ℝ+ → (ℂ D (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑𝑐𝑦))))
7876, 77ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (ℂ D (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑𝑐𝑦)))
79 loge 24887 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (log‘e) = 1
8079oveq1i 6985 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((log‘e) · (e↑𝑐𝑦)) = (1 · (e↑𝑐𝑦))
8170mulid2d 10457 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ℂ → (1 · (e↑𝑐𝑦)) = (e↑𝑐𝑦))
8280, 81syl5eq 2821 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ℂ → ((log‘e) · (e↑𝑐𝑦)) = (e↑𝑐𝑦))
8382mpteq2ia 5015 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℂ ↦ ((log‘e) · (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))
8478, 83eqtri 2797 . . . . . . . . . . . . . . . . . . . . . 22 (ℂ D (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))
8584a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))) = (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)))
86 oveq2 6983 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = -𝑥 → (e↑𝑐𝑦) = (e↑𝑐-𝑥))
8762, 64, 65, 67, 71, 71, 75, 85, 86, 86dvmptco 24288 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ (e↑𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -1)))
8887mptru 1515 . . . . . . . . . . . . . . . . . . 19 (ℝ D (𝑥 ∈ ℝ ↦ (e↑𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -1))
8966a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → -1 ∈ ℝ)
9089recnd 10467 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → -1 ∈ ℂ)
9113, 90mulcomd 10460 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → ((e↑𝑐-𝑥) · -1) = (-1 · (e↑𝑐-𝑥)))
9213mulm1d 10892 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → (-1 · (e↑𝑐-𝑥)) = -(e↑𝑐-𝑥))
9391, 92eqtrd 2809 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ → ((e↑𝑐-𝑥) · -1) = -(e↑𝑐-𝑥))
9493mpteq2ia 5015 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -1)) = (𝑥 ∈ ℝ ↦ -(e↑𝑐-𝑥))
9588, 94eqtri 2797 . . . . . . . . . . . . . . . . . 18 (ℝ D (𝑥 ∈ ℝ ↦ (e↑𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ -(e↑𝑐-𝑥))
9695a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (e↑𝑐-𝑥))) = (𝑥 ∈ ℝ ↦ -(e↑𝑐-𝑥)))
9717adantl 474 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0...𝑅)) → 𝑖 ∈ ℕ0)
98 peano2nn0 11748 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℕ0)
9997, 98syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0...𝑅)) → (𝑖 + 1) ∈ ℕ0)
100 ovex 7007 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 + 1) ∈ V
101 eleq1 2848 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = (𝑖 + 1) → (𝑗 ∈ ℕ0 ↔ (𝑖 + 1) ∈ ℕ0))
102101anbi2d 620 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = (𝑖 + 1) → ((𝜑𝑗 ∈ ℕ0) ↔ (𝜑 ∧ (𝑖 + 1) ∈ ℕ0)))
103 fveq2 6497 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = (𝑖 + 1) → ((ℝ D𝑛 𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘(𝑖 + 1)))
104103feq1d 6327 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = (𝑖 + 1) → (((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ ↔ ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ))
105102, 104imbi12d 337 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑖 + 1) → (((𝜑𝑗 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ) ↔ ((𝜑 ∧ (𝑖 + 1) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)))
106 eleq1 2848 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑗 → (𝑖 ∈ ℕ0𝑗 ∈ ℕ0))
107106anbi2d 620 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑗 → ((𝜑𝑖 ∈ ℕ0) ↔ (𝜑𝑗 ∈ ℕ0)))
108 fveq2 6497 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑗 → ((ℝ D𝑛 𝐹)‘𝑖) = ((ℝ D𝑛 𝐹)‘𝑗))
109108feq1d 6327 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑗 → (((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ ↔ ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ))
110107, 109imbi12d 337 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = 𝑗 → (((𝜑𝑖 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ) ↔ ((𝜑𝑗 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)))
111110, 32chvarv 2328 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
112100, 105, 111vtocl 3473 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑖 + 1) ∈ ℕ0) → ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
11399, 112syldan 583 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
114113adantlr 703 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ)
115114, 35ffvelrnd 6676 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ)
11616, 115fsumcl 14949 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ)
11721, 28, 30, 38etransclem39 42019 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐺:ℝ⟶ℂ)
118117feqmptd 6561 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺 = (𝑥 ∈ ℝ ↦ (𝐺𝑥)))
119118eqcomd 2779 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑥 ∈ ℝ ↦ (𝐺𝑥)) = 𝐺)
120119oveq2d 6991 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝐺𝑥))) = (ℝ D 𝐺))
121 nfcv 2927 . . . . . . . . . . . . . . . . . . 19 𝑥𝐹
122 elfznn0 12815 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ (0...(𝑅 + 1)) → 𝑖 ∈ ℕ0)
123122, 32sylan2 584 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0...(𝑅 + 1))) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
124121, 46, 123, 38etransclem2 41982 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℝ D 𝐺) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
125120, 124eqtrd 2809 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ (𝐺𝑥))) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
1266, 14, 60, 96, 41, 116, 125dvmptmul 24277 . . . . . . . . . . . . . . . 16 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ ℝ ↦ ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥)))))
127116, 14mulcomd 10460 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥)) = ((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)))
128127oveq2d 6991 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥))) = ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + ((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))))
12914negcld 10784 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → -(e↑𝑐-𝑥) ∈ ℂ)
130129, 41mulcld 10459 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → (-(e↑𝑐-𝑥) · (𝐺𝑥)) ∈ ℂ)
13114, 116mulcld 10459 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) ∈ ℂ)
132130, 131addcomd 10641 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + ((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) = (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑𝑐-𝑥) · (𝐺𝑥))))
133131, 42negsubd 10803 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + -((e↑𝑐-𝑥) · (𝐺𝑥))) = (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) − ((e↑𝑐-𝑥) · (𝐺𝑥))))
13414, 41mulneg1d 10893 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (-(e↑𝑐-𝑥) · (𝐺𝑥)) = -((e↑𝑐-𝑥) · (𝐺𝑥)))
135134oveq2d 6991 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑𝑐-𝑥) · (𝐺𝑥))) = (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + -((e↑𝑐-𝑥) · (𝐺𝑥))))
13614, 116, 41subdid 10896 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥))) = (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) − ((e↑𝑐-𝑥) · (𝐺𝑥))))
137133, 135, 1363eqtr4d 2819 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑𝑐-𝑥) · (𝐺𝑥))) = ((e↑𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥))))
13840oveq2d 6991 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥)) = (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)))
13916, 115, 36fsumsub 15002 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)((((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)) = (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)))
140 fveq2 6497 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑖 → ((ℝ D𝑛 𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘𝑖))
141140fveq1d 6499 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑖 → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥))
142103fveq1d 6499 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑖 + 1) → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))
143 fveq2 6497 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 0 → ((ℝ D𝑛 𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘0))
144143fveq1d 6499 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 0 → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D𝑛 𝐹)‘0)‘𝑥))
145 fveq2 6497 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = (𝑅 + 1) → ((ℝ D𝑛 𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘(𝑅 + 1)))
146145fveq1d 6499 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑅 + 1) → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) = (((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥))
147 etransclem46.r . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑅 = ((𝑀 · 𝑃) + (𝑃 − 1))
14821nnnn0d 11766 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑃 ∈ ℕ0)
14928, 148nn0mulcld 11771 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑀 · 𝑃) ∈ ℕ0)
150 nnm1nn0 11749 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ0)
15121, 150syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑃 − 1) ∈ ℕ0)
152149, 151nn0addcld 11770 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) ∈ ℕ0)
153147, 152syl5eqel 2865 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑅 ∈ ℕ0)
154153adantr 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → 𝑅 ∈ ℕ0)
155154nn0zd 11897 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → 𝑅 ∈ ℤ)
156 peano2nn0 11748 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑅 ∈ ℕ0 → (𝑅 + 1) ∈ ℕ0)
157153, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑅 + 1) ∈ ℕ0)
158 nn0uz 12093 . . . . . . . . . . . . . . . . . . . . . . . 24 0 = (ℤ‘0)
159157, 158syl6eleq 2871 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑅 + 1) ∈ (ℤ‘0))
160159adantr 473 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (𝑅 + 1) ∈ (ℤ‘0))
161 elfznn0 12815 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 ∈ (0...(𝑅 + 1)) → 𝑗 ∈ ℕ0)
162161, 111sylan2 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
163162adantlr 703 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)
164 simplr 757 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → 𝑥 ∈ ℝ)
165163, 164ffvelrnd 6676 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ) ∧ 𝑗 ∈ (0...(𝑅 + 1))) → (((ℝ D𝑛 𝐹)‘𝑗)‘𝑥) ∈ ℂ)
166141, 142, 144, 146, 155, 160, 165telfsum2 15019 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → Σ𝑖 ∈ (0...𝑅)((((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)) = ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥)))
167138, 139, 1663eqtr2d 2815 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥)) = ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥)))
168167oveq2d 6991 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) − (𝐺𝑥))) = ((e↑𝑐-𝑥) · ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥))))
169153nn0red 11767 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑅 ∈ ℝ)
170169ltp1d 11370 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑅 < (𝑅 + 1))
171147, 170syl5eqbrr 4962 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) < (𝑅 + 1))
172 etransclem5 41985 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ ℝ ↦ ((𝑦𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ ℝ ↦ ((𝑥𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))))
1736, 19, 21, 28, 30, 157, 171, 172etransclem32 42012 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((ℝ D𝑛 𝐹)‘(𝑅 + 1)) = (𝑥 ∈ ℝ ↦ 0))
174173fveq1d 6499 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) = ((𝑥 ∈ ℝ ↦ 0)‘𝑥))
175 eqid 2773 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℝ ↦ 0) = (𝑥 ∈ ℝ ↦ 0)
176175fvmpt2 6604 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ ℝ ∧ 0 ∈ ℝ) → ((𝑥 ∈ ℝ ↦ 0)‘𝑥) = 0)
17753, 176mpan2 679 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → ((𝑥 ∈ ℝ ↦ 0)‘𝑥) = 0)
178174, 177sylan9eq 2829 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) = 0)
179 cnex 10415 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℂ ∈ V
180179a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ℂ ∈ V)
181 etransclem46.rex . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ℝ ⊆ ℝ)
1826, 181ssexd 5081 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ℝ ∈ V)
183 elpm2r 8223 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:ℝ⟶ℂ ∧ ℝ ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑pm ℝ))
184180, 182, 46, 181, 183syl22anc 827 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹 ∈ (ℂ ↑pm ℝ))
185 dvn0 24240 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℝ ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm ℝ)) → ((ℝ D𝑛 𝐹)‘0) = 𝐹)
18645, 184, 185syl2anc 576 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((ℝ D𝑛 𝐹)‘0) = 𝐹)
187186fveq1d 6499 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((ℝ D𝑛 𝐹)‘0)‘𝑥) = (𝐹𝑥))
188187adantr 473 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → (((ℝ D𝑛 𝐹)‘0)‘𝑥) = (𝐹𝑥))
189178, 188oveq12d 6993 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥)) = (0 − (𝐹𝑥)))
190 df-neg 10672 . . . . . . . . . . . . . . . . . . . . 21 -(𝐹𝑥) = (0 − (𝐹𝑥))
191189, 190syl6eqr 2827 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥)) = -(𝐹𝑥))
192191oveq2d 6991 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · ((((ℝ D𝑛 𝐹)‘(𝑅 + 1))‘𝑥) − (((ℝ D𝑛 𝐹)‘0)‘𝑥))) = ((e↑𝑐-𝑥) · -(𝐹𝑥)))
193137, 168, 1923eqtrd 2813 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ) → (((e↑𝑐-𝑥) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥)) + (-(e↑𝑐-𝑥) · (𝐺𝑥))) = ((e↑𝑐-𝑥) · -(𝐹𝑥)))
194128, 132, 1933eqtrd 2813 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥))) = ((e↑𝑐-𝑥) · -(𝐹𝑥)))
195194mpteq2dva 5019 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ ℝ ↦ ((-(e↑𝑐-𝑥) · (𝐺𝑥)) + (Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) · (e↑𝑐-𝑥)))) = (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -(𝐹𝑥))))
19614, 47mulneg2d 10894 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ) → ((e↑𝑐-𝑥) · -(𝐹𝑥)) = -((e↑𝑐-𝑥) · (𝐹𝑥)))
197196mpteq2dva 5019 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · -(𝐹𝑥))) = (𝑥 ∈ ℝ ↦ -((e↑𝑐-𝑥) · (𝐹𝑥))))
198126, 195, 1973eqtrd 2813 . . . . . . . . . . . . . . 15 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ ((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ ℝ ↦ -((e↑𝑐-𝑥) · (𝐹𝑥))))
1996, 42, 49, 198dvmptneg 24282 . . . . . . . . . . . . . 14 (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ ℝ ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))))
200199adantr 473 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D (𝑥 ∈ ℝ ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ ℝ ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))))
201 0red 10442 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ)
202 elfzelz 12723 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℤ)
203202zred 11899 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℝ)
204203adantl 474 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ)
205201, 204iccssred 41241 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℝ)
206 eqid 2773 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
207206tgioo2 23130 . . . . . . . . . . . . 13 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
208 0red 10442 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 0 ∈ ℝ)
209 iccntr 23148 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ 𝑗 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
210208, 203, 209syl2anc 576 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
211210adantl 474 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → ((int‘(topGen‘ran (,)))‘(0[,]𝑗)) = (0(,)𝑗))
2127, 44, 51, 200, 205, 207, 206, 211dvmptres2 24278 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥)))) = (𝑥 ∈ (0(,)𝑗) ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))))
2139a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0(,)𝑗)) → e ∈ ℂ)
214 elioore 12583 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℝ)
215214recnd 10467 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (0(,)𝑗) → 𝑥 ∈ ℂ)
216215adantl 474 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℂ)
217216negcld 10784 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0(,)𝑗)) → -𝑥 ∈ ℂ)
218213, 217cxpcld 25008 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0(,)𝑗)) → (e↑𝑐-𝑥) ∈ ℂ)
21946adantr 473 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0(,)𝑗)) → 𝐹:ℝ⟶ℂ)
220214adantl 474 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ ℝ)
221219, 220ffvelrnd 6676 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0(,)𝑗)) → (𝐹𝑥) ∈ ℂ)
222218, 221mulcld 10459 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (0(,)𝑗)) → ((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
223222negnegd 10788 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (0(,)𝑗)) → --((e↑𝑐-𝑥) · (𝐹𝑥)) = ((e↑𝑐-𝑥) · (𝐹𝑥)))
224223mpteq2dva 5019 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (0(,)𝑗) ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))))
225224adantr 473 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ --((e↑𝑐-𝑥) · (𝐹𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))))
2265, 212, 2253eqtrd 2813 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))))
227226fveq1d 6499 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ((ℝ D 𝑂)‘𝑥) = ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥))
228227adantr 473 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((ℝ D 𝑂)‘𝑥) = ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥))
229 simpr 477 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (0(,)𝑗)) → 𝑥 ∈ (0(,)𝑗))
230 eqid 2773 . . . . . . . . . . . 12 (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) = (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))
231230fvmpt2 6604 . . . . . . . . . . 11 ((𝑥 ∈ (0(,)𝑗) ∧ ((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥) = ((e↑𝑐-𝑥) · (𝐹𝑥)))
232229, 222, 231syl2anc 576 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0(,)𝑗)) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥) = ((e↑𝑐-𝑥) · (𝐹𝑥)))
233232adantlr 703 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))‘𝑥) = ((e↑𝑐-𝑥) · (𝐹𝑥)))
234228, 233eqtr2d 2810 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑𝑐-𝑥) · (𝐹𝑥)) = ((ℝ D 𝑂)‘𝑥))
235234itgeq2d 41728 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥 = ∫(0(,)𝑗)((ℝ D 𝑂)‘𝑥) d𝑥)
236 elfzle1 12725 . . . . . . . . 9 (𝑗 ∈ (0...𝑀) → 0 ≤ 𝑗)
237236adantl 474 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ≤ 𝑗)
238 eqid 2773 . . . . . . . . . 10 (𝑥 ∈ (0[,]𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) = (𝑥 ∈ (0[,]𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥)))
239 eqidd 2774 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)) = (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)))
24086adantl 474 . . . . . . . . . . . . . . . 16 (((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) ∧ 𝑦 = -𝑥) → (e↑𝑐𝑦) = (e↑𝑐-𝑥))
241208, 203iccssred 41241 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (0...𝑀) → (0[,]𝑗) ⊆ ℝ)
242 ax-resscn 10391 . . . . . . . . . . . . . . . . . . 19 ℝ ⊆ ℂ
243241, 242syl6ss 3865 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (0...𝑀) → (0[,]𝑗) ⊆ ℂ)
244243sselda 3853 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℂ)
245244negcld 10784 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → -𝑥 ∈ ℂ)
2469a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → e ∈ ℂ)
247 negcl 10685 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → -𝑥 ∈ ℂ)
248246, 247cxpcld 25008 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → (e↑𝑐-𝑥) ∈ ℂ)
249244, 248syl 17 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑𝑐-𝑥) ∈ ℂ)
250239, 240, 245, 249fvmptd 6600 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥) = (e↑𝑐-𝑥))
251250eqcomd 2779 . . . . . . . . . . . . . 14 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑𝑐-𝑥) = ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥))
252251adantll 702 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (e↑𝑐-𝑥) = ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥))
253252mpteq2dva 5019 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (e↑𝑐-𝑥)) = (𝑥 ∈ (0[,]𝑗) ↦ ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥)))
254 mnfxr 10497 . . . . . . . . . . . . . . . . . 18 -∞ ∈ ℝ*
255254a1i 11 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → -∞ ∈ ℝ*)
256 0red 10442 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → 0 ∈ ℝ)
257 rpxr 12214 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → e ∈ ℝ*)
258 rpgt0 12217 . . . . . . . . . . . . . . . . 17 (e ∈ ℝ+ → 0 < e)
259255, 256, 257, 258gtnelioc 41226 . . . . . . . . . . . . . . . 16 (e ∈ ℝ+ → ¬ e ∈ (-∞(,]0))
26076, 259ax-mp 5 . . . . . . . . . . . . . . 15 ¬ e ∈ (-∞(,]0)
261 eldif 3834 . . . . . . . . . . . . . . 15 (e ∈ (ℂ ∖ (-∞(,]0)) ↔ (e ∈ ℂ ∧ ¬ e ∈ (-∞(,]0)))
2629, 260, 261mpbir2an 699 . . . . . . . . . . . . . 14 e ∈ (ℂ ∖ (-∞(,]0))
263 cxpcncf2 41643 . . . . . . . . . . . . . 14 (e ∈ (ℂ ∖ (-∞(,]0)) → (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)) ∈ (ℂ–cn→ℂ))
264262, 263mp1i 13 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (e↑𝑐𝑦)) ∈ (ℂ–cn→ℂ))
265 eqid 2773 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) = (𝑥 ∈ (0[,]𝑗) ↦ -𝑥)
266265negcncf 23245 . . . . . . . . . . . . . . 15 ((0[,]𝑗) ⊆ ℂ → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
267243, 266syl 17 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
268267adantl 474 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ -𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
269264, 268cncfmpt1f 23240 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((𝑦 ∈ ℂ ↦ (e↑𝑐𝑦))‘-𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
270253, 269eqeltrd 2861 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (e↑𝑐-𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
271242a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → ℝ ⊆ ℂ)
27221ad2antrr 714 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ)
27328ad2antrr 714 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑀 ∈ ℕ0)
274 etransclem6 41986 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃))) = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦𝑘)↑𝑃)))
27530, 274eqtri 2797 . . . . . . . . . . . . . 14 𝐹 = (𝑦 ∈ ℝ ↦ ((𝑦↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑦𝑘)↑𝑃)))
276241sselda 3853 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (0...𝑀) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℝ)
277276adantll 702 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℝ)
278271, 272, 273, 275, 277etransclem13 41993 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝐹𝑥) = ∏𝑘 ∈ (0...𝑀)((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))
279278mpteq2dva 5019 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐹𝑥)) = (𝑥 ∈ (0[,]𝑗) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))))
280243adantl 474 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℂ)
281 fzfid 13155 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → (0...𝑀) ∈ Fin)
282277recnd 10467 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝑥 ∈ ℂ)
2832823adant3 1113 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → 𝑥 ∈ ℂ)
284 elfzelz 12723 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℤ)
285284zcnd 11900 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℂ)
2862853ad2ant3 1116 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
287283, 286subcld 10797 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥𝑘) ∈ ℂ)
28821adantr 473 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ)
289288, 150syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0[,]𝑗)) → (𝑃 − 1) ∈ ℕ0)
290148adantr 473 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (0[,]𝑗)) → 𝑃 ∈ ℕ0)
291289, 290ifcld 4390 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (0[,]𝑗)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0)
2922913adant3 1113 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0)
2932923adant1r 1158 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0)
294287, 293expcld 13324 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) ∈ ℂ)
295 nfv 1874 . . . . . . . . . . . . . 14 𝑥((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀))
296243adantr 473 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (0[,]𝑗) ⊆ ℂ)
297 ssid 3874 . . . . . . . . . . . . . . . . . 18 ℂ ⊆ ℂ
298297a1i 11 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
299296, 298idcncfg 41615 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ 𝑥) ∈ ((0[,]𝑗)–cn→ℂ))
300285adantl 474 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
301296, 300, 298constcncfg 41614 . . . . . . . . . . . . . . . 16 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ 𝑘) ∈ ((0[,]𝑗)–cn→ℂ))
302299, 301subcncf 41612 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (0...𝑀) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝑥𝑘)) ∈ ((0[,]𝑗)–cn→ℂ))
303302adantll 702 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝑥𝑘)) ∈ ((0[,]𝑗)–cn→ℂ))
304151, 148ifcld 4390 . . . . . . . . . . . . . . . 16 (𝜑 → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0)
305 expcncf 23249 . . . . . . . . . . . . . . . 16 (if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℕ0 → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
306304, 305syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
307306ad2antrr 714 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑦 ∈ ℂ ↦ (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ (ℂ–cn→ℂ))
308297a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
309 oveq1 6982 . . . . . . . . . . . . . 14 (𝑦 = (𝑥𝑘) → (𝑦↑if(𝑘 = 0, (𝑃 − 1), 𝑃)) = ((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))
310295, 303, 307, 308, 309cncfcompt2 41642 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((0[,]𝑗)–cn→ℂ))
311280, 281, 294, 310fprodcncf 41644 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ∏𝑘 ∈ (0...𝑀)((𝑥𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃))) ∈ ((0[,]𝑗)–cn→ℂ))
312279, 311eqeltrd 2861 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐹𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
313270, 312mulcncf 23766 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
314 ioossicc 12637 . . . . . . . . . . 11 (0(,)𝑗) ⊆ (0[,]𝑗)
315314a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (0(,)𝑗) ⊆ (0[,]𝑗))
316297a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ℂ ⊆ ℂ)
317222adantlr 703 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0(,)𝑗)) → ((e↑𝑐-𝑥) · (𝐹𝑥)) ∈ ℂ)
318238, 313, 315, 316, 317cncfmptssg 41613 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) ∈ ((0(,)𝑗)–cn→ℂ))
319226, 318eqeltrd 2861 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) ∈ ((0(,)𝑗)–cn→ℂ))
32019adantr 473 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ℝ ∈ ((TopOpen‘ℂfld) ↾t ℝ))
32121adantr 473 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑃 ∈ ℕ)
32228adantr 473 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑀 ∈ ℕ0)
323 oveq2 6983 . . . . . . . . . . . . . . 15 (𝑗 = 𝑘 → (𝑥𝑗) = (𝑥𝑘))
324323oveq1d 6990 . . . . . . . . . . . . . 14 (𝑗 = 𝑘 → ((𝑥𝑗)↑𝑃) = ((𝑥𝑘)↑𝑃))
325324cbvprodv 15129 . . . . . . . . . . . . 13 𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃) = ∏𝑘 ∈ (1...𝑀)((𝑥𝑘)↑𝑃)
326325oveq2i 6986 . . . . . . . . . . . 12 ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃)) = ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥𝑘)↑𝑃))
327326mpteq2i 5016 . . . . . . . . . . 11 (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥𝑗)↑𝑃))) = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥𝑘)↑𝑃)))
32830, 327eqtri 2797 . . . . . . . . . 10 𝐹 = (𝑥 ∈ ℝ ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑘 ∈ (1...𝑀)((𝑥𝑘)↑𝑃)))
3297, 320, 321, 322, 328, 201, 204etransclem18 41998 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0(,)𝑗) ↦ ((e↑𝑐-𝑥) · (𝐹𝑥))) ∈ 𝐿1)
330226, 329eqeltrd 2861 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (ℝ D 𝑂) ∈ 𝐿1)
331 eqid 2773 . . . . . . . . . . . 12 (𝑥 ∈ ℝ ↦ (𝐺𝑥)) = (𝑥 ∈ ℝ ↦ (𝐺𝑥))
3326, 19, 21, 28, 30, 38etransclem43 42023 . . . . . . . . . . . . . 14 (𝜑𝐺 ∈ (ℝ–cn→ℂ))
333119, 332eqeltrd 2861 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ ℝ ↦ (𝐺𝑥)) ∈ (ℝ–cn→ℂ))
334333adantr 473 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ ℝ ↦ (𝐺𝑥)) ∈ (ℝ–cn→ℂ))
335117ad2antrr 714 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → 𝐺:ℝ⟶ℂ)
336335, 277ffvelrnd 6676 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 ∈ (0[,]𝑗)) → (𝐺𝑥) ∈ ℂ)
337331, 334, 205, 316, 336cncfmptssg 41613 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ (𝐺𝑥)) ∈ ((0[,]𝑗)–cn→ℂ))
338270, 337mulcncf 23766 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ ((e↑𝑐-𝑥) · (𝐺𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
339338negcncfg 41624 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥))) ∈ ((0[,]𝑗)–cn→ℂ))
3403, 339syl5eqel 2865 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑂 ∈ ((0[,]𝑗)–cn→ℂ))
341201, 204, 237, 319, 330, 340ftc2 24360 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((ℝ D 𝑂)‘𝑥) d𝑥 = ((𝑂𝑗) − (𝑂‘0)))
342 negeq 10677 . . . . . . . . . . . . 13 (𝑥 = 𝑗 → -𝑥 = -𝑗)
343342oveq2d 6991 . . . . . . . . . . . 12 (𝑥 = 𝑗 → (e↑𝑐-𝑥) = (e↑𝑐-𝑗))
344 fveq2 6497 . . . . . . . . . . . 12 (𝑥 = 𝑗 → (𝐺𝑥) = (𝐺𝑗))
345343, 344oveq12d 6993 . . . . . . . . . . 11 (𝑥 = 𝑗 → ((e↑𝑐-𝑥) · (𝐺𝑥)) = ((e↑𝑐-𝑗) · (𝐺𝑗)))
346345negeqd 10679 . . . . . . . . . 10 (𝑥 = 𝑗 → -((e↑𝑐-𝑥) · (𝐺𝑥)) = -((e↑𝑐-𝑗) · (𝐺𝑗)))
347201rexrd 10489 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ ℝ*)
348204rexrd 10489 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℝ*)
349 ubicc2 12668 . . . . . . . . . . 11 ((0 ∈ ℝ*𝑗 ∈ ℝ* ∧ 0 ≤ 𝑗) → 𝑗 ∈ (0[,]𝑗))
350347, 348, 237, 349syl3anc 1352 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0[,]𝑗))
3519a1i 11 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → e ∈ ℂ)
352203recnd 10467 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℂ)
353352negcld 10784 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → -𝑗 ∈ ℂ)
354351, 353cxpcld 25008 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → (e↑𝑐-𝑗) ∈ ℂ)
355354adantl 474 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (e↑𝑐-𝑗) ∈ ℂ)
356117adantr 473 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...𝑀)) → 𝐺:ℝ⟶ℂ)
357356, 204ffvelrnd 6676 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐺𝑗) ∈ ℂ)
358355, 357mulcld 10459 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → ((e↑𝑐-𝑗) · (𝐺𝑗)) ∈ ℂ)
359358negcld 10784 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → -((e↑𝑐-𝑗) · (𝐺𝑗)) ∈ ℂ)
3603, 346, 350, 359fvmptd3 6616 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑂𝑗) = -((e↑𝑐-𝑗) · (𝐺𝑗)))
3613a1i 11 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑂 = (𝑥 ∈ (0[,]𝑗) ↦ -((e↑𝑐-𝑥) · (𝐺𝑥))))
362 negeq 10677 . . . . . . . . . . . . . . . 16 (𝑥 = 0 → -𝑥 = -0)
363362oveq2d 6991 . . . . . . . . . . . . . . 15 (𝑥 = 0 → (e↑𝑐-𝑥) = (e↑𝑐-0))
364 neg0 10732 . . . . . . . . . . . . . . . . 17 -0 = 0
365364oveq2i 6986 . . . . . . . . . . . . . . . 16 (e↑𝑐-0) = (e↑𝑐0)
366 cxp0 24970 . . . . . . . . . . . . . . . . 17 (e ∈ ℂ → (e↑𝑐0) = 1)
3679, 366ax-mp 5 . . . . . . . . . . . . . . . 16 (e↑𝑐0) = 1
368365, 367eqtri 2797 . . . . . . . . . . . . . . 15 (e↑𝑐-0) = 1
369363, 368syl6eq 2825 . . . . . . . . . . . . . 14 (𝑥 = 0 → (e↑𝑐-𝑥) = 1)
370 fveq2 6497 . . . . . . . . . . . . . 14 (𝑥 = 0 → (𝐺𝑥) = (𝐺‘0))
371369, 370oveq12d 6993 . . . . . . . . . . . . 13 (𝑥 = 0 → ((e↑𝑐-𝑥) · (𝐺𝑥)) = (1 · (𝐺‘0)))
372 0red 10442 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ ℝ)
373117, 372ffvelrnd 6676 . . . . . . . . . . . . . 14 (𝜑 → (𝐺‘0) ∈ ℂ)
374373mulid2d 10457 . . . . . . . . . . . . 13 (𝜑 → (1 · (𝐺‘0)) = (𝐺‘0))
375371, 374sylan9eqr 2831 . . . . . . . . . . . 12 ((𝜑𝑥 = 0) → ((e↑𝑐-𝑥) · (𝐺𝑥)) = (𝐺‘0))
376375negeqd 10679 . . . . . . . . . . 11 ((𝜑𝑥 = 0) → -((e↑𝑐-𝑥) · (𝐺𝑥)) = -(𝐺‘0))
377376adantlr 703 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑥 = 0) → -((e↑𝑐-𝑥) · (𝐺𝑥)) = -(𝐺‘0))
378 lbicc2 12667 . . . . . . . . . . 11 ((0 ∈ ℝ*𝑗 ∈ ℝ* ∧ 0 ≤ 𝑗) → 0 ∈ (0[,]𝑗))
379347, 348, 237, 378syl3anc 1352 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ (0[,]𝑗))
380373negcld 10784 . . . . . . . . . . 11 (𝜑 → -(𝐺‘0) ∈ ℂ)
381380adantr 473 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → -(𝐺‘0) ∈ ℂ)
382361, 377, 379, 381fvmptd 6600 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝑂‘0) = -(𝐺‘0))
383360, 382oveq12d 6993 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑂𝑗) − (𝑂‘0)) = (-((e↑𝑐-𝑗) · (𝐺𝑗)) − -(𝐺‘0)))
384373adantr 473 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐺‘0) ∈ ℂ)
385359, 384subnegd 10804 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (-((e↑𝑐-𝑗) · (𝐺𝑗)) − -(𝐺‘0)) = (-((e↑𝑐-𝑗) · (𝐺𝑗)) + (𝐺‘0)))
386359, 384addcomd 10641 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → (-((e↑𝑐-𝑗) · (𝐺𝑗)) + (𝐺‘0)) = ((𝐺‘0) + -((e↑𝑐-𝑗) · (𝐺𝑗))))
387384, 358negsubd 10803 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐺‘0) + -((e↑𝑐-𝑗) · (𝐺𝑗))) = ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗))))
388386, 387eqtrd 2809 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (-((e↑𝑐-𝑗) · (𝐺𝑗)) + (𝐺‘0)) = ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗))))
389383, 385, 3883eqtrd 2813 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝑂𝑗) − (𝑂‘0)) = ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗))))
390235, 341, 3893eqtrd 2813 . . . . . 6 ((𝜑𝑗 ∈ (0...𝑀)) → ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥 = ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗))))
391390oveq2d 6991 . . . . 5 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥) = (((𝐴𝑗) · (e↑𝑐𝑗)) · ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗)))))
39225adantr 473 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑄 ∈ (Poly‘ℤ))
393 0zd 11804 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → 0 ∈ ℤ)
394 etransclem46.a . . . . . . . . . . 11 𝐴 = (coeff‘𝑄)
395394coef2 24540 . . . . . . . . . 10 ((𝑄 ∈ (Poly‘ℤ) ∧ 0 ∈ ℤ) → 𝐴:ℕ0⟶ℤ)
396392, 393, 395syl2anc 576 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → 𝐴:ℕ0⟶ℤ)
397 elfznn0 12815 . . . . . . . . . 10 (𝑗 ∈ (0...𝑀) → 𝑗 ∈ ℕ0)
398397adantl 474 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → 𝑗 ∈ ℕ0)
399396, 398ffvelrnd 6676 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐴𝑗) ∈ ℤ)
400399zcnd 11900 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐴𝑗) ∈ ℂ)
401351, 352cxpcld 25008 . . . . . . . 8 (𝑗 ∈ (0...𝑀) → (e↑𝑐𝑗) ∈ ℂ)
402401adantl 474 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → (e↑𝑐𝑗) ∈ ℂ)
403400, 402mulcld 10459 . . . . . 6 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · (e↑𝑐𝑗)) ∈ ℂ)
404403, 384, 358subdid 10896 . . . . 5 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((𝐺‘0) − ((e↑𝑐-𝑗) · (𝐺𝑗)))) = ((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))))
405391, 404eqtrd 2809 . . . 4 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥) = ((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))))
406405sumeq2dv 14919 . . 3 (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ∫(0(,)𝑗)((e↑𝑐-𝑥) · (𝐹𝑥)) d𝑥) = Σ𝑗 ∈ (0...𝑀)((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))))
407 fzfid 13155 . . . . 5 (𝜑 → (0...𝑀) ∈ Fin)
408403, 384mulcld 10459 . . . . 5 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) ∈ ℂ)
409403, 358mulcld 10459 . . . . 5 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) ∈ ℂ)
410407, 408, 409fsumsub 15002 . . . 4 (𝜑 → Σ𝑗 ∈ (0...𝑀)((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))) = (Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))))
411 etransclem46.qe0 . . . . . . . . 9 (𝜑 → (𝑄‘e) = 0)
412411eqcomd 2779 . . . . . . . 8 (𝜑 → 0 = (𝑄‘e))
413394, 23coeid2 24548 . . . . . . . . 9 ((𝑄 ∈ (Poly‘ℤ) ∧ e ∈ ℂ) → (𝑄‘e) = Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑗)))
41425, 9, 413sylancl 578 . . . . . . . 8 (𝜑 → (𝑄‘e) = Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑗)))
415 cxpexp 24968 . . . . . . . . . . . . 13 ((e ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (e↑𝑐𝑗) = (e↑𝑗))
416351, 397, 415syl2anc 576 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (e↑𝑐𝑗) = (e↑𝑗))
417416eqcomd 2779 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑀) → (e↑𝑗) = (e↑𝑐𝑗))
418417oveq2d 6991 . . . . . . . . . 10 (𝑗 ∈ (0...𝑀) → ((𝐴𝑗) · (e↑𝑗)) = ((𝐴𝑗) · (e↑𝑐𝑗)))
419418adantl 474 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · (e↑𝑗)) = ((𝐴𝑗) · (e↑𝑐𝑗)))
420419sumeq2dv 14919 . . . . . . . 8 (𝜑 → Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑗)) = Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑐𝑗)))
421412, 414, 4203eqtrd 2813 . . . . . . 7 (𝜑 → 0 = Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑐𝑗)))
422421oveq1d 6990 . . . . . 6 (𝜑 → (0 · (𝐺‘0)) = (Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)))
423373mul02d 10637 . . . . . 6 (𝜑 → (0 · (𝐺‘0)) = 0)
424407, 373, 403fsummulc1 14999 . . . . . 6 (𝜑 → (Σ𝑗 ∈ (0...𝑀)((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) = Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)))
425422, 423, 4243eqtr3rd 2818 . . . . 5 (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) = 0)
426 fveq2 6497 . . . . . . . . . . . 12 (𝑥 = 𝑗 → (((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) = (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
427426sumeq2sdv 14920 . . . . . . . . . . 11 (𝑥 = 𝑗 → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
428 fzfid 13155 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝑀)) → (0...𝑅) ∈ Fin)
42933adantlr 703 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ)
430204adantr 473 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → 𝑗 ∈ ℝ)
431429, 430ffvelrnd 6676 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑀)) ∧ 𝑖 ∈ (0...𝑅)) → (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
432428, 431fsumcl 14949 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
43338, 427, 204, 432fvmptd3 6616 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → (𝐺𝑗) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
434433oveq2d 6991 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((e↑𝑐-𝑗) · (𝐺𝑗)) = ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
435434oveq2d 6991 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) = (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))))
436355, 432mulcld 10459 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) ∈ ℂ)
437400, 402, 436mulassd 10462 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))) = ((𝐴𝑗) · ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))))
438367eqcomi 2782 . . . . . . . . . . . . . . 15 1 = (e↑𝑐0)
439438a1i 11 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → 1 = (e↑𝑐0))
440352negidd 10787 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...𝑀) → (𝑗 + -𝑗) = 0)
441440eqcomd 2779 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → 0 = (𝑗 + -𝑗))
442441oveq2d 6991 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (e↑𝑐0) = (e↑𝑐(𝑗 + -𝑗)))
44353, 54gtneii 10551 . . . . . . . . . . . . . . . 16 e ≠ 0
444443a1i 11 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑀) → e ≠ 0)
445351, 444, 352, 353cxpaddd 25017 . . . . . . . . . . . . . 14 (𝑗 ∈ (0...𝑀) → (e↑𝑐(𝑗 + -𝑗)) = ((e↑𝑐𝑗) · (e↑𝑐-𝑗)))
446439, 442, 4453eqtrd 2813 . . . . . . . . . . . . 13 (𝑗 ∈ (0...𝑀) → 1 = ((e↑𝑐𝑗) · (e↑𝑐-𝑗)))
447446oveq1d 6990 . . . . . . . . . . . 12 (𝑗 ∈ (0...𝑀) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = (((e↑𝑐𝑗) · (e↑𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
448447adantl 474 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = (((e↑𝑐𝑗) · (e↑𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
449432mulid2d 10457 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (1 · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
450402, 355, 432mulassd 10462 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...𝑀)) → (((e↑𝑐𝑗) · (e↑𝑐-𝑗)) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))))
451448, 449, 4503eqtr3rd 2818 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑀)) → ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))) = Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
452451oveq2d 6991 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))) = ((𝐴𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
453428, 400, 431fsummulc2 14998 . . . . . . . . 9 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
454452, 453eqtrd 2809 . . . . . . . 8 ((𝜑𝑗 ∈ (0...𝑀)) → ((𝐴𝑗) · ((e↑𝑐𝑗) · ((e↑𝑐-𝑗) · Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))) = Σ𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
455435, 437, 4543eqtrd 2813 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑀)) → (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) = Σ𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
456455sumeq2dv 14919 . . . . . 6 (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) = Σ𝑗 ∈ (0...𝑀𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
457 vex 3413 . . . . . . . . . 10 𝑗 ∈ V
458 vex 3413 . . . . . . . . . 10 𝑖 ∈ V
459457, 458op1std 7510 . . . . . . . . 9 (𝑘 = ⟨𝑗, 𝑖⟩ → (1st𝑘) = 𝑗)
460459fveq2d 6501 . . . . . . . 8 (𝑘 = ⟨𝑗, 𝑖⟩ → (𝐴‘(1st𝑘)) = (𝐴𝑗))
461457, 458op2ndd 7511 . . . . . . . . . 10 (𝑘 = ⟨𝑗, 𝑖⟩ → (2nd𝑘) = 𝑖)
462461fveq2d 6501 . . . . . . . . 9 (𝑘 = ⟨𝑗, 𝑖⟩ → ((ℝ D𝑛 𝐹)‘(2nd𝑘)) = ((ℝ D𝑛 𝐹)‘𝑖))
463462, 459fveq12d 6504 . . . . . . . 8 (𝑘 = ⟨𝑗, 𝑖⟩ → (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)) = (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗))
464460, 463oveq12d 6993 . . . . . . 7 (𝑘 = ⟨𝑗, 𝑖⟩ → ((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) = ((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)))
465 fzfid 13155 . . . . . . 7 (𝜑 → (0...𝑅) ∈ Fin)
466400adantrr 705 . . . . . . . 8 ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → (𝐴𝑗) ∈ ℂ)
467431anasss 459 . . . . . . . 8 ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗) ∈ ℂ)
468466, 467mulcld 10459 . . . . . . 7 ((𝜑 ∧ (𝑗 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑅))) → ((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) ∈ ℂ)
469464, 407, 465, 468fsumxp 14986 . . . . . 6 (𝜑 → Σ𝑗 ∈ (0...𝑀𝑖 ∈ (0...𝑅)((𝐴𝑗) · (((ℝ D𝑛 𝐹)‘𝑖)‘𝑗)) = Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
470456, 469eqtrd 2809 . . . . 5 (𝜑 → Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗))) = Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
471425, 470oveq12d 6993 . . . 4 (𝜑 → (Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − Σ𝑗 ∈ (0...𝑀)(((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))) = (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)))))
472 df-neg 10672 . . . . . 6 𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) = (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
473472eqcomi 2782 . . . . 5 (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)))) = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)))
474473a1i 11 . . . 4 (𝜑 → (0 − Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘)))) = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
475410, 471, 4743eqtrd 2813 . . 3 (𝜑 → Σ𝑗 ∈ (0...𝑀)((((𝐴𝑗) · (e↑𝑐𝑗)) · (𝐺‘0)) − (((𝐴𝑗) · (e↑𝑐𝑗)) · ((e↑𝑐-𝑗) · (𝐺𝑗)))) = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
4762, 406, 4753eqtrd 2813 . 2 (𝜑𝐿 = -Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))))
477476oveq1d 6990 1 (𝜑 → (𝐿 / (!‘(𝑃 − 1))) = (-Σ𝑘 ∈ ((0...𝑀) × (0...𝑅))((𝐴‘(1st𝑘)) · (((ℝ D𝑛 𝐹)‘(2nd𝑘))‘(1st𝑘))) / (!‘(𝑃 − 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 387  w3a 1069   = wceq 1508  wtru 1509  wcel 2051  wne 2962  Vcvv 3410  cdif 3821  wss 3824  ifcif 4345  {csn 4436  {cpr 4438  cop 4442   class class class wbr 4926  cmpt 5005   × cxp 5402  ran crn 5405  wf 6182  cfv 6186  (class class class)co 6975  1st c1st 7498  2nd c2nd 7499  pm cpm 8206  cc 10332  cr 10333  0cc0 10334  1c1 10335   + caddc 10337   · cmul 10339  -∞cmnf 10471  *cxr 10472   < clt 10473  cle 10474  cmin 10669  -cneg 10670   / cdiv 11097  cn 11438  0cn0 11706  cz 11792  cuz 12057  +crp 12203  (,)cioo 12553  (,]cioc 12554  [,]cicc 12556  ...cfz 12707  cexp 13243  !cfa 13447  Σcsu 14902  cprod 15118  eceu 15275  t crest 16549  TopOpenctopn 16550  topGenctg 16566  fldccnfld 20263  intcnt 21345  cnccncf 23203  𝐿1cibl 23937  citg 23938  0𝑝c0p 23989   D cdv 24180   D𝑛 cdvn 24181  Polycply 24493  coeffccoe 24495  degcdgr 24496  logclog 24855  𝑐ccxp 24856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-rep 5046  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278  ax-inf2 8897  ax-cc 9654  ax-cnex 10390  ax-resscn 10391  ax-1cn 10392  ax-icn 10393  ax-addcl 10394  ax-addrcl 10395  ax-mulcl 10396  ax-mulrcl 10397  ax-mulcom 10398  ax-addass 10399  ax-mulass 10400  ax-distr 10401  ax-i2m1 10402  ax-1ne0 10403  ax-1rid 10404  ax-rnegex 10405  ax-rrecex 10406  ax-cnre 10407  ax-pre-lttri 10408  ax-pre-lttrn 10409  ax-pre-ltadd 10410  ax-pre-mulgt0 10411  ax-pre-sup 10412  ax-addf 10413  ax-mulf 10414
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-fal 1521  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-nel 3069  df-ral 3088  df-rex 3089  df-reu 3090  df-rmo 3091  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-pss 3840  df-symdif 4101  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-tp 4441  df-op 4443  df-uni 4710  df-int 4747  df-iun 4791  df-iin 4792  df-disj 4895  df-br 4927  df-opab 4989  df-mpt 5006  df-tr 5028  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-se 5364  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-isom 6195  df-riota 6936  df-ov 6978  df-oprab 6979  df-mpo 6980  df-of 7226  df-ofr 7227  df-om 7396  df-1st 7500  df-2nd 7501  df-supp 7633  df-wrecs 7749  df-recs 7811  df-rdg 7849  df-1o 7904  df-2o 7905  df-oadd 7908  df-omul 7909  df-er 8088  df-map 8207  df-pm 8208  df-ixp 8259  df-en 8306  df-dom 8307  df-sdom 8308  df-fin 8309  df-fsupp 8628  df-fi 8669  df-sup 8700  df-inf 8701  df-oi 8768  df-dju 9123  df-card 9161  df-acn 9164  df-cda 9387  df-pnf 10475  df-mnf 10476  df-xr 10477  df-ltxr 10478  df-le 10479  df-sub 10671  df-neg 10672  df-div 11098  df-nn 11439  df-2 11502  df-3 11503  df-4 11504  df-5 11505  df-6 11506  df-7 11507  df-8 11508  df-9 11509  df-n0 11707  df-z 11793  df-dec 11911  df-uz 12058  df-q 12162  df-rp 12204  df-xneg 12323  df-xadd 12324  df-xmul 12325  df-ioo 12557  df-ioc 12558  df-ico 12559  df-icc 12560  df-fz 12708  df-fzo 12849  df-fl 12976  df-mod 13052  df-seq 13184  df-exp 13244  df-fac 13448  df-bc 13477  df-hash 13505  df-shft 14286  df-cj 14318  df-re 14319  df-im 14320  df-sqrt 14454  df-abs 14455  df-limsup 14688  df-clim 14705  df-rlim 14706  df-sum 14903  df-prod 15119  df-ef 15280  df-e 15281  df-sin 15282  df-cos 15283  df-tan 15284  df-pi 15285  df-struct 16340  df-ndx 16341  df-slot 16342  df-base 16344  df-sets 16345  df-ress 16346  df-plusg 16433  df-mulr 16434  df-starv 16435  df-sca 16436  df-vsca 16437  df-ip 16438  df-tset 16439  df-ple 16440  df-ds 16442  df-unif 16443  df-hom 16444  df-cco 16445  df-rest 16551  df-topn 16552  df-0g 16570  df-gsum 16571  df-topgen 16572  df-pt 16573  df-prds 16576  df-xrs 16630  df-qtop 16635  df-imas 16636  df-xps 16638  df-mre 16728  df-mrc 16729  df-acs 16731  df-mgm 17723  df-sgrp 17765  df-mnd 17776  df-submnd 17817  df-mulg 18025  df-cntz 18231  df-cmn 18681  df-psmet 20255  df-xmet 20256  df-met 20257  df-bl 20258  df-mopn 20259  df-fbas 20260  df-fg 20261  df-cnfld 20264  df-top 21222  df-topon 21239  df-topsp 21261  df-bases 21274  df-cld 21347  df-ntr 21348  df-cls 21349  df-nei 21426  df-lp 21464  df-perf 21465  df-cn 21555  df-cnp 21556  df-haus 21643  df-cmp 21715  df-tx 21890  df-hmeo 22083  df-fil 22174  df-fm 22266  df-flim 22267  df-flf 22268  df-xms 22649  df-ms 22650  df-tms 22651  df-cncf 23205  df-ovol 23784  df-vol 23785  df-mbf 23939  df-itg1 23940  df-itg2 23941  df-ibl 23942  df-itg 23943  df-0p 23990  df-limc 24183  df-dv 24184  df-dvn 24185  df-ply 24497  df-coe 24499  df-dgr 24500  df-log 24857  df-cxp 24858
This theorem is referenced by:  etransclem47  42027
  Copyright terms: Public domain W3C validator