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

Theorem lebnumii 22521
Description: Specialize the Lebesgue number lemma lebnum 22519 to the unit interval. (Contributed by Mario Carneiro, 14-Feb-2015.)
Assertion
Ref Expression
lebnumii ((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑢𝑈 (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑢)
Distinct variable group:   𝑘,𝑛,𝑢,𝑈

Proof of Theorem lebnumii
Dummy variables 𝑟 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ii 22436 . . 3 II = (MetOpen‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))
2 cnmet 22333 . . . . 5 (abs ∘ − ) ∈ (Met‘ℂ)
3 unitssre 12149 . . . . . 6 (0[,]1) ⊆ ℝ
4 ax-resscn 9850 . . . . . 6 ℝ ⊆ ℂ
53, 4sstri 3577 . . . . 5 (0[,]1) ⊆ ℂ
6 metres2 21926 . . . . 5 (((abs ∘ − ) ∈ (Met‘ℂ) ∧ (0[,]1) ⊆ ℂ) → ((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))) ∈ (Met‘(0[,]1)))
72, 5, 6mp2an 704 . . . 4 ((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))) ∈ (Met‘(0[,]1))
87a1i 11 . . 3 ((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) → ((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))) ∈ (Met‘(0[,]1)))
9 iicmp 22445 . . . 4 II ∈ Comp
109a1i 11 . . 3 ((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) → II ∈ Comp)
11 simpl 472 . . 3 ((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) → 𝑈 ⊆ II)
12 simpr 476 . . 3 ((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) → (0[,]1) = 𝑈)
131, 8, 10, 11, 12lebnum 22519 . 2 ((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) → ∃𝑟 ∈ ℝ+𝑥 ∈ (0[,]1)∃𝑢𝑈 (𝑥(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) ⊆ 𝑢)
14 rpreccl 11692 . . . . . . . 8 (𝑟 ∈ ℝ+ → (1 / 𝑟) ∈ ℝ+)
1514adantl 481 . . . . . . 7 (((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) → (1 / 𝑟) ∈ ℝ+)
1615rpred 11707 . . . . . 6 (((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) → (1 / 𝑟) ∈ ℝ)
1715rpge0d 11711 . . . . . 6 (((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) → 0 ≤ (1 / 𝑟))
18 flge0nn0 12441 . . . . . 6 (((1 / 𝑟) ∈ ℝ ∧ 0 ≤ (1 / 𝑟)) → (⌊‘(1 / 𝑟)) ∈ ℕ0)
1916, 17, 18syl2anc 691 . . . . 5 (((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) → (⌊‘(1 / 𝑟)) ∈ ℕ0)
20 nn0p1nn 11182 . . . . 5 ((⌊‘(1 / 𝑟)) ∈ ℕ0 → ((⌊‘(1 / 𝑟)) + 1) ∈ ℕ)
2119, 20syl 17 . . . 4 (((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) → ((⌊‘(1 / 𝑟)) + 1) ∈ ℕ)
22 elfznn 12199 . . . . . . . . . . . 12 (𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1)) → 𝑘 ∈ ℕ)
2322adantl 481 . . . . . . . . . . 11 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → 𝑘 ∈ ℕ)
2423nnrpd 11705 . . . . . . . . . 10 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → 𝑘 ∈ ℝ+)
2521adantr 480 . . . . . . . . . . 11 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((⌊‘(1 / 𝑟)) + 1) ∈ ℕ)
2625nnrpd 11705 . . . . . . . . . 10 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((⌊‘(1 / 𝑟)) + 1) ∈ ℝ+)
2724, 26rpdivcld 11724 . . . . . . . . 9 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (𝑘 / ((⌊‘(1 / 𝑟)) + 1)) ∈ ℝ+)
2827rpred 11707 . . . . . . . 8 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (𝑘 / ((⌊‘(1 / 𝑟)) + 1)) ∈ ℝ)
2927rpge0d 11711 . . . . . . . 8 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → 0 ≤ (𝑘 / ((⌊‘(1 / 𝑟)) + 1)))
30 elfzle2 12174 . . . . . . . . . . 11 (𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1)) → 𝑘 ≤ ((⌊‘(1 / 𝑟)) + 1))
3130adantl 481 . . . . . . . . . 10 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → 𝑘 ≤ ((⌊‘(1 / 𝑟)) + 1))
3225nnred 10885 . . . . . . . . . . . 12 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((⌊‘(1 / 𝑟)) + 1) ∈ ℝ)
3332recnd 9925 . . . . . . . . . . 11 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((⌊‘(1 / 𝑟)) + 1) ∈ ℂ)
3433mulid1d 9914 . . . . . . . . . 10 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (((⌊‘(1 / 𝑟)) + 1) · 1) = ((⌊‘(1 / 𝑟)) + 1))
3531, 34breqtrrd 4606 . . . . . . . . 9 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → 𝑘 ≤ (((⌊‘(1 / 𝑟)) + 1) · 1))
3623nnred 10885 . . . . . . . . . 10 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → 𝑘 ∈ ℝ)
37 1re 9896 . . . . . . . . . . 11 1 ∈ ℝ
3837a1i 11 . . . . . . . . . 10 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → 1 ∈ ℝ)
3925nngt0d 10914 . . . . . . . . . 10 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → 0 < ((⌊‘(1 / 𝑟)) + 1))
40 ledivmul 10751 . . . . . . . . . 10 ((𝑘 ∈ ℝ ∧ 1 ∈ ℝ ∧ (((⌊‘(1 / 𝑟)) + 1) ∈ ℝ ∧ 0 < ((⌊‘(1 / 𝑟)) + 1))) → ((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) ≤ 1 ↔ 𝑘 ≤ (((⌊‘(1 / 𝑟)) + 1) · 1)))
4136, 38, 32, 39, 40syl112anc 1322 . . . . . . . . 9 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) ≤ 1 ↔ 𝑘 ≤ (((⌊‘(1 / 𝑟)) + 1) · 1)))
4235, 41mpbird 246 . . . . . . . 8 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (𝑘 / ((⌊‘(1 / 𝑟)) + 1)) ≤ 1)
43 0re 9897 . . . . . . . . 9 0 ∈ ℝ
4443, 37elicc2i 12069 . . . . . . . 8 ((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) ∈ (0[,]1) ↔ ((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) ∈ ℝ ∧ 0 ≤ (𝑘 / ((⌊‘(1 / 𝑟)) + 1)) ∧ (𝑘 / ((⌊‘(1 / 𝑟)) + 1)) ≤ 1))
4528, 29, 42, 44syl3anbrc 1239 . . . . . . 7 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (𝑘 / ((⌊‘(1 / 𝑟)) + 1)) ∈ (0[,]1))
46 oveq1 6534 . . . . . . . . . 10 (𝑥 = (𝑘 / ((⌊‘(1 / 𝑟)) + 1)) → (𝑥(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) = ((𝑘 / ((⌊‘(1 / 𝑟)) + 1))(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟))
4746sseq1d 3595 . . . . . . . . 9 (𝑥 = (𝑘 / ((⌊‘(1 / 𝑟)) + 1)) → ((𝑥(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) ⊆ 𝑢 ↔ ((𝑘 / ((⌊‘(1 / 𝑟)) + 1))(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) ⊆ 𝑢))
4847rexbidv 3034 . . . . . . . 8 (𝑥 = (𝑘 / ((⌊‘(1 / 𝑟)) + 1)) → (∃𝑢𝑈 (𝑥(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) ⊆ 𝑢 ↔ ∃𝑢𝑈 ((𝑘 / ((⌊‘(1 / 𝑟)) + 1))(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) ⊆ 𝑢))
4948rspcv 3278 . . . . . . 7 ((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) ∈ (0[,]1) → (∀𝑥 ∈ (0[,]1)∃𝑢𝑈 (𝑥(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) ⊆ 𝑢 → ∃𝑢𝑈 ((𝑘 / ((⌊‘(1 / 𝑟)) + 1))(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) ⊆ 𝑢))
5045, 49syl 17 . . . . . 6 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (∀𝑥 ∈ (0[,]1)∃𝑢𝑈 (𝑥(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) ⊆ 𝑢 → ∃𝑢𝑈 ((𝑘 / ((⌊‘(1 / 𝑟)) + 1))(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) ⊆ 𝑢))
51 simplr 788 . . . . . . . . . . . . . 14 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → 𝑟 ∈ ℝ+)
5251rpred 11707 . . . . . . . . . . . . 13 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → 𝑟 ∈ ℝ)
5328, 52resubcld 10310 . . . . . . . . . . . 12 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) − 𝑟) ∈ ℝ)
5453rexrd 9946 . . . . . . . . . . 11 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) − 𝑟) ∈ ℝ*)
5528, 52readdcld 9926 . . . . . . . . . . . 12 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) + 𝑟) ∈ ℝ)
5655rexrd 9946 . . . . . . . . . . 11 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) + 𝑟) ∈ ℝ*)
57 nnm1nn0 11184 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → (𝑘 − 1) ∈ ℕ0)
5823, 57syl 17 . . . . . . . . . . . . . 14 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (𝑘 − 1) ∈ ℕ0)
5958nn0red 11202 . . . . . . . . . . . . 13 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (𝑘 − 1) ∈ ℝ)
6059, 25nndivred 10919 . . . . . . . . . . . 12 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1)) ∈ ℝ)
6136recnd 9925 . . . . . . . . . . . . . . 15 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → 𝑘 ∈ ℂ)
6259recnd 9925 . . . . . . . . . . . . . . 15 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (𝑘 − 1) ∈ ℂ)
6325nnne0d 10915 . . . . . . . . . . . . . . 15 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((⌊‘(1 / 𝑟)) + 1) ≠ 0)
6461, 62, 33, 63divsubdird 10692 . . . . . . . . . . . . . 14 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((𝑘 − (𝑘 − 1)) / ((⌊‘(1 / 𝑟)) + 1)) = ((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) − ((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1))))
65 ax-1cn 9851 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
66 nncan 10162 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑘 − (𝑘 − 1)) = 1)
6761, 65, 66sylancl 693 . . . . . . . . . . . . . . 15 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (𝑘 − (𝑘 − 1)) = 1)
6867oveq1d 6542 . . . . . . . . . . . . . 14 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((𝑘 − (𝑘 − 1)) / ((⌊‘(1 / 𝑟)) + 1)) = (1 / ((⌊‘(1 / 𝑟)) + 1)))
6964, 68eqtr3d 2646 . . . . . . . . . . . . 13 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) − ((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1))) = (1 / ((⌊‘(1 / 𝑟)) + 1)))
7051rprecred 11718 . . . . . . . . . . . . . . 15 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (1 / 𝑟) ∈ ℝ)
71 flltp1 12421 . . . . . . . . . . . . . . 15 ((1 / 𝑟) ∈ ℝ → (1 / 𝑟) < ((⌊‘(1 / 𝑟)) + 1))
7270, 71syl 17 . . . . . . . . . . . . . 14 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (1 / 𝑟) < ((⌊‘(1 / 𝑟)) + 1))
73 rpgt0 11679 . . . . . . . . . . . . . . . 16 (𝑟 ∈ ℝ+ → 0 < 𝑟)
7473ad2antlr 759 . . . . . . . . . . . . . . 15 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → 0 < 𝑟)
75 ltdiv23 10766 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ ∧ (𝑟 ∈ ℝ ∧ 0 < 𝑟) ∧ (((⌊‘(1 / 𝑟)) + 1) ∈ ℝ ∧ 0 < ((⌊‘(1 / 𝑟)) + 1))) → ((1 / 𝑟) < ((⌊‘(1 / 𝑟)) + 1) ↔ (1 / ((⌊‘(1 / 𝑟)) + 1)) < 𝑟))
7638, 52, 74, 32, 39, 75syl122anc 1327 . . . . . . . . . . . . . 14 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((1 / 𝑟) < ((⌊‘(1 / 𝑟)) + 1) ↔ (1 / ((⌊‘(1 / 𝑟)) + 1)) < 𝑟))
7772, 76mpbid 221 . . . . . . . . . . . . 13 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (1 / ((⌊‘(1 / 𝑟)) + 1)) < 𝑟)
7869, 77eqbrtrd 4600 . . . . . . . . . . . 12 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) − ((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1))) < 𝑟)
7928, 60, 52, 78ltsub23d 10484 . . . . . . . . . . 11 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) − 𝑟) < ((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1)))
8028, 51ltaddrpd 11740 . . . . . . . . . . 11 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (𝑘 / ((⌊‘(1 / 𝑟)) + 1)) < ((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) + 𝑟))
81 iccssioo 12072 . . . . . . . . . . 11 (((((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) − 𝑟) ∈ ℝ* ∧ ((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) + 𝑟) ∈ ℝ*) ∧ (((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) − 𝑟) < ((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1)) ∧ (𝑘 / ((⌊‘(1 / 𝑟)) + 1)) < ((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) + 𝑟))) → (((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1))[,](𝑘 / ((⌊‘(1 / 𝑟)) + 1))) ⊆ (((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) − 𝑟)(,)((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) + 𝑟)))
8254, 56, 79, 80, 81syl22anc 1319 . . . . . . . . . 10 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1))[,](𝑘 / ((⌊‘(1 / 𝑟)) + 1))) ⊆ (((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) − 𝑟)(,)((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) + 𝑟)))
83 0red 9898 . . . . . . . . . . 11 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → 0 ∈ ℝ)
8458nn0ge0d 11204 . . . . . . . . . . . 12 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → 0 ≤ (𝑘 − 1))
85 divge0 10744 . . . . . . . . . . . 12 ((((𝑘 − 1) ∈ ℝ ∧ 0 ≤ (𝑘 − 1)) ∧ (((⌊‘(1 / 𝑟)) + 1) ∈ ℝ ∧ 0 < ((⌊‘(1 / 𝑟)) + 1))) → 0 ≤ ((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1)))
8659, 84, 32, 39, 85syl22anc 1319 . . . . . . . . . . 11 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → 0 ≤ ((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1)))
87 iccss 12071 . . . . . . . . . . 11 (((0 ∈ ℝ ∧ 1 ∈ ℝ) ∧ (0 ≤ ((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1)) ∧ (𝑘 / ((⌊‘(1 / 𝑟)) + 1)) ≤ 1)) → (((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1))[,](𝑘 / ((⌊‘(1 / 𝑟)) + 1))) ⊆ (0[,]1))
8883, 38, 86, 42, 87syl22anc 1319 . . . . . . . . . 10 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1))[,](𝑘 / ((⌊‘(1 / 𝑟)) + 1))) ⊆ (0[,]1))
8982, 88ssind 3799 . . . . . . . . 9 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1))[,](𝑘 / ((⌊‘(1 / 𝑟)) + 1))) ⊆ ((((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) − 𝑟)(,)((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) + 𝑟)) ∩ (0[,]1)))
90 eqid 2610 . . . . . . . . . . . . 13 ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
9190rexmet 22350 . . . . . . . . . . . 12 ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ)
9291a1i 11 . . . . . . . . . . 11 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ))
93 sseqin2 3779 . . . . . . . . . . . . 13 ((0[,]1) ⊆ ℝ ↔ (ℝ ∩ (0[,]1)) = (0[,]1))
943, 93mpbi 219 . . . . . . . . . . . 12 (ℝ ∩ (0[,]1)) = (0[,]1)
9545, 94syl6eleqr 2699 . . . . . . . . . . 11 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (𝑘 / ((⌊‘(1 / 𝑟)) + 1)) ∈ (ℝ ∩ (0[,]1)))
96 rpxr 11675 . . . . . . . . . . . 12 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
9796ad2antlr 759 . . . . . . . . . . 11 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → 𝑟 ∈ ℝ*)
98 xpss12 5137 . . . . . . . . . . . . . . 15 (((0[,]1) ⊆ ℝ ∧ (0[,]1) ⊆ ℝ) → ((0[,]1) × (0[,]1)) ⊆ (ℝ × ℝ))
993, 3, 98mp2an 704 . . . . . . . . . . . . . 14 ((0[,]1) × (0[,]1)) ⊆ (ℝ × ℝ)
100 resabs1 5334 . . . . . . . . . . . . . 14 (((0[,]1) × (0[,]1)) ⊆ (ℝ × ℝ) → (((abs ∘ − ) ↾ (ℝ × ℝ)) ↾ ((0[,]1) × (0[,]1))) = ((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))
10199, 100ax-mp 5 . . . . . . . . . . . . 13 (((abs ∘ − ) ↾ (ℝ × ℝ)) ↾ ((0[,]1) × (0[,]1))) = ((abs ∘ − ) ↾ ((0[,]1) × (0[,]1)))
102101eqcomi 2619 . . . . . . . . . . . 12 ((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))) = (((abs ∘ − ) ↾ (ℝ × ℝ)) ↾ ((0[,]1) × (0[,]1)))
103102blres 21994 . . . . . . . . . . 11 ((((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (∞Met‘ℝ) ∧ (𝑘 / ((⌊‘(1 / 𝑟)) + 1)) ∈ (ℝ ∩ (0[,]1)) ∧ 𝑟 ∈ ℝ*) → ((𝑘 / ((⌊‘(1 / 𝑟)) + 1))(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) = (((𝑘 / ((⌊‘(1 / 𝑟)) + 1))(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ∩ (0[,]1)))
10492, 95, 97, 103syl3anc 1318 . . . . . . . . . 10 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((𝑘 / ((⌊‘(1 / 𝑟)) + 1))(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) = (((𝑘 / ((⌊‘(1 / 𝑟)) + 1))(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ∩ (0[,]1)))
10590bl2ioo 22351 . . . . . . . . . . . 12 (((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) ∈ ℝ ∧ 𝑟 ∈ ℝ) → ((𝑘 / ((⌊‘(1 / 𝑟)) + 1))(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = (((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) − 𝑟)(,)((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) + 𝑟)))
10628, 52, 105syl2anc 691 . . . . . . . . . . 11 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((𝑘 / ((⌊‘(1 / 𝑟)) + 1))(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) = (((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) − 𝑟)(,)((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) + 𝑟)))
107106ineq1d 3775 . . . . . . . . . 10 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (((𝑘 / ((⌊‘(1 / 𝑟)) + 1))(ball‘((abs ∘ − ) ↾ (ℝ × ℝ)))𝑟) ∩ (0[,]1)) = ((((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) − 𝑟)(,)((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) + 𝑟)) ∩ (0[,]1)))
108104, 107eqtrd 2644 . . . . . . . . 9 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → ((𝑘 / ((⌊‘(1 / 𝑟)) + 1))(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) = ((((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) − 𝑟)(,)((𝑘 / ((⌊‘(1 / 𝑟)) + 1)) + 𝑟)) ∩ (0[,]1)))
10989, 108sseqtr4d 3605 . . . . . . . 8 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1))[,](𝑘 / ((⌊‘(1 / 𝑟)) + 1))) ⊆ ((𝑘 / ((⌊‘(1 / 𝑟)) + 1))(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟))
110 sstr2 3575 . . . . . . . 8 ((((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1))[,](𝑘 / ((⌊‘(1 / 𝑟)) + 1))) ⊆ ((𝑘 / ((⌊‘(1 / 𝑟)) + 1))(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) → (((𝑘 / ((⌊‘(1 / 𝑟)) + 1))(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) ⊆ 𝑢 → (((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1))[,](𝑘 / ((⌊‘(1 / 𝑟)) + 1))) ⊆ 𝑢))
111109, 110syl 17 . . . . . . 7 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (((𝑘 / ((⌊‘(1 / 𝑟)) + 1))(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) ⊆ 𝑢 → (((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1))[,](𝑘 / ((⌊‘(1 / 𝑟)) + 1))) ⊆ 𝑢))
112111reximdv 2999 . . . . . 6 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (∃𝑢𝑈 ((𝑘 / ((⌊‘(1 / 𝑟)) + 1))(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) ⊆ 𝑢 → ∃𝑢𝑈 (((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1))[,](𝑘 / ((⌊‘(1 / 𝑟)) + 1))) ⊆ 𝑢))
11350, 112syld 46 . . . . 5 ((((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))) → (∀𝑥 ∈ (0[,]1)∃𝑢𝑈 (𝑥(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) ⊆ 𝑢 → ∃𝑢𝑈 (((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1))[,](𝑘 / ((⌊‘(1 / 𝑟)) + 1))) ⊆ 𝑢))
114113ralrimdva 2952 . . . 4 (((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) → (∀𝑥 ∈ (0[,]1)∃𝑢𝑈 (𝑥(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) ⊆ 𝑢 → ∀𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))∃𝑢𝑈 (((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1))[,](𝑘 / ((⌊‘(1 / 𝑟)) + 1))) ⊆ 𝑢))
115 oveq2 6535 . . . . . 6 (𝑛 = ((⌊‘(1 / 𝑟)) + 1) → (1...𝑛) = (1...((⌊‘(1 / 𝑟)) + 1)))
116 oveq2 6535 . . . . . . . . 9 (𝑛 = ((⌊‘(1 / 𝑟)) + 1) → ((𝑘 − 1) / 𝑛) = ((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1)))
117 oveq2 6535 . . . . . . . . 9 (𝑛 = ((⌊‘(1 / 𝑟)) + 1) → (𝑘 / 𝑛) = (𝑘 / ((⌊‘(1 / 𝑟)) + 1)))
118116, 117oveq12d 6545 . . . . . . . 8 (𝑛 = ((⌊‘(1 / 𝑟)) + 1) → (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) = (((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1))[,](𝑘 / ((⌊‘(1 / 𝑟)) + 1))))
119118sseq1d 3595 . . . . . . 7 (𝑛 = ((⌊‘(1 / 𝑟)) + 1) → ((((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑢 ↔ (((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1))[,](𝑘 / ((⌊‘(1 / 𝑟)) + 1))) ⊆ 𝑢))
120119rexbidv 3034 . . . . . 6 (𝑛 = ((⌊‘(1 / 𝑟)) + 1) → (∃𝑢𝑈 (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑢 ↔ ∃𝑢𝑈 (((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1))[,](𝑘 / ((⌊‘(1 / 𝑟)) + 1))) ⊆ 𝑢))
121115, 120raleqbidv 3129 . . . . 5 (𝑛 = ((⌊‘(1 / 𝑟)) + 1) → (∀𝑘 ∈ (1...𝑛)∃𝑢𝑈 (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑢 ↔ ∀𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))∃𝑢𝑈 (((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1))[,](𝑘 / ((⌊‘(1 / 𝑟)) + 1))) ⊆ 𝑢))
122121rspcev 3282 . . . 4 ((((⌊‘(1 / 𝑟)) + 1) ∈ ℕ ∧ ∀𝑘 ∈ (1...((⌊‘(1 / 𝑟)) + 1))∃𝑢𝑈 (((𝑘 − 1) / ((⌊‘(1 / 𝑟)) + 1))[,](𝑘 / ((⌊‘(1 / 𝑟)) + 1))) ⊆ 𝑢) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑢𝑈 (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑢)
12321, 114, 122syl6an 566 . . 3 (((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) ∧ 𝑟 ∈ ℝ+) → (∀𝑥 ∈ (0[,]1)∃𝑢𝑈 (𝑥(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) ⊆ 𝑢 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑢𝑈 (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑢))
124123rexlimdva 3013 . 2 ((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) → (∃𝑟 ∈ ℝ+𝑥 ∈ (0[,]1)∃𝑢𝑈 (𝑥(ball‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))))𝑟) ⊆ 𝑢 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑢𝑈 (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑢))
12513, 124mpd 15 1 ((𝑈 ⊆ II ∧ (0[,]1) = 𝑈) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑢𝑈 (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑢)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383   = wceq 1475  wcel 1977  wral 2896  wrex 2897  cin 3539  wss 3540   cuni 4367   class class class wbr 4578   × cxp 5026  cres 5030  ccom 5032  cfv 5790  (class class class)co 6527  cc 9791  cr 9792  0cc0 9793  1c1 9794   + caddc 9796   · cmul 9798  *cxr 9930   < clt 9931  cle 9932  cmin 10118   / cdiv 10536  cn 10870  0cn0 11142  +crp 11667  (,)cioo 12005  [,]cicc 12008  ...cfz 12155  cfl 12411  abscabs 13771  ∞Metcxmt 19501  Metcme 19502  ballcbl 19503  Compccmp 20947  IIcii 22434
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4694  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-inf2 8399  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-pre-sup 9871  ax-addf 9872  ax-mulf 9873
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4368  df-int 4406  df-iun 4452  df-iin 4453  df-br 4579  df-opab 4639  df-mpt 4640  df-tr 4676  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6773  df-om 6936  df-1st 7037  df-2nd 7038  df-supp 7161  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-2o 7426  df-oadd 7429  df-er 7607  df-ec 7609  df-map 7724  df-ixp 7773  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-fsupp 8137  df-fi 8178  df-sup 8209  df-inf 8210  df-oi 8276  df-card 8626  df-cda 8851  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-3 10930  df-4 10931  df-5 10932  df-6 10933  df-7 10934  df-8 10935  df-9 10936  df-n0 11143  df-z 11214  df-dec 11329  df-uz 11523  df-q 11624  df-rp 11668  df-xneg 11781  df-xadd 11782  df-xmul 11783  df-ioo 12009  df-ico 12011  df-icc 12012  df-fz 12156  df-fzo 12293  df-fl 12413  df-seq 12622  df-exp 12681  df-hash 12938  df-cj 13636  df-re 13637  df-im 13638  df-sqrt 13772  df-abs 13773  df-clim 14016  df-sum 14214  df-struct 15646  df-ndx 15647  df-slot 15648  df-base 15649  df-sets 15650  df-ress 15651  df-plusg 15730  df-mulr 15731  df-starv 15732  df-sca 15733  df-vsca 15734  df-ip 15735  df-tset 15736  df-ple 15737  df-ds 15740  df-unif 15741  df-hom 15742  df-cco 15743  df-rest 15855  df-topn 15856  df-0g 15874  df-gsum 15875  df-topgen 15876  df-pt 15877  df-prds 15880  df-xrs 15934  df-qtop 15939  df-imas 15940  df-xps 15942  df-mre 16018  df-mrc 16019  df-acs 16021  df-mgm 17014  df-sgrp 17056  df-mnd 17067  df-submnd 17108  df-mulg 17313  df-cntz 17522  df-cmn 17967  df-psmet 19508  df-xmet 19509  df-met 19510  df-bl 19511  df-mopn 19512  df-cnfld 19517  df-top 20469  df-bases 20470  df-topon 20471  df-topsp 20472  df-cld 20581  df-ntr 20582  df-cls 20583  df-cn 20789  df-cnp 20790  df-cmp 20948  df-tx 21123  df-hmeo 21316  df-xms 21883  df-ms 21884  df-tms 21885  df-ii 22436
This theorem is referenced by:  cvmliftlem15  30328
  Copyright terms: Public domain W3C validator