| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6905 | . . . . . 6
⊢ (𝑛 = 𝑀 →
((𝓑C𝑛‘𝑆)‘𝑛) =
((𝓑C𝑛‘𝑆)‘𝑀)) | 
| 2 | 1 | sseq1d 4014 | . . . . 5
⊢ (𝑛 = 𝑀 →
(((𝓑C𝑛‘𝑆)‘𝑛) ⊆
((𝓑C𝑛‘𝑆)‘𝑀) ↔
((𝓑C𝑛‘𝑆)‘𝑀) ⊆
((𝓑C𝑛‘𝑆)‘𝑀))) | 
| 3 | 2 | imbi2d 340 | . . . 4
⊢ (𝑛 = 𝑀 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((𝓑C𝑛‘𝑆)‘𝑛) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((𝓑C𝑛‘𝑆)‘𝑀) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)))) | 
| 4 |  | fveq2 6905 | . . . . . 6
⊢ (𝑛 = 𝑚 →
((𝓑C𝑛‘𝑆)‘𝑛) =
((𝓑C𝑛‘𝑆)‘𝑚)) | 
| 5 | 4 | sseq1d 4014 | . . . . 5
⊢ (𝑛 = 𝑚 →
(((𝓑C𝑛‘𝑆)‘𝑛) ⊆
((𝓑C𝑛‘𝑆)‘𝑀) ↔
((𝓑C𝑛‘𝑆)‘𝑚) ⊆
((𝓑C𝑛‘𝑆)‘𝑀))) | 
| 6 | 5 | imbi2d 340 | . . . 4
⊢ (𝑛 = 𝑚 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((𝓑C𝑛‘𝑆)‘𝑛) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((𝓑C𝑛‘𝑆)‘𝑚) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)))) | 
| 7 |  | fveq2 6905 | . . . . . 6
⊢ (𝑛 = (𝑚 + 1) →
((𝓑C𝑛‘𝑆)‘𝑛) =
((𝓑C𝑛‘𝑆)‘(𝑚 + 1))) | 
| 8 | 7 | sseq1d 4014 | . . . . 5
⊢ (𝑛 = (𝑚 + 1) →
(((𝓑C𝑛‘𝑆)‘𝑛) ⊆
((𝓑C𝑛‘𝑆)‘𝑀) ↔
((𝓑C𝑛‘𝑆)‘(𝑚 + 1)) ⊆
((𝓑C𝑛‘𝑆)‘𝑀))) | 
| 9 | 8 | imbi2d 340 | . . . 4
⊢ (𝑛 = (𝑚 + 1) → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((𝓑C𝑛‘𝑆)‘𝑛) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((𝓑C𝑛‘𝑆)‘(𝑚 + 1)) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)))) | 
| 10 |  | fveq2 6905 | . . . . . 6
⊢ (𝑛 = 𝑁 →
((𝓑C𝑛‘𝑆)‘𝑛) =
((𝓑C𝑛‘𝑆)‘𝑁)) | 
| 11 | 10 | sseq1d 4014 | . . . . 5
⊢ (𝑛 = 𝑁 →
(((𝓑C𝑛‘𝑆)‘𝑛) ⊆
((𝓑C𝑛‘𝑆)‘𝑀) ↔
((𝓑C𝑛‘𝑆)‘𝑁) ⊆
((𝓑C𝑛‘𝑆)‘𝑀))) | 
| 12 | 11 | imbi2d 340 | . . . 4
⊢ (𝑛 = 𝑁 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((𝓑C𝑛‘𝑆)‘𝑛) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((𝓑C𝑛‘𝑆)‘𝑁) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)))) | 
| 13 |  | ssid 4005 | . . . . 5
⊢
((𝓑C𝑛‘𝑆)‘𝑀) ⊆
((𝓑C𝑛‘𝑆)‘𝑀) | 
| 14 | 13 | 2a1i 12 | . . . 4
⊢ (𝑀 ∈ ℤ → ((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) → ((𝓑C𝑛‘𝑆)‘𝑀) ⊆
((𝓑C𝑛‘𝑆)‘𝑀))) | 
| 15 |  | simprl 770 | . . . . . . . . . . 11
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → 𝑓 ∈ (ℂ ↑pm 𝑆)) | 
| 16 |  | recnprss 25940 | . . . . . . . . . . . . . 14
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) | 
| 17 | 16 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → 𝑆 ⊆ ℂ) | 
| 18 | 17 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → 𝑆 ⊆ ℂ) | 
| 19 |  | simplll 774 | . . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → 𝑆 ∈ {ℝ, ℂ}) | 
| 20 |  | eluznn0 12960 | . . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℕ0
∧ 𝑚 ∈
(ℤ≥‘𝑀)) → 𝑚 ∈ ℕ0) | 
| 21 | 20 | adantll 714 | . . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → 𝑚 ∈ ℕ0) | 
| 22 | 21 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → 𝑚 ∈ ℕ0) | 
| 23 |  | dvnf 25964 | . . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝑓 ∈ (ℂ
↑pm 𝑆)
∧ 𝑚 ∈
ℕ0) → ((𝑆 D𝑛 𝑓)‘𝑚):dom ((𝑆 D𝑛 𝑓)‘𝑚)⟶ℂ) | 
| 24 | 19, 15, 22, 23 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → ((𝑆 D𝑛 𝑓)‘𝑚):dom ((𝑆 D𝑛 𝑓)‘𝑚)⟶ℂ) | 
| 25 |  | dvnbss 25965 | . . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝑓 ∈ (ℂ
↑pm 𝑆)
∧ 𝑚 ∈
ℕ0) → dom ((𝑆 D𝑛 𝑓)‘𝑚) ⊆ dom 𝑓) | 
| 26 | 19, 15, 22, 25 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom ((𝑆 D𝑛 𝑓)‘𝑚) ⊆ dom 𝑓) | 
| 27 |  | dvnp1 25962 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆 ⊆ ℂ ∧ 𝑓 ∈ (ℂ
↑pm 𝑆)
∧ 𝑚 ∈
ℕ0) → ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) = (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚))) | 
| 28 | 18, 15, 22, 27 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) = (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚))) | 
| 29 |  | simprr 772 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ)) | 
| 30 | 28, 29 | eqeltrrd 2841 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚)) ∈ (dom 𝑓–cn→ℂ)) | 
| 31 |  | cncff 24920 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚)) ∈ (dom 𝑓–cn→ℂ) → (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚)):dom 𝑓⟶ℂ) | 
| 32 | 30, 31 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚)):dom 𝑓⟶ℂ) | 
| 33 | 32 | fdmd 6745 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚)) = dom 𝑓) | 
| 34 |  | cnex 11237 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ℂ
∈ V | 
| 35 |  | elpm2g 8885 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((ℂ
∈ V ∧ 𝑆 ∈
{ℝ, ℂ}) → (𝑓 ∈ (ℂ ↑pm 𝑆) ↔ (𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ 𝑆))) | 
| 36 | 34, 19, 35 | sylancr 587 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (𝑓 ∈ (ℂ ↑pm 𝑆) ↔ (𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ 𝑆))) | 
| 37 | 15, 36 | mpbid 232 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ 𝑆)) | 
| 38 | 37 | simprd 495 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom 𝑓 ⊆ 𝑆) | 
| 39 | 26, 38 | sstrd 3993 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom ((𝑆 D𝑛 𝑓)‘𝑚) ⊆ 𝑆) | 
| 40 | 18, 24, 39 | dvbss 25937 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚)) ⊆ dom ((𝑆 D𝑛 𝑓)‘𝑚)) | 
| 41 | 33, 40 | eqsstrrd 4018 | . . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom 𝑓 ⊆ dom ((𝑆 D𝑛 𝑓)‘𝑚)) | 
| 42 | 26, 41 | eqssd 4000 | . . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom ((𝑆 D𝑛 𝑓)‘𝑚) = dom 𝑓) | 
| 43 | 42 | feq2d 6721 | . . . . . . . . . . . . 13
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (((𝑆 D𝑛 𝑓)‘𝑚):dom ((𝑆 D𝑛 𝑓)‘𝑚)⟶ℂ ↔ ((𝑆 D𝑛 𝑓)‘𝑚):dom 𝑓⟶ℂ)) | 
| 44 | 24, 43 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → ((𝑆 D𝑛 𝑓)‘𝑚):dom 𝑓⟶ℂ) | 
| 45 |  | dvcn 25958 | . . . . . . . . . . . 12
⊢ (((𝑆 ⊆ ℂ ∧ ((𝑆 D𝑛 𝑓)‘𝑚):dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ 𝑆) ∧ dom (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚)) = dom 𝑓) → ((𝑆 D𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ)) | 
| 46 | 18, 44, 38, 33, 45 | syl31anc 1374 | . . . . . . . . . . 11
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → ((𝑆 D𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ)) | 
| 47 | 15, 46 | jca 511 | . . . . . . . . . 10
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ))) | 
| 48 | 47 | ex 412 | . . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → ((𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ)) → (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ)))) | 
| 49 |  | peano2nn0 12568 | . . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℕ0) | 
| 50 | 21, 49 | syl 17 | . . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → (𝑚 + 1) ∈
ℕ0) | 
| 51 |  | elcpn 25971 | . . . . . . . . . 10
⊢ ((𝑆 ⊆ ℂ ∧ (𝑚 + 1) ∈
ℕ0) → (𝑓 ∈
((𝓑C𝑛‘𝑆)‘(𝑚 + 1)) ↔ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ)))) | 
| 52 | 17, 50, 51 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → (𝑓 ∈
((𝓑C𝑛‘𝑆)‘(𝑚 + 1)) ↔ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ)))) | 
| 53 |  | elcpn 25971 | . . . . . . . . . 10
⊢ ((𝑆 ⊆ ℂ ∧ 𝑚 ∈ ℕ0)
→ (𝑓 ∈
((𝓑C𝑛‘𝑆)‘𝑚) ↔ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ)))) | 
| 54 | 17, 21, 53 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → (𝑓 ∈
((𝓑C𝑛‘𝑆)‘𝑚) ↔ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ)))) | 
| 55 | 48, 52, 54 | 3imtr4d 294 | . . . . . . . 8
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → (𝑓 ∈
((𝓑C𝑛‘𝑆)‘(𝑚 + 1)) → 𝑓 ∈
((𝓑C𝑛‘𝑆)‘𝑚))) | 
| 56 | 55 | ssrdv 3988 | . . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) →
((𝓑C𝑛‘𝑆)‘(𝑚 + 1)) ⊆
((𝓑C𝑛‘𝑆)‘𝑚)) | 
| 57 |  | sstr2 3989 | . . . . . . 7
⊢
(((𝓑C𝑛‘𝑆)‘(𝑚 + 1)) ⊆
((𝓑C𝑛‘𝑆)‘𝑚) →
(((𝓑C𝑛‘𝑆)‘𝑚) ⊆
((𝓑C𝑛‘𝑆)‘𝑀) →
((𝓑C𝑛‘𝑆)‘(𝑚 + 1)) ⊆
((𝓑C𝑛‘𝑆)‘𝑀))) | 
| 58 | 56, 57 | syl 17 | . . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) →
(((𝓑C𝑛‘𝑆)‘𝑚) ⊆
((𝓑C𝑛‘𝑆)‘𝑀) →
((𝓑C𝑛‘𝑆)‘(𝑚 + 1)) ⊆
((𝓑C𝑛‘𝑆)‘𝑀))) | 
| 59 | 58 | expcom 413 | . . . . 5
⊢ (𝑚 ∈
(ℤ≥‘𝑀) → ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ (((𝓑C𝑛‘𝑆)‘𝑚) ⊆
((𝓑C𝑛‘𝑆)‘𝑀) →
((𝓑C𝑛‘𝑆)‘(𝑚 + 1)) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)))) | 
| 60 | 59 | a2d 29 | . . . 4
⊢ (𝑚 ∈
(ℤ≥‘𝑀) → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((𝓑C𝑛‘𝑆)‘𝑚) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)) → ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((𝓑C𝑛‘𝑆)‘(𝑚 + 1)) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)))) | 
| 61 | 3, 6, 9, 12, 14, 60 | uzind4 12949 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((𝓑C𝑛‘𝑆)‘𝑁) ⊆
((𝓑C𝑛‘𝑆)‘𝑀))) | 
| 62 | 61 | com12 32 | . 2
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) → (𝑁 ∈ (ℤ≥‘𝑀) →
((𝓑C𝑛‘𝑆)‘𝑁) ⊆
((𝓑C𝑛‘𝑆)‘𝑀))) | 
| 63 | 62 | 3impia 1117 | 1
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0 ∧ 𝑁
∈ (ℤ≥‘𝑀)) →
((𝓑C𝑛‘𝑆)‘𝑁) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)) |