| Step | Hyp | Ref
| Expression |
| 1 | | dvnmptconst.n |
. 2
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 2 | | id 22 |
. 2
⊢ (𝜑 → 𝜑) |
| 3 | | fveq2 6906 |
. . . . 5
⊢ (𝑛 = 1 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘1)) |
| 4 | 3 | eqeq1d 2739 |
. . . 4
⊢ (𝑛 = 1 → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 0) ↔ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘1) = (𝑥 ∈ 𝑋 ↦ 0))) |
| 5 | 4 | imbi2d 340 |
. . 3
⊢ (𝑛 = 1 → ((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 0)) ↔ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘1) = (𝑥 ∈ 𝑋 ↦ 0)))) |
| 6 | | fveq2 6906 |
. . . . 5
⊢ (𝑛 = 𝑚 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚)) |
| 7 | 6 | eqeq1d 2739 |
. . . 4
⊢ (𝑛 = 𝑚 → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 0) ↔ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0))) |
| 8 | 7 | imbi2d 340 |
. . 3
⊢ (𝑛 = 𝑚 → ((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 0)) ↔ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0)))) |
| 9 | | fveq2 6906 |
. . . . 5
⊢ (𝑛 = (𝑚 + 1) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑚 + 1))) |
| 10 | 9 | eqeq1d 2739 |
. . . 4
⊢ (𝑛 = (𝑚 + 1) → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 0) ↔ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑚 + 1)) = (𝑥 ∈ 𝑋 ↦ 0))) |
| 11 | 10 | imbi2d 340 |
. . 3
⊢ (𝑛 = (𝑚 + 1) → ((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 0)) ↔ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑚 + 1)) = (𝑥 ∈ 𝑋 ↦ 0)))) |
| 12 | | fveq2 6906 |
. . . . 5
⊢ (𝑛 = 𝑁 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑁)) |
| 13 | 12 | eqeq1d 2739 |
. . . 4
⊢ (𝑛 = 𝑁 → (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 0) ↔ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑁) = (𝑥 ∈ 𝑋 ↦ 0))) |
| 14 | 13 | imbi2d 340 |
. . 3
⊢ (𝑛 = 𝑁 → ((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑛) = (𝑥 ∈ 𝑋 ↦ 0)) ↔ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑁) = (𝑥 ∈ 𝑋 ↦ 0)))) |
| 15 | | dvnmptconst.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
| 16 | | recnprss 25939 |
. . . . . 6
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
| 17 | 15, 16 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
| 18 | | dvnmptconst.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 19 | 18 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) |
| 20 | | restsspw 17476 |
. . . . . . . 8
⊢
((TopOpen‘ℂfld) ↾t 𝑆) ⊆ 𝒫 𝑆 |
| 21 | | dvnmptconst.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈
((TopOpen‘ℂfld) ↾t 𝑆)) |
| 22 | 20, 21 | sselid 3981 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝒫 𝑆) |
| 23 | | elpwi 4607 |
. . . . . . 7
⊢ (𝑋 ∈ 𝒫 𝑆 → 𝑋 ⊆ 𝑆) |
| 24 | 22, 23 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑋 ⊆ 𝑆) |
| 25 | | cnex 11236 |
. . . . . . 7
⊢ ℂ
∈ V |
| 26 | 25 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℂ ∈
V) |
| 27 | 19, 24, 26, 15 | mptelpm 45181 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (ℂ ↑pm 𝑆)) |
| 28 | | dvn1 25962 |
. . . . 5
⊢ ((𝑆 ⊆ ℂ ∧ (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘1) = (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴))) |
| 29 | 17, 27, 28 | syl2anc 584 |
. . . 4
⊢ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘1) = (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴))) |
| 30 | 15, 21, 18 | dvmptconst 45930 |
. . . 4
⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ 0)) |
| 31 | 29, 30 | eqtrd 2777 |
. . 3
⊢ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘1) = (𝑥 ∈ 𝑋 ↦ 0)) |
| 32 | | simp3 1139 |
. . . . 5
⊢ ((𝑚 ∈ ℕ ∧ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0)) ∧ 𝜑) → 𝜑) |
| 33 | | simp1 1137 |
. . . . 5
⊢ ((𝑚 ∈ ℕ ∧ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0)) ∧ 𝜑) → 𝑚 ∈ ℕ) |
| 34 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0)) ∧ 𝜑) → 𝜑) |
| 35 | | simpl 482 |
. . . . . . 7
⊢ (((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0)) ∧ 𝜑) → (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0))) |
| 36 | | pm3.35 803 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0))) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0)) |
| 37 | 34, 35, 36 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0)) ∧ 𝜑) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0)) |
| 38 | 37 | 3adant1 1131 |
. . . . 5
⊢ ((𝑚 ∈ ℕ ∧ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0)) ∧ 𝜑) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0)) |
| 39 | 17 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0)) → 𝑆 ⊆ ℂ) |
| 40 | 27 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0)) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (ℂ ↑pm 𝑆)) |
| 41 | | nnnn0 12533 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℕ0) |
| 42 | 41 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0)) → 𝑚 ∈ ℕ0) |
| 43 | | dvnp1 25961 |
. . . . . . 7
⊢ ((𝑆 ⊆ ℂ ∧ (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (ℂ ↑pm 𝑆) ∧ 𝑚 ∈ ℕ0) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑚 + 1)) = (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚))) |
| 44 | 39, 40, 42, 43 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑚 + 1)) = (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚))) |
| 45 | | oveq2 7439 |
. . . . . . 7
⊢ (((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0) → (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚)) = (𝑆 D (𝑥 ∈ 𝑋 ↦ 0))) |
| 46 | 45 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0)) → (𝑆 D ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚)) = (𝑆 D (𝑥 ∈ 𝑋 ↦ 0))) |
| 47 | | 0cnd 11254 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℂ) |
| 48 | 15, 21, 47 | dvmptconst 45930 |
. . . . . . 7
⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 0)) = (𝑥 ∈ 𝑋 ↦ 0)) |
| 49 | 48 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0)) → (𝑆 D (𝑥 ∈ 𝑋 ↦ 0)) = (𝑥 ∈ 𝑋 ↦ 0)) |
| 50 | 44, 46, 49 | 3eqtrd 2781 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ ∧ ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0)) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑚 + 1)) = (𝑥 ∈ 𝑋 ↦ 0)) |
| 51 | 32, 33, 38, 50 | syl3anc 1373 |
. . . 4
⊢ ((𝑚 ∈ ℕ ∧ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0)) ∧ 𝜑) → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑚 + 1)) = (𝑥 ∈ 𝑋 ↦ 0)) |
| 52 | 51 | 3exp 1120 |
. . 3
⊢ (𝑚 ∈ ℕ → ((𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑚) = (𝑥 ∈ 𝑋 ↦ 0)) → (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘(𝑚 + 1)) = (𝑥 ∈ 𝑋 ↦ 0)))) |
| 53 | 5, 8, 11, 14, 31, 52 | nnind 12284 |
. 2
⊢ (𝑁 ∈ ℕ → (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑁) = (𝑥 ∈ 𝑋 ↦ 0))) |
| 54 | 1, 2, 53 | sylc 65 |
1
⊢ (𝜑 → ((𝑆 D𝑛 (𝑥 ∈ 𝑋 ↦ 𝐴))‘𝑁) = (𝑥 ∈ 𝑋 ↦ 0)) |