Metamath Proof Explorer

Theorem ovoliunlem3

Description: Lemma for ovoliun . (Contributed by Mario Carneiro, 12-Jun-2014)

Ref Expression
Hypotheses ovoliun.t ⊢ T = seq 1 + G
ovoliun.g ⊢ G = n ∈ ℕ ⟼ vol * ⁡ A
ovoliun.a ⊢ φ ∧ n ∈ ℕ → A ⊆ ℝ
ovoliun.v ⊢ φ ∧ n ∈ ℕ → vol * ⁡ A ∈ ℝ
ovoliun.r ⊢ φ → sup ran ⁡ T ℝ * < ∈ ℝ
ovoliun.b ⊢ φ → B ∈ ℝ +
Assertion ovoliunlem3 ⊢ φ → vol * ⁡ ⋃ n ∈ ℕ A ≤ sup ran ⁡ T ℝ * < + B

Proof

Step Hyp Ref Expression
1 ovoliun.t ⊢ T = seq 1 + G
2 ovoliun.g ⊢ G = n ∈ ℕ ⟼ vol * ⁡ A
3 ovoliun.a ⊢ φ ∧ n ∈ ℕ → A ⊆ ℝ
4 ovoliun.v ⊢ φ ∧ n ∈ ℕ → vol * ⁡ A ∈ ℝ
5 ovoliun.r ⊢ φ → sup ran ⁡ T ℝ * < ∈ ℝ
6 ovoliun.b ⊢ φ → B ∈ ℝ +
7 nfcv ⊢ Ⅎ _ m A
8 nfcsb1v ⊢ Ⅎ _ n ⦋ m / n⦌ A
9 csbeq1a ⊢ n = m → A = ⦋ m / n⦌ A
10 7 8 9 cbviun ⊢ ⋃ n ∈ ℕ A = ⋃ m ∈ ℕ ⦋ m / n⦌ A
11 10 fveq2i ⊢ vol * ⁡ ⋃ n ∈ ℕ A = vol * ⁡ ⋃ m ∈ ℕ ⦋ m / n⦌ A
12 2nn ⊢ 2 ∈ ℕ
13 nnnn0 ⊢ n ∈ ℕ → n ∈ ℕ 0
14 nnexpcl ⊢ 2 ∈ ℕ ∧ n ∈ ℕ 0 → 2 n ∈ ℕ
15 12 13 14 sylancr ⊢ n ∈ ℕ → 2 n ∈ ℕ
16 15 nnrpd ⊢ n ∈ ℕ → 2 n ∈ ℝ +
17 rpdivcl ⊢ B ∈ ℝ + ∧ 2 n ∈ ℝ + → B 2 n ∈ ℝ +
18 6 16 17 syl2an ⊢ φ ∧ n ∈ ℕ → B 2 n ∈ ℝ +
19 eqid ⊢ seq 1 + abs ∘ − ∘ f = seq 1 + abs ∘ − ∘ f
20 19 ovolgelb ⊢ A ⊆ ℝ ∧ vol * ⁡ A ∈ ℝ ∧ B 2 n ∈ ℝ + → ∃ f ∈ ≤ ∩ ℝ 2 ℕ A ⊆ ⋃ ran ⁡ . ∘ f ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ≤ vol * ⁡ A + B 2 n
21 3 4 18 20 syl3anc ⊢ φ ∧ n ∈ ℕ → ∃ f ∈ ≤ ∩ ℝ 2 ℕ A ⊆ ⋃ ran ⁡ . ∘ f ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ≤ vol * ⁡ A + B 2 n
22 21 ralrimiva ⊢ φ → ∀ n ∈ ℕ ∃ f ∈ ≤ ∩ ℝ 2 ℕ A ⊆ ⋃ ran ⁡ . ∘ f ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ≤ vol * ⁡ A + B 2 n
23 ovex ⊢ ≤ ∩ ℝ 2 ℕ ∈ V
24 nnenom ⊢ ℕ ≈ ω
25 coeq2 ⊢ f = g ⁡ n → . ∘ f = . ∘ g ⁡ n
26 25 rneqd ⊢ f = g ⁡ n → ran ⁡ . ∘ f = ran ⁡ . ∘ g ⁡ n
27 26 unieqd ⊢ f = g ⁡ n → ⋃ ran ⁡ . ∘ f = ⋃ ran ⁡ . ∘ g ⁡ n
28 27 sseq2d ⊢ f = g ⁡ n → A ⊆ ⋃ ran ⁡ . ∘ f ↔ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n
29 coeq2 ⊢ f = g ⁡ n → abs ∘ − ∘ f = abs ∘ − ∘ g ⁡ n
30 29 seqeq3d ⊢ f = g ⁡ n → seq 1 + abs ∘ − ∘ f = seq 1 + abs ∘ − ∘ g ⁡ n
31 30 rneqd ⊢ f = g ⁡ n → ran ⁡ seq 1 + abs ∘ − ∘ f = ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n
32 31 supeq1d ⊢ f = g ⁡ n → sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < = sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * <
33 32 breq1d ⊢ f = g ⁡ n → sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ≤ vol * ⁡ A + B 2 n ↔ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n
34 28 33 anbi12d ⊢ f = g ⁡ n → A ⊆ ⋃ ran ⁡ . ∘ f ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ≤ vol * ⁡ A + B 2 n ↔ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n
35 23 24 34 axcc4 ⊢ ∀ n ∈ ℕ ∃ f ∈ ≤ ∩ ℝ 2 ℕ A ⊆ ⋃ ran ⁡ . ∘ f ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ≤ vol * ⁡ A + B 2 n → ∃ g g : ℕ ⟶ ≤ ∩ ℝ 2 ℕ ∧ ∀ n ∈ ℕ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n
36 22 35 syl ⊢ φ → ∃ g g : ℕ ⟶ ≤ ∩ ℝ 2 ℕ ∧ ∀ n ∈ ℕ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n
37 xpnnen ⊢ ℕ × ℕ ≈ ℕ
38 37 ensymi ⊢ ℕ ≈ ℕ × ℕ
39 bren ⊢ ℕ ≈ ℕ × ℕ ↔ ∃ j j : ℕ ⟶ 1-1 onto ℕ × ℕ
40 38 39 mpbi ⊢ ∃ j j : ℕ ⟶ 1-1 onto ℕ × ℕ
41 nfcv ⊢ Ⅎ _ m vol * ⁡ A
42 nfcv ⊢ Ⅎ _ n vol *
43 42 8 nffv ⊢ Ⅎ _ n vol * ⁡ ⦋ m / n⦌ A
44 9 fveq2d ⊢ n = m → vol * ⁡ A = vol * ⁡ ⦋ m / n⦌ A
45 41 43 44 cbvmpt ⊢ n ∈ ℕ ⟼ vol * ⁡ A = m ∈ ℕ ⟼ vol * ⁡ ⦋ m / n⦌ A
46 2 45 eqtri ⊢ G = m ∈ ℕ ⟼ vol * ⁡ ⦋ m / n⦌ A
47 3 ralrimiva ⊢ φ → ∀ n ∈ ℕ A ⊆ ℝ
48 nfv ⊢ Ⅎ m A ⊆ ℝ
49 nfcv ⊢ Ⅎ _ n ℝ
50 8 49 nfss ⊢ Ⅎ n ⦋ m / n⦌ A ⊆ ℝ
51 9 sseq1d ⊢ n = m → A ⊆ ℝ ↔ ⦋ m / n⦌ A ⊆ ℝ
52 48 50 51 cbvralw ⊢ ∀ n ∈ ℕ A ⊆ ℝ ↔ ∀ m ∈ ℕ ⦋ m / n⦌ A ⊆ ℝ
53 47 52 sylib ⊢ φ → ∀ m ∈ ℕ ⦋ m / n⦌ A ⊆ ℝ
54 53 r19.21bi ⊢ φ ∧ m ∈ ℕ → ⦋ m / n⦌ A ⊆ ℝ
55 54 ad4ant14 ⊢ φ ∧ j : ℕ ⟶ 1-1 onto ℕ × ℕ ∧ g : ℕ ⟶ ≤ ∩ ℝ 2 ℕ ∧ ∀ n ∈ ℕ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n ∧ m ∈ ℕ → ⦋ m / n⦌ A ⊆ ℝ
56 4 ralrimiva ⊢ φ → ∀ n ∈ ℕ vol * ⁡ A ∈ ℝ
57 41 nfel1 ⊢ Ⅎ m vol * ⁡ A ∈ ℝ
58 43 nfel1 ⊢ Ⅎ n vol * ⁡ ⦋ m / n⦌ A ∈ ℝ
59 44 eleq1d ⊢ n = m → vol * ⁡ A ∈ ℝ ↔ vol * ⁡ ⦋ m / n⦌ A ∈ ℝ
60 57 58 59 cbvralw ⊢ ∀ n ∈ ℕ vol * ⁡ A ∈ ℝ ↔ ∀ m ∈ ℕ vol * ⁡ ⦋ m / n⦌ A ∈ ℝ
61 56 60 sylib ⊢ φ → ∀ m ∈ ℕ vol * ⁡ ⦋ m / n⦌ A ∈ ℝ
62 61 r19.21bi ⊢ φ ∧ m ∈ ℕ → vol * ⁡ ⦋ m / n⦌ A ∈ ℝ
63 62 ad4ant14 ⊢ φ ∧ j : ℕ ⟶ 1-1 onto ℕ × ℕ ∧ g : ℕ ⟶ ≤ ∩ ℝ 2 ℕ ∧ ∀ n ∈ ℕ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n ∧ m ∈ ℕ → vol * ⁡ ⦋ m / n⦌ A ∈ ℝ
64 5 ad2antrr ⊢ φ ∧ j : ℕ ⟶ 1-1 onto ℕ × ℕ ∧ g : ℕ ⟶ ≤ ∩ ℝ 2 ℕ ∧ ∀ n ∈ ℕ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n → sup ran ⁡ T ℝ * < ∈ ℝ
65 6 ad2antrr ⊢ φ ∧ j : ℕ ⟶ 1-1 onto ℕ × ℕ ∧ g : ℕ ⟶ ≤ ∩ ℝ 2 ℕ ∧ ∀ n ∈ ℕ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n → B ∈ ℝ +
66 eqid ⊢ seq 1 + abs ∘ − ∘ g ⁡ m = seq 1 + abs ∘ − ∘ g ⁡ m
67 eqid ⊢ seq 1 + abs ∘ − ∘ k ∈ ℕ ⟼ g ⁡ 1 st ⁡ j ⁡ k ⁡ 2 nd ⁡ j ⁡ k = seq 1 + abs ∘ − ∘ k ∈ ℕ ⟼ g ⁡ 1 st ⁡ j ⁡ k ⁡ 2 nd ⁡ j ⁡ k
68 eqid ⊢ k ∈ ℕ ⟼ g ⁡ 1 st ⁡ j ⁡ k ⁡ 2 nd ⁡ j ⁡ k = k ∈ ℕ ⟼ g ⁡ 1 st ⁡ j ⁡ k ⁡ 2 nd ⁡ j ⁡ k
69 simplr ⊢ φ ∧ j : ℕ ⟶ 1-1 onto ℕ × ℕ ∧ g : ℕ ⟶ ≤ ∩ ℝ 2 ℕ ∧ ∀ n ∈ ℕ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n → j : ℕ ⟶ 1-1 onto ℕ × ℕ
70 simprl ⊢ φ ∧ j : ℕ ⟶ 1-1 onto ℕ × ℕ ∧ g : ℕ ⟶ ≤ ∩ ℝ 2 ℕ ∧ ∀ n ∈ ℕ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n → g : ℕ ⟶ ≤ ∩ ℝ 2 ℕ
71 simprr ⊢ φ ∧ j : ℕ ⟶ 1-1 onto ℕ × ℕ ∧ g : ℕ ⟶ ≤ ∩ ℝ 2 ℕ ∧ ∀ n ∈ ℕ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n → ∀ n ∈ ℕ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n
72 nfv ⊢ Ⅎ m A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n
73 nfcv ⊢ Ⅎ _ n ⋃ ran ⁡ . ∘ g ⁡ m
74 8 73 nfss ⊢ Ⅎ n ⦋ m / n⦌ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ m
75 nfcv ⊢ Ⅎ _ n sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ m ℝ * <
76 nfcv ⊢ Ⅎ _ n ≤
77 nfcv ⊢ Ⅎ _ n +
78 nfcv ⊢ Ⅎ _ n B 2 m
79 43 77 78 nfov ⊢ Ⅎ _ n vol * ⁡ ⦋ m / n⦌ A + B 2 m
80 75 76 79 nfbr ⊢ Ⅎ n sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ m ℝ * < ≤ vol * ⁡ ⦋ m / n⦌ A + B 2 m
81 74 80 nfan ⊢ Ⅎ n ⦋ m / n⦌ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ m ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ m ℝ * < ≤ vol * ⁡ ⦋ m / n⦌ A + B 2 m
82 fveq2 ⊢ n = m → g ⁡ n = g ⁡ m
83 82 coeq2d ⊢ n = m → . ∘ g ⁡ n = . ∘ g ⁡ m
84 83 rneqd ⊢ n = m → ran ⁡ . ∘ g ⁡ n = ran ⁡ . ∘ g ⁡ m
85 84 unieqd ⊢ n = m → ⋃ ran ⁡ . ∘ g ⁡ n = ⋃ ran ⁡ . ∘ g ⁡ m
86 9 85 sseq12d ⊢ n = m → A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ↔ ⦋ m / n⦌ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ m
87 82 coeq2d ⊢ n = m → abs ∘ − ∘ g ⁡ n = abs ∘ − ∘ g ⁡ m
88 87 seqeq3d ⊢ n = m → seq 1 + abs ∘ − ∘ g ⁡ n = seq 1 + abs ∘ − ∘ g ⁡ m
89 88 rneqd ⊢ n = m → ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n = ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ m
90 89 supeq1d ⊢ n = m → sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < = sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ m ℝ * <
91 oveq2 ⊢ n = m → 2 n = 2 m
92 91 oveq2d ⊢ n = m → B 2 n = B 2 m
93 44 92 oveq12d ⊢ n = m → vol * ⁡ A + B 2 n = vol * ⁡ ⦋ m / n⦌ A + B 2 m
94 90 93 breq12d ⊢ n = m → sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n ↔ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ m ℝ * < ≤ vol * ⁡ ⦋ m / n⦌ A + B 2 m
95 86 94 anbi12d ⊢ n = m → A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n ↔ ⦋ m / n⦌ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ m ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ m ℝ * < ≤ vol * ⁡ ⦋ m / n⦌ A + B 2 m
96 72 81 95 cbvralw ⊢ ∀ n ∈ ℕ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n ↔ ∀ m ∈ ℕ ⦋ m / n⦌ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ m ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ m ℝ * < ≤ vol * ⁡ ⦋ m / n⦌ A + B 2 m
97 71 96 sylib ⊢ φ ∧ j : ℕ ⟶ 1-1 onto ℕ × ℕ ∧ g : ℕ ⟶ ≤ ∩ ℝ 2 ℕ ∧ ∀ n ∈ ℕ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n → ∀ m ∈ ℕ ⦋ m / n⦌ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ m ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ m ℝ * < ≤ vol * ⁡ ⦋ m / n⦌ A + B 2 m
98 97 r19.21bi ⊢ φ ∧ j : ℕ ⟶ 1-1 onto ℕ × ℕ ∧ g : ℕ ⟶ ≤ ∩ ℝ 2 ℕ ∧ ∀ n ∈ ℕ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n ∧ m ∈ ℕ → ⦋ m / n⦌ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ m ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ m ℝ * < ≤ vol * ⁡ ⦋ m / n⦌ A + B 2 m
99 98 simpld ⊢ φ ∧ j : ℕ ⟶ 1-1 onto ℕ × ℕ ∧ g : ℕ ⟶ ≤ ∩ ℝ 2 ℕ ∧ ∀ n ∈ ℕ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n ∧ m ∈ ℕ → ⦋ m / n⦌ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ m
100 98 simprd ⊢ φ ∧ j : ℕ ⟶ 1-1 onto ℕ × ℕ ∧ g : ℕ ⟶ ≤ ∩ ℝ 2 ℕ ∧ ∀ n ∈ ℕ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n ∧ m ∈ ℕ → sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ m ℝ * < ≤ vol * ⁡ ⦋ m / n⦌ A + B 2 m
101 1 46 55 63 64 65 66 67 68 69 70 99 100 ovoliunlem2 ⊢ φ ∧ j : ℕ ⟶ 1-1 onto ℕ × ℕ ∧ g : ℕ ⟶ ≤ ∩ ℝ 2 ℕ ∧ ∀ n ∈ ℕ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n → vol * ⁡ ⋃ m ∈ ℕ ⦋ m / n⦌ A ≤ sup ran ⁡ T ℝ * < + B
102 101 exp31 ⊢ φ → j : ℕ ⟶ 1-1 onto ℕ × ℕ → g : ℕ ⟶ ≤ ∩ ℝ 2 ℕ ∧ ∀ n ∈ ℕ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n → vol * ⁡ ⋃ m ∈ ℕ ⦋ m / n⦌ A ≤ sup ran ⁡ T ℝ * < + B
103 102 exlimdv ⊢ φ → ∃ j j : ℕ ⟶ 1-1 onto ℕ × ℕ → g : ℕ ⟶ ≤ ∩ ℝ 2 ℕ ∧ ∀ n ∈ ℕ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n → vol * ⁡ ⋃ m ∈ ℕ ⦋ m / n⦌ A ≤ sup ran ⁡ T ℝ * < + B
104 40 103 mpi ⊢ φ → g : ℕ ⟶ ≤ ∩ ℝ 2 ℕ ∧ ∀ n ∈ ℕ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n → vol * ⁡ ⋃ m ∈ ℕ ⦋ m / n⦌ A ≤ sup ran ⁡ T ℝ * < + B
105 104 exlimdv ⊢ φ → ∃ g g : ℕ ⟶ ≤ ∩ ℝ 2 ℕ ∧ ∀ n ∈ ℕ A ⊆ ⋃ ran ⁡ . ∘ g ⁡ n ∧ sup ran ⁡ seq 1 + abs ∘ − ∘ g ⁡ n ℝ * < ≤ vol * ⁡ A + B 2 n → vol * ⁡ ⋃ m ∈ ℕ ⦋ m / n⦌ A ≤ sup ran ⁡ T ℝ * < + B
106 36 105 mpd ⊢ φ → vol * ⁡ ⋃ m ∈ ℕ ⦋ m / n⦌ A ≤ sup ran ⁡ T ℝ * < + B
107 11 106 eqbrtrid ⊢ φ → vol * ⁡ ⋃ n ∈ ℕ A ≤ sup ran ⁡ T ℝ * < + B