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

Theorem vitalilem5 24367
Description: Lemma for vitali 24368. (Contributed by Mario Carneiro, 16-Jun-2014.)
Hypotheses
Ref Expression
vitali.1 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥𝑦) ∈ ℚ)}
vitali.2 𝑆 = ((0[,]1) / )
vitali.3 (𝜑𝐹 Fn 𝑆)
vitali.4 (𝜑 → ∀𝑧𝑆 (𝑧 ≠ ∅ → (𝐹𝑧) ∈ 𝑧))
vitali.5 (𝜑𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)))
vitali.6 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺𝑛)) ∈ ran 𝐹})
vitali.7 (𝜑 → ¬ ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol))
Assertion
Ref Expression
vitalilem5 ¬ 𝜑
Distinct variable groups:   𝑛,𝑠,𝑥,𝑦,𝑧,𝐺   𝜑,𝑛,𝑥,𝑧   𝑧,𝑆   𝑥,𝑇   𝑛,𝐹,𝑠,𝑥,𝑦,𝑧   ,𝑛,𝑠,𝑥,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑦,𝑠)   𝑆(𝑥,𝑦,𝑛,𝑠)   𝑇(𝑦,𝑧,𝑛,𝑠)

Proof of Theorem vitalilem5
Dummy variable 𝑚 is distinct from all other variables.
StepHypRef Expression
1 0lt1 11243 . . . 4 0 < 1
2 0re 10724 . . . . . 6 0 ∈ ℝ
3 1re 10722 . . . . . 6 1 ∈ ℝ
4 0le1 11244 . . . . . 6 0 ≤ 1
5 ovolicc 24278 . . . . . 6 ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ≤ 1) → (vol*‘(0[,]1)) = (1 − 0))
62, 3, 4, 5mp3an 1462 . . . . 5 (vol*‘(0[,]1)) = (1 − 0)
7 1m0e1 11840 . . . . 5 (1 − 0) = 1
86, 7eqtri 2762 . . . 4 (vol*‘(0[,]1)) = 1
91, 8breqtrri 5058 . . 3 0 < (vol*‘(0[,]1))
108, 3eqeltri 2830 . . . 4 (vol*‘(0[,]1)) ∈ ℝ
112, 10ltnlei 10842 . . 3 (0 < (vol*‘(0[,]1)) ↔ ¬ (vol*‘(0[,]1)) ≤ 0)
129, 11mpbi 233 . 2 ¬ (vol*‘(0[,]1)) ≤ 0
13 vitali.1 . . . . . 6 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥𝑦) ∈ ℚ)}
14 vitali.2 . . . . . 6 𝑆 = ((0[,]1) / )
15 vitali.3 . . . . . 6 (𝜑𝐹 Fn 𝑆)
16 vitali.4 . . . . . 6 (𝜑 → ∀𝑧𝑆 (𝑧 ≠ ∅ → (𝐹𝑧) ∈ 𝑧))
17 vitali.5 . . . . . 6 (𝜑𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)))
18 vitali.6 . . . . . 6 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺𝑛)) ∈ ran 𝐹})
19 vitali.7 . . . . . 6 (𝜑 → ¬ ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol))
2013, 14, 15, 16, 17, 18, 19vitalilem2 24364 . . . . 5 (𝜑 → (ran 𝐹 ⊆ (0[,]1) ∧ (0[,]1) ⊆ 𝑚 ∈ ℕ (𝑇𝑚) ∧ 𝑚 ∈ ℕ (𝑇𝑚) ⊆ (-1[,]2)))
2120simp2d 1144 . . . 4 (𝜑 → (0[,]1) ⊆ 𝑚 ∈ ℕ (𝑇𝑚))
2213vitalilem1 24363 . . . . . . . . . . . . . . . . . . . . . . 23 Er (0[,]1)
23 erdm 8333 . . . . . . . . . . . . . . . . . . . . . . 23 ( Er (0[,]1) → dom = (0[,]1))
2422, 23ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 dom = (0[,]1)
25 simpr 488 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧𝑆) → 𝑧𝑆)
2625, 14eleqtrdi 2844 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧𝑆) → 𝑧 ∈ ((0[,]1) / ))
27 elqsn0 8400 . . . . . . . . . . . . . . . . . . . . . 22 ((dom = (0[,]1) ∧ 𝑧 ∈ ((0[,]1) / )) → 𝑧 ≠ ∅)
2824, 26, 27sylancr 590 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝑆) → 𝑧 ≠ ∅)
2922a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 Er (0[,]1))
3029qsss 8392 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((0[,]1) / ) ⊆ 𝒫 (0[,]1))
3114, 30eqsstrid 3926 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑆 ⊆ 𝒫 (0[,]1))
3231sselda 3878 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑧𝑆) → 𝑧 ∈ 𝒫 (0[,]1))
3332elpwid 4500 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑧𝑆) → 𝑧 ⊆ (0[,]1))
3433sseld 3877 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑧𝑆) → ((𝐹𝑧) ∈ 𝑧 → (𝐹𝑧) ∈ (0[,]1)))
3528, 34embantd 59 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧𝑆) → ((𝑧 ≠ ∅ → (𝐹𝑧) ∈ 𝑧) → (𝐹𝑧) ∈ (0[,]1)))
3635ralimdva 3092 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (∀𝑧𝑆 (𝑧 ≠ ∅ → (𝐹𝑧) ∈ 𝑧) → ∀𝑧𝑆 (𝐹𝑧) ∈ (0[,]1)))
3716, 36mpd 15 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑧𝑆 (𝐹𝑧) ∈ (0[,]1))
38 ffnfv 6895 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑆⟶(0[,]1) ↔ (𝐹 Fn 𝑆 ∧ ∀𝑧𝑆 (𝐹𝑧) ∈ (0[,]1)))
3915, 37, 38sylanbrc 586 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:𝑆⟶(0[,]1))
4039frnd 6513 . . . . . . . . . . . . . . . 16 (𝜑 → ran 𝐹 ⊆ (0[,]1))
41 unitssre 12976 . . . . . . . . . . . . . . . 16 (0[,]1) ⊆ ℝ
4240, 41sstrdi 3890 . . . . . . . . . . . . . . 15 (𝜑 → ran 𝐹 ⊆ ℝ)
43 reex 10709 . . . . . . . . . . . . . . . 16 ℝ ∈ V
4443elpw2 5214 . . . . . . . . . . . . . . 15 (ran 𝐹 ∈ 𝒫 ℝ ↔ ran 𝐹 ⊆ ℝ)
4542, 44sylibr 237 . . . . . . . . . . . . . 14 (𝜑 → ran 𝐹 ∈ 𝒫 ℝ)
4645anim1i 618 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ ran 𝐹 ∈ dom vol) → (ran 𝐹 ∈ 𝒫 ℝ ∧ ¬ ran 𝐹 ∈ dom vol))
47 eldif 3854 . . . . . . . . . . . . 13 (ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol) ↔ (ran 𝐹 ∈ 𝒫 ℝ ∧ ¬ ran 𝐹 ∈ dom vol))
4846, 47sylibr 237 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ ran 𝐹 ∈ dom vol) → ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol))
4948ex 416 . . . . . . . . . . 11 (𝜑 → (¬ ran 𝐹 ∈ dom vol → ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol)))
5019, 49mt3d 150 . . . . . . . . . 10 (𝜑 → ran 𝐹 ∈ dom vol)
51 f1of 6621 . . . . . . . . . . . . 13 (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → 𝐺:ℕ⟶(ℚ ∩ (-1[,]1)))
5217, 51syl 17 . . . . . . . . . . . 12 (𝜑𝐺:ℕ⟶(ℚ ∩ (-1[,]1)))
53 inss1 4120 . . . . . . . . . . . . 13 (ℚ ∩ (-1[,]1)) ⊆ ℚ
54 qssre 12444 . . . . . . . . . . . . 13 ℚ ⊆ ℝ
5553, 54sstri 3887 . . . . . . . . . . . 12 (ℚ ∩ (-1[,]1)) ⊆ ℝ
56 fss 6522 . . . . . . . . . . . 12 ((𝐺:ℕ⟶(ℚ ∩ (-1[,]1)) ∧ (ℚ ∩ (-1[,]1)) ⊆ ℝ) → 𝐺:ℕ⟶ℝ)
5752, 55, 56sylancl 589 . . . . . . . . . . 11 (𝜑𝐺:ℕ⟶ℝ)
5857ffvelrnda 6864 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) ∈ ℝ)
59 shftmbl 24293 . . . . . . . . . 10 ((ran 𝐹 ∈ dom vol ∧ (𝐺𝑛) ∈ ℝ) → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺𝑛)) ∈ ran 𝐹} ∈ dom vol)
6050, 58, 59syl2an2r 685 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺𝑛)) ∈ ran 𝐹} ∈ dom vol)
6160, 18fmptd 6891 . . . . . . . 8 (𝜑𝑇:ℕ⟶dom vol)
6261ffvelrnda 6864 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → (𝑇𝑚) ∈ dom vol)
6362ralrimiva 3097 . . . . . 6 (𝜑 → ∀𝑚 ∈ ℕ (𝑇𝑚) ∈ dom vol)
64 iunmbl 24308 . . . . . 6 (∀𝑚 ∈ ℕ (𝑇𝑚) ∈ dom vol → 𝑚 ∈ ℕ (𝑇𝑚) ∈ dom vol)
6563, 64syl 17 . . . . 5 (𝜑 𝑚 ∈ ℕ (𝑇𝑚) ∈ dom vol)
66 mblss 24286 . . . . 5 ( 𝑚 ∈ ℕ (𝑇𝑚) ∈ dom vol → 𝑚 ∈ ℕ (𝑇𝑚) ⊆ ℝ)
6765, 66syl 17 . . . 4 (𝜑 𝑚 ∈ ℕ (𝑇𝑚) ⊆ ℝ)
68 ovolss 24240 . . . 4 (((0[,]1) ⊆ 𝑚 ∈ ℕ (𝑇𝑚) ∧ 𝑚 ∈ ℕ (𝑇𝑚) ⊆ ℝ) → (vol*‘(0[,]1)) ≤ (vol*‘ 𝑚 ∈ ℕ (𝑇𝑚)))
6921, 67, 68syl2anc 587 . . 3 (𝜑 → (vol*‘(0[,]1)) ≤ (vol*‘ 𝑚 ∈ ℕ (𝑇𝑚)))
70 eqid 2739 . . . . . 6 seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑇𝑚)))) = seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑇𝑚))))
71 eqid 2739 . . . . . 6 (𝑚 ∈ ℕ ↦ (vol*‘(𝑇𝑚))) = (𝑚 ∈ ℕ ↦ (vol*‘(𝑇𝑚)))
72 mblss 24286 . . . . . . 7 ((𝑇𝑚) ∈ dom vol → (𝑇𝑚) ⊆ ℝ)
7362, 72syl 17 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝑇𝑚) ⊆ ℝ)
7413, 14, 15, 16, 17, 18, 19vitalilem4 24366 . . . . . . 7 ((𝜑𝑚 ∈ ℕ) → (vol*‘(𝑇𝑚)) = 0)
7574, 2eqeltrdi 2842 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (vol*‘(𝑇𝑚)) ∈ ℝ)
7674mpteq2dva 5126 . . . . . . . . . 10 (𝜑 → (𝑚 ∈ ℕ ↦ (vol*‘(𝑇𝑚))) = (𝑚 ∈ ℕ ↦ 0))
77 fconstmpt 5586 . . . . . . . . . . 11 (ℕ × {0}) = (𝑚 ∈ ℕ ↦ 0)
78 nnuz 12366 . . . . . . . . . . . 12 ℕ = (ℤ‘1)
7978xpeq1i 5552 . . . . . . . . . . 11 (ℕ × {0}) = ((ℤ‘1) × {0})
8077, 79eqtr3i 2764 . . . . . . . . . 10 (𝑚 ∈ ℕ ↦ 0) = ((ℤ‘1) × {0})
8176, 80eqtrdi 2790 . . . . . . . . 9 (𝜑 → (𝑚 ∈ ℕ ↦ (vol*‘(𝑇𝑚))) = ((ℤ‘1) × {0}))
8281seqeq3d 13471 . . . . . . . 8 (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑇𝑚)))) = seq1( + , ((ℤ‘1) × {0})))
83 1z 12096 . . . . . . . . 9 1 ∈ ℤ
84 serclim0 15027 . . . . . . . . 9 (1 ∈ ℤ → seq1( + , ((ℤ‘1) × {0})) ⇝ 0)
8583, 84ax-mp 5 . . . . . . . 8 seq1( + , ((ℤ‘1) × {0})) ⇝ 0
8682, 85eqbrtrdi 5070 . . . . . . 7 (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑇𝑚)))) ⇝ 0)
87 seqex 13465 . . . . . . . 8 seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑇𝑚)))) ∈ V
88 c0ex 10716 . . . . . . . 8 0 ∈ V
8987, 88breldm 5752 . . . . . . 7 (seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑇𝑚)))) ⇝ 0 → seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑇𝑚)))) ∈ dom ⇝ )
9086, 89syl 17 . . . . . 6 (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (vol*‘(𝑇𝑚)))) ∈ dom ⇝ )
9170, 71, 73, 75, 90ovoliun2 24261 . . . . 5 (𝜑 → (vol*‘ 𝑚 ∈ ℕ (𝑇𝑚)) ≤ Σ𝑚 ∈ ℕ (vol*‘(𝑇𝑚)))
9274sumeq2dv 15156 . . . . . 6 (𝜑 → Σ𝑚 ∈ ℕ (vol*‘(𝑇𝑚)) = Σ𝑚 ∈ ℕ 0)
9378eqimssi 3936 . . . . . . . 8 ℕ ⊆ (ℤ‘1)
9493orci 864 . . . . . . 7 (ℕ ⊆ (ℤ‘1) ∨ ℕ ∈ Fin)
95 sumz 15175 . . . . . . 7 ((ℕ ⊆ (ℤ‘1) ∨ ℕ ∈ Fin) → Σ𝑚 ∈ ℕ 0 = 0)
9694, 95ax-mp 5 . . . . . 6 Σ𝑚 ∈ ℕ 0 = 0
9792, 96eqtrdi 2790 . . . . 5 (𝜑 → Σ𝑚 ∈ ℕ (vol*‘(𝑇𝑚)) = 0)
9891, 97breqtrd 5057 . . . 4 (𝜑 → (vol*‘ 𝑚 ∈ ℕ (𝑇𝑚)) ≤ 0)
99 ovolge0 24236 . . . . 5 ( 𝑚 ∈ ℕ (𝑇𝑚) ⊆ ℝ → 0 ≤ (vol*‘ 𝑚 ∈ ℕ (𝑇𝑚)))
10067, 99syl 17 . . . 4 (𝜑 → 0 ≤ (vol*‘ 𝑚 ∈ ℕ (𝑇𝑚)))
101 ovolcl 24233 . . . . . 6 ( 𝑚 ∈ ℕ (𝑇𝑚) ⊆ ℝ → (vol*‘ 𝑚 ∈ ℕ (𝑇𝑚)) ∈ ℝ*)
10267, 101syl 17 . . . . 5 (𝜑 → (vol*‘ 𝑚 ∈ ℕ (𝑇𝑚)) ∈ ℝ*)
103 0xr 10769 . . . . 5 0 ∈ ℝ*
104 xrletri3 12633 . . . . 5 (((vol*‘ 𝑚 ∈ ℕ (𝑇𝑚)) ∈ ℝ* ∧ 0 ∈ ℝ*) → ((vol*‘ 𝑚 ∈ ℕ (𝑇𝑚)) = 0 ↔ ((vol*‘ 𝑚 ∈ ℕ (𝑇𝑚)) ≤ 0 ∧ 0 ≤ (vol*‘ 𝑚 ∈ ℕ (𝑇𝑚)))))
105102, 103, 104sylancl 589 . . . 4 (𝜑 → ((vol*‘ 𝑚 ∈ ℕ (𝑇𝑚)) = 0 ↔ ((vol*‘ 𝑚 ∈ ℕ (𝑇𝑚)) ≤ 0 ∧ 0 ≤ (vol*‘ 𝑚 ∈ ℕ (𝑇𝑚)))))
10698, 100, 105mpbir2and 713 . . 3 (𝜑 → (vol*‘ 𝑚 ∈ ℕ (𝑇𝑚)) = 0)
10769, 106breqtrd 5057 . 2 (𝜑 → (vol*‘(0[,]1)) ≤ 0)
10812, 107mto 200 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 846   = wceq 1542  wcel 2114  wne 2935  wral 3054  {crab 3058  cdif 3841  cin 3843  wss 3844  c0 4212  𝒫 cpw 4489  {csn 4517   ciun 4882   class class class wbr 5031  {copab 5093  cmpt 5111   × cxp 5524  dom cdm 5526  ran crn 5527   Fn wfn 6335  wf 6336  1-1-ontowf1o 6339  cfv 6340  (class class class)co 7173   Er wer 8320   / cqs 8322  Fincfn 8558  cr 10617  0cc0 10618  1c1 10619   + caddc 10621  *cxr 10755   < clt 10756  cle 10757  cmin 10951  -cneg 10952  cn 11719  2c2 11774  cz 12065  cuz 12327  cq 12433  [,]cicc 12827  seqcseq 13463  cli 14934  Σcsu 15138  vol*covol 24217  volcvol 24218
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5233  ax-pr 5297  ax-un 7482  ax-inf2 9180  ax-cc 9938  ax-cnex 10674  ax-resscn 10675  ax-1cn 10676  ax-icn 10677  ax-addcl 10678  ax-addrcl 10679  ax-mulcl 10680  ax-mulrcl 10681  ax-mulcom 10682  ax-addass 10683  ax-mulass 10684  ax-distr 10685  ax-i2m1 10686  ax-1ne0 10687  ax-1rid 10688  ax-rnegex 10689  ax-rrecex 10690  ax-cnre 10691  ax-pre-lttri 10692  ax-pre-lttrn 10693  ax-pre-ltadd 10694  ax-pre-mulgt0 10695  ax-pre-sup 10696
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ne 2936  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3401  df-sbc 3682  df-csb 3792  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-pss 3863  df-nul 4213  df-if 4416  df-pw 4491  df-sn 4518  df-pr 4520  df-tp 4522  df-op 4524  df-uni 4798  df-int 4838  df-iun 4884  df-disj 4997  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5484  df-se 5485  df-we 5486  df-xp 5532  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-rn 5537  df-res 5538  df-ima 5539  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-isom 6349  df-riota 7130  df-ov 7176  df-oprab 7177  df-mpo 7178  df-of 7428  df-om 7603  df-1st 7717  df-2nd 7718  df-wrecs 7979  df-recs 8040  df-rdg 8078  df-1o 8134  df-2o 8135  df-er 8323  df-ec 8325  df-qs 8329  df-map 8442  df-pm 8443  df-en 8559  df-dom 8560  df-sdom 8561  df-fin 8562  df-fi 8951  df-sup 8982  df-inf 8983  df-oi 9050  df-dju 9406  df-card 9444  df-pnf 10758  df-mnf 10759  df-xr 10760  df-ltxr 10761  df-le 10762  df-sub 10953  df-neg 10954  df-div 11379  df-nn 11720  df-2 11782  df-3 11783  df-n0 11980  df-z 12066  df-uz 12328  df-q 12434  df-rp 12476  df-xneg 12593  df-xadd 12594  df-xmul 12595  df-ioo 12828  df-ico 12830  df-icc 12831  df-fz 12985  df-fzo 13128  df-fl 13256  df-seq 13464  df-exp 13525  df-hash 13786  df-cj 14551  df-re 14552  df-im 14553  df-sqrt 14687  df-abs 14688  df-clim 14938  df-rlim 14939  df-sum 15139  df-rest 16802  df-topgen 16823  df-psmet 20212  df-xmet 20213  df-met 20214  df-bl 20215  df-mopn 20216  df-top 21648  df-topon 21665  df-bases 21700  df-cmp 22141  df-ovol 24219  df-vol 24220
This theorem is referenced by:  vitali  24368
  Copyright terms: Public domain W3C validator