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

Theorem ulmcaulem 24439
Description: Lemma for ulmcau 24440 and ulmcau2 24441: show the equivalence of the four- and five-quantifier forms of the Cauchy convergence condition. Compare cau3 14380. (Contributed by Mario Carneiro, 1-Mar-2015.)
Hypotheses
Ref Expression
ulmcau.z 𝑍 = (ℤ𝑀)
ulmcau.m (𝜑𝑀 ∈ ℤ)
ulmcau.s (𝜑𝑆𝑉)
ulmcau.f (𝜑𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
Assertion
Ref Expression
ulmcaulem (𝜑 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
Distinct variable groups:   𝑗,𝑘,𝑚,𝑥,𝑧,𝐹   𝜑,𝑗,𝑘,𝑚,𝑥,𝑧   𝑆,𝑗,𝑘,𝑚,𝑥,𝑧   𝑗,𝑍,𝑘,𝑚,𝑥,𝑧   𝑗,𝑀,𝑘,𝑧
Allowed substitution hints:   𝑀(𝑥,𝑚)   𝑉(𝑥,𝑧,𝑗,𝑘,𝑚)

Proof of Theorem ulmcaulem
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 breq2 4813 . . . . . 6 (𝑥 = 𝑤 → ((abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 ↔ (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑤))
21ralbidv 3133 . . . . 5 (𝑥 = 𝑤 → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑤))
32rexralbidv 3205 . . . 4 (𝑥 = 𝑤 → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑤))
43cbvralv 3319 . . 3 (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 ↔ ∀𝑤 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑤)
5 rphalfcl 12056 . . . . . . 7 (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ+)
6 breq2 4813 . . . . . . . . . 10 (𝑤 = (𝑥 / 2) → ((abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑤 ↔ (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)))
76ralbidv 3133 . . . . . . . . 9 (𝑤 = (𝑥 / 2) → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑤 ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)))
87rexralbidv 3205 . . . . . . . 8 (𝑤 = (𝑥 / 2) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑤 ↔ ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)))
98rspcv 3457 . . . . . . 7 ((𝑥 / 2) ∈ ℝ+ → (∀𝑤 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)))
105, 9syl 17 . . . . . 6 (𝑥 ∈ ℝ+ → (∀𝑤 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)))
1110adantl 473 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → (∀𝑤 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)))
12 fveq2 6375 . . . . . . . . . . . . 13 (𝑘 = 𝑚 → (𝐹𝑘) = (𝐹𝑚))
1312fveq1d 6377 . . . . . . . . . . . 12 (𝑘 = 𝑚 → ((𝐹𝑘)‘𝑧) = ((𝐹𝑚)‘𝑧))
1413fvoveq1d 6864 . . . . . . . . . . 11 (𝑘 = 𝑚 → (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) = (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))))
1514breq1d 4819 . . . . . . . . . 10 (𝑘 = 𝑚 → ((abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) ↔ (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)))
1615ralbidv 3133 . . . . . . . . 9 (𝑘 = 𝑚 → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)))
1716cbvralv 3319 . . . . . . . 8 (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) ↔ ∀𝑚 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2))
1817biimpi 207 . . . . . . 7 (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) → ∀𝑚 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2))
19 uzss 11907 . . . . . . . . . . . . . . 15 (𝑘 ∈ (ℤ𝑗) → (ℤ𝑘) ⊆ (ℤ𝑗))
2019ad2antlr 718 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)) → (ℤ𝑘) ⊆ (ℤ𝑗))
21 ssralv 3826 . . . . . . . . . . . . . 14 ((ℤ𝑘) ⊆ (ℤ𝑗) → (∀𝑚 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) → ∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)))
2220, 21syl 17 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)) → (∀𝑚 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) → ∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)))
23 r19.26 3211 . . . . . . . . . . . . . . . . 17 (∀𝑧𝑆 ((abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)) ↔ (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)))
24 ulmcau.f . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
2524adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑥 ∈ ℝ+) → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
2625ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑚 ∈ (ℤ𝑘)) → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
27 ulmcau.z . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑍 = (ℤ𝑀)
2827uztrn2 11904 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑗𝑍𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
2928adantll 705 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → 𝑘𝑍)
3027uztrn2 11904 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑘𝑍𝑚 ∈ (ℤ𝑘)) → 𝑚𝑍)
3129, 30sylan 575 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑚 ∈ (ℤ𝑘)) → 𝑚𝑍)
3226, 31ffvelrnd 6550 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑚 ∈ (ℤ𝑘)) → (𝐹𝑚) ∈ (ℂ ↑𝑚 𝑆))
33 elmapi 8082 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑚) ∈ (ℂ ↑𝑚 𝑆) → (𝐹𝑚):𝑆⟶ℂ)
3432, 33syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑚 ∈ (ℤ𝑘)) → (𝐹𝑚):𝑆⟶ℂ)
3534ffvelrnda 6549 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑚 ∈ (ℤ𝑘)) ∧ 𝑧𝑆) → ((𝐹𝑚)‘𝑧) ∈ ℂ)
3625ffvelrnda 6549 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (𝐹𝑗) ∈ (ℂ ↑𝑚 𝑆))
3736ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑚 ∈ (ℤ𝑘)) → (𝐹𝑗) ∈ (ℂ ↑𝑚 𝑆))
38 elmapi 8082 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹𝑗) ∈ (ℂ ↑𝑚 𝑆) → (𝐹𝑗):𝑆⟶ℂ)
3937, 38syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑚 ∈ (ℤ𝑘)) → (𝐹𝑗):𝑆⟶ℂ)
4039ffvelrnda 6549 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑚 ∈ (ℤ𝑘)) ∧ 𝑧𝑆) → ((𝐹𝑗)‘𝑧) ∈ ℂ)
4135, 40abssubd 14477 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑚 ∈ (ℤ𝑘)) ∧ 𝑧𝑆) → (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) = (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑚)‘𝑧))))
4241breq1d 4819 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑚 ∈ (ℤ𝑘)) ∧ 𝑧𝑆) → ((abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) ↔ (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑥 / 2)))
4342biimpd 220 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑚 ∈ (ℤ𝑘)) ∧ 𝑧𝑆) → ((abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) → (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑥 / 2)))
44 ffvelrn 6547 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹:𝑍⟶(ℂ ↑𝑚 𝑆) ∧ 𝑘𝑍) → (𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆))
4525, 28, 44syl2an 589 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆))
4645anassrs 459 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆))
4746adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑚 ∈ (ℤ𝑘)) → (𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆))
48 elmapi 8082 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆) → (𝐹𝑘):𝑆⟶ℂ)
4947, 48syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑚 ∈ (ℤ𝑘)) → (𝐹𝑘):𝑆⟶ℂ)
5049ffvelrnda 6549 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑚 ∈ (ℤ𝑘)) ∧ 𝑧𝑆) → ((𝐹𝑘)‘𝑧) ∈ ℂ)
51 rpre 12036 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
5251ad2antlr 718 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → 𝑥 ∈ ℝ)
5352ad3antrrr 721 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑚 ∈ (ℤ𝑘)) ∧ 𝑧𝑆) → 𝑥 ∈ ℝ)
54 abs3lem 14363 . . . . . . . . . . . . . . . . . . . 20 (((((𝐹𝑘)‘𝑧) ∈ ℂ ∧ ((𝐹𝑚)‘𝑧) ∈ ℂ) ∧ (((𝐹𝑗)‘𝑧) ∈ ℂ ∧ 𝑥 ∈ ℝ)) → (((abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑥 / 2)) → (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
5550, 35, 40, 53, 54syl22anc 867 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑚 ∈ (ℤ𝑘)) ∧ 𝑧𝑆) → (((abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑚)‘𝑧))) < (𝑥 / 2)) → (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
5643, 55sylan2d 598 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑚 ∈ (ℤ𝑘)) ∧ 𝑧𝑆) → (((abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)) → (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
5756ralimdva 3109 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑚 ∈ (ℤ𝑘)) → (∀𝑧𝑆 ((abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) ∧ (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)) → ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
5823, 57syl5bir 234 . . . . . . . . . . . . . . . 16 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑚 ∈ (ℤ𝑘)) → ((∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)) → ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
5958expdimp 444 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑚 ∈ (ℤ𝑘)) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)) → (∀𝑧𝑆 (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) → ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
6059an32s 642 . . . . . . . . . . . . . 14 ((((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)) ∧ 𝑚 ∈ (ℤ𝑘)) → (∀𝑧𝑆 (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) → ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
6160ralimdva 3109 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)) → (∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) → ∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
6222, 61syld 47 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)) → (∀𝑚 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) → ∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
6362impancom 443 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ ∀𝑚 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)) → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) → ∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
6463an32s 642 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ ∀𝑚 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)) ∧ 𝑘 ∈ (ℤ𝑗)) → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) → ∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
6564ralimdva 3109 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) ∧ ∀𝑚 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2)) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
6665ex 401 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑚 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥)))
6766com23 86 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) → (∀𝑚 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑚)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥)))
6818, 67mpdi 45 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) → ∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
6968reximdva 3163 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < (𝑥 / 2) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
7011, 69syld 47 . . . 4 ((𝜑𝑥 ∈ ℝ+) → (∀𝑤 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑤 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
7170ralrimdva 3116 . . 3 (𝜑 → (∀𝑤 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑤 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
724, 71syl5bi 233 . 2 (𝜑 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
73 eluzelz 11896 . . . . . . . . 9 (𝑗 ∈ (ℤ𝑀) → 𝑗 ∈ ℤ)
7473, 27eleq2s 2862 . . . . . . . 8 (𝑗𝑍𝑗 ∈ ℤ)
75 uzid 11901 . . . . . . . 8 (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ𝑗))
7674, 75syl 17 . . . . . . 7 (𝑗𝑍𝑗 ∈ (ℤ𝑗))
7776adantl 473 . . . . . 6 ((𝜑𝑗𝑍) → 𝑗 ∈ (ℤ𝑗))
78 fveq2 6375 . . . . . . . 8 (𝑘 = 𝑗 → (ℤ𝑘) = (ℤ𝑗))
79 fveq2 6375 . . . . . . . . . . . 12 (𝑘 = 𝑗 → (𝐹𝑘) = (𝐹𝑗))
8079fveq1d 6377 . . . . . . . . . . 11 (𝑘 = 𝑗 → ((𝐹𝑘)‘𝑧) = ((𝐹𝑗)‘𝑧))
8180fvoveq1d 6864 . . . . . . . . . 10 (𝑘 = 𝑗 → (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) = (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑚)‘𝑧))))
8281breq1d 4819 . . . . . . . . 9 (𝑘 = 𝑗 → ((abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
8382ralbidv 3133 . . . . . . . 8 (𝑘 = 𝑗 → (∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
8478, 83raleqbidv 3300 . . . . . . 7 (𝑘 = 𝑗 → (∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ ∀𝑚 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
8584rspcv 3457 . . . . . 6 (𝑗 ∈ (ℤ𝑗) → (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 → ∀𝑚 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
8677, 85syl 17 . . . . 5 ((𝜑𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 → ∀𝑚 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
87 fveq2 6375 . . . . . . . . . . . 12 (𝑚 = 𝑘 → (𝐹𝑚) = (𝐹𝑘))
8887fveq1d 6377 . . . . . . . . . . 11 (𝑚 = 𝑘 → ((𝐹𝑚)‘𝑧) = ((𝐹𝑘)‘𝑧))
8988oveq2d 6858 . . . . . . . . . 10 (𝑚 = 𝑘 → (((𝐹𝑗)‘𝑧) − ((𝐹𝑚)‘𝑧)) = (((𝐹𝑗)‘𝑧) − ((𝐹𝑘)‘𝑧)))
9089fveq2d 6379 . . . . . . . . 9 (𝑚 = 𝑘 → (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑚)‘𝑧))) = (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑘)‘𝑧))))
9190breq1d 4819 . . . . . . . 8 (𝑚 = 𝑘 → ((abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑘)‘𝑧))) < 𝑥))
9291ralbidv 3133 . . . . . . 7 (𝑚 = 𝑘 → (∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑘)‘𝑧))) < 𝑥))
9392cbvralv 3319 . . . . . 6 (∀𝑚 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑘)‘𝑧))) < 𝑥)
9424ffvelrnda 6549 . . . . . . . . . . . . 13 ((𝜑𝑗𝑍) → (𝐹𝑗) ∈ (ℂ ↑𝑚 𝑆))
9594adantr 472 . . . . . . . . . . . 12 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑗) ∈ (ℂ ↑𝑚 𝑆))
9695, 38syl 17 . . . . . . . . . . 11 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑗):𝑆⟶ℂ)
9796ffvelrnda 6549 . . . . . . . . . 10 ((((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → ((𝐹𝑗)‘𝑧) ∈ ℂ)
9824, 28, 44syl2an 589 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑗𝑍𝑘 ∈ (ℤ𝑗))) → (𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆))
9998anassrs 459 . . . . . . . . . . . 12 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘) ∈ (ℂ ↑𝑚 𝑆))
10099, 48syl 17 . . . . . . . . . . 11 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (𝐹𝑘):𝑆⟶ℂ)
101100ffvelrnda 6549 . . . . . . . . . 10 ((((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → ((𝐹𝑘)‘𝑧) ∈ ℂ)
10297, 101abssubd 14477 . . . . . . . . 9 ((((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑘)‘𝑧))) = (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))))
103102breq1d 4819 . . . . . . . 8 ((((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) ∧ 𝑧𝑆) → ((abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑘)‘𝑧))) < 𝑥 ↔ (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
104103ralbidva 3132 . . . . . . 7 (((𝜑𝑗𝑍) ∧ 𝑘 ∈ (ℤ𝑗)) → (∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑘)‘𝑧))) < 𝑥 ↔ ∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
105104ralbidva 3132 . . . . . 6 ((𝜑𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑘)‘𝑧))) < 𝑥 ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
10693, 105syl5bb 274 . . . . 5 ((𝜑𝑗𝑍) → (∀𝑚 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑗)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 ↔ ∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
10786, 106sylibd 230 . . . 4 ((𝜑𝑗𝑍) → (∀𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 → ∀𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
108107reximdva 3163 . . 3 (𝜑 → (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
109108ralimdv 3110 . 2 (𝜑 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥 → ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥))
11072, 109impbid 203 1 (𝜑 → (∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑗)‘𝑧))) < 𝑥 ↔ ∀𝑥 ∈ ℝ+𝑗𝑍𝑘 ∈ (ℤ𝑗)∀𝑚 ∈ (ℤ𝑘)∀𝑧𝑆 (abs‘(((𝐹𝑘)‘𝑧) − ((𝐹𝑚)‘𝑧))) < 𝑥))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wral 3055  wrex 3056  wss 3732   class class class wbr 4809  wf 6064  cfv 6068  (class class class)co 6842  𝑚 cmap 8060  cc 10187  cr 10188   < clt 10328  cmin 10520   / cdiv 10938  2c2 11327  cz 11624  cuz 11886  +crp 12028  abscabs 14259
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-er 7947  df-map 8062  df-en 8161  df-dom 8162  df-sdom 8163  df-sup 8555  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-n0 11539  df-z 11625  df-uz 11887  df-rp 12029  df-seq 13009  df-exp 13068  df-cj 14124  df-re 14125  df-im 14126  df-sqrt 14260  df-abs 14261
This theorem is referenced by:  ulmcau  24440  ulmcau2  24441
  Copyright terms: Public domain W3C validator