Step | Hyp | Ref
| Expression |
1 | | eldmg 5319 |
. . . 4
⊢ (𝐹 ∈ dom
(⇝𝑢‘𝑆) → (𝐹 ∈ dom
(⇝𝑢‘𝑆) ↔ ∃𝑔 𝐹(⇝𝑢‘𝑆)𝑔)) |
2 | 1 | ibi 256 |
. . 3
⊢ (𝐹 ∈ dom
(⇝𝑢‘𝑆) → ∃𝑔 𝐹(⇝𝑢‘𝑆)𝑔) |
3 | | ulmcau.z |
. . . . . . . 8
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | | ulmcau.m |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
5 | 4 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → 𝑀 ∈
ℤ) |
6 | | ulmcau.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚
𝑆)) |
7 | 6 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → 𝐹:𝑍⟶(ℂ ↑𝑚
𝑆)) |
8 | | eqidd 2623 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑘)‘𝑧) = ((𝐹‘𝑘)‘𝑧)) |
9 | | eqidd 2623 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑧 ∈ 𝑆) → (𝑔‘𝑧) = (𝑔‘𝑧)) |
10 | | simplr 792 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → 𝐹(⇝𝑢‘𝑆)𝑔) |
11 | | rphalfcl 11858 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) ∈
ℝ+) |
12 | 11 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈
ℝ+) |
13 | 3, 5, 7, 8, 9, 10,
12 | ulmi 24140 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2)) |
14 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ 𝑍) |
15 | 14, 3 | syl6eleq 2711 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ (ℤ≥‘𝑀)) |
16 | | eluzelz 11697 |
. . . . . . . . . 10
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑗 ∈ ℤ) |
17 | | uzid 11702 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℤ → 𝑗 ∈
(ℤ≥‘𝑗)) |
18 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑗 → (𝐹‘𝑘) = (𝐹‘𝑗)) |
19 | 18 | fveq1d 6193 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑗 → ((𝐹‘𝑘)‘𝑧) = ((𝐹‘𝑗)‘𝑧)) |
20 | 19 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑗 → (((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧)) = (((𝐹‘𝑗)‘𝑧) − (𝑔‘𝑧))) |
21 | 20 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑗 → (abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) = (abs‘(((𝐹‘𝑗)‘𝑧) − (𝑔‘𝑧)))) |
22 | 21 | breq1d 4663 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → ((abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) ↔ (abs‘(((𝐹‘𝑗)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2))) |
23 | 22 | ralbidv 2986 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → (∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) ↔ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑗)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2))) |
24 | 23 | rspcv 3305 |
. . . . . . . . . 10
⊢ (𝑗 ∈
(ℤ≥‘𝑗) → (∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) → ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑗)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2))) |
25 | 15, 16, 17, 24 | 4syl 19 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) → ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑗)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2))) |
26 | | r19.26 3064 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧 ∈
𝑆 ((abs‘(((𝐹‘𝑗)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2)) ↔ (∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑗)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2))) |
27 | 7 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) ∈ (ℂ ↑𝑚
𝑆)) |
28 | 27 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑗) ∈ (ℂ ↑𝑚
𝑆)) |
29 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹‘𝑗) ∈ (ℂ ↑𝑚
𝑆) → (𝐹‘𝑗):𝑆⟶ℂ) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑗):𝑆⟶ℂ) |
31 | 30 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → ((𝐹‘𝑗)‘𝑧) ∈ ℂ) |
32 | | ulmcl 24135 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹(⇝𝑢‘𝑆)𝑔 → 𝑔:𝑆⟶ℂ) |
33 | 32 | ad4antlr 769 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑔:𝑆⟶ℂ) |
34 | 33 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → (𝑔‘𝑧) ∈ ℂ) |
35 | 31, 34 | abssubd 14192 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → (abs‘(((𝐹‘𝑗)‘𝑧) − (𝑔‘𝑧))) = (abs‘((𝑔‘𝑧) − ((𝐹‘𝑗)‘𝑧)))) |
36 | 35 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → ((abs‘(((𝐹‘𝑗)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) ↔ (abs‘((𝑔‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < (𝑥 / 2))) |
37 | 36 | biimpd 219 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → ((abs‘(((𝐹‘𝑗)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) → (abs‘((𝑔‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < (𝑥 / 2))) |
38 | 3 | uztrn2 11705 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
39 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹:𝑍⟶(ℂ ↑𝑚
𝑆) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ (ℂ ↑𝑚
𝑆)) |
40 | 7, 38, 39 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (𝐹‘𝑘) ∈ (ℂ ↑𝑚
𝑆)) |
41 | 40 | anassrs 680 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈ (ℂ ↑𝑚
𝑆)) |
42 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹‘𝑘) ∈ (ℂ ↑𝑚
𝑆) → (𝐹‘𝑘):𝑆⟶ℂ) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘):𝑆⟶ℂ) |
44 | 43 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → ((𝐹‘𝑘)‘𝑧) ∈ ℂ) |
45 | | rpre 11839 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
46 | 45 | ad4antlr 769 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → 𝑥 ∈ ℝ) |
47 | | abs3lem 14078 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝐹‘𝑘)‘𝑧) ∈ ℂ ∧ ((𝐹‘𝑗)‘𝑧) ∈ ℂ) ∧ ((𝑔‘𝑧) ∈ ℂ ∧ 𝑥 ∈ ℝ)) →
(((abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) ∧ (abs‘((𝑔‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < (𝑥 / 2)) → (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥)) |
48 | 44, 31, 34, 46, 47 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → (((abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) ∧ (abs‘((𝑔‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < (𝑥 / 2)) → (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥)) |
49 | 37, 48 | sylan2d 499 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → (((abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹‘𝑗)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2)) → (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥)) |
50 | 49 | ancomsd 470 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑧 ∈ 𝑆) → (((abs‘(((𝐹‘𝑗)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2)) → (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥)) |
51 | 50 | ralimdva 2962 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (∀𝑧 ∈ 𝑆 ((abs‘(((𝐹‘𝑗)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2)) → ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥)) |
52 | 26, 51 | syl5bir 233 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑗)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2)) → ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥)) |
53 | 52 | expdimp 453 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑗)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2)) → (∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) → ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥)) |
54 | 53 | an32s 846 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑗)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2)) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) → ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥)) |
55 | 54 | ralimdva 2962 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑗)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2)) → (∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥)) |
56 | 55 | ex 450 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → (∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑗)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) → (∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥))) |
57 | 56 | com23 86 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) → (∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑗)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥))) |
58 | 25, 57 | mpdd 43 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥)) |
59 | 58 | reximdva 3017 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) →
(∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝑔‘𝑧))) < (𝑥 / 2) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥)) |
60 | 13, 59 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) |
61 | 60 | ralrimiva 2966 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹(⇝𝑢‘𝑆)𝑔) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) |
62 | 61 | ex 450 |
. . . 4
⊢ (𝜑 → (𝐹(⇝𝑢‘𝑆)𝑔 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥)) |
63 | 62 | exlimdv 1861 |
. . 3
⊢ (𝜑 → (∃𝑔 𝐹(⇝𝑢‘𝑆)𝑔 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥)) |
64 | 2, 63 | syl5 34 |
. 2
⊢ (𝜑 → (𝐹 ∈ dom
(⇝𝑢‘𝑆) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥)) |
65 | | ulmrel 24132 |
. . . 4
⊢ Rel
(⇝𝑢‘𝑆) |
66 | | ulmcau.s |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
67 | 3, 4, 66, 6 | ulmcaulem 24148 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < 𝑥)) |
68 | 67 | biimpa 501 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < 𝑥) |
69 | | rphalfcl 11858 |
. . . . . . . 8
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) ∈
ℝ+) |
70 | | breq2 4657 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑟 / 2) → ((abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < 𝑥 ↔ (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < (𝑟 / 2))) |
71 | 70 | ralbidv 2986 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑟 / 2) → (∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < 𝑥 ↔ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < (𝑟 / 2))) |
72 | 71 | 2ralbidv 2989 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑟 / 2) → (∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < (𝑟 / 2))) |
73 | 72 | rexbidv 3052 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑟 / 2) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < 𝑥 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < (𝑟 / 2))) |
74 | | ralcom 3098 |
. . . . . . . . . . . . . 14
⊢
(∀𝑤 ∈
𝑆 ∀𝑚 ∈
(ℤ≥‘𝑞)(abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑚 ∈ (ℤ≥‘𝑞)∀𝑤 ∈ 𝑆 (abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2)) |
75 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = 𝑘 → (ℤ≥‘𝑞) =
(ℤ≥‘𝑘)) |
76 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑧 → ((𝐹‘𝑞)‘𝑤) = ((𝐹‘𝑞)‘𝑧)) |
77 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑧 → ((𝐹‘𝑚)‘𝑤) = ((𝐹‘𝑚)‘𝑧)) |
78 | 76, 77 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑧 → (((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤)) = (((𝐹‘𝑞)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) |
79 | 78 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑧 → (abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) = (abs‘(((𝐹‘𝑞)‘𝑧) − ((𝐹‘𝑚)‘𝑧)))) |
80 | 79 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑧 → ((abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) ↔ (abs‘(((𝐹‘𝑞)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < (𝑟 / 2))) |
81 | 80 | cbvralv 3171 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑤 ∈
𝑆 (abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑞)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < (𝑟 / 2)) |
82 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑞 = 𝑘 → (𝐹‘𝑞) = (𝐹‘𝑘)) |
83 | 82 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 = 𝑘 → ((𝐹‘𝑞)‘𝑧) = ((𝐹‘𝑘)‘𝑧)) |
84 | 83 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑞 = 𝑘 → (((𝐹‘𝑞)‘𝑧) − ((𝐹‘𝑚)‘𝑧)) = (((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) |
85 | 84 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑞 = 𝑘 → (abs‘(((𝐹‘𝑞)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) = (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧)))) |
86 | 85 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 = 𝑘 → ((abs‘(((𝐹‘𝑞)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < (𝑟 / 2) ↔ (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < (𝑟 / 2))) |
87 | 86 | ralbidv 2986 |
. . . . . . . . . . . . . . . 16
⊢ (𝑞 = 𝑘 → (∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑞)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < (𝑟 / 2) ↔ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < (𝑟 / 2))) |
88 | 81, 87 | syl5bb 272 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = 𝑘 → (∀𝑤 ∈ 𝑆 (abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < (𝑟 / 2))) |
89 | 75, 88 | raleqbidv 3152 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 𝑘 → (∀𝑚 ∈ (ℤ≥‘𝑞)∀𝑤 ∈ 𝑆 (abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < (𝑟 / 2))) |
90 | 74, 89 | syl5bb 272 |
. . . . . . . . . . . . 13
⊢ (𝑞 = 𝑘 → (∀𝑤 ∈ 𝑆 ∀𝑚 ∈ (ℤ≥‘𝑞)(abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < (𝑟 / 2))) |
91 | 90 | cbvralv 3171 |
. . . . . . . . . . . 12
⊢
(∀𝑞 ∈
(ℤ≥‘𝑝)∀𝑤 ∈ 𝑆 ∀𝑚 ∈ (ℤ≥‘𝑞)(abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑘 ∈ (ℤ≥‘𝑝)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < (𝑟 / 2)) |
92 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑗 → (ℤ≥‘𝑝) =
(ℤ≥‘𝑗)) |
93 | 92 | raleqdv 3144 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑗 → (∀𝑘 ∈ (ℤ≥‘𝑝)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < (𝑟 / 2) ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < (𝑟 / 2))) |
94 | 91, 93 | syl5bb 272 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑗 → (∀𝑞 ∈ (ℤ≥‘𝑝)∀𝑤 ∈ 𝑆 ∀𝑚 ∈ (ℤ≥‘𝑞)(abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < (𝑟 / 2))) |
95 | 94 | cbvrexv 3172 |
. . . . . . . . . 10
⊢
(∃𝑝 ∈
𝑍 ∀𝑞 ∈
(ℤ≥‘𝑝)∀𝑤 ∈ 𝑆 ∀𝑚 ∈ (ℤ≥‘𝑞)(abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < (𝑟 / 2)) |
96 | 73, 95 | syl6bbr 278 |
. . . . . . . . 9
⊢ (𝑥 = (𝑟 / 2) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < 𝑥 ↔ ∃𝑝 ∈ 𝑍 ∀𝑞 ∈ (ℤ≥‘𝑝)∀𝑤 ∈ 𝑆 ∀𝑚 ∈ (ℤ≥‘𝑞)(abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2))) |
97 | 96 | rspccva 3308 |
. . . . . . . 8
⊢
((∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑚 ∈ (ℤ≥‘𝑘)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑚)‘𝑧))) < 𝑥 ∧ (𝑟 / 2) ∈ ℝ+) →
∃𝑝 ∈ 𝑍 ∀𝑞 ∈ (ℤ≥‘𝑝)∀𝑤 ∈ 𝑆 ∀𝑚 ∈ (ℤ≥‘𝑞)(abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2)) |
98 | 68, 69, 97 | syl2an 494 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) →
∃𝑝 ∈ 𝑍 ∀𝑞 ∈ (ℤ≥‘𝑝)∀𝑤 ∈ 𝑆 ∀𝑚 ∈ (ℤ≥‘𝑞)(abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2)) |
99 | 3 | uztrn2 11705 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ 𝑍 ∧ 𝑞 ∈ (ℤ≥‘𝑝)) → 𝑞 ∈ 𝑍) |
100 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘𝑞) = (ℤ≥‘𝑞) |
101 | | eluzelz 11697 |
. . . . . . . . . . . . . . . 16
⊢ (𝑞 ∈
(ℤ≥‘𝑀) → 𝑞 ∈ ℤ) |
102 | 101, 3 | eleq2s 2719 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 ∈ 𝑍 → 𝑞 ∈ ℤ) |
103 | 102 | ad2antlr 763 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) → 𝑞 ∈ ℤ) |
104 | 69 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈
ℝ+) |
105 | 104 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) → (𝑟 / 2) ∈
ℝ+) |
106 | | simplr 792 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) → 𝑞 ∈ 𝑍) |
107 | 3 | uztrn2 11705 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ 𝑍 ∧ 𝑚 ∈ (ℤ≥‘𝑞)) → 𝑚 ∈ 𝑍) |
108 | 106, 107 | sylan 488 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) ∧ 𝑚 ∈ (ℤ≥‘𝑞)) → 𝑚 ∈ 𝑍) |
109 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚)) |
110 | 109 | fveq1d 6193 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → ((𝐹‘𝑛)‘𝑤) = ((𝐹‘𝑚)‘𝑤)) |
111 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤)) = (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤)) |
112 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑚)‘𝑤) ∈ V |
113 | 110, 111,
112 | fvmpt 6282 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ 𝑍 → ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))‘𝑚) = ((𝐹‘𝑚)‘𝑤)) |
114 | 108, 113 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) ∧ 𝑚 ∈ (ℤ≥‘𝑞)) → ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))‘𝑚) = ((𝐹‘𝑚)‘𝑤)) |
115 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) → 𝐹:𝑍⟶(ℂ ↑𝑚
𝑆)) |
116 | 115 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ (ℂ ↑𝑚
𝑆)) |
117 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹‘𝑛) ∈ (ℂ ↑𝑚
𝑆) → (𝐹‘𝑛):𝑆⟶ℂ) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):𝑆⟶ℂ) |
119 | 118 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑛 ∈ 𝑍) ∧ 𝑦 ∈ 𝑆) → ((𝐹‘𝑛)‘𝑦) ∈ ℂ) |
120 | 119 | an32s 846 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑦 ∈ 𝑆) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑦) ∈ ℂ) |
121 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)) = (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)) |
122 | 120, 121 | fmptd 6385 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑦 ∈ 𝑆) → (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)):𝑍⟶ℂ) |
123 | 122 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑦 ∈ 𝑆) ∧ 𝑞 ∈ 𝑍) → ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑞) ∈ ℂ) |
124 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 = 𝑦 → ((𝐹‘𝑘)‘𝑧) = ((𝐹‘𝑘)‘𝑦)) |
125 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 = 𝑦 → ((𝐹‘𝑗)‘𝑧) = ((𝐹‘𝑗)‘𝑦)) |
126 | 124, 125 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 = 𝑦 → (((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧)) = (((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) |
127 | 126 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 = 𝑦 → (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) = (abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦)))) |
128 | 127 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 = 𝑦 → ((abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥 ↔ (abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) < 𝑥)) |
129 | 128 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ 𝑆 → (∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥 → (abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) < 𝑥)) |
130 | 129 | ralimdv 2963 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ 𝑆 → (∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥 → ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) < 𝑥)) |
131 | 130 | reximdv 3016 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ 𝑆 → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) < 𝑥)) |
132 | 131 | ralimdv 2963 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ 𝑆 → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) < 𝑥)) |
133 | 132 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥 ∧ 𝑦 ∈ 𝑆) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) < 𝑥) |
134 | 133 | adantll 750 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑦 ∈ 𝑆) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) < 𝑥) |
135 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑞 = 𝑘 → ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑞) = ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘)) |
136 | 135 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑞 = 𝑘 → (((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑞) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑝)) = (((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑝))) |
137 | 136 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑞 = 𝑘 → (abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑞) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑝))) = (abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑝)))) |
138 | 137 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑞 = 𝑘 → ((abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑞) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ (abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑝))) < 𝑟)) |
139 | 138 | cbvralv 3171 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∀𝑞 ∈
(ℤ≥‘𝑝)(abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑞) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∀𝑘 ∈ (ℤ≥‘𝑝)(abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑝))) < 𝑟) |
140 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑝 = 𝑗 → ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑝) = ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑗)) |
141 | 140 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑝 = 𝑗 → (((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑝)) = (((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑗))) |
142 | 141 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑝 = 𝑗 → (abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑝))) = (abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑗)))) |
143 | 142 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑝 = 𝑗 → ((abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ (abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑗))) < 𝑟)) |
144 | 92, 143 | raleqbidv 3152 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑝 = 𝑗 → (∀𝑘 ∈ (ℤ≥‘𝑝)(abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑗))) < 𝑟)) |
145 | 139, 144 | syl5bb 272 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑝 = 𝑗 → (∀𝑞 ∈ (ℤ≥‘𝑝)(abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑞) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑗))) < 𝑟)) |
146 | 145 | cbvrexv 3172 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∃𝑝 ∈
𝑍 ∀𝑞 ∈
(ℤ≥‘𝑝)(abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑞) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑗))) < 𝑟) |
147 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) |
148 | 147 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛)‘𝑦) = ((𝐹‘𝑘)‘𝑦)) |
149 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐹‘𝑘)‘𝑦) ∈ V |
150 | 148, 121,
149 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑘 ∈ 𝑍 → ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) = ((𝐹‘𝑘)‘𝑦)) |
151 | 38, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) = ((𝐹‘𝑘)‘𝑦)) |
152 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑛 = 𝑗 → (𝐹‘𝑛) = (𝐹‘𝑗)) |
153 | 152 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑛 = 𝑗 → ((𝐹‘𝑛)‘𝑦) = ((𝐹‘𝑗)‘𝑦)) |
154 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐹‘𝑗)‘𝑦) ∈ V |
155 | 153, 121,
154 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 ∈ 𝑍 → ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑗) = ((𝐹‘𝑗)‘𝑦)) |
156 | 155 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑗) = ((𝐹‘𝑗)‘𝑦)) |
157 | 151, 156 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑗)) = (((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) |
158 | 157 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑗))) = (abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦)))) |
159 | 158 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑗))) < 𝑟 ↔ (abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) < 𝑟)) |
160 | 159 | ralbidva 2985 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ 𝑍 → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑗))) < 𝑟 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) < 𝑟)) |
161 | 160 | rexbiia 3040 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑘) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑗))) < 𝑟 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) < 𝑟) |
162 | 146, 161 | bitri 264 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∃𝑝 ∈
𝑍 ∀𝑞 ∈
(ℤ≥‘𝑝)(abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑞) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) < 𝑟) |
163 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑟 = 𝑥 → ((abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) < 𝑟 ↔ (abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) < 𝑥)) |
164 | 163 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑟 = 𝑥 → (∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) < 𝑟 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) < 𝑥)) |
165 | 164 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑟 = 𝑥 → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) < 𝑟 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) < 𝑥)) |
166 | 162, 165 | syl5bb 272 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 = 𝑥 → (∃𝑝 ∈ 𝑍 ∀𝑞 ∈ (ℤ≥‘𝑝)(abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑞) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) < 𝑥)) |
167 | 166 | cbvralv 3171 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑟 ∈
ℝ+ ∃𝑝 ∈ 𝑍 ∀𝑞 ∈ (ℤ≥‘𝑝)(abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑞) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑦) − ((𝐹‘𝑗)‘𝑦))) < 𝑥) |
168 | 134, 167 | sylibr 224 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑦 ∈ 𝑆) → ∀𝑟 ∈ ℝ+ ∃𝑝 ∈ 𝑍 ∀𝑞 ∈ (ℤ≥‘𝑝)(abs‘(((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑞) − ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))‘𝑝))) < 𝑟) |
169 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(ℤ≥‘𝑀) ∈ V |
170 | 3, 169 | eqeltri 2697 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑍 ∈ V |
171 | 170 | mptex 6486 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)) ∈ V |
172 | 171 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑦 ∈ 𝑆) → (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)) ∈ V) |
173 | 3, 123, 168, 172 | caucvg 14409 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑦 ∈ 𝑆) → (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)) ∈ dom ⇝ ) |
174 | 173 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) → ∀𝑦 ∈ 𝑆 (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)) ∈ dom ⇝ ) |
175 | 174 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) → ∀𝑦 ∈ 𝑆 (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)) ∈ dom ⇝ ) |
176 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑤 → ((𝐹‘𝑛)‘𝑦) = ((𝐹‘𝑛)‘𝑤)) |
177 | 176 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑤 → (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)) = (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))) |
178 | 177 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑤 → ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)) ∈ dom ⇝ ↔ (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤)) ∈ dom ⇝ )) |
179 | 178 | rspccva 3308 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑦 ∈
𝑆 (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)) ∈ dom ⇝ ∧ 𝑤 ∈ 𝑆) → (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤)) ∈ dom ⇝ ) |
180 | 175, 179 | sylan 488 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) → (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤)) ∈ dom ⇝ ) |
181 | | climdm 14285 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤)) ∈ dom ⇝ ↔ (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤)) ⇝ ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤)))) |
182 | 180, 181 | sylib 208 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) → (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤)) ⇝ ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤)))) |
183 | 100, 103,
105, 114, 182 | climi2 14242 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) → ∃𝑣 ∈ (ℤ≥‘𝑞)∀𝑚 ∈ (ℤ≥‘𝑣)(abs‘(((𝐹‘𝑚)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < (𝑟 / 2)) |
184 | 100 | r19.29uz 14090 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑚 ∈
(ℤ≥‘𝑞)(abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) ∧ ∃𝑣 ∈ (ℤ≥‘𝑞)∀𝑚 ∈ (ℤ≥‘𝑣)(abs‘(((𝐹‘𝑚)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < (𝑟 / 2)) → ∃𝑣 ∈ (ℤ≥‘𝑞)∀𝑚 ∈ (ℤ≥‘𝑣)((abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹‘𝑚)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < (𝑟 / 2))) |
185 | 100 | r19.2uz 14091 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑣 ∈
(ℤ≥‘𝑞)∀𝑚 ∈ (ℤ≥‘𝑣)((abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹‘𝑚)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < (𝑟 / 2)) → ∃𝑚 ∈ (ℤ≥‘𝑞)((abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹‘𝑚)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < (𝑟 / 2))) |
186 | 184, 185 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((∀𝑚 ∈
(ℤ≥‘𝑞)(abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) ∧ ∃𝑣 ∈ (ℤ≥‘𝑞)∀𝑚 ∈ (ℤ≥‘𝑣)(abs‘(((𝐹‘𝑚)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < (𝑟 / 2)) → ∃𝑚 ∈ (ℤ≥‘𝑞)((abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹‘𝑚)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < (𝑟 / 2))) |
187 | 6 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) → 𝐹:𝑍⟶(ℂ ↑𝑚
𝑆)) |
188 | 187 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) → (𝐹‘𝑞) ∈ (ℂ ↑𝑚
𝑆)) |
189 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑞) ∈ (ℂ ↑𝑚
𝑆) → (𝐹‘𝑞):𝑆⟶ℂ) |
190 | 188, 189 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) → (𝐹‘𝑞):𝑆⟶ℂ) |
191 | 190 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) → ((𝐹‘𝑞)‘𝑤) ∈ ℂ) |
192 | 191 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) ∧ 𝑚 ∈ (ℤ≥‘𝑞)) → ((𝐹‘𝑞)‘𝑤) ∈ ℂ) |
193 | | climcl 14230 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤)) ⇝ ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))) → ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))) ∈ ℂ) |
194 | 182, 193 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) → ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))) ∈ ℂ) |
195 | 194 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) ∧ 𝑚 ∈ (ℤ≥‘𝑞)) → ( ⇝
‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))) ∈ ℂ) |
196 | 6 | ad5antr 770 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) ∧ 𝑚 ∈ (ℤ≥‘𝑞)) → 𝐹:𝑍⟶(ℂ ↑𝑚
𝑆)) |
197 | 196, 108 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) ∧ 𝑚 ∈ (ℤ≥‘𝑞)) → (𝐹‘𝑚) ∈ (ℂ ↑𝑚
𝑆)) |
198 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑚) ∈ (ℂ ↑𝑚
𝑆) → (𝐹‘𝑚):𝑆⟶ℂ) |
199 | 197, 198 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) ∧ 𝑚 ∈ (ℤ≥‘𝑞)) → (𝐹‘𝑚):𝑆⟶ℂ) |
200 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) ∧ 𝑚 ∈ (ℤ≥‘𝑞)) → 𝑤 ∈ 𝑆) |
201 | 199, 200 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) ∧ 𝑚 ∈ (ℤ≥‘𝑞)) → ((𝐹‘𝑚)‘𝑤) ∈ ℂ) |
202 | | rpre 11839 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
203 | 202 | ad4antlr 769 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) ∧ 𝑚 ∈ (ℤ≥‘𝑞)) → 𝑟 ∈ ℝ) |
204 | | abs3lem 14078 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐹‘𝑞)‘𝑤) ∈ ℂ ∧ ( ⇝
‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))) ∈ ℂ) ∧ (((𝐹‘𝑚)‘𝑤) ∈ ℂ ∧ 𝑟 ∈ ℝ)) →
(((abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹‘𝑚)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < (𝑟 / 2)) → (abs‘(((𝐹‘𝑞)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < 𝑟)) |
205 | 192, 195,
201, 203, 204 | syl22anc 1327 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) ∧ 𝑚 ∈ (ℤ≥‘𝑞)) → (((abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹‘𝑚)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < (𝑟 / 2)) → (abs‘(((𝐹‘𝑞)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < 𝑟)) |
206 | 205 | rexlimdva 3031 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) → (∃𝑚 ∈ (ℤ≥‘𝑞)((abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹‘𝑚)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < (𝑟 / 2)) → (abs‘(((𝐹‘𝑞)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < 𝑟)) |
207 | 186, 206 | syl5 34 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) → ((∀𝑚 ∈ (ℤ≥‘𝑞)(abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) ∧ ∃𝑣 ∈ (ℤ≥‘𝑞)∀𝑚 ∈ (ℤ≥‘𝑣)(abs‘(((𝐹‘𝑚)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < (𝑟 / 2)) → (abs‘(((𝐹‘𝑞)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < 𝑟)) |
208 | 183, 207 | mpan2d 710 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) ∧ 𝑤 ∈ 𝑆) → (∀𝑚 ∈ (ℤ≥‘𝑞)(abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) → (abs‘(((𝐹‘𝑞)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < 𝑟)) |
209 | 208 | ralimdva 2962 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞 ∈ 𝑍) → (∀𝑤 ∈ 𝑆 ∀𝑚 ∈ (ℤ≥‘𝑞)(abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) → ∀𝑤 ∈ 𝑆 (abs‘(((𝐹‘𝑞)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < 𝑟)) |
210 | 99, 209 | sylan2 491 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ (𝑝 ∈ 𝑍 ∧ 𝑞 ∈ (ℤ≥‘𝑝))) → (∀𝑤 ∈ 𝑆 ∀𝑚 ∈ (ℤ≥‘𝑞)(abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) → ∀𝑤 ∈ 𝑆 (abs‘(((𝐹‘𝑞)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < 𝑟)) |
211 | 210 | anassrs 680 |
. . . . . . . . 9
⊢
(((((𝜑 ∧
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑝 ∈ 𝑍) ∧ 𝑞 ∈ (ℤ≥‘𝑝)) → (∀𝑤 ∈ 𝑆 ∀𝑚 ∈ (ℤ≥‘𝑞)(abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) → ∀𝑤 ∈ 𝑆 (abs‘(((𝐹‘𝑞)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < 𝑟)) |
212 | 211 | ralimdva 2962 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑝 ∈ 𝑍) → (∀𝑞 ∈ (ℤ≥‘𝑝)∀𝑤 ∈ 𝑆 ∀𝑚 ∈ (ℤ≥‘𝑞)(abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) → ∀𝑞 ∈ (ℤ≥‘𝑝)∀𝑤 ∈ 𝑆 (abs‘(((𝐹‘𝑞)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < 𝑟)) |
213 | 212 | reximdva 3017 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) →
(∃𝑝 ∈ 𝑍 ∀𝑞 ∈ (ℤ≥‘𝑝)∀𝑤 ∈ 𝑆 ∀𝑚 ∈ (ℤ≥‘𝑞)(abs‘(((𝐹‘𝑞)‘𝑤) − ((𝐹‘𝑚)‘𝑤))) < (𝑟 / 2) → ∃𝑝 ∈ 𝑍 ∀𝑞 ∈ (ℤ≥‘𝑝)∀𝑤 ∈ 𝑆 (abs‘(((𝐹‘𝑞)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < 𝑟)) |
214 | 98, 213 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) →
∃𝑝 ∈ 𝑍 ∀𝑞 ∈ (ℤ≥‘𝑝)∀𝑤 ∈ 𝑆 (abs‘(((𝐹‘𝑞)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < 𝑟) |
215 | 214 | ralrimiva 2966 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) → ∀𝑟 ∈ ℝ+ ∃𝑝 ∈ 𝑍 ∀𝑞 ∈ (ℤ≥‘𝑝)∀𝑤 ∈ 𝑆 (abs‘(((𝐹‘𝑞)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < 𝑟) |
216 | 4 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) → 𝑀 ∈ ℤ) |
217 | | eqidd 2623 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ (𝑞 ∈ 𝑍 ∧ 𝑤 ∈ 𝑆)) → ((𝐹‘𝑞)‘𝑤) = ((𝐹‘𝑞)‘𝑤)) |
218 | 177 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))) = ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤)))) |
219 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑆 ↦ ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)))) = (𝑦 ∈ 𝑆 ↦ ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)))) |
220 | | fvex 6201 |
. . . . . . . 8
⊢ ( ⇝
‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))) ∈ V |
221 | 218, 219,
220 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑤 ∈ 𝑆 → ((𝑦 ∈ 𝑆 ↦ ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))))‘𝑤) = ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤)))) |
222 | 221 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑤 ∈ 𝑆) → ((𝑦 ∈ 𝑆 ↦ ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))))‘𝑤) = ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤)))) |
223 | | climdm 14285 |
. . . . . . . . 9
⊢ ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)) ∈ dom ⇝ ↔ (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)) ⇝ ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)))) |
224 | 173, 223 | sylib 208 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑦 ∈ 𝑆) → (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)) ⇝ ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)))) |
225 | | climcl 14230 |
. . . . . . . 8
⊢ ((𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)) ⇝ ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))) → ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))) ∈ ℂ) |
226 | 224, 225 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) ∧ 𝑦 ∈ 𝑆) → ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))) ∈ ℂ) |
227 | 226, 219 | fmptd 6385 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) → (𝑦 ∈ 𝑆 ↦ ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)))):𝑆⟶ℂ) |
228 | 66 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) → 𝑆 ∈ 𝑉) |
229 | 3, 216, 115, 217, 222, 227, 228 | ulm2 24139 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) → (𝐹(⇝𝑢‘𝑆)(𝑦 ∈ 𝑆 ↦ ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦)))) ↔ ∀𝑟 ∈ ℝ+ ∃𝑝 ∈ 𝑍 ∀𝑞 ∈ (ℤ≥‘𝑝)∀𝑤 ∈ 𝑆 (abs‘(((𝐹‘𝑞)‘𝑤) − ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑤))))) < 𝑟)) |
230 | 215, 229 | mpbird 247 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) → 𝐹(⇝𝑢‘𝑆)(𝑦 ∈ 𝑆 ↦ ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))))) |
231 | | releldm 5358 |
. . . 4
⊢ ((Rel
(⇝𝑢‘𝑆) ∧ 𝐹(⇝𝑢‘𝑆)(𝑦 ∈ 𝑆 ↦ ( ⇝ ‘(𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑦))))) → 𝐹 ∈ dom
(⇝𝑢‘𝑆)) |
232 | 65, 230, 231 | sylancr 695 |
. . 3
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥) → 𝐹 ∈ dom
(⇝𝑢‘𝑆)) |
233 | 232 | ex 450 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥 → 𝐹 ∈ dom
(⇝𝑢‘𝑆))) |
234 | 64, 233 | impbid 202 |
1
⊢ (𝜑 → (𝐹 ∈ dom
(⇝𝑢‘𝑆) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − ((𝐹‘𝑗)‘𝑧))) < 𝑥)) |