Step | Hyp | Ref
| Expression |
1 | | etransclem2.g |
. . 3
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)) |
2 | 1 | oveq2i 7224 |
. 2
⊢ (ℝ
D 𝐺) = (ℝ D (𝑥 ∈ ℝ ↦
Σ𝑖 ∈ (0...𝑅)(((ℝ
D𝑛 𝐹)‘𝑖)‘𝑥))) |
3 | | eqid 2737 |
. . . 4
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
4 | 3 | tgioo2 23700 |
. . 3
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
5 | | reelprrecn 10821 |
. . . 4
⊢ ℝ
∈ {ℝ, ℂ} |
6 | 5 | a1i 11 |
. . 3
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
7 | | reopn 42500 |
. . . 4
⊢ ℝ
∈ (topGen‘ran (,)) |
8 | 7 | a1i 11 |
. . 3
⊢ (𝜑 → ℝ ∈
(topGen‘ran (,))) |
9 | | fzfid 13546 |
. . 3
⊢ (𝜑 → (0...𝑅) ∈ Fin) |
10 | | fzelp1 13164 |
. . . . . 6
⊢ (𝑖 ∈ (0...𝑅) → 𝑖 ∈ (0...(𝑅 + 1))) |
11 | | etransclem2.dvnf |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑅 + 1))) → ((ℝ
D𝑛 𝐹)‘𝑖):ℝ⟶ℂ) |
12 | 10, 11 | sylan2 596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛
𝐹)‘𝑖):ℝ⟶ℂ) |
13 | 12 | 3adant3 1134 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅) ∧ 𝑥 ∈ ℝ) → ((ℝ
D𝑛 𝐹)‘𝑖):ℝ⟶ℂ) |
14 | | simp3 1140 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) |
15 | 13, 14 | ffvelrnd 6905 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅) ∧ 𝑥 ∈ ℝ) → (((ℝ
D𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ) |
16 | | fzp1elp1 13165 |
. . . . . 6
⊢ (𝑖 ∈ (0...𝑅) → (𝑖 + 1) ∈ (0...(𝑅 + 1))) |
17 | | ovex 7246 |
. . . . . . 7
⊢ (𝑖 + 1) ∈ V |
18 | | eleq1 2825 |
. . . . . . . . 9
⊢ (𝑗 = (𝑖 + 1) → (𝑗 ∈ (0...(𝑅 + 1)) ↔ (𝑖 + 1) ∈ (0...(𝑅 + 1)))) |
19 | 18 | anbi2d 632 |
. . . . . . . 8
⊢ (𝑗 = (𝑖 + 1) → ((𝜑 ∧ 𝑗 ∈ (0...(𝑅 + 1))) ↔ (𝜑 ∧ (𝑖 + 1) ∈ (0...(𝑅 + 1))))) |
20 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑗 = (𝑖 + 1) → ((ℝ D𝑛
𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘(𝑖 + 1))) |
21 | 20 | feq1d 6530 |
. . . . . . . 8
⊢ (𝑗 = (𝑖 + 1) → (((ℝ D𝑛
𝐹)‘𝑗):ℝ⟶ℂ ↔ ((ℝ
D𝑛 𝐹)‘(𝑖 +
1)):ℝ⟶ℂ)) |
22 | 19, 21 | imbi12d 348 |
. . . . . . 7
⊢ (𝑗 = (𝑖 + 1) → (((𝜑 ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ
D𝑛 𝐹)‘𝑗):ℝ⟶ℂ) ↔ ((𝜑 ∧ (𝑖 + 1) ∈ (0...(𝑅 + 1))) → ((ℝ
D𝑛 𝐹)‘(𝑖 +
1)):ℝ⟶ℂ))) |
23 | | eleq1 2825 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → (𝑖 ∈ (0...(𝑅 + 1)) ↔ 𝑗 ∈ (0...(𝑅 + 1)))) |
24 | 23 | anbi2d 632 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ (0...(𝑅 + 1))) ↔ (𝜑 ∧ 𝑗 ∈ (0...(𝑅 + 1))))) |
25 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → ((ℝ D𝑛 𝐹)‘𝑖) = ((ℝ D𝑛 𝐹)‘𝑗)) |
26 | 25 | feq1d 6530 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → (((ℝ D𝑛
𝐹)‘𝑖):ℝ⟶ℂ ↔ ((ℝ
D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)) |
27 | 24, 26 | imbi12d 348 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ (0...(𝑅 + 1))) → ((ℝ
D𝑛 𝐹)‘𝑖):ℝ⟶ℂ) ↔ ((𝜑 ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ
D𝑛 𝐹)‘𝑗):ℝ⟶ℂ))) |
28 | 27, 11 | chvarvv 2007 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ
D𝑛 𝐹)‘𝑗):ℝ⟶ℂ) |
29 | 17, 22, 28 | vtocl 3474 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 + 1) ∈ (0...(𝑅 + 1))) → ((ℝ
D𝑛 𝐹)‘(𝑖 +
1)):ℝ⟶ℂ) |
30 | 16, 29 | sylan2 596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛
𝐹)‘(𝑖 +
1)):ℝ⟶ℂ) |
31 | 30 | 3adant3 1134 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅) ∧ 𝑥 ∈ ℝ) → ((ℝ
D𝑛 𝐹)‘(𝑖 +
1)):ℝ⟶ℂ) |
32 | 31, 14 | ffvelrnd 6905 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅) ∧ 𝑥 ∈ ℝ) → (((ℝ
D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ) |
33 | 12 | ffnd 6546 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛
𝐹)‘𝑖) Fn ℝ) |
34 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑥ℝ |
35 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑥
D𝑛 |
36 | | etransclem2.xf |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐹 |
37 | 34, 35, 36 | nfov 7243 |
. . . . . . . . 9
⊢
Ⅎ𝑥(ℝ D𝑛 𝐹) |
38 | | nfcv 2904 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑖 |
39 | 37, 38 | nffv 6727 |
. . . . . . . 8
⊢
Ⅎ𝑥((ℝ D𝑛 𝐹)‘𝑖) |
40 | 39 | dffn5f 6783 |
. . . . . . 7
⊢
(((ℝ D𝑛 𝐹)‘𝑖) Fn ℝ ↔ ((ℝ
D𝑛 𝐹)‘𝑖) = (𝑥 ∈ ℝ ↦ (((ℝ
D𝑛 𝐹)‘𝑖)‘𝑥))) |
41 | 33, 40 | sylib 221 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛
𝐹)‘𝑖) = (𝑥 ∈ ℝ ↦ (((ℝ
D𝑛 𝐹)‘𝑖)‘𝑥))) |
42 | 41 | eqcomd 2743 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → (𝑥 ∈ ℝ ↦ (((ℝ
D𝑛 𝐹)‘𝑖)‘𝑥)) = ((ℝ D𝑛 𝐹)‘𝑖)) |
43 | 42 | oveq2d 7229 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → (ℝ D (𝑥 ∈ ℝ ↦ (((ℝ
D𝑛 𝐹)‘𝑖)‘𝑥))) = (ℝ D ((ℝ
D𝑛 𝐹)‘𝑖))) |
44 | | ax-resscn 10786 |
. . . . . 6
⊢ ℝ
⊆ ℂ |
45 | 44 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ℝ ⊆
ℂ) |
46 | | etransclem2.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℝ⟶ℂ) |
47 | | ffdm 6575 |
. . . . . . . 8
⊢ (𝐹:ℝ⟶ℂ →
(𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ)) |
48 | 46, 47 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ)) |
49 | | cnex 10810 |
. . . . . . . . 9
⊢ ℂ
∈ V |
50 | 49 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℂ ∈
V) |
51 | | reex 10820 |
. . . . . . . 8
⊢ ℝ
∈ V |
52 | | elpm2g 8525 |
. . . . . . . 8
⊢ ((ℂ
∈ V ∧ ℝ ∈ V) → (𝐹 ∈ (ℂ ↑pm
ℝ) ↔ (𝐹:dom
𝐹⟶ℂ ∧ dom
𝐹 ⊆
ℝ))) |
53 | 50, 51, 52 | sylancl 589 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ∈ (ℂ ↑pm
ℝ) ↔ (𝐹:dom
𝐹⟶ℂ ∧ dom
𝐹 ⊆
ℝ))) |
54 | 48, 53 | mpbird 260 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
55 | 54 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
56 | | elfznn0 13205 |
. . . . . 6
⊢ (𝑖 ∈ (0...𝑅) → 𝑖 ∈ ℕ0) |
57 | 56 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → 𝑖 ∈ ℕ0) |
58 | | dvnp1 24822 |
. . . . 5
⊢ ((ℝ
⊆ ℂ ∧ 𝐹
∈ (ℂ ↑pm ℝ) ∧ 𝑖 ∈ ℕ0) → ((ℝ
D𝑛 𝐹)‘(𝑖 + 1)) = (ℝ D ((ℝ
D𝑛 𝐹)‘𝑖))) |
59 | 45, 55, 57, 58 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛
𝐹)‘(𝑖 + 1)) = (ℝ D ((ℝ
D𝑛 𝐹)‘𝑖))) |
60 | 30 | ffnd 6546 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛
𝐹)‘(𝑖 + 1)) Fn
ℝ) |
61 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑖 + 1) |
62 | 37, 61 | nffv 6727 |
. . . . . 6
⊢
Ⅎ𝑥((ℝ D𝑛 𝐹)‘(𝑖 + 1)) |
63 | 62 | dffn5f 6783 |
. . . . 5
⊢
(((ℝ D𝑛 𝐹)‘(𝑖 + 1)) Fn ℝ ↔ ((ℝ
D𝑛 𝐹)‘(𝑖 + 1)) = (𝑥 ∈ ℝ ↦ (((ℝ
D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) |
64 | 60, 63 | sylib 221 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛
𝐹)‘(𝑖 + 1)) = (𝑥 ∈ ℝ ↦ (((ℝ
D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) |
65 | 43, 59, 64 | 3eqtr2d 2783 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → (ℝ D (𝑥 ∈ ℝ ↦ (((ℝ
D𝑛 𝐹)‘𝑖)‘𝑥))) = (𝑥 ∈ ℝ ↦ (((ℝ
D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) |
66 | 4, 3, 6, 8, 9, 15,
32, 65 | dvmptfsum 24872 |
. 2
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦
Σ𝑖 ∈ (0...𝑅)(((ℝ
D𝑛 𝐹)‘𝑖)‘𝑥))) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) |
67 | 2, 66 | syl5eq 2790 |
1
⊢ (𝜑 → (ℝ D 𝐺) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) |