Step | Hyp | Ref
| Expression |
1 | | fveq2 6446 |
. . . . . . . . 9
⊢ (𝑥 = 0 → ((ℂ
D𝑛 𝐹)‘𝑥) = ((ℂ D𝑛 𝐹)‘0)) |
2 | 1 | dmeqd 5571 |
. . . . . . . 8
⊢ (𝑥 = 0 → dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom ((ℂ D𝑛 𝐹)‘0)) |
3 | 2 | eqeq1d 2779 |
. . . . . . 7
⊢ (𝑥 = 0 → (dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 ↔ dom ((ℂ D𝑛
𝐹)‘0) = dom 𝐹)) |
4 | | fveq2 6446 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0)) |
5 | 1 | reseq1d 5641 |
. . . . . . . 8
⊢ (𝑥 = 0 → (((ℂ
D𝑛 𝐹)‘𝑥) ↾ 𝑆) = (((ℂ D𝑛 𝐹)‘0) ↾ 𝑆)) |
6 | 4, 5 | eqeq12d 2792 |
. . . . . . 7
⊢ (𝑥 = 0 → (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆) ↔ ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (((ℂ
D𝑛 𝐹)‘0) ↾ 𝑆))) |
7 | 3, 6 | imbi12d 336 |
. . . . . 6
⊢ (𝑥 = 0 → ((dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆)) ↔ (dom ((ℂ
D𝑛 𝐹)‘0) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (((ℂ
D𝑛 𝐹)‘0) ↾ 𝑆)))) |
8 | 7 | imbi2d 332 |
. . . . 5
⊢ (𝑥 = 0 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆))) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘0) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (((ℂ
D𝑛 𝐹)‘0) ↾ 𝑆))))) |
9 | | fveq2 6446 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → ((ℂ D𝑛 𝐹)‘𝑥) = ((ℂ D𝑛 𝐹)‘𝑛)) |
10 | 9 | dmeqd 5571 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → dom ((ℂ D𝑛
𝐹)‘𝑥) = dom ((ℂ D𝑛 𝐹)‘𝑛)) |
11 | 10 | eqeq1d 2779 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (dom ((ℂ D𝑛
𝐹)‘𝑥) = dom 𝐹 ↔ dom ((ℂ D𝑛
𝐹)‘𝑛) = dom 𝐹)) |
12 | | fveq2 6446 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛)) |
13 | 9 | reseq1d 5641 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → (((ℂ D𝑛
𝐹)‘𝑥) ↾ 𝑆) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)) |
14 | 12, 13 | eqeq12d 2792 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆) ↔ ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆))) |
15 | 11, 14 | imbi12d 336 |
. . . . . 6
⊢ (𝑥 = 𝑛 → ((dom ((ℂ D𝑛
𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆)) ↔ (dom ((ℂ
D𝑛 𝐹)‘𝑛) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)))) |
16 | 15 | imbi2d 332 |
. . . . 5
⊢ (𝑥 = 𝑛 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆))) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘𝑛) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆))))) |
17 | | fveq2 6446 |
. . . . . . . . 9
⊢ (𝑥 = (𝑛 + 1) → ((ℂ D𝑛
𝐹)‘𝑥) = ((ℂ D𝑛 𝐹)‘(𝑛 + 1))) |
18 | 17 | dmeqd 5571 |
. . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom ((ℂ D𝑛 𝐹)‘(𝑛 + 1))) |
19 | 18 | eqeq1d 2779 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 ↔ dom ((ℂ D𝑛
𝐹)‘(𝑛 + 1)) = dom 𝐹)) |
20 | | fveq2 6446 |
. . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1))) |
21 | 17 | reseq1d 5641 |
. . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → (((ℂ D𝑛
𝐹)‘𝑥) ↾ 𝑆) = (((ℂ D𝑛 𝐹)‘(𝑛 + 1)) ↾ 𝑆)) |
22 | 20, 21 | eqeq12d 2792 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆) ↔ ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆))) |
23 | 19, 22 | imbi12d 336 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → ((dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆)) ↔ (dom ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆)))) |
24 | 23 | imbi2d 332 |
. . . . 5
⊢ (𝑥 = (𝑛 + 1) → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆))) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆))))) |
25 | | fveq2 6446 |
. . . . . . . . 9
⊢ (𝑥 = 𝑁 → ((ℂ D𝑛
𝐹)‘𝑥) = ((ℂ D𝑛 𝐹)‘𝑁)) |
26 | 25 | dmeqd 5571 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → dom ((ℂ D𝑛
𝐹)‘𝑥) = dom ((ℂ D𝑛 𝐹)‘𝑁)) |
27 | 26 | eqeq1d 2779 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (dom ((ℂ D𝑛
𝐹)‘𝑥) = dom 𝐹 ↔ dom ((ℂ D𝑛
𝐹)‘𝑁) = dom 𝐹)) |
28 | | fveq2 6446 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁)) |
29 | 25 | reseq1d 5641 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (((ℂ D𝑛
𝐹)‘𝑥) ↾ 𝑆) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)) |
30 | 28, 29 | eqeq12d 2792 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆) ↔ ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆))) |
31 | 27, 30 | imbi12d 336 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆)) ↔ (dom ((ℂ
D𝑛 𝐹)‘𝑁) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)))) |
32 | 31 | imbi2d 332 |
. . . . 5
⊢ (𝑥 = 𝑁 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆))) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘𝑁) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆))))) |
33 | | recnprss 24105 |
. . . . . . . . 9
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
34 | 33 | adantr 474 |
. . . . . . . 8
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → 𝑆 ⊆ ℂ) |
35 | | pmresg 8168 |
. . . . . . . 8
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → (𝐹 ↾ 𝑆) ∈ (ℂ ↑pm
𝑆)) |
36 | | dvn0 24124 |
. . . . . . . 8
⊢ ((𝑆 ⊆ ℂ ∧ (𝐹 ↾ 𝑆) ∈ (ℂ ↑pm
𝑆)) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (𝐹 ↾ 𝑆)) |
37 | 34, 35, 36 | syl2anc 579 |
. . . . . . 7
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (𝐹 ↾ 𝑆)) |
38 | | ssidd 3842 |
. . . . . . . . 9
⊢ (𝑆 ∈ {ℝ, ℂ}
→ ℂ ⊆ ℂ) |
39 | | dvn0 24124 |
. . . . . . . . 9
⊢ ((ℂ
⊆ ℂ ∧ 𝐹
∈ (ℂ ↑pm ℂ)) → ((ℂ
D𝑛 𝐹)‘0) = 𝐹) |
40 | 38, 39 | sylan 575 |
. . . . . . . 8
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → ((ℂ D𝑛
𝐹)‘0) = 𝐹) |
41 | 40 | reseq1d 5641 |
. . . . . . 7
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → (((ℂ D𝑛
𝐹)‘0) ↾ 𝑆) = (𝐹 ↾ 𝑆)) |
42 | 37, 41 | eqtr4d 2816 |
. . . . . 6
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (((ℂ
D𝑛 𝐹)‘0) ↾ 𝑆)) |
43 | 42 | a1d 25 |
. . . . 5
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘0) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (((ℂ
D𝑛 𝐹)‘0) ↾ 𝑆))) |
44 | | cnelprrecn 10365 |
. . . . . . . . . . 11
⊢ ℂ
∈ {ℝ, ℂ} |
45 | 44 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → ℂ ∈ {ℝ,
ℂ}) |
46 | | simplr 759 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
47 | | simprl 761 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → 𝑛 ∈ ℕ0) |
48 | | dvnbss 24128 |
. . . . . . . . . 10
⊢ ((ℂ
∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm
ℂ) ∧ 𝑛 ∈
ℕ0) → dom ((ℂ D𝑛 𝐹)‘𝑛) ⊆ dom 𝐹) |
49 | 45, 46, 47, 48 | syl3anc 1439 |
. . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘𝑛) ⊆ dom 𝐹) |
50 | | simprr 763 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹) |
51 | | ssidd 3842 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → ℂ ⊆
ℂ) |
52 | | dvnp1 24125 |
. . . . . . . . . . . . 13
⊢ ((ℂ
⊆ ℂ ∧ 𝐹
∈ (ℂ ↑pm ℂ) ∧ 𝑛 ∈ ℕ0) → ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛))) |
53 | 51, 46, 47, 52 | syl3anc 1439 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → ((ℂ D𝑛
𝐹)‘(𝑛 + 1)) = (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛))) |
54 | 53 | dmeqd 5571 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = dom (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛))) |
55 | 50, 54 | eqtr3d 2815 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom 𝐹 = dom (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛))) |
56 | | dvnf 24127 |
. . . . . . . . . . . 12
⊢ ((ℂ
∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm
ℂ) ∧ 𝑛 ∈
ℕ0) → ((ℂ D𝑛 𝐹)‘𝑛):dom ((ℂ D𝑛 𝐹)‘𝑛)⟶ℂ) |
57 | 45, 46, 47, 56 | syl3anc 1439 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → ((ℂ D𝑛
𝐹)‘𝑛):dom ((ℂ D𝑛 𝐹)‘𝑛)⟶ℂ) |
58 | | cnex 10353 |
. . . . . . . . . . . . . . 15
⊢ ℂ
∈ V |
59 | 58, 58 | elpm2 8172 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (ℂ
↑pm ℂ) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ)) |
60 | 59 | simprbi 492 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (ℂ
↑pm ℂ) → dom 𝐹 ⊆ ℂ) |
61 | 46, 60 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom 𝐹 ⊆ ℂ) |
62 | 49, 61 | sstrd 3830 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘𝑛) ⊆ ℂ) |
63 | 51, 57, 62 | dvbss 24102 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) ⊆ dom ((ℂ
D𝑛 𝐹)‘𝑛)) |
64 | 55, 63 | eqsstrd 3857 |
. . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom 𝐹 ⊆ dom ((ℂ D𝑛
𝐹)‘𝑛)) |
65 | 49, 64 | eqssd 3837 |
. . . . . . . 8
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘𝑛) = dom 𝐹) |
66 | 65 | expr 450 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ 𝑛 ∈ ℕ0) → (dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹 → dom ((ℂ D𝑛
𝐹)‘𝑛) = dom 𝐹)) |
67 | 66 | imim1d 82 |
. . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ 𝑛 ∈ ℕ0) → ((dom
((ℂ D𝑛 𝐹)‘𝑛) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)) → (dom ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)))) |
68 | | oveq2 6930 |
. . . . . . 7
⊢ (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆) → (𝑆 D ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛)) = (𝑆 D (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆))) |
69 | 34 | adantr 474 |
. . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → 𝑆 ⊆ ℂ) |
70 | 35 | adantr 474 |
. . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (𝐹 ↾ 𝑆) ∈ (ℂ ↑pm
𝑆)) |
71 | | dvnp1 24125 |
. . . . . . . . 9
⊢ ((𝑆 ⊆ ℂ ∧ (𝐹 ↾ 𝑆) ∈ (ℂ ↑pm
𝑆) ∧ 𝑛 ∈ ℕ0) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (𝑆 D ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛))) |
72 | 69, 70, 47, 71 | syl3anc 1439 |
. . . . . . . 8
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (𝑆 D ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛))) |
73 | 53 | reseq1d 5641 |
. . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆) = ((ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) ↾ 𝑆)) |
74 | | simpll 757 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → 𝑆 ∈ {ℝ, ℂ}) |
75 | | eqid 2777 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
76 | 75 | cnfldtop 22995 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) ∈ Top |
77 | 75 | cnfldtopon 22994 |
. . . . . . . . . . . . . . 15
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
78 | 77 | toponunii 21128 |
. . . . . . . . . . . . . 14
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
79 | 78 | ntrss2 21269 |
. . . . . . . . . . . . 13
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ dom ((ℂ
D𝑛 𝐹)‘𝑛) ⊆ ℂ) →
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛)) ⊆ dom ((ℂ
D𝑛 𝐹)‘𝑛)) |
80 | 76, 62, 79 | sylancr 581 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) →
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛)) ⊆ dom ((ℂ
D𝑛 𝐹)‘𝑛)) |
81 | 77 | toponrestid 21133 |
. . . . . . . . . . . . . . 15
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
82 | 51, 57, 62, 81, 75 | dvbssntr 24101 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) ⊆
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛))) |
83 | 55, 82 | eqsstrd 3857 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom 𝐹 ⊆
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛))) |
84 | 49, 83 | sstrd 3830 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘𝑛) ⊆
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛))) |
85 | 80, 84 | eqssd 3837 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) →
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛)) = dom ((ℂ D𝑛
𝐹)‘𝑛)) |
86 | 78 | isopn3 21278 |
. . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ dom ((ℂ
D𝑛 𝐹)‘𝑛) ⊆ ℂ) → (dom ((ℂ
D𝑛 𝐹)‘𝑛) ∈
(TopOpen‘ℂfld) ↔
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛)) = dom ((ℂ D𝑛
𝐹)‘𝑛))) |
87 | 76, 62, 86 | sylancr 581 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (dom ((ℂ
D𝑛 𝐹)‘𝑛) ∈
(TopOpen‘ℂfld) ↔
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛)) = dom ((ℂ D𝑛
𝐹)‘𝑛))) |
88 | 85, 87 | mpbird 249 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘𝑛) ∈
(TopOpen‘ℂfld)) |
89 | 65, 55 | eqtr2d 2814 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) = dom ((ℂ D𝑛
𝐹)‘𝑛)) |
90 | 75 | dvres3a 24115 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
((ℂ D𝑛 𝐹)‘𝑛):dom ((ℂ D𝑛 𝐹)‘𝑛)⟶ℂ) ∧ (dom ((ℂ
D𝑛 𝐹)‘𝑛) ∈
(TopOpen‘ℂfld) ∧ dom (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) = dom ((ℂ D𝑛
𝐹)‘𝑛))) → (𝑆 D (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)) = ((ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) ↾ 𝑆)) |
91 | 74, 57, 88, 89, 90 | syl22anc 829 |
. . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (𝑆 D (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)) = ((ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) ↾ 𝑆)) |
92 | 73, 91 | eqtr4d 2816 |
. . . . . . . 8
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆) = (𝑆 D (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆))) |
93 | 72, 92 | eqeq12d 2792 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆) ↔ (𝑆 D ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛)) = (𝑆 D (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)))) |
94 | 68, 93 | syl5ibr 238 |
. . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆))) |
95 | 67, 94 | animpimp2impd 835 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
→ (((𝑆 ∈
{ℝ, ℂ} ∧ 𝐹
∈ (ℂ ↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘𝑛) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆))) → ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆))))) |
96 | 8, 16, 24, 32, 43, 95 | nn0ind 11824 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ((𝑆 ∈ {ℝ,
ℂ} ∧ 𝐹 ∈
(ℂ ↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘𝑁) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)))) |
97 | 96 | com12 32 |
. . 3
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → (𝑁 ∈ ℕ0 → (dom
((ℂ D𝑛 𝐹)‘𝑁) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)))) |
98 | 97 | 3impia 1106 |
. 2
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ) ∧ 𝑁 ∈ ℕ0) → (dom
((ℂ D𝑛 𝐹)‘𝑁) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆))) |
99 | 98 | imp 397 |
1
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ) ∧ 𝑁 ∈ ℕ0) ∧ dom
((ℂ D𝑛 𝐹)‘𝑁) = dom 𝐹) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)) |