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

Theorem uniioombllem6 23402
 Description: Lemma for uniioombl 23403. (Contributed by Mario Carneiro, 26-Mar-2015.)
Hypotheses
Ref Expression
uniioombl.1 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
uniioombl.2 (𝜑Disj 𝑥 ∈ ℕ ((,)‘(𝐹𝑥)))
uniioombl.3 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
uniioombl.a 𝐴 = ran ((,) ∘ 𝐹)
uniioombl.e (𝜑 → (vol*‘𝐸) ∈ ℝ)
uniioombl.c (𝜑𝐶 ∈ ℝ+)
uniioombl.g (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
uniioombl.s (𝜑𝐸 ran ((,) ∘ 𝐺))
uniioombl.t 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
uniioombl.v (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))
Assertion
Ref Expression
uniioombllem6 (𝜑 → ((vol*‘(𝐸𝐴)) + (vol*‘(𝐸𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶)))
Distinct variable groups:   𝑥,𝐹   𝑥,𝐺   𝑥,𝐴   𝑥,𝐶   𝜑,𝑥   𝑥,𝑇
Allowed substitution hints:   𝑆(𝑥)   𝐸(𝑥)

Proof of Theorem uniioombllem6
Dummy variables 𝑎 𝑖 𝑗 𝑘 𝑛 𝑦 𝑧 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 11761 . . . 4 ℕ = (ℤ‘1)
2 1zzd 11446 . . . 4 (𝜑 → 1 ∈ ℤ)
3 uniioombl.c . . . 4 (𝜑𝐶 ∈ ℝ+)
4 eqidd 2652 . . . 4 ((𝜑𝑚 ∈ ℕ) → (𝑇𝑚) = (𝑇𝑚))
5 uniioombl.t . . . . . 6 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
6 eqidd 2652 . . . . . 6 ((𝜑𝑎 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑎) = (((abs ∘ − ) ∘ 𝐺)‘𝑎))
7 uniioombl.g . . . . . . . . . 10 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
8 eqid 2651 . . . . . . . . . . 11 ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
98ovolfsf 23286 . . . . . . . . . 10 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
107, 9syl 17 . . . . . . . . 9 (𝜑 → ((abs ∘ − ) ∘ 𝐺):ℕ⟶(0[,)+∞))
1110ffvelrnda 6399 . . . . . . . 8 ((𝜑𝑎 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑎) ∈ (0[,)+∞))
12 elrege0 12316 . . . . . . . 8 ((((abs ∘ − ) ∘ 𝐺)‘𝑎) ∈ (0[,)+∞) ↔ ((((abs ∘ − ) ∘ 𝐺)‘𝑎) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑎)))
1311, 12sylib 208 . . . . . . 7 ((𝜑𝑎 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐺)‘𝑎) ∈ ℝ ∧ 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑎)))
1413simpld 474 . . . . . 6 ((𝜑𝑎 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑎) ∈ ℝ)
1513simprd 478 . . . . . 6 ((𝜑𝑎 ∈ ℕ) → 0 ≤ (((abs ∘ − ) ∘ 𝐺)‘𝑎))
16 uniioombl.1 . . . . . . . 8 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
17 uniioombl.2 . . . . . . . 8 (𝜑Disj 𝑥 ∈ ℕ ((,)‘(𝐹𝑥)))
18 uniioombl.3 . . . . . . . 8 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
19 uniioombl.a . . . . . . . 8 𝐴 = ran ((,) ∘ 𝐹)
20 uniioombl.e . . . . . . . 8 (𝜑 → (vol*‘𝐸) ∈ ℝ)
21 uniioombl.s . . . . . . . 8 (𝜑𝐸 ran ((,) ∘ 𝐺))
22 uniioombl.v . . . . . . . 8 (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))
2316, 17, 18, 19, 20, 3, 7, 21, 5, 22uniioombllem1 23395 . . . . . . 7 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
248, 5ovolsf 23287 . . . . . . . . . . . . 13 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
257, 24syl 17 . . . . . . . . . . . 12 (𝜑𝑇:ℕ⟶(0[,)+∞))
26 frn 6091 . . . . . . . . . . . 12 (𝑇:ℕ⟶(0[,)+∞) → ran 𝑇 ⊆ (0[,)+∞))
2725, 26syl 17 . . . . . . . . . . 11 (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
28 icossxr 12296 . . . . . . . . . . 11 (0[,)+∞) ⊆ ℝ*
2927, 28syl6ss 3648 . . . . . . . . . 10 (𝜑 → ran 𝑇 ⊆ ℝ*)
30 supxrub 12192 . . . . . . . . . 10 ((ran 𝑇 ⊆ ℝ*𝑥 ∈ ran 𝑇) → 𝑥 ≤ sup(ran 𝑇, ℝ*, < ))
3129, 30sylan 487 . . . . . . . . 9 ((𝜑𝑥 ∈ ran 𝑇) → 𝑥 ≤ sup(ran 𝑇, ℝ*, < ))
3231ralrimiva 2995 . . . . . . . 8 (𝜑 → ∀𝑥 ∈ ran 𝑇 𝑥 ≤ sup(ran 𝑇, ℝ*, < ))
33 ffn 6083 . . . . . . . . . 10 (𝑇:ℕ⟶(0[,)+∞) → 𝑇 Fn ℕ)
3425, 33syl 17 . . . . . . . . 9 (𝜑𝑇 Fn ℕ)
35 breq1 4688 . . . . . . . . . 10 (𝑥 = (𝑇𝑚) → (𝑥 ≤ sup(ran 𝑇, ℝ*, < ) ↔ (𝑇𝑚) ≤ sup(ran 𝑇, ℝ*, < )))
3635ralrn 6402 . . . . . . . . 9 (𝑇 Fn ℕ → (∀𝑥 ∈ ran 𝑇 𝑥 ≤ sup(ran 𝑇, ℝ*, < ) ↔ ∀𝑚 ∈ ℕ (𝑇𝑚) ≤ sup(ran 𝑇, ℝ*, < )))
3734, 36syl 17 . . . . . . . 8 (𝜑 → (∀𝑥 ∈ ran 𝑇 𝑥 ≤ sup(ran 𝑇, ℝ*, < ) ↔ ∀𝑚 ∈ ℕ (𝑇𝑚) ≤ sup(ran 𝑇, ℝ*, < )))
3832, 37mpbid 222 . . . . . . 7 (𝜑 → ∀𝑚 ∈ ℕ (𝑇𝑚) ≤ sup(ran 𝑇, ℝ*, < ))
39 breq2 4689 . . . . . . . . 9 (𝑥 = sup(ran 𝑇, ℝ*, < ) → ((𝑇𝑚) ≤ 𝑥 ↔ (𝑇𝑚) ≤ sup(ran 𝑇, ℝ*, < )))
4039ralbidv 3015 . . . . . . . 8 (𝑥 = sup(ran 𝑇, ℝ*, < ) → (∀𝑚 ∈ ℕ (𝑇𝑚) ≤ 𝑥 ↔ ∀𝑚 ∈ ℕ (𝑇𝑚) ≤ sup(ran 𝑇, ℝ*, < )))
4140rspcev 3340 . . . . . . 7 ((sup(ran 𝑇, ℝ*, < ) ∈ ℝ ∧ ∀𝑚 ∈ ℕ (𝑇𝑚) ≤ sup(ran 𝑇, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑚 ∈ ℕ (𝑇𝑚) ≤ 𝑥)
4223, 38, 41syl2anc 694 . . . . . 6 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑚 ∈ ℕ (𝑇𝑚) ≤ 𝑥)
431, 5, 2, 6, 14, 15, 42isumsup2 14622 . . . . 5 (𝜑𝑇 ⇝ sup(ran 𝑇, ℝ, < ))
44 rge0ssre 12318 . . . . . . 7 (0[,)+∞) ⊆ ℝ
4527, 44syl6ss 3648 . . . . . 6 (𝜑 → ran 𝑇 ⊆ ℝ)
46 1nn 11069 . . . . . . . . 9 1 ∈ ℕ
47 fdm 6089 . . . . . . . . . 10 (𝑇:ℕ⟶(0[,)+∞) → dom 𝑇 = ℕ)
4825, 47syl 17 . . . . . . . . 9 (𝜑 → dom 𝑇 = ℕ)
4946, 48syl5eleqr 2737 . . . . . . . 8 (𝜑 → 1 ∈ dom 𝑇)
50 ne0i 3954 . . . . . . . 8 (1 ∈ dom 𝑇 → dom 𝑇 ≠ ∅)
5149, 50syl 17 . . . . . . 7 (𝜑 → dom 𝑇 ≠ ∅)
52 dm0rn0 5374 . . . . . . . 8 (dom 𝑇 = ∅ ↔ ran 𝑇 = ∅)
5352necon3bii 2875 . . . . . . 7 (dom 𝑇 ≠ ∅ ↔ ran 𝑇 ≠ ∅)
5451, 53sylib 208 . . . . . 6 (𝜑 → ran 𝑇 ≠ ∅)
55 breq2 4689 . . . . . . . . 9 (𝑦 = sup(ran 𝑇, ℝ*, < ) → (𝑥𝑦𝑥 ≤ sup(ran 𝑇, ℝ*, < )))
5655ralbidv 3015 . . . . . . . 8 (𝑦 = sup(ran 𝑇, ℝ*, < ) → (∀𝑥 ∈ ran 𝑇 𝑥𝑦 ↔ ∀𝑥 ∈ ran 𝑇 𝑥 ≤ sup(ran 𝑇, ℝ*, < )))
5756rspcev 3340 . . . . . . 7 ((sup(ran 𝑇, ℝ*, < ) ∈ ℝ ∧ ∀𝑥 ∈ ran 𝑇 𝑥 ≤ sup(ran 𝑇, ℝ*, < )) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ran 𝑇 𝑥𝑦)
5823, 32, 57syl2anc 694 . . . . . 6 (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ran 𝑇 𝑥𝑦)
59 supxrre 12195 . . . . . 6 ((ran 𝑇 ⊆ ℝ ∧ ran 𝑇 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ ran 𝑇 𝑥𝑦) → sup(ran 𝑇, ℝ*, < ) = sup(ran 𝑇, ℝ, < ))
6045, 54, 58, 59syl3anc 1366 . . . . 5 (𝜑 → sup(ran 𝑇, ℝ*, < ) = sup(ran 𝑇, ℝ, < ))
6143, 60breqtrrd 4713 . . . 4 (𝜑𝑇 ⇝ sup(ran 𝑇, ℝ*, < ))
621, 2, 3, 4, 61climi2 14286 . . 3 (𝜑 → ∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ𝑗)(abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)
631r19.2uz 14135 . . 3 (∃𝑗 ∈ ℕ ∀𝑚 ∈ (ℤ𝑗)(abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶 → ∃𝑚 ∈ ℕ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)
6462, 63syl 17 . 2 (𝜑 → ∃𝑚 ∈ ℕ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)
65 1zzd 11446 . . . . . . . . 9 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → 1 ∈ ℤ)
663ad2antrr 762 . . . . . . . . . 10 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → 𝐶 ∈ ℝ+)
67 simplrl 817 . . . . . . . . . . 11 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → 𝑚 ∈ ℕ)
6867nnrpd 11908 . . . . . . . . . 10 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → 𝑚 ∈ ℝ+)
6966, 68rpdivcld 11927 . . . . . . . . 9 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (𝐶 / 𝑚) ∈ ℝ+)
70 fvex 6239 . . . . . . . . . . . . . . . 16 ((,)‘(𝐹𝑧)) ∈ V
7170inex1 4832 . . . . . . . . . . . . . . 15 (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗))) ∈ V
7271rgenw 2953 . . . . . . . . . . . . . 14 𝑧 ∈ ℕ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗))) ∈ V
73 eqid 2651 . . . . . . . . . . . . . . 15 (𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗)))) = (𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗))))
7473fnmpt 6058 . . . . . . . . . . . . . 14 (∀𝑧 ∈ ℕ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗))) ∈ V → (𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗)))) Fn ℕ)
7572, 74mp1i 13 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) → (𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗)))) Fn ℕ)
76 elfznn 12408 . . . . . . . . . . . . 13 (𝑖 ∈ (1...𝑛) → 𝑖 ∈ ℕ)
77 fvco2 6312 . . . . . . . . . . . . 13 (((𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗)))) Fn ℕ ∧ 𝑖 ∈ ℕ) → ((vol* ∘ (𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗)))))‘𝑖) = (vol*‘((𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗))))‘𝑖)))
7875, 76, 77syl2an 493 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → ((vol* ∘ (𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗)))))‘𝑖) = (vol*‘((𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗))))‘𝑖)))
7976adantl 481 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → 𝑖 ∈ ℕ)
80 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑖 → (𝐹𝑧) = (𝐹𝑖))
8180fveq2d 6233 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑖 → ((,)‘(𝐹𝑧)) = ((,)‘(𝐹𝑖)))
8281ineq1d 3846 . . . . . . . . . . . . . . 15 (𝑧 = 𝑖 → (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
83 fvex 6239 . . . . . . . . . . . . . . . 16 ((,)‘(𝐹𝑖)) ∈ V
8483inex1 4832 . . . . . . . . . . . . . . 15 (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ V
8582, 73, 84fvmpt 6321 . . . . . . . . . . . . . 14 (𝑖 ∈ ℕ → ((𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗))))‘𝑖) = (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
8679, 85syl 17 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → ((𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗))))‘𝑖) = (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
8786fveq2d 6233 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → (vol*‘((𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗))))‘𝑖)) = (vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
8878, 87eqtrd 2685 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → ((vol* ∘ (𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗)))))‘𝑖) = (vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
89 simpr 476 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
9089, 1syl6eleq 2740 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ‘1))
91 inss2 3867 . . . . . . . . . . . . . 14 (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((,)‘(𝐺𝑗))
9291a1i 11 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((,)‘(𝐺𝑗)))
93 inss2 3867 . . . . . . . . . . . . . . . . . . 19 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
947adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
95 elfznn 12408 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...𝑚) → 𝑗 ∈ ℕ)
96 ffvelrn 6397 . . . . . . . . . . . . . . . . . . . 20 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
9794, 95, 96syl2an 493 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (𝐺𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
9893, 97sseldi 3634 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (𝐺𝑗) ∈ (ℝ × ℝ))
99 1st2nd2 7249 . . . . . . . . . . . . . . . . . 18 ((𝐺𝑗) ∈ (ℝ × ℝ) → (𝐺𝑗) = ⟨(1st ‘(𝐺𝑗)), (2nd ‘(𝐺𝑗))⟩)
10098, 99syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (𝐺𝑗) = ⟨(1st ‘(𝐺𝑗)), (2nd ‘(𝐺𝑗))⟩)
101100fveq2d 6233 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ((,)‘(𝐺𝑗)) = ((,)‘⟨(1st ‘(𝐺𝑗)), (2nd ‘(𝐺𝑗))⟩))
102 df-ov 6693 . . . . . . . . . . . . . . . 16 ((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗))) = ((,)‘⟨(1st ‘(𝐺𝑗)), (2nd ‘(𝐺𝑗))⟩)
103101, 102syl6eqr 2703 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ((,)‘(𝐺𝑗)) = ((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗))))
104 ioossre 12273 . . . . . . . . . . . . . . 15 ((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗))) ⊆ ℝ
105103, 104syl6eqss 3688 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ((,)‘(𝐺𝑗)) ⊆ ℝ)
106105ad2antrr 762 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → ((,)‘(𝐺𝑗)) ⊆ ℝ)
107103fveq2d 6233 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (vol*‘((,)‘(𝐺𝑗))) = (vol*‘((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗)))))
108 ovolfcl 23281 . . . . . . . . . . . . . . . . . 18 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1st ‘(𝐺𝑗)) ∈ ℝ ∧ (2nd ‘(𝐺𝑗)) ∈ ℝ ∧ (1st ‘(𝐺𝑗)) ≤ (2nd ‘(𝐺𝑗))))
10994, 95, 108syl2an 493 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ((1st ‘(𝐺𝑗)) ∈ ℝ ∧ (2nd ‘(𝐺𝑗)) ∈ ℝ ∧ (1st ‘(𝐺𝑗)) ≤ (2nd ‘(𝐺𝑗))))
110 ovolioo 23382 . . . . . . . . . . . . . . . . 17 (((1st ‘(𝐺𝑗)) ∈ ℝ ∧ (2nd ‘(𝐺𝑗)) ∈ ℝ ∧ (1st ‘(𝐺𝑗)) ≤ (2nd ‘(𝐺𝑗))) → (vol*‘((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗)))) = ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))))
111109, 110syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (vol*‘((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗)))) = ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))))
112107, 111eqtrd 2685 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (vol*‘((,)‘(𝐺𝑗))) = ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))))
113109simp2d 1094 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (2nd ‘(𝐺𝑗)) ∈ ℝ)
114109simp1d 1093 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (1st ‘(𝐺𝑗)) ∈ ℝ)
115113, 114resubcld 10496 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))) ∈ ℝ)
116112, 115eqeltrd 2730 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → (vol*‘((,)‘(𝐺𝑗))) ∈ ℝ)
117116ad2antrr 762 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → (vol*‘((,)‘(𝐺𝑗))) ∈ ℝ)
118 ovolsscl 23300 . . . . . . . . . . . . 13 (((((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((,)‘(𝐺𝑗)) ∧ ((,)‘(𝐺𝑗)) ⊆ ℝ ∧ (vol*‘((,)‘(𝐺𝑗))) ∈ ℝ) → (vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
11992, 106, 117, 118syl3anc 1366 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → (vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
120119recnd 10106 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ (1...𝑛)) → (vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℂ)
12188, 90, 120fsumser 14505 . . . . . . . . . 10 ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) → Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = (seq1( + , (vol* ∘ (𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗))))))‘𝑛))
122121eqcomd 2657 . . . . . . . . 9 ((((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) ∧ 𝑛 ∈ ℕ) → (seq1( + , (vol* ∘ (𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗))))))‘𝑛) = Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
123 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑧 = 𝑘 → (𝐹𝑧) = (𝐹𝑘))
124123fveq2d 6233 . . . . . . . . . . . . . 14 (𝑧 = 𝑘 → ((,)‘(𝐹𝑧)) = ((,)‘(𝐹𝑘)))
125124ineq1d 3846 . . . . . . . . . . . . 13 (𝑧 = 𝑘 → (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐹𝑘)) ∩ ((,)‘(𝐺𝑗))))
126125cbvmptv 4783 . . . . . . . . . . . 12 (𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗)))) = (𝑘 ∈ ℕ ↦ (((,)‘(𝐹𝑘)) ∩ ((,)‘(𝐺𝑗))))
127 eqeq1 2655 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → (𝑧 = ∅ ↔ 𝑥 = ∅))
128 infeq1 8423 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → inf(𝑧, ℝ*, < ) = inf(𝑥, ℝ*, < ))
129 supeq1 8392 . . . . . . . . . . . . . . 15 (𝑧 = 𝑥 → sup(𝑧, ℝ*, < ) = sup(𝑥, ℝ*, < ))
130128, 129opeq12d 4441 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → ⟨inf(𝑧, ℝ*, < ), sup(𝑧, ℝ*, < )⟩ = ⟨inf(𝑥, ℝ*, < ), sup(𝑥, ℝ*, < )⟩)
131127, 130ifbieq2d 4144 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → if(𝑧 = ∅, ⟨0, 0⟩, ⟨inf(𝑧, ℝ*, < ), sup(𝑧, ℝ*, < )⟩) = if(𝑥 = ∅, ⟨0, 0⟩, ⟨inf(𝑥, ℝ*, < ), sup(𝑥, ℝ*, < )⟩))
132131cbvmptv 4783 . . . . . . . . . . . 12 (𝑧 ∈ ran (,) ↦ if(𝑧 = ∅, ⟨0, 0⟩, ⟨inf(𝑧, ℝ*, < ), sup(𝑧, ℝ*, < )⟩)) = (𝑥 ∈ ran (,) ↦ if(𝑥 = ∅, ⟨0, 0⟩, ⟨inf(𝑥, ℝ*, < ), sup(𝑥, ℝ*, < )⟩))
13316, 17, 18, 19, 20, 3, 7, 21, 5, 22, 126, 132uniioombllem2 23397 . . . . . . . . . . 11 ((𝜑𝑗 ∈ ℕ) → seq1( + , (vol* ∘ (𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗)))))) ⇝ (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))
13495, 133sylan2 490 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑚)) → seq1( + , (vol* ∘ (𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗)))))) ⇝ (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))
135134adantlr 751 . . . . . . . . 9 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → seq1( + , (vol* ∘ (𝑧 ∈ ℕ ↦ (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗)))))) ⇝ (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))
1361, 65, 69, 122, 135climi2 14286 . . . . . . . 8 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ∃𝑎 ∈ ℕ ∀𝑛 ∈ (ℤ𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚))
137 1z 11445 . . . . . . . . 9 1 ∈ ℤ
1381rexuz3 14132 . . . . . . . . 9 (1 ∈ ℤ → (∃𝑎 ∈ ℕ ∀𝑛 ∈ (ℤ𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))
139137, 138ax-mp 5 . . . . . . . 8 (∃𝑎 ∈ ℕ ∀𝑛 ∈ (ℤ𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚))
140136, 139sylib 208 . . . . . . 7 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ 𝑗 ∈ (1...𝑚)) → ∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚))
141140ralrimiva 2995 . . . . . 6 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) → ∀𝑗 ∈ (1...𝑚)∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚))
142 fzfi 12811 . . . . . . 7 (1...𝑚) ∈ Fin
143 rexfiuz 14131 . . . . . . 7 ((1...𝑚) ∈ Fin → (∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∀𝑗 ∈ (1...𝑚)∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))
144142, 143ax-mp 5 . . . . . 6 (∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∀𝑗 ∈ (1...𝑚)∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ𝑎)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚))
145141, 144sylibr 224 . . . . 5 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) → ∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚))
1461rexuz3 14132 . . . . . 6 (1 ∈ ℤ → (∃𝑎 ∈ ℕ ∀𝑛 ∈ (ℤ𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))
147137, 146ax-mp 5 . . . . 5 (∃𝑎 ∈ ℕ ∀𝑛 ∈ (ℤ𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∃𝑎 ∈ ℤ ∀𝑛 ∈ (ℤ𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚))
148145, 147sylibr 224 . . . 4 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) → ∃𝑎 ∈ ℕ ∀𝑛 ∈ (ℤ𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚))
1491r19.2uz 14135 . . . 4 (∃𝑎 ∈ ℕ ∀𝑛 ∈ (ℤ𝑎)∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) → ∃𝑛 ∈ ℕ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚))
150148, 149syl 17 . . 3 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) → ∃𝑛 ∈ ℕ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚))
15116adantr 480 . . . . 5 ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
15217adantr 480 . . . . 5 ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → Disj 𝑥 ∈ ℕ ((,)‘(𝐹𝑥)))
15320adantr 480 . . . . 5 ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → (vol*‘𝐸) ∈ ℝ)
1543adantr 480 . . . . 5 ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → 𝐶 ∈ ℝ+)
1557adantr 480 . . . . 5 ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
15621adantr 480 . . . . 5 ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → 𝐸 ran ((,) ∘ 𝐺))
15722adantr 480 . . . . 5 ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))
158 simprll 819 . . . . 5 ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → 𝑚 ∈ ℕ)
159 simprlr 820 . . . . 5 ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)
160 eqid 2651 . . . . 5 (((,) ∘ 𝐺) “ (1...𝑚)) = (((,) ∘ 𝐺) “ (1...𝑚))
161 simprrl 821 . . . . 5 ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → 𝑛 ∈ ℕ)
162 simprrr 822 . . . . . 6 ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚))
163 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑖 = 𝑧 → (𝐹𝑖) = (𝐹𝑧))
164163fveq2d 6233 . . . . . . . . . . . . . 14 (𝑖 = 𝑧 → ((,)‘(𝐹𝑖)) = ((,)‘(𝐹𝑧)))
165164ineq1d 3846 . . . . . . . . . . . . 13 (𝑖 = 𝑧 → (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗))))
166165fveq2d 6233 . . . . . . . . . . . 12 (𝑖 = 𝑧 → (vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = (vol*‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗)))))
167166cbvsumv 14470 . . . . . . . . . . 11 Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗))))
168 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑗 = 𝑘 → (𝐺𝑗) = (𝐺𝑘))
169168fveq2d 6233 . . . . . . . . . . . . . 14 (𝑗 = 𝑘 → ((,)‘(𝐺𝑗)) = ((,)‘(𝐺𝑘)))
170169ineq2d 3847 . . . . . . . . . . . . 13 (𝑗 = 𝑘 → (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑘))))
171170fveq2d 6233 . . . . . . . . . . . 12 (𝑗 = 𝑘 → (vol*‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗)))) = (vol*‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑘)))))
172171sumeq2sdv 14479 . . . . . . . . . . 11 (𝑗 = 𝑘 → Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑗)))) = Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑘)))))
173167, 172syl5eq 2697 . . . . . . . . . 10 (𝑗 = 𝑘 → Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑘)))))
174169ineq1d 3846 . . . . . . . . . . 11 (𝑗 = 𝑘 → (((,)‘(𝐺𝑗)) ∩ 𝐴) = (((,)‘(𝐺𝑘)) ∩ 𝐴))
175174fveq2d 6233 . . . . . . . . . 10 (𝑗 = 𝑘 → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) = (vol*‘(((,)‘(𝐺𝑘)) ∩ 𝐴)))
176173, 175oveq12d 6708 . . . . . . . . 9 (𝑗 = 𝑘 → (Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴))) = (Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑘)))) − (vol*‘(((,)‘(𝐺𝑘)) ∩ 𝐴))))
177176fveq2d 6233 . . . . . . . 8 (𝑗 = 𝑘 → (abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) = (abs‘(Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑘)))) − (vol*‘(((,)‘(𝐺𝑘)) ∩ 𝐴)))))
178177breq1d 4695 . . . . . . 7 (𝑗 = 𝑘 → ((abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ (abs‘(Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑘)))) − (vol*‘(((,)‘(𝐺𝑘)) ∩ 𝐴)))) < (𝐶 / 𝑚)))
179178cbvralv 3201 . . . . . 6 (∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚) ↔ ∀𝑘 ∈ (1...𝑚)(abs‘(Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑘)))) − (vol*‘(((,)‘(𝐺𝑘)) ∩ 𝐴)))) < (𝐶 / 𝑚))
180162, 179sylib 208 . . . . 5 ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → ∀𝑘 ∈ (1...𝑚)(abs‘(Σ𝑧 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑧)) ∩ ((,)‘(𝐺𝑘)))) − (vol*‘(((,)‘(𝐺𝑘)) ∩ 𝐴)))) < (𝐶 / 𝑚))
181 eqid 2651 . . . . 5 (((,) ∘ 𝐹) “ (1...𝑛)) = (((,) ∘ 𝐹) “ (1...𝑛))
182151, 152, 18, 19, 153, 154, 155, 156, 5, 157, 158, 159, 160, 161, 180, 181uniioombllem5 23401 . . . 4 ((𝜑 ∧ ((𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚)))) → ((vol*‘(𝐸𝐴)) + (vol*‘(𝐸𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶)))
183182anassrs 681 . . 3 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) ∧ (𝑛 ∈ ℕ ∧ ∀𝑗 ∈ (1...𝑚)(abs‘(Σ𝑖 ∈ (1...𝑛)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑚))) → ((vol*‘(𝐸𝐴)) + (vol*‘(𝐸𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶)))
184150, 183rexlimddv 3064 . 2 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (abs‘((𝑇𝑚) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)) → ((vol*‘(𝐸𝐴)) + (vol*‘(𝐸𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶)))
18564, 184rexlimddv 3064 1 (𝜑 → ((vol*‘(𝐸𝐴)) + (vol*‘(𝐸𝐴))) ≤ ((vol*‘𝐸) + (4 · 𝐶)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  Vcvv 3231   ∖ cdif 3604   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  ifcif 4119  ⟨cop 4216  ∪ cuni 4468  Disj wdisj 4652   class class class wbr 4685   ↦ cmpt 4762   × cxp 5141  dom cdm 5143  ran crn 5144   “ cima 5146   ∘ ccom 5147   Fn wfn 5921  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690  1st c1st 7208  2nd c2nd 7209  Fincfn 7997  supcsup 8387  infcinf 8388  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  +∞cpnf 10109  ℝ*cxr 10111   < clt 10112   ≤ cle 10113   − cmin 10304   / cdiv 10722  ℕcn 11058  4c4 11110  ℤcz 11415  ℤ≥cuz 11725  ℝ+crp 11870  (,)cioo 12213  [,)cico 12215  ...cfz 12364  seqcseq 12841  abscabs 14018   ⇝ cli 14259  Σcsu 14460  vol*covol 23277 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-disj 4653  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-acn 8806  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-n0 11331  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-rlim 14264  df-sum 14461  df-rest 16130  df-topgen 16151  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-top 20747  df-topon 20764  df-bases 20798  df-cmp 21238  df-ovol 23279  df-vol 23280 This theorem is referenced by:  uniioombl  23403
 Copyright terms: Public domain W3C validator