Step | Hyp | Ref
| Expression |
1 | | fveq2 6771 |
. . . . . 6
⊢ (𝑛 = 𝑀 →
((𝓑C𝑛‘𝑆)‘𝑛) =
((𝓑C𝑛‘𝑆)‘𝑀)) |
2 | 1 | sseq1d 3957 |
. . . . 5
⊢ (𝑛 = 𝑀 →
(((𝓑C𝑛‘𝑆)‘𝑛) ⊆
((𝓑C𝑛‘𝑆)‘𝑀) ↔
((𝓑C𝑛‘𝑆)‘𝑀) ⊆
((𝓑C𝑛‘𝑆)‘𝑀))) |
3 | 2 | imbi2d 341 |
. . . 4
⊢ (𝑛 = 𝑀 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((𝓑C𝑛‘𝑆)‘𝑛) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((𝓑C𝑛‘𝑆)‘𝑀) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)))) |
4 | | fveq2 6771 |
. . . . . 6
⊢ (𝑛 = 𝑚 →
((𝓑C𝑛‘𝑆)‘𝑛) =
((𝓑C𝑛‘𝑆)‘𝑚)) |
5 | 4 | sseq1d 3957 |
. . . . 5
⊢ (𝑛 = 𝑚 →
(((𝓑C𝑛‘𝑆)‘𝑛) ⊆
((𝓑C𝑛‘𝑆)‘𝑀) ↔
((𝓑C𝑛‘𝑆)‘𝑚) ⊆
((𝓑C𝑛‘𝑆)‘𝑀))) |
6 | 5 | imbi2d 341 |
. . . 4
⊢ (𝑛 = 𝑚 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((𝓑C𝑛‘𝑆)‘𝑛) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((𝓑C𝑛‘𝑆)‘𝑚) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)))) |
7 | | fveq2 6771 |
. . . . . 6
⊢ (𝑛 = (𝑚 + 1) →
((𝓑C𝑛‘𝑆)‘𝑛) =
((𝓑C𝑛‘𝑆)‘(𝑚 + 1))) |
8 | 7 | sseq1d 3957 |
. . . . 5
⊢ (𝑛 = (𝑚 + 1) →
(((𝓑C𝑛‘𝑆)‘𝑛) ⊆
((𝓑C𝑛‘𝑆)‘𝑀) ↔
((𝓑C𝑛‘𝑆)‘(𝑚 + 1)) ⊆
((𝓑C𝑛‘𝑆)‘𝑀))) |
9 | 8 | imbi2d 341 |
. . . 4
⊢ (𝑛 = (𝑚 + 1) → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((𝓑C𝑛‘𝑆)‘𝑛) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((𝓑C𝑛‘𝑆)‘(𝑚 + 1)) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)))) |
10 | | fveq2 6771 |
. . . . . 6
⊢ (𝑛 = 𝑁 →
((𝓑C𝑛‘𝑆)‘𝑛) =
((𝓑C𝑛‘𝑆)‘𝑁)) |
11 | 10 | sseq1d 3957 |
. . . . 5
⊢ (𝑛 = 𝑁 →
(((𝓑C𝑛‘𝑆)‘𝑛) ⊆
((𝓑C𝑛‘𝑆)‘𝑀) ↔
((𝓑C𝑛‘𝑆)‘𝑁) ⊆
((𝓑C𝑛‘𝑆)‘𝑀))) |
12 | 11 | imbi2d 341 |
. . . 4
⊢ (𝑛 = 𝑁 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((𝓑C𝑛‘𝑆)‘𝑛) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((𝓑C𝑛‘𝑆)‘𝑁) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)))) |
13 | | ssid 3948 |
. . . . 5
⊢
((𝓑C𝑛‘𝑆)‘𝑀) ⊆
((𝓑C𝑛‘𝑆)‘𝑀) |
14 | 13 | 2a1i 12 |
. . . 4
⊢ (𝑀 ∈ ℤ → ((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) → ((𝓑C𝑛‘𝑆)‘𝑀) ⊆
((𝓑C𝑛‘𝑆)‘𝑀))) |
15 | | simprl 768 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → 𝑓 ∈ (ℂ ↑pm 𝑆)) |
16 | | recnprss 25066 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
17 | 16 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → 𝑆 ⊆ ℂ) |
18 | 17 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → 𝑆 ⊆ ℂ) |
19 | | simplll 772 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → 𝑆 ∈ {ℝ, ℂ}) |
20 | | eluznn0 12656 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℕ0
∧ 𝑚 ∈
(ℤ≥‘𝑀)) → 𝑚 ∈ ℕ0) |
21 | 20 | adantll 711 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → 𝑚 ∈ ℕ0) |
22 | 21 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → 𝑚 ∈ ℕ0) |
23 | | dvnf 25089 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝑓 ∈ (ℂ
↑pm 𝑆)
∧ 𝑚 ∈
ℕ0) → ((𝑆 D𝑛 𝑓)‘𝑚):dom ((𝑆 D𝑛 𝑓)‘𝑚)⟶ℂ) |
24 | 19, 15, 22, 23 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → ((𝑆 D𝑛 𝑓)‘𝑚):dom ((𝑆 D𝑛 𝑓)‘𝑚)⟶ℂ) |
25 | | dvnbss 25090 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝑓 ∈ (ℂ
↑pm 𝑆)
∧ 𝑚 ∈
ℕ0) → dom ((𝑆 D𝑛 𝑓)‘𝑚) ⊆ dom 𝑓) |
26 | 19, 15, 22, 25 | syl3anc 1370 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom ((𝑆 D𝑛 𝑓)‘𝑚) ⊆ dom 𝑓) |
27 | | dvnp1 25087 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆 ⊆ ℂ ∧ 𝑓 ∈ (ℂ
↑pm 𝑆)
∧ 𝑚 ∈
ℕ0) → ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) = (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚))) |
28 | 18, 15, 22, 27 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) = (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚))) |
29 | | simprr 770 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ)) |
30 | 28, 29 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚)) ∈ (dom 𝑓–cn→ℂ)) |
31 | | cncff 24054 |
. . . . . . . . . . . . . . . . . 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 6609 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚)) = dom 𝑓) |
34 | | cnex 10953 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℂ
∈ V |
35 | | elpm2g 8615 |
. . . . . . . . . . . . . . . . . . . . 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 231 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ 𝑆)) |
38 | 37 | simprd 496 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom 𝑓 ⊆ 𝑆) |
39 | 26, 38 | sstrd 3936 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom ((𝑆 D𝑛 𝑓)‘𝑚) ⊆ 𝑆) |
40 | 18, 24, 39 | dvbss 25063 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚)) ⊆ dom ((𝑆 D𝑛 𝑓)‘𝑚)) |
41 | 33, 40 | eqsstrrd 3965 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom 𝑓 ⊆ dom ((𝑆 D𝑛 𝑓)‘𝑚)) |
42 | 26, 41 | eqssd 3943 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom ((𝑆 D𝑛 𝑓)‘𝑚) = dom 𝑓) |
43 | 42 | feq2d 6584 |
. . . . . . . . . . . . 13
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (((𝑆 D𝑛 𝑓)‘𝑚):dom ((𝑆 D𝑛 𝑓)‘𝑚)⟶ℂ ↔ ((𝑆 D𝑛 𝑓)‘𝑚):dom 𝑓⟶ℂ)) |
44 | 24, 43 | mpbid 231 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → ((𝑆 D𝑛 𝑓)‘𝑚):dom 𝑓⟶ℂ) |
45 | | dvcn 25083 |
. . . . . . . . . . . 12
⊢ (((𝑆 ⊆ ℂ ∧ ((𝑆 D𝑛 𝑓)‘𝑚):dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ 𝑆) ∧ dom (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚)) = dom 𝑓) → ((𝑆 D𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ)) |
46 | 18, 44, 38, 33, 45 | syl31anc 1372 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → ((𝑆 D𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ)) |
47 | 15, 46 | jca 512 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ))) |
48 | 47 | ex 413 |
. . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → ((𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ)) → (𝑓 ∈ (ℂ ↑pm 𝑆) ∧ ((𝑆 D𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ)))) |
49 | | peano2nn0 12273 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℕ0) |
50 | 21, 49 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → (𝑚 + 1) ∈
ℕ0) |
51 | | elcpn 25096 |
. . . . . . . . . 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 25096 |
. . . . . . . . . 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 3932 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) →
((𝓑C𝑛‘𝑆)‘(𝑚 + 1)) ⊆
((𝓑C𝑛‘𝑆)‘𝑚)) |
57 | | sstr2 3933 |
. . . . . . 7
⊢
(((𝓑C𝑛‘𝑆)‘(𝑚 + 1)) ⊆
((𝓑C𝑛‘𝑆)‘𝑚) →
(((𝓑C𝑛‘𝑆)‘𝑚) ⊆
((𝓑C𝑛‘𝑆)‘𝑀) →
((𝓑C𝑛‘𝑆)‘(𝑚 + 1)) ⊆
((𝓑C𝑛‘𝑆)‘𝑀))) |
58 | 56, 57 | syl 17 |
. . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) →
(((𝓑C𝑛‘𝑆)‘𝑚) ⊆
((𝓑C𝑛‘𝑆)‘𝑀) →
((𝓑C𝑛‘𝑆)‘(𝑚 + 1)) ⊆
((𝓑C𝑛‘𝑆)‘𝑀))) |
59 | 58 | expcom 414 |
. . . . 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 12645 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((𝓑C𝑛‘𝑆)‘𝑁) ⊆
((𝓑C𝑛‘𝑆)‘𝑀))) |
62 | 61 | com12 32 |
. 2
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) → (𝑁 ∈ (ℤ≥‘𝑀) →
((𝓑C𝑛‘𝑆)‘𝑁) ⊆
((𝓑C𝑛‘𝑆)‘𝑀))) |
63 | 62 | 3impia 1116 |
1
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0 ∧ 𝑁
∈ (ℤ≥‘𝑀)) →
((𝓑C𝑛‘𝑆)‘𝑁) ⊆
((𝓑C𝑛‘𝑆)‘𝑀)) |