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 ) ) ‘ 𝑥 ) ) ) |