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

Theorem ulmcau 25102
 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 25103 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 5744 . . . 4 (𝐹 ∈ dom (⇝𝑢𝑆) → (𝐹 ∈ dom (⇝𝑢𝑆) ↔ ∃𝑔 𝐹(⇝𝑢𝑆)𝑔))
21ibi 270 . . 3 (𝐹 ∈ dom (⇝𝑢𝑆) → ∃𝑔 𝐹(⇝𝑢𝑆)𝑔)
3 ulmcau.z . . . . . . . 8 𝑍 = (ℤ𝑀)
4 ulmcau.m . . . . . . . . 9 (𝜑𝑀 ∈ ℤ)
54ad2antrr 725 . . . . . . . 8 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → 𝑀 ∈ ℤ)
6 ulmcau.f . . . . . . . . 9 (𝜑𝐹:𝑍⟶(ℂ ↑m 𝑆))
76ad2antrr 725 . . . . . . . 8 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → 𝐹:𝑍⟶(ℂ ↑m 𝑆))
8 eqidd 2759 . . . . . . . 8 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ (𝑘𝑍𝑧𝑆)) → ((𝐹𝑘)‘𝑧) = ((𝐹𝑘)‘𝑧))
9 eqidd 2759 . . . . . . . 8 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑧𝑆) → (𝑔𝑧) = (𝑔𝑧))
10 simplr 768 . . . . . . . 8 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → 𝐹(⇝𝑢𝑆)𝑔)
11 rphalfcl 12470 . . . . . . . . 9 (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ+)
1211adantl 485 . . . . . . . 8 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ+)
133, 5, 7, 8, 9, 10, 12ulmi 25093 . . . . . . 7 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2))
14 simpr 488 . . . . . . . . . . 11 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → 𝑗𝑍)
1514, 3eleqtrdi 2862 . . . . . . . . . 10 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → 𝑗 ∈ (ℤ𝑀))
16 eluzelz 12305 . . . . . . . . . 10 (𝑗 ∈ (ℤ𝑀) → 𝑗 ∈ ℤ)
17 uzid 12310 . . . . . . . . . 10 (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ𝑗))
18 fveq2 6663 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → (𝐹𝑘) = (𝐹𝑗))
1918fveq1d 6665 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → ((𝐹𝑘)‘𝑧) = ((𝐹𝑗)‘𝑧))
2019fvoveq1d 7178 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) = (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))))
2120breq1d 5046 . . . . . . . . . . . 12 (𝑘 = 𝑗 → ((abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ↔ (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)))
2221ralbidv 3126 . . . . . . . . . . 11 (𝑘 = 𝑗 → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)))
2322rspcv 3538 . . . . . . . . . 10 (𝑗 ∈ (ℤ𝑗) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)))
2415, 16, 17, 234syl 19 . . . . . . . . 9 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)))
25 r19.26 3101 . . . . . . . . . . . . . . 15 (∀𝑧𝑆 ((abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) ↔ (∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)))
267ffvelrnda 6848 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (𝐹𝑗) ∈ (ℂ ↑m 𝑆))
2726adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑗) ∈ (ℂ ↑m 𝑆))
28 elmapi 8444 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑗) ∈ (ℂ ↑m 𝑆) → (𝐹𝑗):𝑆⟶ℂ)
2927, 28syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑗):𝑆⟶ℂ)
3029ffvelrnda 6848 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → ((𝐹𝑗)‘𝑧) ∈ ℂ)
31 ulmcl 25088 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹(⇝𝑢𝑆)𝑔𝑔:𝑆⟶ℂ)
3231ad4antlr 732 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑔:𝑆⟶ℂ)
3332ffvelrnda 6848 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → (𝑔𝑧) ∈ ℂ)
3430, 33abssubd 14874 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) = (abs‘((𝑔𝑧) − ((𝐹𝑗)‘𝑧))))
3534breq1d 5046 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → ((abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ↔ (abs‘((𝑔𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)))
3635biimpd 232 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → ((abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → (abs‘((𝑔𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)))
373uztrn2 12314 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
38 ffvelrn 6846 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹:𝑍⟶(ℂ ↑m 𝑆) ∧ 𝑘𝑍) → (𝐹𝑘) ∈ (ℂ ↑m 𝑆))
397, 37, 38syl2an 598 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (𝐹𝑘) ∈ (ℂ ↑m 𝑆))
4039anassrs 471 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ (ℂ ↑m 𝑆))
41 elmapi 8444 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑘) ∈ (ℂ ↑m 𝑆) → (𝐹𝑘):𝑆⟶ℂ)
4240, 41syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘):𝑆⟶ℂ)
4342ffvelrnda 6848 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → ((𝐹𝑘)‘𝑧) ∈ ℂ)
44 rpre 12451 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
4544ad4antlr 732 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → 𝑥 ∈ ℝ)
46 abs3lem 14759 . . . . . . . . . . . . . . . . . . 19 (((((𝐹𝑘)‘𝑧) ∈ ℂ ∧ ((𝐹𝑗)‘𝑧) ∈ ℂ) ∧ ((𝑔𝑧) ∈ ℂ ∧ 𝑥 ∈ ℝ)) → (((abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ (abs‘((𝑔𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)) → (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
4743, 30, 33, 45, 46syl22anc 837 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → (((abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ (abs‘((𝑔𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)) → (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
4836, 47sylan2d 607 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → (((abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) → (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
4948ancomsd 469 . . . . . . . . . . . . . . . 16 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → (((abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) → (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5049ralimdva 3108 . . . . . . . . . . . . . . 15 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (∀𝑧𝑆 ((abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) → ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5125, 50syl5bir 246 . . . . . . . . . . . . . 14 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → ((∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) → ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5251expdimp 456 . . . . . . . . . . . . 13 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5352an32s 651 . . . . . . . . . . . 12 ((((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) ∧ 𝑘 ∈ (ℤ𝑗)) → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5453ralimdva 3108 . . . . . . . . . . 11 (((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2)) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5554ex 416 . . . . . . . . . 10 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥)))
5655com23 86 . . . . . . . . 9 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → (∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥)))
5724, 56mpdd 43 . . . . . . . 8 ((((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5857reximdva 3198 . . . . . . 7 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − (𝑔𝑧))) < (𝑥 / 2) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
5913, 58mpd 15 . . . . . 6 (((𝜑𝐹(⇝𝑢𝑆)𝑔) ∧ 𝑥 ∈ ℝ+) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥)
6059ralrimiva 3113 . . . . 5 ((𝜑𝐹(⇝𝑢𝑆)𝑔) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥)
6160ex 416 . . . 4 (𝜑 → (𝐹(⇝𝑢𝑆)𝑔 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
6261exlimdv 1934 . . 3 (𝜑 → (∃𝑔 𝐹(⇝𝑢𝑆)𝑔 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
632, 62syl5 34 . 2 (𝜑 → (𝐹 ∈ dom (⇝𝑢𝑆) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
64 ulmrel 25085 . . . 4 Rel (⇝𝑢𝑆)
65 ulmcau.s . . . . . . . . . 10 (𝜑𝑆𝑉)
663, 4, 65, 6ulmcaulem 25101 . . . . . . . . 9 (𝜑 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
6766biimpa 480 . . . . . . . 8 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥)
68 rphalfcl 12470 . . . . . . . 8 (𝑟 ∈ ℝ+ → (𝑟 / 2) ∈ ℝ+)
69 breq2 5040 . . . . . . . . . . . . 13 (𝑥 = (𝑟 / 2) → ((abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
7069ralbidv 3126 . . . . . . . . . . . 12 (𝑥 = (𝑟 / 2) → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
71702ralbidv 3128 . . . . . . . . . . 11 (𝑥 = (𝑟 / 2) → (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
7271rexbidv 3221 . . . . . . . . . 10 (𝑥 = (𝑟 / 2) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
73 ralcom 3272 . . . . . . . . . . . . . 14 (∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑚 ∈ (ℤ𝑞)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2))
74 fveq2 6663 . . . . . . . . . . . . . . 15 (𝑞 = 𝑘 → (ℤ𝑞) = (ℤ𝑘))
75 fveq2 6663 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑧 → ((𝐹𝑞)‘𝑤) = ((𝐹𝑞)‘𝑧))
76 fveq2 6663 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑧 → ((𝐹𝑚)‘𝑤) = ((𝐹𝑚)‘𝑧))
7775, 76oveq12d 7174 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑧 → (((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤)) = (((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧)))
7877fveq2d 6667 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑧 → (abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) = (abs‘(((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧))))
7978breq1d 5046 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑧 → ((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ (abs‘(((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
8079cbvralvw 3361 . . . . . . . . . . . . . . . 16 (∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2))
81 fveq2 6663 . . . . . . . . . . . . . . . . . . . 20 (𝑞 = 𝑘 → (𝐹𝑞) = (𝐹𝑘))
8281fveq1d 6665 . . . . . . . . . . . . . . . . . . 19 (𝑞 = 𝑘 → ((𝐹𝑞)‘𝑧) = ((𝐹𝑘)‘𝑧))
8382fvoveq1d 7178 . . . . . . . . . . . . . . . . . 18 (𝑞 = 𝑘 → (abs‘(((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧))) = (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))))
8483breq1d 5046 . . . . . . . . . . . . . . . . 17 (𝑞 = 𝑘 → ((abs‘(((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2) ↔ (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
8584ralbidv 3126 . . . . . . . . . . . . . . . 16 (𝑞 = 𝑘 → (∀𝑧𝑆 (abs‘(((𝐹𝑞)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2) ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
8680, 85syl5bb 286 . . . . . . . . . . . . . . 15 (𝑞 = 𝑘 → (∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
8774, 86raleqbidv 3319 . . . . . . . . . . . . . 14 (𝑞 = 𝑘 → (∀𝑚 ∈ (ℤ𝑞)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
8873, 87syl5bb 286 . . . . . . . . . . . . 13 (𝑞 = 𝑘 → (∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
8988cbvralvw 3361 . . . . . . . . . . . 12 (∀𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑘 ∈ (ℤ𝑝)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2))
90 fveq2 6663 . . . . . . . . . . . . 13 (𝑝 = 𝑗 → (ℤ𝑝) = (ℤ𝑗))
9190raleqdv 3329 . . . . . . . . . . . 12 (𝑝 = 𝑗 → (∀𝑘 ∈ (ℤ𝑝)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
9289, 91syl5bb 286 . . . . . . . . . . 11 (𝑝 = 𝑗 → (∀𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2)))
9392cbvrexvw 3362 . . . . . . . . . 10 (∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑟 / 2))
9472, 93bitr4di 292 . . . . . . . . 9 (𝑥 = (𝑟 / 2) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ ∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2)))
9594rspccva 3542 . . . . . . . 8 ((∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ∧ (𝑟 / 2) ∈ ℝ+) → ∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2))
9667, 68, 95syl2an 598 . . . . . . 7 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) → ∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2))
973uztrn2 12314 . . . . . . . . . . 11 ((𝑝𝑍𝑞 ∈ (ℤ𝑝)) → 𝑞𝑍)
98 eqid 2758 . . . . . . . . . . . . . 14 (ℤ𝑞) = (ℤ𝑞)
99 eluzelz 12305 . . . . . . . . . . . . . . . 16 (𝑞 ∈ (ℤ𝑀) → 𝑞 ∈ ℤ)
10099, 3eleq2s 2870 . . . . . . . . . . . . . . 15 (𝑞𝑍𝑞 ∈ ℤ)
101100ad2antlr 726 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → 𝑞 ∈ ℤ)
10268adantl 485 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈ ℝ+)
103102ad2antrr 725 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → (𝑟 / 2) ∈ ℝ+)
104 simplr 768 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → 𝑞𝑍)
1053uztrn2 12314 . . . . . . . . . . . . . . . 16 ((𝑞𝑍𝑚 ∈ (ℤ𝑞)) → 𝑚𝑍)
106104, 105sylan 583 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → 𝑚𝑍)
107 fveq2 6663 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → (𝐹𝑛) = (𝐹𝑚))
108107fveq1d 6665 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚 → ((𝐹𝑛)‘𝑤) = ((𝐹𝑚)‘𝑤))
109 eqid 2758 . . . . . . . . . . . . . . . 16 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) = (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))
110 fvex 6676 . . . . . . . . . . . . . . . 16 ((𝐹𝑚)‘𝑤) ∈ V
111108, 109, 110fvmpt 6764 . . . . . . . . . . . . . . 15 (𝑚𝑍 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))‘𝑚) = ((𝐹𝑚)‘𝑤))
112106, 111syl 17 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))‘𝑚) = ((𝐹𝑚)‘𝑤))
1136adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → 𝐹:𝑍⟶(ℂ ↑m 𝑆))
114113ffvelrnda 6848 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑛𝑍) → (𝐹𝑛) ∈ (ℂ ↑m 𝑆))
115 elmapi 8444 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑛) ∈ (ℂ ↑m 𝑆) → (𝐹𝑛):𝑆⟶ℂ)
116114, 115syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑛𝑍) → (𝐹𝑛):𝑆⟶ℂ)
117116ffvelrnda 6848 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑛𝑍) ∧ 𝑦𝑆) → ((𝐹𝑛)‘𝑦) ∈ ℂ)
118117an32s 651 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) ∧ 𝑛𝑍) → ((𝐹𝑛)‘𝑦) ∈ ℂ)
119118fmpttd 6876 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)):𝑍⟶ℂ)
120119ffvelrnda 6848 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) ∧ 𝑞𝑍) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) ∈ ℂ)
121 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = 𝑦 → ((𝐹𝑘)‘𝑧) = ((𝐹𝑘)‘𝑦))
122 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑧 = 𝑦 → ((𝐹𝑗)‘𝑧) = ((𝐹𝑗)‘𝑦))
123121, 122oveq12d 7174 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧 = 𝑦 → (((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧)) = (((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦)))
124123fveq2d 6667 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑦 → (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) = (abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))))
125124breq1d 5046 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 = 𝑦 → ((abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 ↔ (abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
126125rspcv 3538 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦𝑆 → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 → (abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
127126ralimdv 3109 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦𝑆 → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 → ∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
128127reximdv 3197 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝑆 → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
129128ralimdv 3109 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝑆 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
130129impcom 411 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥𝑦𝑆) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥)
131130adantll 713 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥)
132 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑞 = 𝑘 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) = ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘))
133132fvoveq1d 7178 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑞 = 𝑘 → (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) = (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))))
134133breq1d 5046 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑞 = 𝑘 → ((abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟))
135134cbvralvw 3361 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∀𝑘 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟)
136 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑝 = 𝑗 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝) = ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))
137136oveq2d 7172 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑝 = 𝑗 → (((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝)) = (((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗)))
138137fveq2d 6667 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑝 = 𝑗 → (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) = (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))))
139138breq1d 5046 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 = 𝑗 → ((abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟))
14090, 139raleqbidv 3319 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑝 = 𝑗 → (∀𝑘 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟))
141135, 140syl5bb 286 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑝 = 𝑗 → (∀𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟))
142141cbvrexvw 3362 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑝𝑍𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟)
143 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
144143fveq1d 6665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑘 → ((𝐹𝑛)‘𝑦) = ((𝐹𝑘)‘𝑦))
145 eqid 2758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) = (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))
146 fvex 6676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐹𝑘)‘𝑦) ∈ V
147144, 145, 146fvmpt 6764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘𝑍 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) = ((𝐹𝑘)‘𝑦))
14837, 147syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) = ((𝐹𝑘)‘𝑦))
149 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = 𝑗 → (𝐹𝑛) = (𝐹𝑗))
150149fveq1d 6665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 𝑗 → ((𝐹𝑛)‘𝑦) = ((𝐹𝑗)‘𝑦))
151 fvex 6676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐹𝑗)‘𝑦) ∈ V
152150, 145, 151fvmpt 6764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗𝑍 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗) = ((𝐹𝑗)‘𝑦))
153152adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗) = ((𝐹𝑗)‘𝑦))
154148, 153oveq12d 7174 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → (((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗)) = (((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦)))
155154fveq2d 6667 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → (abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) = (abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))))
156155breq1d 5046 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → ((abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟 ↔ (abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟))
157156ralbidva 3125 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗𝑍 → (∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟 ↔ ∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟))
158157rexbiia 3174 . . . . . . . . . . . . . . . . . . . . . . 23 (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑘) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑗))) < 𝑟 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟)
159142, 158bitri 278 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑝𝑍𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟)
160 breq2 5040 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑟 = 𝑥 → ((abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟 ↔ (abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
161160ralbidv 3126 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑟 = 𝑥 → (∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟 ↔ ∀𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
162161rexbidv 3221 . . . . . . . . . . . . . . . . . . . . . 22 (𝑟 = 𝑥 → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑟 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
163159, 162syl5bb 286 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 = 𝑥 → (∃𝑝𝑍𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥))
164163cbvralvw 3361 . . . . . . . . . . . . . . . . . . . 20 (∀𝑟 ∈ ℝ+𝑝𝑍𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟 ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)(abs‘(((𝐹𝑘)‘𝑦) − ((𝐹𝑗)‘𝑦))) < 𝑥)
165131, 164sylibr 237 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → ∀𝑟 ∈ ℝ+𝑝𝑍𝑞 ∈ (ℤ𝑝)(abs‘(((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑞) − ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))‘𝑝))) < 𝑟)
1663fvexi 6677 . . . . . . . . . . . . . . . . . . . . 21 𝑍 ∈ V
167166mptex 6983 . . . . . . . . . . . . . . . . . . . 20 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ V
168167a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ V)
1693, 120, 165, 168caucvg 15096 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ dom ⇝ )
170169ralrimiva 3113 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → ∀𝑦𝑆 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ dom ⇝ )
171170ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) → ∀𝑦𝑆 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ dom ⇝ )
172 fveq2 6663 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑤 → ((𝐹𝑛)‘𝑦) = ((𝐹𝑛)‘𝑤))
173172mpteq2dv 5132 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑤 → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) = (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)))
174173eleq1d 2836 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑤 → ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ dom ⇝ ↔ (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ∈ dom ⇝ ))
175174rspccva 3542 . . . . . . . . . . . . . . . 16 ((∀𝑦𝑆 (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ dom ⇝ ∧ 𝑤𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ∈ dom ⇝ )
176171, 175sylan 583 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ∈ dom ⇝ )
177 climdm 14972 . . . . . . . . . . . . . . 15 ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ∈ dom ⇝ ↔ (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ⇝ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))
178176, 177sylib 221 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ⇝ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))
17998, 101, 103, 112, 178climi2 14929 . . . . . . . . . . . . 13 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → ∃𝑣 ∈ (ℤ𝑞)∀𝑚 ∈ (ℤ𝑣)(abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2))
18098r19.29uz 14771 . . . . . . . . . . . . . . 15 ((∀𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ ∃𝑣 ∈ (ℤ𝑞)∀𝑚 ∈ (ℤ𝑣)(abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → ∃𝑣 ∈ (ℤ𝑞)∀𝑚 ∈ (ℤ𝑣)((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)))
18198r19.2uz 14772 . . . . . . . . . . . . . . 15 (∃𝑣 ∈ (ℤ𝑞)∀𝑚 ∈ (ℤ𝑣)((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → ∃𝑚 ∈ (ℤ𝑞)((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)))
182180, 181syl 17 . . . . . . . . . . . . . 14 ((∀𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ ∃𝑣 ∈ (ℤ𝑞)∀𝑚 ∈ (ℤ𝑣)(abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → ∃𝑚 ∈ (ℤ𝑞)((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)))
1836ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) → 𝐹:𝑍⟶(ℂ ↑m 𝑆))
184183ffvelrnda 6848 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) → (𝐹𝑞) ∈ (ℂ ↑m 𝑆))
185 elmapi 8444 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑞) ∈ (ℂ ↑m 𝑆) → (𝐹𝑞):𝑆⟶ℂ)
186184, 185syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) → (𝐹𝑞):𝑆⟶ℂ)
187186ffvelrnda 6848 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → ((𝐹𝑞)‘𝑤) ∈ ℂ)
188187adantr 484 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → ((𝐹𝑞)‘𝑤) ∈ ℂ)
189 climcl 14917 . . . . . . . . . . . . . . . . . 18 ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤)) ⇝ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))) → ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))) ∈ ℂ)
190178, 189syl 17 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))) ∈ ℂ)
191190adantr 484 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))) ∈ ℂ)
1926ad5antr 733 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → 𝐹:𝑍⟶(ℂ ↑m 𝑆))
193192, 106ffvelrnd 6849 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → (𝐹𝑚) ∈ (ℂ ↑m 𝑆))
194 elmapi 8444 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑚) ∈ (ℂ ↑m 𝑆) → (𝐹𝑚):𝑆⟶ℂ)
195193, 194syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → (𝐹𝑚):𝑆⟶ℂ)
196 simplr 768 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → 𝑤𝑆)
197195, 196ffvelrnd 6849 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → ((𝐹𝑚)‘𝑤) ∈ ℂ)
198 rpre 12451 . . . . . . . . . . . . . . . . 17 (𝑟 ∈ ℝ+𝑟 ∈ ℝ)
199198ad4antlr 732 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → 𝑟 ∈ ℝ)
200 abs3lem 14759 . . . . . . . . . . . . . . . 16 (((((𝐹𝑞)‘𝑤) ∈ ℂ ∧ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))) ∈ ℂ) ∧ (((𝐹𝑚)‘𝑤) ∈ ℂ ∧ 𝑟 ∈ ℝ)) → (((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
201188, 191, 197, 199, 200syl22anc 837 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) ∧ 𝑚 ∈ (ℤ𝑞)) → (((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
202201rexlimdva 3208 . . . . . . . . . . . . . 14 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → (∃𝑚 ∈ (ℤ𝑞)((abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
203182, 202syl5 34 . . . . . . . . . . . . 13 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → ((∀𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) ∧ ∃𝑣 ∈ (ℤ𝑞)∀𝑚 ∈ (ℤ𝑣)(abs‘(((𝐹𝑚)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < (𝑟 / 2)) → (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
204179, 203mpan2d 693 . . . . . . . . . . . 12 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) ∧ 𝑤𝑆) → (∀𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) → (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
205204ralimdva 3108 . . . . . . . . . . 11 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑞𝑍) → (∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) → ∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
20697, 205sylan2 595 . . . . . . . . . 10 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ (𝑝𝑍𝑞 ∈ (ℤ𝑝))) → (∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) → ∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
207206anassrs 471 . . . . . . . . 9 (((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑝𝑍) ∧ 𝑞 ∈ (ℤ𝑝)) → (∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) → ∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
208207ralimdva 3108 . . . . . . . 8 ((((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑝𝑍) → (∀𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) → ∀𝑞 ∈ (ℤ𝑝)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
209208reximdva 3198 . . . . . . 7 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) → (∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆𝑚 ∈ (ℤ𝑞)(abs‘(((𝐹𝑞)‘𝑤) − ((𝐹𝑚)‘𝑤))) < (𝑟 / 2) → ∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
21096, 209mpd 15 . . . . . 6 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑟 ∈ ℝ+) → ∃𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟)
211210ralrimiva 3113 . . . . 5 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → ∀𝑟 ∈ ℝ+𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟)
2124adantr 484 . . . . . 6 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → 𝑀 ∈ ℤ)
213 eqidd 2759 . . . . . 6 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ (𝑞𝑍𝑤𝑆)) → ((𝐹𝑞)‘𝑤) = ((𝐹𝑞)‘𝑤))
214173fveq2d 6667 . . . . . . . 8 (𝑦 = 𝑤 → ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))) = ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))
215 eqid 2758 . . . . . . . 8 (𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)))) = (𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))))
216 fvex 6676 . . . . . . . 8 ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))) ∈ V
217214, 215, 216fvmpt 6764 . . . . . . 7 (𝑤𝑆 → ((𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))))‘𝑤) = ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))
218217adantl 485 . . . . . 6 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑤𝑆) → ((𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))))‘𝑤) = ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))
219 climdm 14972 . . . . . . . . 9 ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ∈ dom ⇝ ↔ (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ⇝ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))))
220169, 219sylib 221 . . . . . . . 8 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → (𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ⇝ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))))
221 climcl 14917 . . . . . . . 8 ((𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)) ⇝ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))) → ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))) ∈ ℂ)
222220, 221syl 17 . . . . . . 7 (((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) ∧ 𝑦𝑆) → ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))) ∈ ℂ)
223222fmpttd 6876 . . . . . 6 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → (𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)))):𝑆⟶ℂ)
22465adantr 484 . . . . . 6 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → 𝑆𝑉)
2253, 212, 113, 213, 218, 223, 224ulm2 25092 . . . . 5 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → (𝐹(⇝𝑢𝑆)(𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)))) ↔ ∀𝑟 ∈ ℝ+𝑝𝑍𝑞 ∈ (ℤ𝑝)∀𝑤𝑆 (abs‘(((𝐹𝑞)‘𝑤) − ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑤))))) < 𝑟))
226211, 225mpbird 260 . . . 4 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → 𝐹(⇝𝑢𝑆)(𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦)))))
227 releldm 5790 . . . 4 ((Rel (⇝𝑢𝑆) ∧ 𝐹(⇝𝑢𝑆)(𝑦𝑆 ↦ ( ⇝ ‘(𝑛𝑍 ↦ ((𝐹𝑛)‘𝑦))))) → 𝐹 ∈ dom (⇝𝑢𝑆))
22864, 226, 227sylancr 590 . . 3 ((𝜑 ∧ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥) → 𝐹 ∈ dom (⇝𝑢𝑆))
229228ex 416 . 2 (𝜑 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥𝐹 ∈ dom (⇝𝑢𝑆)))
23063, 229impbid 215 1 (𝜑 → (𝐹 ∈ dom (⇝𝑢𝑆) ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∀wral 3070  ∃wrex 3071  Vcvv 3409   class class class wbr 5036   ↦ cmpt 5116  dom cdm 5528  Rel wrel 5533  ⟶wf 6336  ‘cfv 6340  (class class class)co 7156   ↑m cmap 8422  ℂcc 10586  ℝcr 10587   < clt 10726   − cmin 10921   / cdiv 11348  2c2 11742  ℤcz 12033  ℤ≥cuz 12295  ℝ+crp 12443  abscabs 14654   ⇝ cli 14902  ⇝𝑢culm 25083 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5160  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465  ax-cnex 10644  ax-resscn 10645  ax-1cn 10646  ax-icn 10647  ax-addcl 10648  ax-addrcl 10649  ax-mulcl 10650  ax-mulrcl 10651  ax-mulcom 10652  ax-addass 10653  ax-mulass 10654  ax-distr 10655  ax-i2m1 10656  ax-1ne0 10657  ax-1rid 10658  ax-rnegex 10659  ax-rrecex 10660  ax-cnre 10661  ax-pre-lttri 10662  ax-pre-lttrn 10663  ax-pre-ltadd 10664  ax-pre-mulgt0 10665  ax-pre-sup 10666  ax-addf 10667  ax-mulf 10668 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-iun 4888  df-br 5037  df-opab 5099  df-mpt 5117  df-tr 5143  df-id 5434  df-eprel 5439  df-po 5447  df-so 5448  df-fr 5487  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6131  df-ord 6177  df-on 6178  df-lim 6179  df-suc 6180  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7586  df-1st 7699  df-2nd 7700  df-wrecs 7963  df-recs 8024  df-rdg 8062  df-er 8305  df-map 8424  df-pm 8425  df-en 8541  df-dom 8542  df-sdom 8543  df-sup 8952  df-inf 8953  df-pnf 10728  df-mnf 10729  df-xr 10730  df-ltxr 10731  df-le 10732  df-sub 10923  df-neg 10924  df-div 11349  df-nn 11688  df-2 11750  df-3 11751  df-n0 11948  df-z 12034  df-uz 12296  df-rp 12444  df-ico 12798  df-fl 13224  df-seq 13432  df-exp 13493  df-cj 14519  df-re 14520  df-im 14521  df-sqrt 14655  df-abs 14656  df-limsup 14889  df-clim 14906  df-rlim 14907  df-ulm 25084 This theorem is referenced by:  ulmcau2  25103  mtest  25111
 Copyright terms: Public domain W3C validator