MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ulmcau Structured version   Visualization version   GIF version

Theorem ulmcau 26453
Description: A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every 0 < 𝑥 there is a 𝑗 such that for all 𝑗𝑘 the functions 𝐹(𝑘) and 𝐹(𝑗) are uniformly within 𝑥 of each other on 𝑆. This is the four-quantifier version, see ulmcau2 26454 for the more conventional five-quantifier version. (Contributed by Mario Carneiro, 1-Mar-2015.)
Hypotheses
Ref Expression
ulmcau.z 𝑍 = (ℤ𝑀)
ulmcau.m (𝜑𝑀 ∈ ℤ)
ulmcau.s (𝜑𝑆𝑉)
ulmcau.f (𝜑𝐹:𝑍⟶(ℂ ↑m 𝑆))
Assertion
Ref Expression
ulmcau (𝜑 → (𝐹 ∈ dom (⇝𝑢𝑆) ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
Distinct variable groups:   𝑗,𝑘,𝑥,𝑧,𝐹   𝜑,𝑗,𝑘,𝑥,𝑧   𝑆,𝑗,𝑘,𝑥,𝑧   𝑗,𝑍,𝑘,𝑥,𝑧   𝑗,𝑀,𝑘,𝑧
Allowed substitution hints:   𝑀(𝑥)   𝑉(𝑥,𝑧,𝑗,𝑘)

Proof of Theorem ulmcau
Dummy variables 𝑔 𝑚 𝑛 𝑝 𝑞 𝑟 𝑣 𝑤 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eldmg 5912 . . . 4 (𝐹 ∈ dom (⇝𝑢𝑆) → (𝐹 ∈ dom (⇝𝑢𝑆) ↔ ∃𝑔 𝐹(⇝𝑢𝑆)𝑔))
21ibi 267 . . 3 (𝐹 ∈ dom (⇝𝑢𝑆) → ∃𝑔 𝐹(⇝𝑢𝑆)𝑔)
3 ulmcau.z . . . . . . . 8 𝑍 = (ℤ𝑀)
4 ulmcau.m . . . . . . . . 9 (𝜑𝑀 ∈ ℤ)
54ad2antrr 726 . . . . . . . 8 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → 𝑀 ∈ ℤ)
6 ulmcau.f . . . . . . . . 9 (𝜑𝐹:𝑍⟶(ℂ ↑m 𝑆))
76ad2antrr 726 . . . . . . . 8 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → 𝐹:𝑍⟶(ℂ ↑m 𝑆))
8 eqidd 2736 . . . . . . . 8 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ (𝑘𝑍𝑧𝑆)) → ((𝐹𝑘)‘𝑧) = ((𝐹𝑘)‘𝑧))
9 eqidd 2736 . . . . . . . 8 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑧𝑆) → (𝑔𝑧) = (𝑔𝑧))
10 simplr 769 . . . . . . . 8 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → 𝐹(⇝𝑢𝑆)𝑔)
11 rphalfcl 13060 . . . . . . . . 9 (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ+)
1211adantl 481 . . . . . . . 8 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ+)
133, 5, 7, 8, 9, 10, 12ulmi 26444 . . . . . . 7 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2))
14 simpr 484 . . . . . . . . . . 11 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → 𝑗𝑍)
1514, 3eleqtrdi 2849 . . . . . . . . . 10 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → 𝑗 ∈ (ℤ𝑀))
16 eluzelz 12886 . . . . . . . . . 10 (𝑗 ∈ (ℤ𝑀) → 𝑗 ∈ ℤ)
17 uzid 12891 . . . . . . . . . 10 (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ𝑗))
18 fveq2 6907 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → (𝐹𝑘) = (𝐹𝑗))
1918fveq1d 6909 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → ((𝐹𝑘)‘𝑧) = ((𝐹𝑗)‘𝑧))
2019fvoveq1d 7453 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) = (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))))
2120breq1d 5158 . . . . . . . . . . . 12 (𝑘 = 𝑗 → ((abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ↔ (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)))
2221ralbidv 3176 . . . . . . . . . . 11 (𝑘 = 𝑗 → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)))
2322rspcv 3618 . . . . . . . . . 10 (𝑗 ∈ (ℤ𝑗) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)))
2415, 16, 17, 234syl 19 . . . . . . . . 9 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)))
25 r19.26 3109 . . . . . . . . . . . . . . 15 (∀𝑧𝑆 ((abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) ↔ (∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)))
267ffvelcdmda 7104 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (𝐹𝑗) ∈ (ℂ ↑m 𝑆))
2726adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑗) ∈ (ℂ ↑m 𝑆))
28 elmapi 8888 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑗) ∈ (ℂ ↑m 𝑆) → (𝐹𝑗):𝑆⟶ℂ)
2927, 28syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑗):𝑆⟶ℂ)
3029ffvelcdmda 7104 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → ((𝐹𝑗)‘𝑧) ∈ ℂ)
31 ulmcl 26439 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹(⇝𝑢𝑆)𝑔𝑔:𝑆⟶ℂ)
3231ad4antlr 733 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑔:𝑆⟶ℂ)
3332ffvelcdmda 7104 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → (𝑔𝑧) ∈ ℂ)
3430, 33abssubd 15489 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) = (abs‘((𝑔𝑧) − ((𝐹𝑗)‘𝑧))))
3534breq1d 5158 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → ((abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ↔ (abs‘((𝑔𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)))
3635biimpd 229 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → ((abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → (abs‘((𝑔𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)))
373uztrn2 12895 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
38 ffvelcdm 7101 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹:𝑍⟶(ℂ ↑m 𝑆) ∧ 𝑘𝑍) → (𝐹𝑘) ∈ (ℂ ↑m 𝑆))
397, 37, 38syl2an 596 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (𝐹𝑘) ∈ (ℂ ↑m 𝑆))
4039anassrs 467 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ (ℂ ↑m 𝑆))
41 elmapi 8888 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑘) ∈ (ℂ ↑m 𝑆) → (𝐹𝑘):𝑆⟶ℂ)
4240, 41syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘):𝑆⟶ℂ)
4342ffvelcdmda 7104 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → ((𝐹𝑘)‘𝑧) ∈ ℂ)
44 rpre 13041 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
4544ad4antlr 733 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → 𝑥 ∈ ℝ)
46 abs3lem 15374 . . . . . . . . . . . . . . . . . . 19 (((((𝐹𝑘)‘𝑧) ∈ ℂ ∧ ((𝐹𝑗)‘𝑧) ∈ ℂ) ∧ ((𝑔𝑧) ∈ ℂ ∧ 𝑥 ∈ ℝ)) → (((abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ (abs‘((𝑔𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)) → (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
4743, 30, 33, 45, 46syl22anc 839 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → (((abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ (abs‘((𝑔𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)) → (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
4836, 47sylan2d 605 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → (((abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) → (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
4948ancomsd 465 . . . . . . . . . . . . . . . 16 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → (((abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) → (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5049ralimdva 3165 . . . . . . . . . . . . . . 15 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (∀𝑧𝑆 ((abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) → ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5125, 50biimtrrid 243 . . . . . . . . . . . . . 14 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ((∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) → ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5251expdimp 452 . . . . . . . . . . . . 13 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5352an32s 652 . . . . . . . . . . . 12 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) ∧ 𝑘 ∈ (ℤ𝑗)) → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5453ralimdva 3165 . . . . . . . . . . 11 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5554ex 412 . . . . . . . . . 10 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥)))
5655com23 86 . . . . . . . . 9 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → (∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥)))
5724, 56mpdd 43 . . . . . . . 8 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5857reximdva 3166 . . . . . . 7 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5913, 58mpd 15 . . . . . 6 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥)
6059ralrimiva 3144 . . . . 5 ((𝜑𝐹(⇝𝑢𝑆)𝑔) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥)
6160ex 412 . . . 4 (𝜑 → (𝐹(⇝𝑢𝑆)𝑔 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
6261exlimdv 1931 . . 3 (𝜑 → (∃𝑔 𝐹(⇝𝑢𝑆)𝑔 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
632, 62syl5 34 . 2 (𝜑 → (𝐹 ∈ dom (⇝𝑢𝑆) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
64 ulmrel 26436 . . . 4 Rel (⇝𝑢𝑆)
65 ulmcau.s . . . . . . . . . 10 (𝜑𝑆𝑉)
663, 4, 65, 6ulmcaulem 26452 . . . . . . . . 9 (𝜑 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
6766biimpa 476 . . . . . . . 8 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥)
68 rphalfcl 13060 . . . . . . . 8 (𝑟 ∈ ℝ+ → (𝑟 / 2) ∈ ℝ+)
69 breq2 5152 . . . . . . . . . . . . 13 (𝑥 = (𝑟 / 2) → ((abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
7069ralbidv 3176 . . . . . . . . . . . 12 (𝑥 = (𝑟 / 2) → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
71702ralbidv 3219 . . . . . . . . . . 11 (𝑥 = (𝑟 / 2) → (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
7271rexbidv 3177 . . . . . . . . . 10 (𝑥 = (𝑟 / 2) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
73 ralcom 3287 . . . . . . . . . . . . . 14 (∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑚 ∈ (ℤ𝑞)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2))
74 fveq2 6907 . . . . . . . . . . . . . . 15 (𝑞 = 𝑘 → (ℤ𝑞) = (ℤ𝑘))
75 fveq2 6907 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑧 → ((𝐹𝑞)‘𝑤) = ((𝐹𝑞)‘𝑧))
76 fveq2 6907 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑧 → ((𝐹𝑚)‘𝑤) = ((𝐹𝑚)‘𝑧))
7775, 76oveq12d 7449 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑧 → (((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤)) = (((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧)))
7877fveq2d 6911 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑧 → (abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) = (abs‘(((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧))))
7978breq1d 5158 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑧 → ((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ (abs‘(((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
8079cbvralvw 3235 . . . . . . . . . . . . . . . 16 (∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2))
81 fveq2 6907 . . . . . . . . . . . . . . . . . . . 20 (𝑞 = 𝑘 → (𝐹𝑞) = (𝐹𝑘))
8281fveq1d 6909 . . . . . . . . . . . . . . . . . . 19 (𝑞 = 𝑘 → ((𝐹𝑞)‘𝑧) = ((𝐹𝑘)‘𝑧))
8382fvoveq1d 7453 . . . . . . . . . . . . . . . . . 18 (𝑞 = 𝑘 → (abs‘(((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧))) = (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))))
8483breq1d 5158 . . . . . . . . . . . . . . . . 17 (𝑞 = 𝑘 → ((abs‘(((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2) ↔ (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
8584ralbidv 3176 . . . . . . . . . . . . . . . 16 (𝑞 = 𝑘 → (∀𝑧𝑆 (abs‘(((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2) ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
8680, 85bitrid 283 . . . . . . . . . . . . . . 15 (𝑞 = 𝑘 → (∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
8774, 86raleqbidv 3344 . . . . . . . . . . . . . 14 (𝑞 = 𝑘 → (∀𝑚 ∈ (ℤ𝑞)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
8873, 87bitrid 283 . . . . . . . . . . . . 13 (𝑞 = 𝑘 → (∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
8988cbvralvw 3235 . . . . . . . . . . . 12 (∀𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑘 ∈ (ℤ𝑝)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2))
90 fveq2 6907 . . . . . . . . . . . . 13 (𝑝 = 𝑗 → (ℤ𝑝) = (ℤ𝑗))
9190raleqdv 3324 . . . . . . . . . . . 12 (𝑝 = 𝑗 → (∀𝑘 ∈ (ℤ𝑝)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
9289, 91bitrid 283 . . . . . . . . . . 11 (𝑝 = 𝑗 → (∀𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
9392cbvrexvw 3236 . . . . . . . . . 10 (∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2))
9472, 93bitr4di 289 . . . . . . . . 9 (𝑥 = (𝑟 / 2) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ ∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2)))
9594rspccva 3621 . . . . . . . 8 ((∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ∧ (𝑟 / 2) ∈ ℝ+) → ∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2))
9667, 68, 95syl2an 596 . . . . . . 7 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) → ∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2))
973uztrn2 12895 . . . . . . . . . . 11 ((𝑝𝑍𝑞 ∈ (ℤ𝑝)) → 𝑞𝑍)
98 eqid 2735 . . . . . . . . . . . . . 14 (ℤ𝑞) = (ℤ𝑞)
99 eluzelz 12886 . . . . . . . . . . . . . . . 16 (𝑞 ∈ (ℤ𝑀) → 𝑞 ∈ ℤ)
10099, 3eleq2s 2857 . . . . . . . . . . . . . . 15 (𝑞𝑍𝑞 ∈ ℤ)
101100ad2antlr 727 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → 𝑞 ∈ ℤ)
10268adantl 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈ ℝ+)
103102ad2antrr 726 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → (𝑟 / 2) ∈ ℝ+)
104 simplr 769 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → 𝑞𝑍)
1053uztrn2 12895 . . . . . . . . . . . . . . . 16 ((𝑞𝑍𝑚 ∈ (ℤ𝑞)) → 𝑚𝑍)
106104, 105sylan 580 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → 𝑚𝑍)
107 fveq2 6907 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → (𝐹𝑛) = (𝐹𝑚))
108107fveq1d 6909 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚 → ((𝐹𝑛)‘𝑤) = ((𝐹𝑚)‘𝑤))
109 eqid 2735 . . . . . . . . . . . . . . . 16 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) = (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))
110 fvex 6920 . . . . . . . . . . . . . . . 16 ((𝐹𝑚)‘𝑤) ∈ V
111108, 109, 110fvmpt 7016 . . . . . . . . . . . . . . 15 (𝑚𝑍 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))‘𝑚) = ((𝐹𝑚)‘𝑤))
112106, 111syl 17 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))‘𝑚) = ((𝐹𝑚)‘𝑤))
1136adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → 𝐹:𝑍⟶(ℂ ↑m 𝑆))
114113ffvelcdmda 7104 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑛𝑍) → (𝐹𝑛) ∈ (ℂ ↑m 𝑆))
115 elmapi 8888 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑛) ∈ (ℂ ↑m 𝑆) → (𝐹𝑛):𝑆⟶ℂ)
116114, 115syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑛𝑍) → (𝐹𝑛):𝑆⟶ℂ)
117116ffvelcdmda 7104 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑛𝑍) ∧ 𝑦𝑆) → ((𝐹𝑛)‘𝑦) ∈ ℂ)
118117an32s 652 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) ∧ 𝑛𝑍) → ((𝐹𝑛)‘𝑦) ∈ ℂ)
119118fmpttd 7135 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)):𝑍⟶ℂ)
120119ffvelcdmda 7104 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) ∧ 𝑞𝑍) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) ∈ ℂ)
121 fveq2 6907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = 𝑦 → ((𝐹𝑘)‘𝑧) = ((𝐹𝑘)‘𝑦))
122 fveq2 6907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = 𝑦 → ((𝐹𝑗)‘𝑧) = ((𝐹𝑗)‘𝑦))
123121, 122oveq12d 7449 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑦 → (((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧)) = (((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦)))
124123fveq2d 6911 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑦 → (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) = (abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))))
125124breq1d 5158 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = 𝑦 → ((abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 ↔ (abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
126125rspcv 3618 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦𝑆 → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 → (abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
127126ralimdv 3167 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦𝑆 → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 → ∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
128127reximdv 3168 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝑆 → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
129128ralimdv 3167 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝑆 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
130129impcom 407 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥𝑦𝑆) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥)
131130adantll 714 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥)
132 fveq2 6907 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑞 = 𝑘 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) = ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘))
133132fvoveq1d 7453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑞 = 𝑘 → (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) = (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))))
134133breq1d 5158 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑞 = 𝑘 → ((abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟))
135134cbvralvw 3235 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∀𝑘 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟)
136 fveq2 6907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑝 = 𝑗 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝) = ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))
137136oveq2d 7447 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 = 𝑗 → (((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝)) = (((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗)))
138137fveq2d 6911 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑝 = 𝑗 → (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) = (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))))
139138breq1d 5158 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 = 𝑗 → ((abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟))
14090, 139raleqbidv 3344 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = 𝑗 → (∀𝑘 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟))
141135, 140bitrid 283 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = 𝑗 → (∀𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟))
142141cbvrexvw 3236 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑝𝑍𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟)
143 fveq2 6907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
144143fveq1d 6909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑘 → ((𝐹𝑛)‘𝑦) = ((𝐹𝑘)‘𝑦))
145 eqid 2735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) = (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))
146 fvex 6920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐹𝑘)‘𝑦) ∈ V
147144, 145, 146fvmpt 7016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘𝑍 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) = ((𝐹𝑘)‘𝑦))
14837, 147syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) = ((𝐹𝑘)‘𝑦))
149 fveq2 6907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = 𝑗 → (𝐹𝑛) = (𝐹𝑗))
150149fveq1d 6909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑗 → ((𝐹𝑛)‘𝑦) = ((𝐹𝑗)‘𝑦))
151 fvex 6920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐹𝑗)‘𝑦) ∈ V
152150, 145, 151fvmpt 7016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗𝑍 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗) = ((𝐹𝑗)‘𝑦))
153152adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗) = ((𝐹𝑗)‘𝑦))
154148, 153oveq12d 7449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → (((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗)) = (((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦)))
155154fveq2d 6911 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) = (abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))))
156155breq1d 5158 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → ((abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟 ↔ (abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟))
157156ralbidva 3174 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗𝑍 → (∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟 ↔ ∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟))
158157rexbiia 3090 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟)
159142, 158bitri 275 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑝𝑍𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟)
160 breq2 5152 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑟 = 𝑥 → ((abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟 ↔ (abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
161160ralbidv 3176 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑟 = 𝑥 → (∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟 ↔ ∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
162161rexbidv 3177 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟 = 𝑥 → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
163159, 162bitrid 283 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = 𝑥 → (∃𝑝𝑍𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
164163cbvralvw 3235 . . . . . . . . . . . . . . . . . . . 20 (∀𝑟 ∈ ℝ+𝑝𝑍𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥)
165131, 164sylibr 234 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → ∀𝑟 ∈ ℝ+𝑝𝑍𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟)
1663fvexi 6921 . . . . . . . . . . . . . . . . . . . . 21 𝑍 ∈ V
167166mptex 7243 . . . . . . . . . . . . . . . . . . . 20 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ V
168167a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ V)
1693, 120, 165, 168caucvg 15712 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ dom ⇝ )
170169ralrimiva 3144 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → ∀𝑦𝑆 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ dom ⇝ )
171170ad2antrr 726 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) → ∀𝑦𝑆 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ dom ⇝ )
172 fveq2 6907 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑤 → ((𝐹𝑛)‘𝑦) = ((𝐹𝑛)‘𝑤))
173172mpteq2dv 5250 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑤 → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) = (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)))
174173eleq1d 2824 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑤 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ dom ⇝ ↔ (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ∈ dom ⇝ ))
175174rspccva 3621 . . . . . . . . . . . . . . . 16 ((∀𝑦𝑆 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ dom ⇝ ∧ 𝑤𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ∈ dom ⇝ )
176171, 175sylan 580 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ∈ dom ⇝ )
177 climdm 15587 . . . . . . . . . . . . . . 15 ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ∈ dom ⇝ ↔ (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ⇝ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))
178176, 177sylib 218 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ⇝ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))
17998, 101, 103, 112, 178climi2 15544 . . . . . . . . . . . . 13 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → ∃𝑣 ∈ (ℤ𝑞)∀𝑚 ∈ (ℤ𝑣)(abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2))
18098r19.29uz 15386 . . . . . . . . . . . . . . 15 ((∀𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ ∃𝑣 ∈ (ℤ𝑞)∀𝑚 ∈ (ℤ𝑣)(abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → ∃𝑣 ∈ (ℤ𝑞)∀𝑚 ∈ (ℤ𝑣)((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)))
18198r19.2uz 15387 . . . . . . . . . . . . . . 15 (∃𝑣 ∈ (ℤ𝑞)∀𝑚 ∈ (ℤ𝑣)((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → ∃𝑚 ∈ (ℤ𝑞)((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)))
182180, 181syl 17 . . . . . . . . . . . . . 14 ((∀𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ ∃𝑣 ∈ (ℤ𝑞)∀𝑚 ∈ (ℤ𝑣)(abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → ∃𝑚 ∈ (ℤ𝑞)((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)))
1836ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) → 𝐹:𝑍⟶(ℂ ↑m 𝑆))
184183ffvelcdmda 7104 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) → (𝐹𝑞) ∈ (ℂ ↑m 𝑆))
185 elmapi 8888 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑞) ∈ (ℂ ↑m 𝑆) → (𝐹𝑞):𝑆⟶ℂ)
186184, 185syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) → (𝐹𝑞):𝑆⟶ℂ)
187186ffvelcdmda 7104 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → ((𝐹𝑞)‘𝑤) ∈ ℂ)
188187adantr 480 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → ((𝐹𝑞)‘𝑤) ∈ ℂ)
189 climcl 15532 . . . . . . . . . . . . . . . . . 18 ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ⇝ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))) → ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))) ∈ ℂ)
190178, 189syl 17 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))) ∈ ℂ)
191190adantr 480 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))) ∈ ℂ)
1926ad5antr 734 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → 𝐹:𝑍⟶(ℂ ↑m 𝑆))
193192, 106ffvelcdmd 7105 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → (𝐹𝑚) ∈ (ℂ ↑m 𝑆))
194 elmapi 8888 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑚) ∈ (ℂ ↑m 𝑆) → (𝐹𝑚):𝑆⟶ℂ)
195193, 194syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → (𝐹𝑚):𝑆⟶ℂ)
196 simplr 769 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → 𝑤𝑆)
197195, 196ffvelcdmd 7105 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → ((𝐹𝑚)‘𝑤) ∈ ℂ)
198 rpre 13041 . . . . . . . . . . . . . . . . 17 (𝑟 ∈ ℝ+𝑟 ∈ ℝ)
199198ad4antlr 733 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → 𝑟 ∈ ℝ)
200 abs3lem 15374 . . . . . . . . . . . . . . . 16 (((((𝐹𝑞)‘𝑤) ∈ ℂ ∧ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))) ∈ ℂ) ∧ (((𝐹𝑚)‘𝑤) ∈ ℂ ∧ 𝑟 ∈ ℝ)) → (((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
201188, 191, 197, 199, 200syl22anc 839 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → (((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
202201rexlimdva 3153 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → (∃𝑚 ∈ (ℤ𝑞)((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
203182, 202syl5 34 . . . . . . . . . . . . 13 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → ((∀𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ ∃𝑣 ∈ (ℤ𝑞)∀𝑚 ∈ (ℤ𝑣)(abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
204179, 203mpan2d 694 . . . . . . . . . . . 12 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → (∀𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) → (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
205204ralimdva 3165 . . . . . . . . . . 11 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) → (∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) → ∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
20697, 205sylan2 593 . . . . . . . . . 10 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ (𝑝𝑍𝑞 ∈ (ℤ𝑝))) → (∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) → ∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
207206anassrs 467 . . . . . . . . 9 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑝𝑍) ∧ 𝑞 ∈ (ℤ𝑝)) → (∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) → ∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
208207ralimdva 3165 . . . . . . . 8 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑝𝑍) → (∀𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) → ∀𝑞 ∈ (ℤ𝑝)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
209208reximdva 3166 . . . . . . 7 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) → (∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) → ∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
21096, 209mpd 15 . . . . . 6 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) → ∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟)
211210ralrimiva 3144 . . . . 5 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → ∀𝑟 ∈ ℝ+𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟)
2124adantr 480 . . . . . 6 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → 𝑀 ∈ ℤ)
213 eqidd 2736 . . . . . 6 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ (𝑞𝑍𝑤𝑆)) → ((𝐹𝑞)‘𝑤) = ((𝐹𝑞)‘𝑤))
214173fveq2d 6911 . . . . . . . 8 (𝑦 = 𝑤 → ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))) = ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))
215 eqid 2735 . . . . . . . 8 (𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)))) = (𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))))
216 fvex 6920 . . . . . . . 8 ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))) ∈ V
217214, 215, 216fvmpt 7016 . . . . . . 7 (𝑤𝑆 → ((𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))))‘𝑤) = ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))
218217adantl 481 . . . . . 6 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑤𝑆) → ((𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))))‘𝑤) = ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))
219 climdm 15587 . . . . . . . . 9 ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ dom ⇝ ↔ (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ⇝ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))))
220169, 219sylib 218 . . . . . . . 8 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ⇝ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))))
221 climcl 15532 . . . . . . . 8 ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ⇝ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))) → ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))) ∈ ℂ)
222220, 221syl 17 . . . . . . 7 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))) ∈ ℂ)
223222fmpttd 7135 . . . . . 6 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → (𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)))):𝑆⟶ℂ)
22465adantr 480 . . . . . 6 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → 𝑆𝑉)
2253, 212, 113, 213, 218, 223, 224ulm2 26443 . . . . 5 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → (𝐹(⇝𝑢𝑆)(𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)))) ↔ ∀𝑟 ∈ ℝ+𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
226211, 225mpbird 257 . . . 4 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → 𝐹(⇝𝑢𝑆)(𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)))))
227 releldm 5958 . . . 4 ((Rel (⇝𝑢𝑆) ∧ 𝐹(⇝𝑢𝑆)(𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))))) → 𝐹 ∈ dom (⇝𝑢𝑆))
22864, 226, 227sylancr 587 . . 3 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → 𝐹 ∈ dom (⇝𝑢𝑆))
229228ex 412 . 2 (𝜑 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥𝐹 ∈ dom (⇝𝑢𝑆)))
23063, 229impbid 212 1 (𝜑 → (𝐹 ∈ dom (⇝𝑢𝑆) ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wex 1776  wcel 2106  wral 3059  wrex 3068  Vcvv 3478   class class class wbr 5148  cmpt 5231  dom cdm 5689  Rel wrel 5694  wf 6559  cfv 6563  (class class class)co 7431  m cmap 8865  cc 11151  cr 11152   < clt 11293  cmin 11490   / cdiv 11918  2c2 12319  cz 12611  cuz 12876  +crp 13032  abscabs 15270  cli 15517  𝑢culm 26434
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-er 8744  df-map 8867  df-pm 8868  df-en 8985  df-dom 8986  df-sdom 8987  df-sup 9480  df-inf 9481  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-3 12328  df-n0 12525  df-z 12612  df-uz 12877  df-rp 13033  df-ico 13390  df-fl 13829  df-seq 14040  df-exp 14100  df-cj 15135  df-re 15136  df-im 15137  df-sqrt 15271  df-abs 15272  df-limsup 15504  df-clim 15521  df-rlim 15522  df-ulm 26435
This theorem is referenced by:  ulmcau2  26454  mtest  26462
  Copyright terms: Public domain W3C validator