| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑥 = 0 → ((ℂ
D𝑛 𝐹)‘𝑥) = ((ℂ D𝑛 𝐹)‘0)) | 
| 2 | 1 | dmeqd 5915 | . . . . . . . 8
⊢ (𝑥 = 0 → dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom ((ℂ D𝑛 𝐹)‘0)) | 
| 3 | 2 | eqeq1d 2738 | . . . . . . 7
⊢ (𝑥 = 0 → (dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 ↔ dom ((ℂ D𝑛
𝐹)‘0) = dom 𝐹)) | 
| 4 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑥 = 0 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0)) | 
| 5 | 1 | reseq1d 5995 | . . . . . . . 8
⊢ (𝑥 = 0 → (((ℂ
D𝑛 𝐹)‘𝑥) ↾ 𝑆) = (((ℂ D𝑛 𝐹)‘0) ↾ 𝑆)) | 
| 6 | 4, 5 | eqeq12d 2752 | . . . . . . 7
⊢ (𝑥 = 0 → (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆) ↔ ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (((ℂ
D𝑛 𝐹)‘0) ↾ 𝑆))) | 
| 7 | 3, 6 | imbi12d 344 | . . . . . 6
⊢ (𝑥 = 0 → ((dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆)) ↔ (dom ((ℂ
D𝑛 𝐹)‘0) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (((ℂ
D𝑛 𝐹)‘0) ↾ 𝑆)))) | 
| 8 | 7 | imbi2d 340 | . . . . 5
⊢ (𝑥 = 0 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆))) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ D𝑛 𝐹)‘0) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (((ℂ
D𝑛 𝐹)‘0) ↾ 𝑆))))) | 
| 9 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑥 = 𝑛 → ((ℂ D𝑛 𝐹)‘𝑥) = ((ℂ D𝑛 𝐹)‘𝑛)) | 
| 10 | 9 | dmeqd 5915 | . . . . . . . 8
⊢ (𝑥 = 𝑛 → dom ((ℂ D𝑛
𝐹)‘𝑥) = dom ((ℂ D𝑛 𝐹)‘𝑛)) | 
| 11 | 10 | eqeq1d 2738 | . . . . . . 7
⊢ (𝑥 = 𝑛 → (dom ((ℂ D𝑛
𝐹)‘𝑥) = dom 𝐹 ↔ dom ((ℂ D𝑛
𝐹)‘𝑛) = dom 𝐹)) | 
| 12 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑥 = 𝑛 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛)) | 
| 13 | 9 | reseq1d 5995 | . . . . . . . 8
⊢ (𝑥 = 𝑛 → (((ℂ D𝑛
𝐹)‘𝑥) ↾ 𝑆) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)) | 
| 14 | 12, 13 | eqeq12d 2752 | . . . . . . 7
⊢ (𝑥 = 𝑛 → (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆) ↔ ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆))) | 
| 15 | 11, 14 | imbi12d 344 | . . . . . 6
⊢ (𝑥 = 𝑛 → ((dom ((ℂ D𝑛
𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆)) ↔ (dom ((ℂ
D𝑛 𝐹)‘𝑛) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)))) | 
| 16 | 15 | imbi2d 340 | . . . . 5
⊢ (𝑥 = 𝑛 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆))) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ D𝑛 𝐹)‘𝑛) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆))))) | 
| 17 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑥 = (𝑛 + 1) → ((ℂ D𝑛
𝐹)‘𝑥) = ((ℂ D𝑛 𝐹)‘(𝑛 + 1))) | 
| 18 | 17 | dmeqd 5915 | . . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom ((ℂ D𝑛 𝐹)‘(𝑛 + 1))) | 
| 19 | 18 | eqeq1d 2738 | . . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 ↔ dom ((ℂ D𝑛
𝐹)‘(𝑛 + 1)) = dom 𝐹)) | 
| 20 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1))) | 
| 21 | 17 | reseq1d 5995 | . . . . . . . 8
⊢ (𝑥 = (𝑛 + 1) → (((ℂ D𝑛
𝐹)‘𝑥) ↾ 𝑆) = (((ℂ D𝑛 𝐹)‘(𝑛 + 1)) ↾ 𝑆)) | 
| 22 | 20, 21 | eqeq12d 2752 | . . . . . . 7
⊢ (𝑥 = (𝑛 + 1) → (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆) ↔ ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆))) | 
| 23 | 19, 22 | imbi12d 344 | . . . . . 6
⊢ (𝑥 = (𝑛 + 1) → ((dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆)) ↔ (dom ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆)))) | 
| 24 | 23 | imbi2d 340 | . . . . 5
⊢ (𝑥 = (𝑛 + 1) → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆))) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆))))) | 
| 25 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑥 = 𝑁 → ((ℂ D𝑛
𝐹)‘𝑥) = ((ℂ D𝑛 𝐹)‘𝑁)) | 
| 26 | 25 | dmeqd 5915 | . . . . . . . 8
⊢ (𝑥 = 𝑁 → dom ((ℂ D𝑛
𝐹)‘𝑥) = dom ((ℂ D𝑛 𝐹)‘𝑁)) | 
| 27 | 26 | eqeq1d 2738 | . . . . . . 7
⊢ (𝑥 = 𝑁 → (dom ((ℂ D𝑛
𝐹)‘𝑥) = dom 𝐹 ↔ dom ((ℂ D𝑛
𝐹)‘𝑁) = dom 𝐹)) | 
| 28 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑥 = 𝑁 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁)) | 
| 29 | 25 | reseq1d 5995 | . . . . . . . 8
⊢ (𝑥 = 𝑁 → (((ℂ D𝑛
𝐹)‘𝑥) ↾ 𝑆) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)) | 
| 30 | 28, 29 | eqeq12d 2752 | . . . . . . 7
⊢ (𝑥 = 𝑁 → (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆) ↔ ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆))) | 
| 31 | 27, 30 | imbi12d 344 | . . . . . 6
⊢ (𝑥 = 𝑁 → ((dom ((ℂ
D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆)) ↔ (dom ((ℂ
D𝑛 𝐹)‘𝑁) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)))) | 
| 32 | 31 | imbi2d 340 | . . . . 5
⊢ (𝑥 = 𝑁 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ D𝑛 𝐹)‘𝑥) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑥) = (((ℂ D𝑛 𝐹)‘𝑥) ↾ 𝑆))) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ D𝑛 𝐹)‘𝑁) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆))))) | 
| 33 |  | recnprss 25940 | . . . . . . . . 9
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) | 
| 34 | 33 | adantr 480 | . . . . . . . 8
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → 𝑆 ⊆ ℂ) | 
| 35 |  | pmresg 8911 | . . . . . . . 8
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → (𝐹 ↾ 𝑆) ∈ (ℂ ↑pm 𝑆)) | 
| 36 |  | dvn0 25961 | . . . . . . . 8
⊢ ((𝑆 ⊆ ℂ ∧ (𝐹 ↾ 𝑆) ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (𝐹 ↾ 𝑆)) | 
| 37 | 34, 35, 36 | syl2anc 584 | . . . . . . 7
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (𝐹 ↾ 𝑆)) | 
| 38 |  | ssidd 4006 | . . . . . . . . 9
⊢ (𝑆 ∈ {ℝ, ℂ}
→ ℂ ⊆ ℂ) | 
| 39 |  | dvn0 25961 | . . . . . . . . 9
⊢ ((ℂ
⊆ ℂ ∧ 𝐹
∈ (ℂ ↑pm ℂ)) → ((ℂ
D𝑛 𝐹)‘0) = 𝐹) | 
| 40 | 38, 39 | sylan 580 | . . . . . . . 8
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → ((ℂ D𝑛 𝐹)‘0) = 𝐹) | 
| 41 | 40 | reseq1d 5995 | . . . . . . 7
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → (((ℂ D𝑛 𝐹)‘0) ↾ 𝑆) = (𝐹 ↾ 𝑆)) | 
| 42 | 37, 41 | eqtr4d 2779 | . . . . . 6
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (((ℂ
D𝑛 𝐹)‘0) ↾ 𝑆)) | 
| 43 | 42 | a1d 25 | . . . . 5
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ D𝑛 𝐹)‘0) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘0) = (((ℂ
D𝑛 𝐹)‘0) ↾ 𝑆))) | 
| 44 |  | cnelprrecn 11249 | . . . . . . . . . 10
⊢ ℂ
∈ {ℝ, ℂ} | 
| 45 |  | simplr 768 | . . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → 𝐹 ∈ (ℂ ↑pm
ℂ)) | 
| 46 |  | simprl 770 | . . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → 𝑛 ∈ ℕ0) | 
| 47 |  | dvnbss 25965 | . . . . . . . . . 10
⊢ ((ℂ
∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm
ℂ) ∧ 𝑛 ∈
ℕ0) → dom ((ℂ D𝑛 𝐹)‘𝑛) ⊆ dom 𝐹) | 
| 48 | 44, 45, 46, 47 | mp3an2i 1467 | . . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘𝑛) ⊆ dom 𝐹) | 
| 49 |  | simprr 772 | . . . . . . . . . . 11
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹) | 
| 50 |  | ssidd 4006 | . . . . . . . . . . . . 13
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → ℂ ⊆
ℂ) | 
| 51 |  | dvnp1 25962 | . . . . . . . . . . . . 13
⊢ ((ℂ
⊆ ℂ ∧ 𝐹
∈ (ℂ ↑pm ℂ) ∧ 𝑛 ∈ ℕ0) → ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛))) | 
| 52 | 50, 45, 46, 51 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → ((ℂ D𝑛
𝐹)‘(𝑛 + 1)) = (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛))) | 
| 53 | 52 | dmeqd 5915 | . . . . . . . . . . 11
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = dom (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛))) | 
| 54 | 49, 53 | eqtr3d 2778 | . . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom 𝐹 = dom (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛))) | 
| 55 |  | dvnf 25964 | . . . . . . . . . . . 12
⊢ ((ℂ
∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm
ℂ) ∧ 𝑛 ∈
ℕ0) → ((ℂ D𝑛 𝐹)‘𝑛):dom ((ℂ D𝑛 𝐹)‘𝑛)⟶ℂ) | 
| 56 | 44, 45, 46, 55 | mp3an2i 1467 | . . . . . . . . . . 11
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → ((ℂ D𝑛
𝐹)‘𝑛):dom ((ℂ D𝑛 𝐹)‘𝑛)⟶ℂ) | 
| 57 |  | cnex 11237 | . . . . . . . . . . . . . . 15
⊢ ℂ
∈ V | 
| 58 | 57, 57 | elpm2 8915 | . . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (ℂ
↑pm ℂ) ↔ (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ)) | 
| 59 | 58 | simprbi 496 | . . . . . . . . . . . . 13
⊢ (𝐹 ∈ (ℂ
↑pm ℂ) → dom 𝐹 ⊆ ℂ) | 
| 60 | 45, 59 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom 𝐹 ⊆ ℂ) | 
| 61 | 48, 60 | sstrd 3993 | . . . . . . . . . . 11
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘𝑛) ⊆ ℂ) | 
| 62 | 50, 56, 61 | dvbss 25937 | . . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) ⊆ dom ((ℂ
D𝑛 𝐹)‘𝑛)) | 
| 63 | 54, 62 | eqsstrd 4017 | . . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom 𝐹 ⊆ dom ((ℂ D𝑛
𝐹)‘𝑛)) | 
| 64 | 48, 63 | eqssd 4000 | . . . . . . . 8
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘𝑛) = dom 𝐹) | 
| 65 | 64 | expr 456 | . . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ 𝑛 ∈ ℕ0) → (dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹 → dom ((ℂ D𝑛
𝐹)‘𝑛) = dom 𝐹)) | 
| 66 | 65 | imim1d 82 | . . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ 𝑛 ∈ ℕ0) → ((dom
((ℂ D𝑛 𝐹)‘𝑛) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)) → (dom ((ℂ
D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)))) | 
| 67 |  | oveq2 7440 | . . . . . . 7
⊢ (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆) → (𝑆 D ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛)) = (𝑆 D (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆))) | 
| 68 | 34 | adantr 480 | . . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → 𝑆 ⊆ ℂ) | 
| 69 | 35 | adantr 480 | . . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (𝐹 ↾ 𝑆) ∈ (ℂ ↑pm 𝑆)) | 
| 70 |  | dvnp1 25962 | . . . . . . . . 9
⊢ ((𝑆 ⊆ ℂ ∧ (𝐹 ↾ 𝑆) ∈ (ℂ ↑pm 𝑆) ∧ 𝑛 ∈ ℕ0) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (𝑆 D ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛))) | 
| 71 | 68, 69, 46, 70 | syl3anc 1372 | . . . . . . . 8
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (𝑆 D ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛))) | 
| 72 | 52 | reseq1d 5995 | . . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆) = ((ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) ↾ 𝑆)) | 
| 73 |  | simpll 766 | . . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → 𝑆 ∈ {ℝ, ℂ}) | 
| 74 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 75 | 74 | cnfldtop 24805 | . . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) ∈ Top | 
| 76 |  | unicntop 24807 | . . . . . . . . . . . . . 14
⊢ ℂ =
∪
(TopOpen‘ℂfld) | 
| 77 | 76 | ntrss2 23066 | . . . . . . . . . . . . 13
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ dom ((ℂ
D𝑛 𝐹)‘𝑛) ⊆ ℂ) →
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛)) ⊆ dom ((ℂ
D𝑛 𝐹)‘𝑛)) | 
| 78 | 75, 61, 77 | sylancr 587 | . . . . . . . . . . . 12
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) →
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛)) ⊆ dom ((ℂ
D𝑛 𝐹)‘𝑛)) | 
| 79 | 74 | cnfldtopon 24804 | . . . . . . . . . . . . . . . 16
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) | 
| 80 | 79 | toponrestid 22928 | . . . . . . . . . . . . . . 15
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) | 
| 81 | 50, 56, 61, 80, 74 | dvbssntr 25936 | . . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) ⊆
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛))) | 
| 82 | 54, 81 | eqsstrd 4017 | . . . . . . . . . . . . 13
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom 𝐹 ⊆
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛))) | 
| 83 | 48, 82 | sstrd 3993 | . . . . . . . . . . . 12
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘𝑛) ⊆
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛))) | 
| 84 | 78, 83 | eqssd 4000 | . . . . . . . . . . 11
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) →
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛)) = dom ((ℂ D𝑛
𝐹)‘𝑛)) | 
| 85 | 76 | isopn3 23075 | . . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ dom ((ℂ
D𝑛 𝐹)‘𝑛) ⊆ ℂ) → (dom ((ℂ
D𝑛 𝐹)‘𝑛) ∈
(TopOpen‘ℂfld) ↔
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛)) = dom ((ℂ D𝑛
𝐹)‘𝑛))) | 
| 86 | 75, 61, 85 | sylancr 587 | . . . . . . . . . . 11
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (dom ((ℂ
D𝑛 𝐹)‘𝑛) ∈
(TopOpen‘ℂfld) ↔
((int‘(TopOpen‘ℂfld))‘dom ((ℂ
D𝑛 𝐹)‘𝑛)) = dom ((ℂ D𝑛
𝐹)‘𝑛))) | 
| 87 | 84, 86 | mpbird 257 | . . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom ((ℂ
D𝑛 𝐹)‘𝑛) ∈
(TopOpen‘ℂfld)) | 
| 88 | 64, 54 | eqtr2d 2777 | . . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → dom (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) = dom ((ℂ D𝑛
𝐹)‘𝑛)) | 
| 89 | 74 | dvres3a 25950 | . . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
((ℂ D𝑛 𝐹)‘𝑛):dom ((ℂ D𝑛 𝐹)‘𝑛)⟶ℂ) ∧ (dom ((ℂ
D𝑛 𝐹)‘𝑛) ∈
(TopOpen‘ℂfld) ∧ dom (ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) = dom ((ℂ D𝑛
𝐹)‘𝑛))) → (𝑆 D (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)) = ((ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) ↾ 𝑆)) | 
| 90 | 73, 56, 87, 88, 89 | syl22anc 838 | . . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (𝑆 D (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)) = ((ℂ D ((ℂ
D𝑛 𝐹)‘𝑛)) ↾ 𝑆)) | 
| 91 | 72, 90 | eqtr4d 2779 | . . . . . . . 8
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆) = (𝑆 D (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆))) | 
| 92 | 71, 91 | eqeq12d 2752 | . . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆) ↔ (𝑆 D ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛)) = (𝑆 D (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆)))) | 
| 93 | 67, 92 | imbitrrid 246 | . . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) ∧ (𝑛 ∈ ℕ0 ∧ dom
((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹)) → (((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆))) | 
| 94 | 66, 93 | animpimp2impd 846 | . . . . 5
⊢ (𝑛 ∈ ℕ0
→ (((𝑆 ∈
{ℝ, ℂ} ∧ 𝐹
∈ (ℂ ↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘𝑛) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑛) = (((ℂ D𝑛 𝐹)‘𝑛) ↾ 𝑆))) → ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ
↑pm ℂ)) → (dom ((ℂ D𝑛 𝐹)‘(𝑛 + 1)) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘(𝑛 + 1)) = (((ℂ D𝑛
𝐹)‘(𝑛 + 1)) ↾ 𝑆))))) | 
| 95 | 8, 16, 24, 32, 43, 94 | nn0ind 12715 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ ((𝑆 ∈ {ℝ,
ℂ} ∧ 𝐹 ∈
(ℂ ↑pm ℂ)) → (dom ((ℂ
D𝑛 𝐹)‘𝑁) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)))) | 
| 96 | 95 | com12 32 | . . 3
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ)) → (𝑁 ∈ ℕ0 → (dom
((ℂ D𝑛 𝐹)‘𝑁) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)))) | 
| 97 | 96 | 3impia 1117 | . 2
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ) ∧ 𝑁 ∈ ℕ0) → (dom
((ℂ D𝑛 𝐹)‘𝑁) = dom 𝐹 → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆))) | 
| 98 | 97 | imp 406 | 1
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm ℂ) ∧ 𝑁 ∈ ℕ0) ∧ dom
((ℂ D𝑛 𝐹)‘𝑁) = dom 𝐹) → ((𝑆 D𝑛 (𝐹 ↾ 𝑆))‘𝑁) = (((ℂ D𝑛 𝐹)‘𝑁) ↾ 𝑆)) |