Step | Hyp | Ref
| Expression |
1 | | etransclem2.g |
. . 3
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘𝑖)‘𝑥)) |
2 | 1 | oveq2i 6560 |
. 2
⊢ (ℝ
D 𝐺) = (ℝ D (𝑥 ∈ ℝ ↦
Σ𝑖 ∈ (0...𝑅)(((ℝ
D𝑛 𝐹)‘𝑖)‘𝑥))) |
3 | | eqid 2610 |
. . . 4
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
4 | 3 | tgioo2 22414 |
. . 3
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
5 | | reelprrecn 9907 |
. . . 4
⊢ ℝ
∈ {ℝ, ℂ} |
6 | 5 | a1i 11 |
. . 3
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
7 | | reopn 38442 |
. . . 4
⊢ ℝ
∈ (topGen‘ran (,)) |
8 | 7 | a1i 11 |
. . 3
⊢ (𝜑 → ℝ ∈
(topGen‘ran (,))) |
9 | | fzfid 12634 |
. . 3
⊢ (𝜑 → (0...𝑅) ∈ Fin) |
10 | | fzelp1 12263 |
. . . . . 6
⊢ (𝑖 ∈ (0...𝑅) → 𝑖 ∈ (0...(𝑅 + 1))) |
11 | | etransclem2.dvnf |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑅 + 1))) → ((ℝ
D𝑛 𝐹)‘𝑖):ℝ⟶ℂ) |
12 | 10, 11 | sylan2 490 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛
𝐹)‘𝑖):ℝ⟶ℂ) |
13 | 12 | 3adant3 1074 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅) ∧ 𝑥 ∈ ℝ) → ((ℝ
D𝑛 𝐹)‘𝑖):ℝ⟶ℂ) |
14 | | simp3 1056 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) |
15 | 13, 14 | ffvelrnd 6268 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅) ∧ 𝑥 ∈ ℝ) → (((ℝ
D𝑛 𝐹)‘𝑖)‘𝑥) ∈ ℂ) |
16 | | fzp1elp1 12264 |
. . . . . 6
⊢ (𝑖 ∈ (0...𝑅) → (𝑖 + 1) ∈ (0...(𝑅 + 1))) |
17 | | ovex 6577 |
. . . . . . 7
⊢ (𝑖 + 1) ∈ V |
18 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑗 = (𝑖 + 1) → (𝑗 ∈ (0...(𝑅 + 1)) ↔ (𝑖 + 1) ∈ (0...(𝑅 + 1)))) |
19 | 18 | anbi2d 736 |
. . . . . . . 8
⊢ (𝑗 = (𝑖 + 1) → ((𝜑 ∧ 𝑗 ∈ (0...(𝑅 + 1))) ↔ (𝜑 ∧ (𝑖 + 1) ∈ (0...(𝑅 + 1))))) |
20 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑗 = (𝑖 + 1) → ((ℝ D𝑛
𝐹)‘𝑗) = ((ℝ D𝑛 𝐹)‘(𝑖 + 1))) |
21 | 20 | feq1d 5943 |
. . . . . . . 8
⊢ (𝑗 = (𝑖 + 1) → (((ℝ D𝑛
𝐹)‘𝑗):ℝ⟶ℂ ↔ ((ℝ
D𝑛 𝐹)‘(𝑖 +
1)):ℝ⟶ℂ)) |
22 | 19, 21 | imbi12d 333 |
. . . . . . 7
⊢ (𝑗 = (𝑖 + 1) → (((𝜑 ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ
D𝑛 𝐹)‘𝑗):ℝ⟶ℂ) ↔ ((𝜑 ∧ (𝑖 + 1) ∈ (0...(𝑅 + 1))) → ((ℝ
D𝑛 𝐹)‘(𝑖 +
1)):ℝ⟶ℂ))) |
23 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → (𝑖 ∈ (0...(𝑅 + 1)) ↔ 𝑗 ∈ (0...(𝑅 + 1)))) |
24 | 23 | anbi2d 736 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → ((𝜑 ∧ 𝑖 ∈ (0...(𝑅 + 1))) ↔ (𝜑 ∧ 𝑗 ∈ (0...(𝑅 + 1))))) |
25 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → ((ℝ D𝑛 𝐹)‘𝑖) = ((ℝ D𝑛 𝐹)‘𝑗)) |
26 | 25 | feq1d 5943 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → (((ℝ D𝑛
𝐹)‘𝑖):ℝ⟶ℂ ↔ ((ℝ
D𝑛 𝐹)‘𝑗):ℝ⟶ℂ)) |
27 | 24, 26 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → (((𝜑 ∧ 𝑖 ∈ (0...(𝑅 + 1))) → ((ℝ
D𝑛 𝐹)‘𝑖):ℝ⟶ℂ) ↔ ((𝜑 ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ
D𝑛 𝐹)‘𝑗):ℝ⟶ℂ))) |
28 | 27, 11 | chvarv 2251 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑅 + 1))) → ((ℝ
D𝑛 𝐹)‘𝑗):ℝ⟶ℂ) |
29 | 17, 22, 28 | vtocl 3232 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 + 1) ∈ (0...(𝑅 + 1))) → ((ℝ
D𝑛 𝐹)‘(𝑖 +
1)):ℝ⟶ℂ) |
30 | 16, 29 | sylan2 490 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛
𝐹)‘(𝑖 +
1)):ℝ⟶ℂ) |
31 | 30 | 3adant3 1074 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅) ∧ 𝑥 ∈ ℝ) → ((ℝ
D𝑛 𝐹)‘(𝑖 +
1)):ℝ⟶ℂ) |
32 | 31, 14 | ffvelrnd 6268 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅) ∧ 𝑥 ∈ ℝ) → (((ℝ
D𝑛 𝐹)‘(𝑖 + 1))‘𝑥) ∈ ℂ) |
33 | | ffn 5958 |
. . . . . . . 8
⊢
(((ℝ D𝑛 𝐹)‘𝑖):ℝ⟶ℂ → ((ℝ
D𝑛 𝐹)‘𝑖) Fn ℝ) |
34 | 12, 33 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛
𝐹)‘𝑖) Fn ℝ) |
35 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑥ℝ |
36 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑥
D𝑛 |
37 | | etransclem2.xf |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐹 |
38 | 35, 36, 37 | nfov 6575 |
. . . . . . . . 9
⊢
Ⅎ𝑥(ℝ D𝑛 𝐹) |
39 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑖 |
40 | 38, 39 | nffv 6110 |
. . . . . . . 8
⊢
Ⅎ𝑥((ℝ D𝑛 𝐹)‘𝑖) |
41 | 40 | dffn5f 6162 |
. . . . . . 7
⊢
(((ℝ D𝑛 𝐹)‘𝑖) Fn ℝ ↔ ((ℝ
D𝑛 𝐹)‘𝑖) = (𝑥 ∈ ℝ ↦ (((ℝ
D𝑛 𝐹)‘𝑖)‘𝑥))) |
42 | 34, 41 | sylib 207 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛
𝐹)‘𝑖) = (𝑥 ∈ ℝ ↦ (((ℝ
D𝑛 𝐹)‘𝑖)‘𝑥))) |
43 | 42 | eqcomd 2616 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → (𝑥 ∈ ℝ ↦ (((ℝ
D𝑛 𝐹)‘𝑖)‘𝑥)) = ((ℝ D𝑛 𝐹)‘𝑖)) |
44 | 43 | oveq2d 6565 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → (ℝ D (𝑥 ∈ ℝ ↦ (((ℝ
D𝑛 𝐹)‘𝑖)‘𝑥))) = (ℝ D ((ℝ
D𝑛 𝐹)‘𝑖))) |
45 | | ax-resscn 9872 |
. . . . . 6
⊢ ℝ
⊆ ℂ |
46 | 45 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ℝ ⊆
ℂ) |
47 | | etransclem2.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℝ⟶ℂ) |
48 | | ffdm 5975 |
. . . . . . . 8
⊢ (𝐹:ℝ⟶ℂ →
(𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ)) |
49 | 47, 48 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ)) |
50 | | cnex 9896 |
. . . . . . . . 9
⊢ ℂ
∈ V |
51 | 50 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℂ ∈
V) |
52 | | reex 9906 |
. . . . . . . 8
⊢ ℝ
∈ V |
53 | | elpm2g 7760 |
. . . . . . . 8
⊢ ((ℂ
∈ V ∧ ℝ ∈ V) → (𝐹 ∈ (ℂ ↑pm
ℝ) ↔ (𝐹:dom
𝐹⟶ℂ ∧ dom
𝐹 ⊆
ℝ))) |
54 | 51, 52, 53 | sylancl 693 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ∈ (ℂ ↑pm
ℝ) ↔ (𝐹:dom
𝐹⟶ℂ ∧ dom
𝐹 ⊆
ℝ))) |
55 | 49, 54 | mpbird 246 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
56 | 55 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
57 | | elfznn0 12302 |
. . . . . 6
⊢ (𝑖 ∈ (0...𝑅) → 𝑖 ∈ ℕ0) |
58 | 57 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → 𝑖 ∈ ℕ0) |
59 | | dvnp1 23494 |
. . . . 5
⊢ ((ℝ
⊆ ℂ ∧ 𝐹
∈ (ℂ ↑pm ℝ) ∧ 𝑖 ∈ ℕ0) → ((ℝ
D𝑛 𝐹)‘(𝑖 + 1)) = (ℝ D ((ℝ
D𝑛 𝐹)‘𝑖))) |
60 | 46, 56, 58, 59 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛
𝐹)‘(𝑖 + 1)) = (ℝ D ((ℝ
D𝑛 𝐹)‘𝑖))) |
61 | | ffn 5958 |
. . . . . 6
⊢
(((ℝ D𝑛 𝐹)‘(𝑖 + 1)):ℝ⟶ℂ →
((ℝ D𝑛 𝐹)‘(𝑖 + 1)) Fn ℝ) |
62 | 30, 61 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛
𝐹)‘(𝑖 + 1)) Fn
ℝ) |
63 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑖 + 1) |
64 | 38, 63 | nffv 6110 |
. . . . . 6
⊢
Ⅎ𝑥((ℝ D𝑛 𝐹)‘(𝑖 + 1)) |
65 | 64 | dffn5f 6162 |
. . . . 5
⊢
(((ℝ D𝑛 𝐹)‘(𝑖 + 1)) Fn ℝ ↔ ((ℝ
D𝑛 𝐹)‘(𝑖 + 1)) = (𝑥 ∈ ℝ ↦ (((ℝ
D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) |
66 | 62, 65 | sylib 207 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → ((ℝ D𝑛
𝐹)‘(𝑖 + 1)) = (𝑥 ∈ ℝ ↦ (((ℝ
D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) |
67 | 44, 60, 66 | 3eqtr2d 2650 |
. . 3
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑅)) → (ℝ D (𝑥 ∈ ℝ ↦ (((ℝ
D𝑛 𝐹)‘𝑖)‘𝑥))) = (𝑥 ∈ ℝ ↦ (((ℝ
D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) |
68 | 4, 3, 6, 8, 9, 15,
32, 67 | dvmptfsum 23542 |
. 2
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦
Σ𝑖 ∈ (0...𝑅)(((ℝ
D𝑛 𝐹)‘𝑖)‘𝑥))) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) |
69 | 2, 68 | syl5eq 2656 |
1
⊢ (𝜑 → (ℝ D 𝐺) = (𝑥 ∈ ℝ ↦ Σ𝑖 ∈ (0...𝑅)(((ℝ D𝑛 𝐹)‘(𝑖 + 1))‘𝑥))) |