Metamath Proof Explorer


Theorem 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 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
7 6 tgioo2 ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
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 ffvelrnd ( ( 𝜑𝑖 ∈ ( 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 ffvelrnd ( ( 𝜑𝑖 ∈ ( 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 ... 𝑅 ) → 𝑖 ∈ ℕ0 )
57 56 adantl ( ( 𝜑𝑖 ∈ ( 0 ... 𝑅 ) ) → 𝑖 ∈ ℕ0 )
58 dvnp1 ( ( ℝ ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ 𝑖 ∈ ℕ0 ) → ( ( ℝ 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 7 6 9 11 12 17 34 65 dvmptfsum ( 𝜑 → ( ℝ D ( 𝑥 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... 𝑅 ) ( ( ( ℝ D𝑛 𝐹 ) ‘ 𝑖 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... 𝑅 ) ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) ‘ 𝑥 ) ) )
67 5 66 syl5eq ( 𝜑 → ( ℝ D 𝐺 ) = ( 𝑥 ∈ ℝ ↦ Σ 𝑖 ∈ ( 0 ... 𝑅 ) ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑖 + 1 ) ) ‘ 𝑥 ) ) )