Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . . 6
⊢ (𝑛 = 𝑀 → ((Cn‘𝑆)‘𝑛) = ((Cn‘𝑆)‘𝑀)) |
2 | 1 | sseq1d 3595 |
. . . . 5
⊢ (𝑛 = 𝑀 → (((Cn‘𝑆)‘𝑛) ⊆ ((Cn‘𝑆)‘𝑀) ↔ ((Cn‘𝑆)‘𝑀) ⊆ ((Cn‘𝑆)‘𝑀))) |
3 | 2 | imbi2d 329 |
. . . 4
⊢ (𝑛 = 𝑀 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((Cn‘𝑆)‘𝑛) ⊆ ((Cn‘𝑆)‘𝑀)) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((Cn‘𝑆)‘𝑀) ⊆ ((Cn‘𝑆)‘𝑀)))) |
4 | | fveq2 6103 |
. . . . . 6
⊢ (𝑛 = 𝑚 → ((Cn‘𝑆)‘𝑛) = ((Cn‘𝑆)‘𝑚)) |
5 | 4 | sseq1d 3595 |
. . . . 5
⊢ (𝑛 = 𝑚 → (((Cn‘𝑆)‘𝑛) ⊆ ((Cn‘𝑆)‘𝑀) ↔ ((Cn‘𝑆)‘𝑚) ⊆ ((Cn‘𝑆)‘𝑀))) |
6 | 5 | imbi2d 329 |
. . . 4
⊢ (𝑛 = 𝑚 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((Cn‘𝑆)‘𝑛) ⊆ ((Cn‘𝑆)‘𝑀)) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((Cn‘𝑆)‘𝑚) ⊆ ((Cn‘𝑆)‘𝑀)))) |
7 | | fveq2 6103 |
. . . . . 6
⊢ (𝑛 = (𝑚 + 1) →
((Cn‘𝑆)‘𝑛) = ((Cn‘𝑆)‘(𝑚 + 1))) |
8 | 7 | sseq1d 3595 |
. . . . 5
⊢ (𝑛 = (𝑚 + 1) →
(((Cn‘𝑆)‘𝑛) ⊆ ((Cn‘𝑆)‘𝑀) ↔ ((Cn‘𝑆)‘(𝑚 + 1)) ⊆
((Cn‘𝑆)‘𝑀))) |
9 | 8 | imbi2d 329 |
. . . 4
⊢ (𝑛 = (𝑚 + 1) → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((Cn‘𝑆)‘𝑛) ⊆ ((Cn‘𝑆)‘𝑀)) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((Cn‘𝑆)‘(𝑚 + 1)) ⊆
((Cn‘𝑆)‘𝑀)))) |
10 | | fveq2 6103 |
. . . . . 6
⊢ (𝑛 = 𝑁 → ((Cn‘𝑆)‘𝑛) = ((Cn‘𝑆)‘𝑁)) |
11 | 10 | sseq1d 3595 |
. . . . 5
⊢ (𝑛 = 𝑁 → (((Cn‘𝑆)‘𝑛) ⊆ ((Cn‘𝑆)‘𝑀) ↔ ((Cn‘𝑆)‘𝑁) ⊆ ((Cn‘𝑆)‘𝑀))) |
12 | 11 | imbi2d 329 |
. . . 4
⊢ (𝑛 = 𝑁 → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((Cn‘𝑆)‘𝑛) ⊆ ((Cn‘𝑆)‘𝑀)) ↔ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((Cn‘𝑆)‘𝑁) ⊆ ((Cn‘𝑆)‘𝑀)))) |
13 | | ssid 3587 |
. . . . 5
⊢
((Cn‘𝑆)‘𝑀) ⊆ ((Cn‘𝑆)‘𝑀) |
14 | 13 | 2a1i 12 |
. . . 4
⊢ (𝑀 ∈ ℤ → ((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) → ((Cn‘𝑆)‘𝑀) ⊆ ((Cn‘𝑆)‘𝑀))) |
15 | | simprl 790 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → 𝑓 ∈ (ℂ ↑pm
𝑆)) |
16 | | recnprss 23474 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
17 | 16 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → 𝑆 ⊆ ℂ) |
18 | 17 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → 𝑆 ⊆ ℂ) |
19 | | simplll 794 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → 𝑆 ∈ {ℝ, ℂ}) |
20 | | eluznn0 11633 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℕ0
∧ 𝑚 ∈
(ℤ≥‘𝑀)) → 𝑚 ∈ ℕ0) |
21 | 20 | adantll 746 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → 𝑚 ∈ ℕ0) |
22 | 21 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → 𝑚 ∈ ℕ0) |
23 | | dvnf 23496 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝑓 ∈ (ℂ
↑pm 𝑆) ∧ 𝑚 ∈ ℕ0) → ((𝑆 D𝑛 𝑓)‘𝑚):dom ((𝑆 D𝑛 𝑓)‘𝑚)⟶ℂ) |
24 | 19, 15, 22, 23 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → ((𝑆 D𝑛 𝑓)‘𝑚):dom ((𝑆 D𝑛 𝑓)‘𝑚)⟶ℂ) |
25 | | dvnbss 23497 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝑓 ∈ (ℂ
↑pm 𝑆) ∧ 𝑚 ∈ ℕ0) → dom
((𝑆 D𝑛
𝑓)‘𝑚) ⊆ dom 𝑓) |
26 | 19, 15, 22, 25 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom ((𝑆 D𝑛 𝑓)‘𝑚) ⊆ dom 𝑓) |
27 | | dvnp1 23494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆 ⊆ ℂ ∧ 𝑓 ∈ (ℂ
↑pm 𝑆) ∧ 𝑚 ∈ ℕ0) → ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) = (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚))) |
28 | 18, 15, 22, 27 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) = (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚))) |
29 | | simprr 792 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ)) |
30 | 28, 29 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚)) ∈ (dom 𝑓–cn→ℂ)) |
31 | | cncff 22504 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚)) ∈ (dom 𝑓–cn→ℂ) → (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚)):dom 𝑓⟶ℂ) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚)):dom 𝑓⟶ℂ) |
33 | | fdm 5964 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚)):dom 𝑓⟶ℂ → dom (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚)) = dom 𝑓) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚)) = dom 𝑓) |
35 | | cnex 9896 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℂ
∈ V |
36 | | elpm2g 7760 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((ℂ
∈ V ∧ 𝑆 ∈
{ℝ, ℂ}) → (𝑓 ∈ (ℂ ↑pm
𝑆) ↔ (𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ 𝑆))) |
37 | 35, 19, 36 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (𝑓 ∈ (ℂ ↑pm
𝑆) ↔ (𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ 𝑆))) |
38 | 15, 37 | mpbid 221 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ 𝑆)) |
39 | 38 | simprd 478 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom 𝑓 ⊆ 𝑆) |
40 | 26, 39 | sstrd 3578 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom ((𝑆 D𝑛 𝑓)‘𝑚) ⊆ 𝑆) |
41 | 18, 24, 40 | dvbss 23471 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚)) ⊆ dom ((𝑆 D𝑛 𝑓)‘𝑚)) |
42 | 34, 41 | eqsstr3d 3603 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom 𝑓 ⊆ dom ((𝑆 D𝑛 𝑓)‘𝑚)) |
43 | 26, 42 | eqssd 3585 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → dom ((𝑆 D𝑛 𝑓)‘𝑚) = dom 𝑓) |
44 | 43 | feq2d 5944 |
. . . . . . . . . . . . 13
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (((𝑆 D𝑛 𝑓)‘𝑚):dom ((𝑆 D𝑛 𝑓)‘𝑚)⟶ℂ ↔ ((𝑆 D𝑛 𝑓)‘𝑚):dom 𝑓⟶ℂ)) |
45 | 24, 44 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → ((𝑆 D𝑛 𝑓)‘𝑚):dom 𝑓⟶ℂ) |
46 | | dvcn 23490 |
. . . . . . . . . . . 12
⊢ (((𝑆 ⊆ ℂ ∧ ((𝑆 D𝑛 𝑓)‘𝑚):dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ 𝑆) ∧ dom (𝑆 D ((𝑆 D𝑛 𝑓)‘𝑚)) = dom 𝑓) → ((𝑆 D𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ)) |
47 | 18, 45, 39, 34, 46 | syl31anc 1321 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → ((𝑆 D𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ)) |
48 | 15, 47 | jca 553 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) ∧ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ))) → (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ))) |
49 | 48 | ex 449 |
. . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → ((𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ)) → (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ)))) |
50 | | peano2nn0 11210 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℕ0) |
51 | 21, 50 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → (𝑚 + 1) ∈
ℕ0) |
52 | | elcpn 23503 |
. . . . . . . . . 10
⊢ ((𝑆 ⊆ ℂ ∧ (𝑚 + 1) ∈
ℕ0) → (𝑓 ∈ ((Cn‘𝑆)‘(𝑚 + 1)) ↔ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ)))) |
53 | 17, 51, 52 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → (𝑓 ∈ ((Cn‘𝑆)‘(𝑚 + 1)) ↔ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘(𝑚 + 1)) ∈ (dom 𝑓–cn→ℂ)))) |
54 | | elcpn 23503 |
. . . . . . . . . 10
⊢ ((𝑆 ⊆ ℂ ∧ 𝑚 ∈ ℕ0)
→ (𝑓 ∈
((Cn‘𝑆)‘𝑚) ↔ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ)))) |
55 | 17, 21, 54 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → (𝑓 ∈ ((Cn‘𝑆)‘𝑚) ↔ (𝑓 ∈ (ℂ ↑pm
𝑆) ∧ ((𝑆 D𝑛 𝑓)‘𝑚) ∈ (dom 𝑓–cn→ℂ)))) |
56 | 49, 53, 55 | 3imtr4d 282 |
. . . . . . . 8
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → (𝑓 ∈ ((Cn‘𝑆)‘(𝑚 + 1)) → 𝑓 ∈ ((Cn‘𝑆)‘𝑚))) |
57 | 56 | ssrdv 3574 |
. . . . . . 7
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) →
((Cn‘𝑆)‘(𝑚 + 1)) ⊆
((Cn‘𝑆)‘𝑚)) |
58 | | sstr2 3575 |
. . . . . . 7
⊢
(((Cn‘𝑆)‘(𝑚 + 1)) ⊆
((Cn‘𝑆)‘𝑚) → (((Cn‘𝑆)‘𝑚) ⊆ ((Cn‘𝑆)‘𝑀) → ((Cn‘𝑆)‘(𝑚 + 1)) ⊆
((Cn‘𝑆)‘𝑀))) |
59 | 57, 58 | syl 17 |
. . . . . 6
⊢ (((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) →
(((Cn‘𝑆)‘𝑚) ⊆ ((Cn‘𝑆)‘𝑀) → ((Cn‘𝑆)‘(𝑚 + 1)) ⊆
((Cn‘𝑆)‘𝑀))) |
60 | 59 | expcom 450 |
. . . . 5
⊢ (𝑚 ∈
(ℤ≥‘𝑀) → ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ (((Cn‘𝑆)‘𝑚) ⊆ ((Cn‘𝑆)‘𝑀) → ((Cn‘𝑆)‘(𝑚 + 1)) ⊆
((Cn‘𝑆)‘𝑀)))) |
61 | 60 | a2d 29 |
. . . 4
⊢ (𝑚 ∈
(ℤ≥‘𝑀) → (((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((Cn‘𝑆)‘𝑚) ⊆ ((Cn‘𝑆)‘𝑀)) → ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((Cn‘𝑆)‘(𝑚 + 1)) ⊆
((Cn‘𝑆)‘𝑀)))) |
62 | 3, 6, 9, 12, 14, 61 | uzind4 11622 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → ((𝑆 ∈ {ℝ, ℂ} ∧ 𝑀 ∈ ℕ0)
→ ((Cn‘𝑆)‘𝑁) ⊆ ((Cn‘𝑆)‘𝑀))) |
63 | 62 | com12 32 |
. 2
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0) → (𝑁 ∈ (ℤ≥‘𝑀) →
((Cn‘𝑆)‘𝑁) ⊆ ((Cn‘𝑆)‘𝑀))) |
64 | 63 | 3impia 1253 |
1
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝑀 ∈
ℕ0 ∧ 𝑁
∈ (ℤ≥‘𝑀)) → ((Cn‘𝑆)‘𝑁) ⊆ ((Cn‘𝑆)‘𝑀)) |