etransclem2

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

	Ref	Expression
Hypotheses	etransclem2.xf	$⊢ \underline{Ⅎ} x F$
	etransclem2.f	$⊢ φ \to F : ℝ ⟶ ℂ$
	etransclem2.dvnf	$⊢ (φ \land i \in (0 \dots R + 1)) \to (ℝ D^{n} F) (i) : ℝ ⟶ ℂ$
	etransclem2.g	$⊢ G = (x \in ℝ ⟼ \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (x))$
Assertion	etransclem2	$⊢ φ \to ℝ D G = (x \in ℝ ⟼ \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x))$

Proof

Step	Hyp	Ref	Expression
1		etransclem2.xf	$⊢ \underline{Ⅎ} x F$
2		etransclem2.f	$⊢ φ \to F : ℝ ⟶ ℂ$
3		etransclem2.dvnf	$⊢ (φ \land i \in (0 \dots R + 1)) \to (ℝ D^{n} F) (i) : ℝ ⟶ ℂ$
4		etransclem2.g	$⊢ G = (x \in ℝ ⟼ \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (x))$
5	4	oveq2i	$⊢ ℝ D G = \frac{d (x \in ℝ⟼ \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (x))}{d_{ℝ} x}$
6		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
7	6	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
8		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
9	8	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
10		reopn	$⊢ ℝ \in topGen (ran (.))$
11	10	a1i	$⊢ φ \to ℝ \in topGen (ran (.))$
12		fzfid	$⊢ φ \to (0 \dots R) \in Fin$
13		fzelp1	$⊢ i \in (0 \dots R) \to i \in (0 \dots R + 1)$
14	13 3	sylan2	$⊢ (φ \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i) : ℝ ⟶ ℂ$
15	14	3adant3	$⊢ (φ \land i \in (0 \dots R) \land x \in ℝ) \to (ℝ D^{n} F) (i) : ℝ ⟶ ℂ$
16		simp3	$⊢ (φ \land i \in (0 \dots R) \land x \in ℝ) \to x \in ℝ$
17	15 16	ffvelrnd	$⊢ (φ \land i \in (0 \dots R) \land x \in ℝ) \to (ℝ D^{n} F) (i) (x) \in ℂ$
18		fzp1elp1	$⊢ i \in (0 \dots R) \to i + 1 \in (0 \dots R + 1)$
19		ovex	$⊢ i + 1 \in V$
20		eleq1	$⊢ j = i + 1 \to (j \in (0 \dots R + 1) \leftrightarrow i + 1 \in (0 \dots R + 1))$
21	20	anbi2d	$⊢ j = i + 1 \to ((φ \land j \in (0 \dots R + 1)) \leftrightarrow (φ \land i + 1 \in (0 \dots R + 1)))$
22		fveq2	$⊢ j = i + 1 \to (ℝ D^{n} F) (j) = (ℝ D^{n} F) (i + 1)$
23	22	feq1d	$⊢ j = i + 1 \to ((ℝ D^{n} F) (j) : ℝ ⟶ ℂ \leftrightarrow (ℝ D^{n} F) (i + 1) : ℝ ⟶ ℂ)$
24	21 23	imbi12d	$⊢ j = i + 1 \to (((φ \land j \in (0 \dots R + 1)) \to (ℝ D^{n} F) (j) : ℝ ⟶ ℂ) \leftrightarrow ((φ \land i + 1 \in (0 \dots R + 1)) \to (ℝ D^{n} F) (i + 1) : ℝ ⟶ ℂ))$
25		eleq1	$⊢ i = j \to (i \in (0 \dots R + 1) \leftrightarrow j \in (0 \dots R + 1))$
26	25	anbi2d	$⊢ i = j \to ((φ \land i \in (0 \dots R + 1)) \leftrightarrow (φ \land j \in (0 \dots R + 1)))$
27		fveq2	$⊢ i = j \to (ℝ D^{n} F) (i) = (ℝ D^{n} F) (j)$
28	27	feq1d	$⊢ i = j \to ((ℝ D^{n} F) (i) : ℝ ⟶ ℂ \leftrightarrow (ℝ D^{n} F) (j) : ℝ ⟶ ℂ)$
29	26 28	imbi12d	$⊢ i = j \to (((φ \land i \in (0 \dots R + 1)) \to (ℝ D^{n} F) (i) : ℝ ⟶ ℂ) \leftrightarrow ((φ \land j \in (0 \dots R + 1)) \to (ℝ D^{n} F) (j) : ℝ ⟶ ℂ))$
30	29 3	chvarvv	$⊢ (φ \land j \in (0 \dots R + 1)) \to (ℝ D^{n} F) (j) : ℝ ⟶ ℂ$
31	19 24 30	vtocl	$⊢ (φ \land i + 1 \in (0 \dots R + 1)) \to (ℝ D^{n} F) (i + 1) : ℝ ⟶ ℂ$
32	18 31	sylan2	$⊢ (φ \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i + 1) : ℝ ⟶ ℂ$
33	32	3adant3	$⊢ (φ \land i \in (0 \dots R) \land x \in ℝ) \to (ℝ D^{n} F) (i + 1) : ℝ ⟶ ℂ$
34	33 16	ffvelrnd	$⊢ (φ \land i \in (0 \dots R) \land x \in ℝ) \to (ℝ D^{n} F) (i + 1) (x) \in ℂ$
35	14	ffnd	$⊢ (φ \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i) Fn ℝ$
36		nfcv	$⊢ \underline{Ⅎ} x ℝ$
37		nfcv	$⊢ \underline{Ⅎ} x D^{n}$
38	36 37 1	nfov	$⊢ \underline{Ⅎ} x (ℝ D^{n} F)$
39		nfcv	$⊢ \underline{Ⅎ} x i$
40	38 39	nffv	$⊢ \underline{Ⅎ} x (ℝ D^{n} F) (i)$
41	40	dffn5f	$⊢ (ℝ D^{n} F) (i) Fn ℝ \leftrightarrow (ℝ D^{n} F) (i) = (x \in ℝ ⟼ (ℝ D^{n} F) (i) (x))$
42	35 41	sylib	$⊢ (φ \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i) = (x \in ℝ ⟼ (ℝ D^{n} F) (i) (x))$
43	42	eqcomd	$⊢ (φ \land i \in (0 \dots R)) \to (x \in ℝ ⟼ (ℝ D^{n} F) (i) (x)) = (ℝ D^{n} F) (i)$
44	43	oveq2d	$⊢ (φ \land i \in (0 \dots R)) \to \frac{d (x \in ℝ⟼ (ℝ D^{n} F) (i) (x))}{d_{ℝ} x} = ℝ D (ℝ D^{n} F) (i)$
45		ax-resscn	$⊢ ℝ \subseteq ℂ$
46	45	a1i	$⊢ (φ \land i \in (0 \dots R)) \to ℝ \subseteq ℂ$
47		ffdm	$⊢ F : ℝ ⟶ ℂ \to (F : dom F ⟶ ℂ \land dom F \subseteq ℝ)$
48	2 47	syl	$⊢ φ \to (F : dom F ⟶ ℂ \land dom F \subseteq ℝ)$
49		cnex	$⊢ ℂ \in V$
50	49	a1i	$⊢ φ \to ℂ \in V$
51		reex	$⊢ ℝ \in V$
52		elpm2g	$⊢ (ℂ \in V \land ℝ \in V) \to (F \in (ℂ ↑_{𝑝𝑚} ℝ) \leftrightarrow (F : dom F ⟶ ℂ \land dom F \subseteq ℝ))$
53	50 51 52	sylancl	$⊢ φ \to (F \in (ℂ ↑_{𝑝𝑚} ℝ) \leftrightarrow (F : dom F ⟶ ℂ \land dom F \subseteq ℝ))$
54	48 53	mpbird	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
55	54	adantr	$⊢ (φ \land i \in (0 \dots R)) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
56		elfznn0	$⊢ i \in (0 \dots R) \to i \in ℕ_{0}$
57	56	adantl	$⊢ (φ \land i \in (0 \dots R)) \to i \in ℕ_{0}$
58		dvnp1	$⊢ (ℝ \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} ℝ) \land i \in ℕ_{0}) \to (ℝ D^{n} F) (i + 1) = ℝ D (ℝ D^{n} F) (i)$
59	46 55 57 58	syl3anc	$⊢ (φ \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i + 1) = ℝ D (ℝ D^{n} F) (i)$
60	32	ffnd	$⊢ (φ \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i + 1) Fn ℝ$
61		nfcv	$⊢ \underline{Ⅎ} x (i + 1)$
62	38 61	nffv	$⊢ \underline{Ⅎ} x (ℝ D^{n} F) (i + 1)$
63	62	dffn5f	$⊢ (ℝ D^{n} F) (i + 1) Fn ℝ \leftrightarrow (ℝ D^{n} F) (i + 1) = (x \in ℝ ⟼ (ℝ D^{n} F) (i + 1) (x))$
64	60 63	sylib	$⊢ (φ \land i \in (0 \dots R)) \to (ℝ D^{n} F) (i + 1) = (x \in ℝ ⟼ (ℝ D^{n} F) (i + 1) (x))$
65	44 59 64	3eqtr2d	$⊢ (φ \land i \in (0 \dots R)) \to \frac{d (x \in ℝ⟼ (ℝ D^{n} F) (i) (x))}{d_{ℝ} x} = (x \in ℝ ⟼ (ℝ D^{n} F) (i + 1) (x))$
66	7 6 9 11 12 17 34 65	dvmptfsum	$⊢ φ \to \frac{d (x \in ℝ⟼ \sum_{i = 0}^{R} (ℝ D^{n} F) (i) (x))}{d_{ℝ} x} = (x \in ℝ ⟼ \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x))$
67	5 66	syl5eq	$⊢ φ \to ℝ D G = (x \in ℝ ⟼ \sum_{i = 0}^{R} (ℝ D^{n} F) (i + 1) (x))$

Metamath Proof Explorer

Theorem etransclem2

Proof