Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = 0 → ((ℂ
D𝑛 𝐹)‘𝑥) = ((ℂ D𝑛 𝐹)‘0)) |
2 | 1 | dmeqd 5248 |
. . . . . . . 8
⊢ (𝑥 = 0 → dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom ((ℂ D𝑛 𝐹)‘0)) |
3 | 2 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑥 = 0 → (dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 ↔ dom ((ℂ D𝑛
𝐹)‘0) = dom 𝐹)) |
4 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 0 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0)) |
5 | 1 | reseq1d 5316 |
. . . . . . . 8
⊢ (𝑥 = 0 → (((ℂ
D𝑛 𝐹)‘𝑥) ↾ 𝑆) = (((ℂ D𝑛 𝐹)‘0) ↾ 𝑆)) |
6 | 4, 5 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑥 = 0 → (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆) ↔ ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (((ℂ
D𝑛 𝐹)‘0) ↾ 𝑆))) |
7 | 3, 6 | imbi12d 333 |
. . . . . 6
⊢ (𝑥 = 0 → ((dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆)) ↔ (dom ((ℂ
D𝑛 𝐹)‘0) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (((ℂ
D𝑛 𝐹)‘0) ↾ 𝑆)))) |
8 | 7 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = 0 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆))) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘0) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (((ℂ
D𝑛 𝐹)‘0) ↾ 𝑆))))) |
9 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → ((ℂ D𝑛 𝐹)‘𝑥) = ((ℂ D𝑛 𝐹)‘𝑛)) |
10 | 9 | dmeqd 5248 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → dom ((ℂ D𝑛
𝐹)‘𝑥) = dom ((ℂ D𝑛 𝐹)‘𝑛)) |
11 | 10 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (dom ((ℂ D𝑛
𝐹)‘𝑥) = dom 𝐹 ↔ dom ((ℂ D𝑛
𝐹)‘𝑛) = dom 𝐹)) |
12 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛)) |
13 | 9 | reseq1d 5316 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → (((ℂ D𝑛
𝐹)‘𝑥) ↾ 𝑆) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)) |
14 | 12, 13 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆) ↔ ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆))) |
15 | 11, 14 | imbi12d 333 |
. . . . . 6
⊢ (𝑥 = 𝑛 → ((dom ((ℂ D𝑛
𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆)) ↔ (dom ((ℂ
D𝑛 𝐹)‘𝑛) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)))) |
16 | 15 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = 𝑛 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆))) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘𝑛) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆))))) |
17 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = (𝑛 + 1) → ((ℂ D𝑛
𝐹)‘𝑥) = ((ℂ D𝑛 𝐹)‘(𝑛 + 1))) |
18 | 17 | dmeqd 5248 |
. . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom ((ℂ D𝑛 𝐹)‘(𝑛 + 1))) |
19 | 18 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 ↔ dom ((ℂ D𝑛
𝐹)‘(𝑛 + 1)) = dom 𝐹)) |
20 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1))) |
21 | 17 | reseq1d 5316 |
. . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → (((ℂ D𝑛
𝐹)‘𝑥) ↾ 𝑆) = (((ℂ D𝑛 𝐹)‘(𝑛 + 1)) ↾ 𝑆)) |
22 | 20, 21 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆) ↔ ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆))) |
23 | 19, 22 | imbi12d 333 |
. . . . . 6
⊢ (𝑥 = (𝑛 + 1) → ((dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆)) ↔ (dom ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆)))) |
24 | 23 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = (𝑛 + 1) → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆))) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆))))) |
25 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = 𝑁 → ((ℂ D𝑛
𝐹)‘𝑥) = ((ℂ D𝑛 𝐹)‘𝑁)) |
26 | 25 | dmeqd 5248 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → dom ((ℂ D𝑛
𝐹)‘𝑥) = dom ((ℂ D𝑛 𝐹)‘𝑁)) |
27 | 26 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (dom ((ℂ D𝑛
𝐹)‘𝑥) = dom 𝐹 ↔ dom ((ℂ D𝑛
𝐹)‘𝑁) = dom 𝐹)) |
28 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁)) |
29 | 25 | reseq1d 5316 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (((ℂ D𝑛
𝐹)‘𝑥) ↾ 𝑆) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)) |
30 | 28, 29 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆) ↔ ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆))) |
31 | 27, 30 | imbi12d 333 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆)) ↔ (dom ((ℂ
D𝑛 𝐹)‘𝑁) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)))) |
32 | 31 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = 𝑁 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆))) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘𝑁) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆))))) |
33 | | recnprss 23474 |
. . . . . . . . 9
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
34 | 33 | adantr 480 |
. . . . . . . 8
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → 𝑆 ⊆ ℂ) |
35 | | pmresg 7771 |
. . . . . . . 8
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → (𝐹 ↾ 𝑆) ∈ (ℂ ↑pm
𝑆)) |
36 | | dvn0 23493 |
. . . . . . . 8
⊢ ((𝑆 ⊆ ℂ ∧ (𝐹 ↾ 𝑆) ∈ (ℂ ↑pm
𝑆)) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (𝐹 ↾ 𝑆)) |
37 | 34, 35, 36 | syl2anc 691 |
. . . . . . 7
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (𝐹 ↾ 𝑆)) |
38 | | ssid 3587 |
. . . . . . . . . 10
⊢ ℂ
⊆ ℂ |
39 | 38 | a1i 11 |
. . . . . . . . 9
⊢ (𝑆 ∈ {ℝ, ℂ}
→ ℂ ⊆ ℂ) |
40 | | dvn0 23493 |
. . . . . . . . 9
⊢ ((ℂ
⊆ ℂ ∧ 𝐹
∈ (ℂ ↑pm ℂ)) → ((ℂ
D𝑛 𝐹)‘0) = 𝐹) |
41 | 39, 40 | sylan 487 |
. . . . . . . 8
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → ((ℂ D𝑛
𝐹)‘0) = 𝐹) |
42 | 41 | reseq1d 5316 |
. . . . . . 7
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → (((ℂ D𝑛
𝐹)‘0) ↾ 𝑆) = (𝐹 ↾ 𝑆)) |
43 | 37, 42 | eqtr4d 2647 |
. . . . . 6
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (((ℂ
D𝑛 𝐹)‘0) ↾ 𝑆)) |
44 | 43 | a1d 25 |
. . . . 5
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘0) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (((ℂ
D𝑛 𝐹)‘0) ↾ 𝑆))) |
45 | | cnelprrecn 9908 |
. . . . . . . . . . . . 13
⊢ ℂ
∈ {ℝ, ℂ} |
46 | 45 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → ℂ ∈ {ℝ,
ℂ}) |
47 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → 𝐹 ∈ (ℂ ↑pm
ℂ)) |
48 | | simprl 790 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → 𝑛 ∈ ℕ0) |
49 | | dvnbss 23497 |
. . . . . . . . . . . 12
⊢ ((ℂ
∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm
ℂ) ∧ 𝑛 ∈
ℕ0) → dom ((ℂ D𝑛 𝐹)‘𝑛) ⊆ dom 𝐹) |
50 | 46, 47, 48, 49 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘𝑛) ⊆ dom 𝐹) |
51 | | simprr 792 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹) |
52 | 38 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → ℂ ⊆
ℂ) |
53 | | dvnp1 23494 |
. . . . . . . . . . . . . . 15
⊢ ((ℂ
⊆ ℂ ∧ 𝐹
∈ (ℂ ↑pm ℂ) ∧ 𝑛 ∈ ℕ0) → ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛))) |
54 | 52, 47, 48, 53 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → ((ℂ D𝑛
𝐹)‘(𝑛 + 1)) = (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛))) |
55 | 54 | dmeqd 5248 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = dom (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛))) |
56 | 51, 55 | eqtr3d 2646 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom 𝐹 = dom (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛))) |
57 | | dvnf 23496 |
. . . . . . . . . . . . . 14
⊢ ((ℂ
∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm
ℂ) ∧ 𝑛 ∈
ℕ0) → ((ℂ D𝑛 𝐹)‘𝑛):dom ((ℂ D𝑛 𝐹)‘𝑛)⟶ℂ) |
58 | 46, 47, 48, 57 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → ((ℂ D𝑛
𝐹)‘𝑛):dom ((ℂ D𝑛 𝐹)‘𝑛)⟶ℂ) |
59 | | cnex 9896 |
. . . . . . . . . . . . . . . . 17
⊢ ℂ
∈ V |
60 | 59, 59 | elpm2 7775 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (ℂ
↑pm ℂ) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ)) |
61 | 60 | simprbi 479 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ (ℂ
↑pm ℂ) → dom 𝐹 ⊆ ℂ) |
62 | 47, 61 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom 𝐹 ⊆ ℂ) |
63 | 50, 62 | sstrd 3578 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘𝑛) ⊆ ℂ) |
64 | 52, 58, 63 | dvbss 23471 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) ⊆ dom ((ℂ
D𝑛 𝐹)‘𝑛)) |
65 | 56, 64 | eqsstrd 3602 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom 𝐹 ⊆ dom ((ℂ D𝑛
𝐹)‘𝑛)) |
66 | 50, 65 | eqssd 3585 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘𝑛) = dom 𝐹) |
67 | 66 | expr 641 |
. . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ 𝑛 ∈ ℕ0) → (dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹 → dom ((ℂ D𝑛
𝐹)‘𝑛) = dom 𝐹)) |
68 | 67 | imim1d 80 |
. . . . . . . 8
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ 𝑛 ∈ ℕ0) → ((dom
((ℂ D𝑛 𝐹)‘𝑛) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)) → (dom ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)))) |
69 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆) → (𝑆 D ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛)) = (𝑆 D (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆))) |
70 | 34 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → 𝑆 ⊆ ℂ) |
71 | 35 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (𝐹 ↾ 𝑆) ∈ (ℂ ↑pm
𝑆)) |
72 | | dvnp1 23494 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ⊆ ℂ ∧ (𝐹 ↾ 𝑆) ∈ (ℂ ↑pm
𝑆) ∧ 𝑛 ∈ ℕ0) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (𝑆 D ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛))) |
73 | 70, 71, 48, 72 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (𝑆 D ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛))) |
74 | 54 | reseq1d 5316 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆) = ((ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) ↾ 𝑆)) |
75 | | simpll 786 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → 𝑆 ∈ {ℝ, ℂ}) |
76 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
77 | 76 | cnfldtop 22397 |
. . . . . . . . . . . . . . . . 17
⊢
(TopOpen‘ℂfld) ∈ Top |
78 | 76 | cnfldtopon 22396 |
. . . . . . . . . . . . . . . . . . 19
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
79 | 78 | toponunii 20547 |
. . . . . . . . . . . . . . . . . 18
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
80 | 79 | ntrss2 20671 |
. . . . . . . . . . . . . . . . 17
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ dom ((ℂ
D𝑛 𝐹)‘𝑛) ⊆ ℂ) →
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛)) ⊆ dom ((ℂ
D𝑛 𝐹)‘𝑛)) |
81 | 77, 63, 80 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) →
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛)) ⊆ dom ((ℂ
D𝑛 𝐹)‘𝑛)) |
82 | 79 | restid 15917 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
83 | 77, 82 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
84 | 83 | eqcomi 2619 |
. . . . . . . . . . . . . . . . . . 19
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
85 | 52, 58, 63, 84, 76 | dvbssntr 23470 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) ⊆
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛))) |
86 | 56, 85 | eqsstrd 3602 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom 𝐹 ⊆
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛))) |
87 | 50, 86 | sstrd 3578 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘𝑛) ⊆
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛))) |
88 | 81, 87 | eqssd 3585 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) →
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛)) = dom ((ℂ D𝑛
𝐹)‘𝑛)) |
89 | 79 | isopn3 20680 |
. . . . . . . . . . . . . . . 16
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ dom ((ℂ
D𝑛 𝐹)‘𝑛) ⊆ ℂ) → (dom ((ℂ
D𝑛 𝐹)‘𝑛) ∈
(TopOpen‘ℂfld) ↔
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛)) = dom ((ℂ D𝑛
𝐹)‘𝑛))) |
90 | 77, 63, 89 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (dom ((ℂ
D𝑛 𝐹)‘𝑛) ∈
(TopOpen‘ℂfld) ↔
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛)) = dom ((ℂ D𝑛
𝐹)‘𝑛))) |
91 | 88, 90 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘𝑛) ∈
(TopOpen‘ℂfld)) |
92 | 66, 56 | eqtr2d 2645 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) = dom ((ℂ D𝑛
𝐹)‘𝑛)) |
93 | 76 | dvres3a 23484 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
((ℂ D𝑛 𝐹)‘𝑛):dom ((ℂ D𝑛 𝐹)‘𝑛)⟶ℂ) ∧ (dom ((ℂ
D𝑛 𝐹)‘𝑛) ∈
(TopOpen‘ℂfld) ∧ dom (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) = dom ((ℂ D𝑛
𝐹)‘𝑛))) → (𝑆 D (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)) = ((ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) ↾ 𝑆)) |
94 | 75, 58, 91, 92, 93 | syl22anc 1319 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (𝑆 D (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)) = ((ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) ↾ 𝑆)) |
95 | 74, 94 | eqtr4d 2647 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆) = (𝑆 D (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆))) |
96 | 73, 95 | eqeq12d 2625 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆) ↔ (𝑆 D ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛)) = (𝑆 D (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)))) |
97 | 69, 96 | syl5ibr 235 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆))) |
98 | 97 | expr 641 |
. . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ 𝑛 ∈ ℕ0) → (dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹 → (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆)))) |
99 | 98 | a2d 29 |
. . . . . . . 8
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ 𝑛 ∈ ℕ0) → ((dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)) → (dom ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆)))) |
100 | 68, 99 | syld 46 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ 𝑛 ∈ ℕ0) → ((dom
((ℂ D𝑛 𝐹)‘𝑛) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)) → (dom ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆)))) |
101 | 100 | expcom 450 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
→ ((𝑆 ∈ {ℝ,
ℂ} ∧ 𝐹 ∈
(ℂ ↑pm ℂ)) → ((dom ((ℂ
D𝑛 𝐹)‘𝑛) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)) → (dom ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆))))) |
102 | 101 | a2d 29 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
→ (((𝑆 ∈
{ℝ, ℂ} ∧ 𝐹
∈ (ℂ ↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘𝑛) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆))) → ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆))))) |
103 | 8, 16, 24, 32, 44, 102 | nn0ind 11348 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ((𝑆 ∈ {ℝ,
ℂ} ∧ 𝐹 ∈
(ℂ ↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘𝑁) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)))) |
104 | 103 | com12 32 |
. . 3
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → (𝑁 ∈ ℕ0 → (dom
((ℂ D𝑛 𝐹)‘𝑁) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)))) |
105 | 104 | 3impia 1253 |
. 2
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ) ∧ 𝑁 ∈ ℕ0) → (dom
((ℂ D𝑛 𝐹)‘𝑁) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆))) |
106 | 105 | imp 444 |
1
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ) ∧ 𝑁 ∈ ℕ0) ∧ dom
((ℂ D𝑛 𝐹)‘𝑁) = dom 𝐹) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)) |