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

Theorem iscmet3lem1 22812
Description: Lemma for iscmet3 22814. (Contributed by Mario Carneiro, 15-Oct-2015.)
Hypotheses
Ref Expression
iscmet3.1 𝑍 = (ℤ𝑀)
iscmet3.2 𝐽 = (MetOpen‘𝐷)
iscmet3.3 (𝜑𝑀 ∈ ℤ)
iscmet3.4 (𝜑𝐷 ∈ (Met‘𝑋))
iscmet3.6 (𝜑𝐹:𝑍𝑋)
iscmet3.9 (𝜑 → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑆𝑘)∀𝑣 ∈ (𝑆𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘))
iscmet3.10 (𝜑 → ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝐹𝑘) ∈ (𝑆𝑛))
Assertion
Ref Expression
iscmet3lem1 (𝜑𝐹 ∈ (Cau‘𝐷))
Distinct variable groups:   𝑘,𝑛,𝑢,𝑣,𝐷   𝑘,𝐹,𝑛,𝑢,𝑣   𝑘,𝑋,𝑛   𝑘,𝐽,𝑛   𝑆,𝑘,𝑛,𝑢,𝑣   𝑘,𝑍,𝑛   𝑘,𝑀,𝑛   𝜑,𝑘,𝑛
Allowed substitution hints:   𝜑(𝑣,𝑢)   𝐽(𝑣,𝑢)   𝑀(𝑣,𝑢)   𝑋(𝑣,𝑢)   𝑍(𝑣,𝑢)

Proof of Theorem iscmet3lem1
Dummy variables 𝑗 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iscmet3.3 . . . . . 6 (𝜑𝑀 ∈ ℤ)
2 iscmet3.1 . . . . . . 7 𝑍 = (ℤ𝑀)
32iscmet3lem3 22811 . . . . . 6 ((𝑀 ∈ ℤ ∧ 𝑟 ∈ ℝ+) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)((1 / 2)↑𝑘) < 𝑟)
41, 3sylan 486 . . . . 5 ((𝜑𝑟 ∈ ℝ+) → ∃𝑗𝑍𝑘 ∈ (ℤ𝑗)((1 / 2)↑𝑘) < 𝑟)
52r19.2uz 13882 . . . . 5 (∃𝑗𝑍𝑘 ∈ (ℤ𝑗)((1 / 2)↑𝑘) < 𝑟 → ∃𝑘𝑍 ((1 / 2)↑𝑘) < 𝑟)
64, 5syl 17 . . . 4 ((𝜑𝑟 ∈ ℝ+) → ∃𝑘𝑍 ((1 / 2)↑𝑘) < 𝑟)
7 simpl 471 . . . . . . . . . . . . 13 ((𝑘𝑍𝑗 ∈ (ℤ𝑘)) → 𝑘𝑍)
87adantl 480 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → 𝑘𝑍)
98, 2syl6eleq 2694 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → 𝑘 ∈ (ℤ𝑀))
10 eluzfz2 12172 . . . . . . . . . . 11 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ (𝑀...𝑘))
119, 10syl 17 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → 𝑘 ∈ (𝑀...𝑘))
12 iscmet3.10 . . . . . . . . . . . 12 (𝜑 → ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝐹𝑘) ∈ (𝑆𝑛))
1312ad2antrr 757 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → ∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝐹𝑘) ∈ (𝑆𝑛))
14 rsp 2909 . . . . . . . . . . 11 (∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝐹𝑘) ∈ (𝑆𝑛) → (𝑘𝑍 → ∀𝑛 ∈ (𝑀...𝑘)(𝐹𝑘) ∈ (𝑆𝑛)))
1513, 8, 14sylc 62 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → ∀𝑛 ∈ (𝑀...𝑘)(𝐹𝑘) ∈ (𝑆𝑛))
16 fveq2 6085 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (𝑆𝑛) = (𝑆𝑘))
1716eleq2d 2669 . . . . . . . . . . 11 (𝑛 = 𝑘 → ((𝐹𝑘) ∈ (𝑆𝑛) ↔ (𝐹𝑘) ∈ (𝑆𝑘)))
1817rspcv 3274 . . . . . . . . . 10 (𝑘 ∈ (𝑀...𝑘) → (∀𝑛 ∈ (𝑀...𝑘)(𝐹𝑘) ∈ (𝑆𝑛) → (𝐹𝑘) ∈ (𝑆𝑘)))
1911, 15, 18sylc 62 . . . . . . . . 9 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → (𝐹𝑘) ∈ (𝑆𝑘))
20 simprr 791 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → 𝑗 ∈ (ℤ𝑘))
21 elfzuzb 12159 . . . . . . . . . . 11 (𝑘 ∈ (𝑀...𝑗) ↔ (𝑘 ∈ (ℤ𝑀) ∧ 𝑗 ∈ (ℤ𝑘)))
229, 20, 21sylanbrc 694 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → 𝑘 ∈ (𝑀...𝑗))
232uztrn2 11534 . . . . . . . . . . . 12 ((𝑘𝑍𝑗 ∈ (ℤ𝑘)) → 𝑗𝑍)
2423adantl 480 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → 𝑗𝑍)
25 oveq2 6532 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → (𝑀...𝑘) = (𝑀...𝑗))
26 fveq2 6085 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → (𝐹𝑘) = (𝐹𝑗))
2726eleq1d 2668 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → ((𝐹𝑘) ∈ (𝑆𝑛) ↔ (𝐹𝑗) ∈ (𝑆𝑛)))
2825, 27raleqbidv 3125 . . . . . . . . . . . 12 (𝑘 = 𝑗 → (∀𝑛 ∈ (𝑀...𝑘)(𝐹𝑘) ∈ (𝑆𝑛) ↔ ∀𝑛 ∈ (𝑀...𝑗)(𝐹𝑗) ∈ (𝑆𝑛)))
2928rspcv 3274 . . . . . . . . . . 11 (𝑗𝑍 → (∀𝑘𝑍𝑛 ∈ (𝑀...𝑘)(𝐹𝑘) ∈ (𝑆𝑛) → ∀𝑛 ∈ (𝑀...𝑗)(𝐹𝑗) ∈ (𝑆𝑛)))
3024, 13, 29sylc 62 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → ∀𝑛 ∈ (𝑀...𝑗)(𝐹𝑗) ∈ (𝑆𝑛))
3116eleq2d 2669 . . . . . . . . . . 11 (𝑛 = 𝑘 → ((𝐹𝑗) ∈ (𝑆𝑛) ↔ (𝐹𝑗) ∈ (𝑆𝑘)))
3231rspcv 3274 . . . . . . . . . 10 (𝑘 ∈ (𝑀...𝑗) → (∀𝑛 ∈ (𝑀...𝑗)(𝐹𝑗) ∈ (𝑆𝑛) → (𝐹𝑗) ∈ (𝑆𝑘)))
3322, 30, 32sylc 62 . . . . . . . . 9 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → (𝐹𝑗) ∈ (𝑆𝑘))
34 iscmet3.9 . . . . . . . . . . 11 (𝜑 → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑆𝑘)∀𝑣 ∈ (𝑆𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘))
3534ad2antrr 757 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑆𝑘)∀𝑣 ∈ (𝑆𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘))
36 eluzelz 11526 . . . . . . . . . . . 12 (𝑘 ∈ (ℤ𝑀) → 𝑘 ∈ ℤ)
3736, 2eleq2s 2702 . . . . . . . . . . 11 (𝑘𝑍𝑘 ∈ ℤ)
3837ad2antrl 759 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → 𝑘 ∈ ℤ)
39 rsp 2909 . . . . . . . . . 10 (∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑆𝑘)∀𝑣 ∈ (𝑆𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘) → (𝑘 ∈ ℤ → ∀𝑢 ∈ (𝑆𝑘)∀𝑣 ∈ (𝑆𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)))
4035, 38, 39sylc 62 . . . . . . . . 9 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → ∀𝑢 ∈ (𝑆𝑘)∀𝑣 ∈ (𝑆𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘))
41 oveq1 6531 . . . . . . . . . . 11 (𝑢 = (𝐹𝑘) → (𝑢𝐷𝑣) = ((𝐹𝑘)𝐷𝑣))
4241breq1d 4584 . . . . . . . . . 10 (𝑢 = (𝐹𝑘) → ((𝑢𝐷𝑣) < ((1 / 2)↑𝑘) ↔ ((𝐹𝑘)𝐷𝑣) < ((1 / 2)↑𝑘)))
43 oveq2 6532 . . . . . . . . . . 11 (𝑣 = (𝐹𝑗) → ((𝐹𝑘)𝐷𝑣) = ((𝐹𝑘)𝐷(𝐹𝑗)))
4443breq1d 4584 . . . . . . . . . 10 (𝑣 = (𝐹𝑗) → (((𝐹𝑘)𝐷𝑣) < ((1 / 2)↑𝑘) ↔ ((𝐹𝑘)𝐷(𝐹𝑗)) < ((1 / 2)↑𝑘)))
4542, 44rspc2va 3290 . . . . . . . . 9 ((((𝐹𝑘) ∈ (𝑆𝑘) ∧ (𝐹𝑗) ∈ (𝑆𝑘)) ∧ ∀𝑢 ∈ (𝑆𝑘)∀𝑣 ∈ (𝑆𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)) → ((𝐹𝑘)𝐷(𝐹𝑗)) < ((1 / 2)↑𝑘))
4619, 33, 40, 45syl21anc 1316 . . . . . . . 8 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → ((𝐹𝑘)𝐷(𝐹𝑗)) < ((1 / 2)↑𝑘))
47 iscmet3.4 . . . . . . . . . . 11 (𝜑𝐷 ∈ (Met‘𝑋))
4847ad2antrr 757 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → 𝐷 ∈ (Met‘𝑋))
49 iscmet3.6 . . . . . . . . . . . 12 (𝜑𝐹:𝑍𝑋)
5049adantr 479 . . . . . . . . . . 11 ((𝜑𝑟 ∈ ℝ+) → 𝐹:𝑍𝑋)
51 ffvelrn 6247 . . . . . . . . . . 11 ((𝐹:𝑍𝑋𝑘𝑍) → (𝐹𝑘) ∈ 𝑋)
5250, 7, 51syl2an 492 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → (𝐹𝑘) ∈ 𝑋)
53 ffvelrn 6247 . . . . . . . . . . 11 ((𝐹:𝑍𝑋𝑗𝑍) → (𝐹𝑗) ∈ 𝑋)
5450, 23, 53syl2an 492 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → (𝐹𝑗) ∈ 𝑋)
55 metcl 21885 . . . . . . . . . 10 ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹𝑘) ∈ 𝑋 ∧ (𝐹𝑗) ∈ 𝑋) → ((𝐹𝑘)𝐷(𝐹𝑗)) ∈ ℝ)
5648, 52, 54, 55syl3anc 1317 . . . . . . . . 9 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → ((𝐹𝑘)𝐷(𝐹𝑗)) ∈ ℝ)
57 1rp 11665 . . . . . . . . . . . 12 1 ∈ ℝ+
58 rphalfcl 11687 . . . . . . . . . . . 12 (1 ∈ ℝ+ → (1 / 2) ∈ ℝ+)
5957, 58ax-mp 5 . . . . . . . . . . 11 (1 / 2) ∈ ℝ+
60 rpexpcl 12693 . . . . . . . . . . 11 (((1 / 2) ∈ ℝ+𝑘 ∈ ℤ) → ((1 / 2)↑𝑘) ∈ ℝ+)
6159, 38, 60sylancr 693 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → ((1 / 2)↑𝑘) ∈ ℝ+)
6261rpred 11701 . . . . . . . . 9 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → ((1 / 2)↑𝑘) ∈ ℝ)
63 rpre 11668 . . . . . . . . . 10 (𝑟 ∈ ℝ+𝑟 ∈ ℝ)
6463ad2antlr 758 . . . . . . . . 9 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → 𝑟 ∈ ℝ)
65 lttr 9962 . . . . . . . . 9 ((((𝐹𝑘)𝐷(𝐹𝑗)) ∈ ℝ ∧ ((1 / 2)↑𝑘) ∈ ℝ ∧ 𝑟 ∈ ℝ) → ((((𝐹𝑘)𝐷(𝐹𝑗)) < ((1 / 2)↑𝑘) ∧ ((1 / 2)↑𝑘) < 𝑟) → ((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑟))
6656, 62, 64, 65syl3anc 1317 . . . . . . . 8 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → ((((𝐹𝑘)𝐷(𝐹𝑗)) < ((1 / 2)↑𝑘) ∧ ((1 / 2)↑𝑘) < 𝑟) → ((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑟))
6746, 66mpand 706 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘𝑍𝑗 ∈ (ℤ𝑘))) → (((1 / 2)↑𝑘) < 𝑟 → ((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑟))
6867anassrs 677 . . . . . 6 ((((𝜑𝑟 ∈ ℝ+) ∧ 𝑘𝑍) ∧ 𝑗 ∈ (ℤ𝑘)) → (((1 / 2)↑𝑘) < 𝑟 → ((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑟))
6968ralrimdva 2948 . . . . 5 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑘𝑍) → (((1 / 2)↑𝑘) < 𝑟 → ∀𝑗 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑟))
7069reximdva 2996 . . . 4 ((𝜑𝑟 ∈ ℝ+) → (∃𝑘𝑍 ((1 / 2)↑𝑘) < 𝑟 → ∃𝑘𝑍𝑗 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑟))
716, 70mpd 15 . . 3 ((𝜑𝑟 ∈ ℝ+) → ∃𝑘𝑍𝑗 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑟)
7271ralrimiva 2945 . 2 (𝜑 → ∀𝑟 ∈ ℝ+𝑘𝑍𝑗 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑟)
73 metxmet 21887 . . . 4 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
7447, 73syl 17 . . 3 (𝜑𝐷 ∈ (∞Met‘𝑋))
75 eqidd 2607 . . 3 ((𝜑𝑗𝑍) → (𝐹𝑗) = (𝐹𝑗))
76 eqidd 2607 . . 3 ((𝜑𝑘𝑍) → (𝐹𝑘) = (𝐹𝑘))
772, 74, 1, 75, 76, 49iscauf 22801 . 2 (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ ∀𝑟 ∈ ℝ+𝑘𝑍𝑗 ∈ (ℤ𝑘)((𝐹𝑘)𝐷(𝐹𝑗)) < 𝑟))
7872, 77mpbird 245 1 (𝜑𝐹 ∈ (Cau‘𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976  wral 2892  wrex 2893   class class class wbr 4574  wf 5783  cfv 5787  (class class class)co 6524  cr 9788  1c1 9790   < clt 9927   / cdiv 10530  2c2 10914  cz 11207  cuz 11516  +crp 11661  ...cfz 12149  cexp 12674  ∞Metcxmt 19495  Metcme 19496  MetOpencmopn 19500  Caucca 22774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-cnex 9845  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865  ax-pre-mulgt0 9866  ax-pre-sup 9867
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-om 6932  df-1st 7033  df-2nd 7034  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-er 7603  df-map 7720  df-pm 7721  df-en 7816  df-dom 7817  df-sdom 7818  df-sup 8205  df-inf 8206  df-pnf 9929  df-mnf 9930  df-xr 9931  df-ltxr 9932  df-le 9933  df-sub 10116  df-neg 10117  df-div 10531  df-nn 10865  df-2 10923  df-3 10924  df-n0 11137  df-z 11208  df-uz 11517  df-rp 11662  df-xneg 11775  df-xadd 11776  df-fz 12150  df-fl 12407  df-seq 12616  df-exp 12675  df-cj 13630  df-re 13631  df-im 13632  df-sqrt 13766  df-abs 13767  df-clim 14010  df-rlim 14011  df-psmet 19502  df-xmet 19503  df-met 19504  df-bl 19505  df-cau 22777
This theorem is referenced by:  iscmet3  22814
  Copyright terms: Public domain W3C validator