Step | Hyp | Ref
| Expression |
1 | | ulmss.u |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐴)(⇝𝑢‘𝑆)𝐺) |
2 | | ulmss.z |
. . . . . . . . 9
⊢ 𝑍 =
(ℤ≥‘𝑀) |
3 | 2 | uztrn2 11581 |
. . . . . . . 8
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
4 | | ulmss.t |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ⊆ 𝑆) |
5 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑇 ⊆ 𝑆) |
6 | | ssralv 3629 |
. . . . . . . . . 10
⊢ (𝑇 ⊆ 𝑆 → (∀𝑧 ∈ 𝑆 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 → ∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (∀𝑧 ∈ 𝑆 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 → ∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
8 | | fvres 6117 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑇 → ((𝐴 ↾ 𝑇)‘𝑧) = (𝐴‘𝑧)) |
9 | 8 | ad2antll 761 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇)) → ((𝐴 ↾ 𝑇)‘𝑧) = (𝐴‘𝑧)) |
10 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇)) → 𝑥 ∈ 𝑍) |
11 | | ulmss.a |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐴 ∈ 𝑊) |
12 | 11 | adantrr 749 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇)) → 𝐴 ∈ 𝑊) |
13 | | resexg 5362 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ 𝑊 → (𝐴 ↾ 𝑇) ∈ V) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇)) → (𝐴 ↾ 𝑇) ∈ V) |
15 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇)) = (𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇)) |
16 | 15 | fvmpt2 6200 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑍 ∧ (𝐴 ↾ 𝑇) ∈ V) → ((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥) = (𝐴 ↾ 𝑇)) |
17 | 10, 14, 16 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇)) → ((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥) = (𝐴 ↾ 𝑇)) |
18 | 17 | fveq1d 6105 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇)) → (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥)‘𝑧) = ((𝐴 ↾ 𝑇)‘𝑧)) |
19 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑍 ↦ 𝐴) = (𝑥 ∈ 𝑍 ↦ 𝐴) |
20 | 19 | fvmpt2 6200 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑍 ∧ 𝐴 ∈ 𝑊) → ((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥) = 𝐴) |
21 | 10, 12, 20 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇)) → ((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥) = 𝐴) |
22 | 21 | fveq1d 6105 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇)) → (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥)‘𝑧) = (𝐴‘𝑧)) |
23 | 9, 18, 22 | 3eqtr4d 2654 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇)) → (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥)‘𝑧)) |
24 | 23 | ralrimivva 2954 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ 𝑍 ∀𝑧 ∈ 𝑇 (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥)‘𝑧)) |
25 | | nfv 1830 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘∀𝑧 ∈ 𝑇 (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥)‘𝑧) |
26 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝑇 |
27 | | nffvmpt1 6111 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘) |
28 | | nfcv 2751 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥𝑧 |
29 | 27, 28 | nffv 6110 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) |
30 | | nffvmpt1 6111 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘) |
31 | 30, 28 | nffv 6110 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) |
32 | 29, 31 | nfeq 2762 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) |
33 | 26, 32 | nfral 2929 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥∀𝑧 ∈ 𝑇 (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) |
34 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑘 → ((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥) = ((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)) |
35 | 34 | fveq1d 6105 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑘 → (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧)) |
36 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑘 → ((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥) = ((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)) |
37 | 36 | fveq1d 6105 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑘 → (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧)) |
38 | 35, 37 | eqeq12d 2625 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑘 → ((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥)‘𝑧) ↔ (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧))) |
39 | 38 | ralbidv 2969 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑘 → (∀𝑧 ∈ 𝑇 (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥)‘𝑧) ↔ ∀𝑧 ∈ 𝑇 (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧))) |
40 | 25, 33, 39 | cbvral 3143 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝑍 ∀𝑧 ∈ 𝑇 (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑥)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑥)‘𝑧) ↔ ∀𝑘 ∈ 𝑍 ∀𝑧 ∈ 𝑇 (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧)) |
41 | 24, 40 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 ∀𝑧 ∈ 𝑇 (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧)) |
42 | 41 | r19.21bi 2916 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∀𝑧 ∈ 𝑇 (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧)) |
43 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ ((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) → ((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧)) = ((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) |
44 | 43 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) → (abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) = (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧)))) |
45 | 44 | breq1d 4593 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) → ((abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 ↔ (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
46 | 45 | ralimi 2936 |
. . . . . . . . . 10
⊢
(∀𝑧 ∈
𝑇 (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) → ∀𝑧 ∈ 𝑇 ((abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 ↔ (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
47 | | ralbi 3050 |
. . . . . . . . . 10
⊢
(∀𝑧 ∈
𝑇 ((abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 ↔ (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟) → (∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 ↔ ∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
48 | 42, 46, 47 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 ↔ ∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
49 | 7, 48 | sylibrd 248 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (∀𝑧 ∈ 𝑆 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 → ∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
50 | 3, 49 | sylan2 490 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (∀𝑧 ∈ 𝑆 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 → ∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
51 | 50 | anassrs 678 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (∀𝑧 ∈ 𝑆 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 → ∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
52 | 51 | ralimdva 2945 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 → ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
53 | 52 | reximdva 3000 |
. . . 4
⊢ (𝜑 → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
54 | 53 | ralimdv 2946 |
. . 3
⊢ (𝜑 → (∀𝑟 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟 → ∀𝑟 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
55 | | ulmf 23940 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑍 ↦ 𝐴)(⇝𝑢‘𝑆)𝐺 → ∃𝑚 ∈ ℤ (𝑥 ∈ 𝑍 ↦ 𝐴):(ℤ≥‘𝑚)⟶(ℂ
↑𝑚 𝑆)) |
56 | 1, 55 | syl 17 |
. . . . 5
⊢ (𝜑 → ∃𝑚 ∈ ℤ (𝑥 ∈ 𝑍 ↦ 𝐴):(ℤ≥‘𝑚)⟶(ℂ
↑𝑚 𝑆)) |
57 | | fdm 5964 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑍 ↦ 𝐴):(ℤ≥‘𝑚)⟶(ℂ
↑𝑚 𝑆) → dom (𝑥 ∈ 𝑍 ↦ 𝐴) = (ℤ≥‘𝑚)) |
58 | 19 | dmmptss 5548 |
. . . . . . . 8
⊢ dom
(𝑥 ∈ 𝑍 ↦ 𝐴) ⊆ 𝑍 |
59 | 57, 58 | syl6eqssr 3619 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑍 ↦ 𝐴):(ℤ≥‘𝑚)⟶(ℂ
↑𝑚 𝑆) → (ℤ≥‘𝑚) ⊆ 𝑍) |
60 | | uzid 11578 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
(ℤ≥‘𝑚)) |
61 | 60 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → 𝑚 ∈ (ℤ≥‘𝑚)) |
62 | | ssel 3562 |
. . . . . . . . 9
⊢
((ℤ≥‘𝑚) ⊆ 𝑍 → (𝑚 ∈ (ℤ≥‘𝑚) → 𝑚 ∈ 𝑍)) |
63 | | eluzel2 11568 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
64 | 63, 2 | eleq2s 2706 |
. . . . . . . . 9
⊢ (𝑚 ∈ 𝑍 → 𝑀 ∈ ℤ) |
65 | 62, 64 | syl6 34 |
. . . . . . . 8
⊢
((ℤ≥‘𝑚) ⊆ 𝑍 → (𝑚 ∈ (ℤ≥‘𝑚) → 𝑀 ∈ ℤ)) |
66 | 61, 65 | syl5com 31 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) →
((ℤ≥‘𝑚) ⊆ 𝑍 → 𝑀 ∈ ℤ)) |
67 | 59, 66 | syl5 33 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℤ) → ((𝑥 ∈ 𝑍 ↦ 𝐴):(ℤ≥‘𝑚)⟶(ℂ
↑𝑚 𝑆) → 𝑀 ∈ ℤ)) |
68 | 67 | rexlimdva 3013 |
. . . . 5
⊢ (𝜑 → (∃𝑚 ∈ ℤ (𝑥 ∈ 𝑍 ↦ 𝐴):(ℤ≥‘𝑚)⟶(ℂ
↑𝑚 𝑆) → 𝑀 ∈ ℤ)) |
69 | 56, 68 | mpd 15 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
70 | 11 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝑍 𝐴 ∈ 𝑊) |
71 | 19 | fnmpt 5933 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑍 𝐴 ∈ 𝑊 → (𝑥 ∈ 𝑍 ↦ 𝐴) Fn 𝑍) |
72 | 70, 71 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐴) Fn 𝑍) |
73 | | frn 5966 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑍 ↦ 𝐴):(ℤ≥‘𝑚)⟶(ℂ
↑𝑚 𝑆) → ran (𝑥 ∈ 𝑍 ↦ 𝐴) ⊆ (ℂ
↑𝑚 𝑆)) |
74 | 73 | rexlimivw 3011 |
. . . . . 6
⊢
(∃𝑚 ∈
ℤ (𝑥 ∈ 𝑍 ↦ 𝐴):(ℤ≥‘𝑚)⟶(ℂ
↑𝑚 𝑆) → ran (𝑥 ∈ 𝑍 ↦ 𝐴) ⊆ (ℂ
↑𝑚 𝑆)) |
75 | 56, 74 | syl 17 |
. . . . 5
⊢ (𝜑 → ran (𝑥 ∈ 𝑍 ↦ 𝐴) ⊆ (ℂ
↑𝑚 𝑆)) |
76 | | df-f 5808 |
. . . . 5
⊢ ((𝑥 ∈ 𝑍 ↦ 𝐴):𝑍⟶(ℂ ↑𝑚
𝑆) ↔ ((𝑥 ∈ 𝑍 ↦ 𝐴) Fn 𝑍 ∧ ran (𝑥 ∈ 𝑍 ↦ 𝐴) ⊆ (ℂ
↑𝑚 𝑆))) |
77 | 72, 75, 76 | sylanbrc 695 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ 𝐴):𝑍⟶(ℂ ↑𝑚
𝑆)) |
78 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧)) |
79 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = (𝐺‘𝑧)) |
80 | | ulmcl 23939 |
. . . . 5
⊢ ((𝑥 ∈ 𝑍 ↦ 𝐴)(⇝𝑢‘𝑆)𝐺 → 𝐺:𝑆⟶ℂ) |
81 | 1, 80 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺:𝑆⟶ℂ) |
82 | | ulmscl 23937 |
. . . . 5
⊢ ((𝑥 ∈ 𝑍 ↦ 𝐴)(⇝𝑢‘𝑆)𝐺 → 𝑆 ∈ V) |
83 | 1, 82 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ V) |
84 | 2, 69, 77, 78, 79, 81, 83 | ulm2 23943 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝑍 ↦ 𝐴)(⇝𝑢‘𝑆)𝐺 ↔ ∀𝑟 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘((((𝑥 ∈ 𝑍 ↦ 𝐴)‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
85 | 19 | fmpt 6289 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑍 𝐴 ∈ (ℂ ↑𝑚
𝑆) ↔ (𝑥 ∈ 𝑍 ↦ 𝐴):𝑍⟶(ℂ ↑𝑚
𝑆)) |
86 | 77, 85 | sylibr 223 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝑍 𝐴 ∈ (ℂ ↑𝑚
𝑆)) |
87 | 86 | r19.21bi 2916 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐴 ∈ (ℂ ↑𝑚
𝑆)) |
88 | | elmapi 7765 |
. . . . . . . 8
⊢ (𝐴 ∈ (ℂ
↑𝑚 𝑆) → 𝐴:𝑆⟶ℂ) |
89 | 87, 88 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐴:𝑆⟶ℂ) |
90 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝑇 ⊆ 𝑆) |
91 | 89, 90 | fssresd 5984 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → (𝐴 ↾ 𝑇):𝑇⟶ℂ) |
92 | | cnex 9896 |
. . . . . . 7
⊢ ℂ
∈ V |
93 | 83, 4 | ssexd 4733 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ V) |
94 | 93 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝑇 ∈ V) |
95 | | elmapg 7757 |
. . . . . . 7
⊢ ((ℂ
∈ V ∧ 𝑇 ∈ V)
→ ((𝐴 ↾ 𝑇) ∈ (ℂ
↑𝑚 𝑇) ↔ (𝐴 ↾ 𝑇):𝑇⟶ℂ)) |
96 | 92, 94, 95 | sylancr 694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → ((𝐴 ↾ 𝑇) ∈ (ℂ ↑𝑚
𝑇) ↔ (𝐴 ↾ 𝑇):𝑇⟶ℂ)) |
97 | 91, 96 | mpbird 246 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → (𝐴 ↾ 𝑇) ∈ (ℂ ↑𝑚
𝑇)) |
98 | 97, 15 | fmptd 6292 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇)):𝑍⟶(ℂ ↑𝑚
𝑇)) |
99 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑇)) → (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) = (((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧)) |
100 | | fvres 6117 |
. . . . 5
⊢ (𝑧 ∈ 𝑇 → ((𝐺 ↾ 𝑇)‘𝑧) = (𝐺‘𝑧)) |
101 | 100 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑇) → ((𝐺 ↾ 𝑇)‘𝑧) = (𝐺‘𝑧)) |
102 | 81, 4 | fssresd 5984 |
. . . 4
⊢ (𝜑 → (𝐺 ↾ 𝑇):𝑇⟶ℂ) |
103 | 2, 69, 98, 99, 101, 102, 93 | ulm2 23943 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))(⇝𝑢‘𝑇)(𝐺 ↾ 𝑇) ↔ ∀𝑟 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑇 (abs‘((((𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑟)) |
104 | 54, 84, 103 | 3imtr4d 282 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝑍 ↦ 𝐴)(⇝𝑢‘𝑆)𝐺 → (𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))(⇝𝑢‘𝑇)(𝐺 ↾ 𝑇))) |
105 | 1, 104 | mpd 15 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑍 ↦ (𝐴 ↾ 𝑇))(⇝𝑢‘𝑇)(𝐺 ↾ 𝑇)) |