etransclem2

Description: Derivative of G . (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem2.xf	⊢ Ⅎ 𝑥 𝐹
	etransclem2.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
	etransclem2.dvnf	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝑅 + 1 ) ) ) → ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) : ℝ ⟶ ℂ )
	etransclem2.g	⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... 𝑅 ) ( ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) )
Assertion	etransclem2	⊢ ( 𝜑 → ( ℝ D 𝐺 ) = ( 𝑥 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... 𝑅 ) ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		etransclem2.xf	⊢ Ⅎ 𝑥 𝐹
2		etransclem2.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
3		etransclem2.dvnf	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝑅 + 1 ) ) ) → ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) : ℝ ⟶ ℂ )
4		etransclem2.g	⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... 𝑅 ) ( ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) )
5	4	oveq2i	⊢ ( ℝ D 𝐺 ) = ( ℝ D ( 𝑥 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... 𝑅 ) ( ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) ) )
6		tgioo4	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂ_fld ) ↾_t ℝ )
7		eqid	⊢ ( TopOpen ‘ ℂ_fld ) = ( TopOpen ‘ ℂ_fld )
8		reelprrecn	⊢ ℝ ∈ { ℝ , ℂ }
9	8	a1i	⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
10		reopn	⊢ ℝ ∈ ( topGen ‘ ran (,) )
11	10	a1i	⊢ ( 𝜑 → ℝ ∈ ( topGen ‘ ran (,) ) )
12		fzfid	⊢ ( 𝜑 → ( 0 ... 𝑅 ) ∈ Fin )
13		fzelp1	⊢ ( 𝑖 ∈ ( 0 ... 𝑅 ) → 𝑖 ∈ ( 0 ... ( 𝑅 + 1 ) ) )
14	13 3	sylan2	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) : ℝ ⟶ ℂ )
15	14	3adant3	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ∧ 𝑥 ∈ ℝ ) → ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) : ℝ ⟶ ℂ )
16		simp3	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
17	15 16	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) ∈ ℂ )
18		fzp1elp1	⊢ ( 𝑖 ∈ ( 0 ... 𝑅 ) → ( 𝑖 + 1 ) ∈ ( 0 ... ( 𝑅 + 1 ) ) )
19		ovex	⊢ ( 𝑖 + 1 ) ∈ V
20		eleq1	⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( 𝑗 ∈ ( 0 ... ( 𝑅 + 1 ) ) ↔ ( 𝑖 + 1 ) ∈ ( 0 ... ( 𝑅 + 1 ) ) ) )
21	20	anbi2d	⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝑅 + 1 ) ) ) ↔ ( 𝜑 ∧ ( 𝑖 + 1 ) ∈ ( 0 ... ( 𝑅 + 1 ) ) ) ) )
22		fveq2	⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑗 ) = ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) )
23	22	feq1d	⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑗 ) : ℝ ⟶ ℂ ↔ ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) : ℝ ⟶ ℂ ) )
24	21 23	imbi12d	⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝑅 + 1 ) ) ) → ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑗 ) : ℝ ⟶ ℂ ) ↔ ( ( 𝜑 ∧ ( 𝑖 + 1 ) ∈ ( 0 ... ( 𝑅 + 1 ) ) ) → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) : ℝ ⟶ ℂ ) ) )
25		eleq1	⊢ ( 𝑖 = 𝑗 → ( 𝑖 ∈ ( 0 ... ( 𝑅 + 1 ) ) ↔ 𝑗 ∈ ( 0 ... ( 𝑅 + 1 ) ) ) )
26	25	anbi2d	⊢ ( 𝑖 = 𝑗 → ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝑅 + 1 ) ) ) ↔ ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝑅 + 1 ) ) ) ) )
27		fveq2	⊢ ( 𝑖 = 𝑗 → ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) = ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑗 ) )
28	27	feq1d	⊢ ( 𝑖 = 𝑗 → ( ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) : ℝ ⟶ ℂ ↔ ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑗 ) : ℝ ⟶ ℂ ) )
29	26 28	imbi12d	⊢ ( 𝑖 = 𝑗 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝑅 + 1 ) ) ) → ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) : ℝ ⟶ ℂ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝑅 + 1 ) ) ) → ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑗 ) : ℝ ⟶ ℂ ) ) )
30	29 3	chvarvv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝑅 + 1 ) ) ) → ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑗 ) : ℝ ⟶ ℂ )
31	19 24 30	vtocl	⊢ ( ( 𝜑 ∧ ( 𝑖 + 1 ) ∈ ( 0 ... ( 𝑅 + 1 ) ) ) → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) : ℝ ⟶ ℂ )
32	18 31	sylan2	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) : ℝ ⟶ ℂ )
33	32	3adant3	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ∧ 𝑥 ∈ ℝ ) → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) : ℝ ⟶ ℂ )
34	33 16	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) ‘ 𝑥 ) ∈ ℂ )
35	14	ffnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) Fn ℝ )
36		nfcv	⊢ Ⅎ 𝑥 ℝ
37		nfcv	⊢ Ⅎ 𝑥 D^𝑛
38	36 37 1	nfov	⊢ Ⅎ 𝑥 ( ℝ D^𝑛 𝐹 )
39		nfcv	⊢ Ⅎ 𝑥 𝑖
40	38 39	nffv	⊢ Ⅎ 𝑥 ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 )
41	40	dffn5f	⊢ ( ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) Fn ℝ ↔ ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) = ( 𝑥 ∈ ℝ ↦ ( ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) ) )
42	35 41	sylib	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) = ( 𝑥 ∈ ℝ ↦ ( ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) ) )
43	42	eqcomd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ( 𝑥 ∈ ℝ ↦ ( ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) ) = ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) )
44	43	oveq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ( ℝ D ( 𝑥 ∈ ℝ ↦ ( ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) ) ) = ( ℝ D ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) ) )
45		ax-resscn	⊢ ℝ ⊆ ℂ
46	45	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ℝ ⊆ ℂ )
47		ffdm	⊢ ( 𝐹 : ℝ ⟶ ℂ → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℝ ) )
48	2 47	syl	⊢ ( 𝜑 → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℝ ) )
49		cnex	⊢ ℂ ∈ V
50	49	a1i	⊢ ( 𝜑 → ℂ ∈ V )
51		reex	⊢ ℝ ∈ V
52		elpm2g	⊢ ( ( ℂ ∈ V ∧ ℝ ∈ V ) → ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℝ ) ) )
53	50 51 52	sylancl	⊢ ( 𝜑 → ( 𝐹 ∈ ( ℂ ↑_pm ℝ ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℝ ) ) )
54	48 53	mpbird	⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑_pm ℝ ) )
55	54	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → 𝐹 ∈ ( ℂ ↑_pm ℝ ) )
56		elfznn0	⊢ ( 𝑖 ∈ ( 0 ... 𝑅 ) → 𝑖 ∈ ℕ₀ )
57	56	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → 𝑖 ∈ ℕ₀ )
58		dvnp1	⊢ ( ( ℝ ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑_pm ℝ ) ∧ 𝑖 ∈ ℕ₀ ) → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) = ( ℝ D ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) ) )
59	46 55 57 58	syl3anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) = ( ℝ D ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) ) )
60	32	ffnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) Fn ℝ )
61		nfcv	⊢ Ⅎ 𝑥 ( 𝑖 + 1 )
62	38 61	nffv	⊢ Ⅎ 𝑥 ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) )
63	62	dffn5f	⊢ ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) Fn ℝ ↔ ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) = ( 𝑥 ∈ ℝ ↦ ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) ‘ 𝑥 ) ) )
64	60 63	sylib	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) = ( 𝑥 ∈ ℝ ↦ ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) ‘ 𝑥 ) ) )
65	44 59 64	3eqtr2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑅 ) ) → ( ℝ D ( 𝑥 ∈ ℝ ↦ ( ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) ‘ 𝑥 ) ) )
66	6 7 9 11 12 17 34 65	dvmptfsum	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... 𝑅 ) ( ( ( ℝ D^𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... 𝑅 ) ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) ‘ 𝑥 ) ) )
67	5 66	eqtrid	⊢ ( 𝜑 → ( ℝ D 𝐺 ) = ( 𝑥 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... 𝑅 ) ( ( ( ℝ D^𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) ‘ 𝑥 ) ) )

Metamath Proof Explorer

Theorem etransclem2

Proof