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

Theorem uniioombllem4 25634
Description: Lemma for uniioombl 25637. (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*‘𝐸) + 𝐶))
uniioombl.m (𝜑𝑀 ∈ ℕ)
uniioombl.m2 (𝜑 → (abs‘((𝑇𝑀) − sup(ran 𝑇, ℝ*, < ))) < 𝐶)
uniioombl.k 𝐾 = (((,) ∘ 𝐺) “ (1...𝑀))
uniioombl.n (𝜑𝑁 ∈ ℕ)
uniioombl.n2 (𝜑 → ∀𝑗 ∈ (1...𝑀)(abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))
uniioombl.l 𝐿 = (((,) ∘ 𝐹) “ (1...𝑁))
Assertion
Ref Expression
uniioombllem4 (𝜑 → (vol*‘(𝐾𝐴)) ≤ ((vol*‘(𝐾𝐿)) + 𝐶))
Distinct variable groups:   𝑖,𝑗,𝑥,𝐹   𝑖,𝐺,𝑗,𝑥   𝑗,𝐾,𝑥   𝐴,𝑗,𝑥   𝐶,𝑖,𝑗,𝑥   𝑖,𝑀,𝑗,𝑥   𝑖,𝑁,𝑗   𝜑,𝑖,𝑗,𝑥   𝑇,𝑖,𝑗,𝑥
Allowed substitution hints:   𝐴(𝑖)   𝑆(𝑥,𝑖,𝑗)   𝐸(𝑥,𝑖,𝑗)   𝐾(𝑖)   𝐿(𝑥,𝑖,𝑗)   𝑁(𝑥)

Proof of Theorem uniioombllem4
StepHypRef Expression
1 inss1 4244 . . 3 (𝐾𝐴) ⊆ 𝐾
2 uniioombl.k . . . . 5 𝐾 = (((,) ∘ 𝐺) “ (1...𝑀))
3 imassrn 6090 . . . . . 6 (((,) ∘ 𝐺) “ (1...𝑀)) ⊆ ran ((,) ∘ 𝐺)
43unissi 4920 . . . . 5 (((,) ∘ 𝐺) “ (1...𝑀)) ⊆ ran ((,) ∘ 𝐺)
52, 4eqsstri 4029 . . . 4 𝐾 ran ((,) ∘ 𝐺)
6 uniioombl.g . . . . . . 7 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
76uniiccdif 25626 . . . . . 6 (𝜑 → ( ran ((,) ∘ 𝐺) ⊆ ran ([,] ∘ 𝐺) ∧ (vol*‘( ran ([,] ∘ 𝐺) ∖ ran ((,) ∘ 𝐺))) = 0))
87simpld 494 . . . . 5 (𝜑 ran ((,) ∘ 𝐺) ⊆ ran ([,] ∘ 𝐺))
9 ovolficcss 25517 . . . . . 6 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ran ([,] ∘ 𝐺) ⊆ ℝ)
106, 9syl 17 . . . . 5 (𝜑 ran ([,] ∘ 𝐺) ⊆ ℝ)
118, 10sstrd 4005 . . . 4 (𝜑 ran ((,) ∘ 𝐺) ⊆ ℝ)
125, 11sstrid 4006 . . 3 (𝜑𝐾 ⊆ ℝ)
13 uniioombl.1 . . . . . 6 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
14 uniioombl.2 . . . . . 6 (𝜑Disj 𝑥 ∈ ℕ ((,)‘(𝐹𝑥)))
15 uniioombl.3 . . . . . 6 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
16 uniioombl.a . . . . . 6 𝐴 = ran ((,) ∘ 𝐹)
17 uniioombl.e . . . . . 6 (𝜑 → (vol*‘𝐸) ∈ ℝ)
18 uniioombl.c . . . . . 6 (𝜑𝐶 ∈ ℝ+)
19 uniioombl.s . . . . . 6 (𝜑𝐸 ran ((,) ∘ 𝐺))
20 uniioombl.t . . . . . 6 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
21 uniioombl.v . . . . . 6 (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ ((vol*‘𝐸) + 𝐶))
2213, 14, 15, 16, 17, 18, 6, 19, 20, 21uniioombllem1 25629 . . . . 5 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
23 ssid 4017 . . . . . 6 ran ((,) ∘ 𝐺) ⊆ ran ((,) ∘ 𝐺)
2420ovollb 25527 . . . . . 6 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ran ((,) ∘ 𝐺) ⊆ ran ((,) ∘ 𝐺)) → (vol*‘ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, < ))
256, 23, 24sylancl 586 . . . . 5 (𝜑 → (vol*‘ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, < ))
26 ovollecl 25531 . . . . 5 (( ran ((,) ∘ 𝐺) ⊆ ℝ ∧ sup(ran 𝑇, ℝ*, < ) ∈ ℝ ∧ (vol*‘ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ*, < )) → (vol*‘ ran ((,) ∘ 𝐺)) ∈ ℝ)
2711, 22, 25, 26syl3anc 1370 . . . 4 (𝜑 → (vol*‘ ran ((,) ∘ 𝐺)) ∈ ℝ)
28 ovolsscl 25534 . . . 4 ((𝐾 ran ((,) ∘ 𝐺) ∧ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol*‘ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol*‘𝐾) ∈ ℝ)
295, 11, 27, 28mp3an2i 1465 . . 3 (𝜑 → (vol*‘𝐾) ∈ ℝ)
30 ovolsscl 25534 . . 3 (((𝐾𝐴) ⊆ 𝐾𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) → (vol*‘(𝐾𝐴)) ∈ ℝ)
311, 12, 29, 30mp3an2i 1465 . 2 (𝜑 → (vol*‘(𝐾𝐴)) ∈ ℝ)
32 inss1 4244 . . . 4 (𝐾𝐿) ⊆ 𝐾
33 ovolsscl 25534 . . . 4 (((𝐾𝐿) ⊆ 𝐾𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) → (vol*‘(𝐾𝐿)) ∈ ℝ)
3432, 12, 29, 33mp3an2i 1465 . . 3 (𝜑 → (vol*‘(𝐾𝐿)) ∈ ℝ)
35 ssun2 4188 . . . . . 6 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((𝐾𝐿) ∪ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
36 nnuz 12918 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
37 uniioombl.n . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℕ)
3837peano2nnd 12280 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 + 1) ∈ ℕ)
3938, 36eleqtrdi 2848 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁 + 1) ∈ (ℤ‘1))
40 uzsplit 13632 . . . . . . . . . . . . . . 15 ((𝑁 + 1) ∈ (ℤ‘1) → (ℤ‘1) = ((1...((𝑁 + 1) − 1)) ∪ (ℤ‘(𝑁 + 1))))
4139, 40syl 17 . . . . . . . . . . . . . 14 (𝜑 → (ℤ‘1) = ((1...((𝑁 + 1) − 1)) ∪ (ℤ‘(𝑁 + 1))))
4236, 41eqtrid 2786 . . . . . . . . . . . . 13 (𝜑 → ℕ = ((1...((𝑁 + 1) − 1)) ∪ (ℤ‘(𝑁 + 1))))
4337nncnd 12279 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℂ)
44 ax-1cn 11210 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
45 pncan 11511 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
4643, 44, 45sylancl 586 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
4746oveq2d 7446 . . . . . . . . . . . . . 14 (𝜑 → (1...((𝑁 + 1) − 1)) = (1...𝑁))
4847uneq1d 4176 . . . . . . . . . . . . 13 (𝜑 → ((1...((𝑁 + 1) − 1)) ∪ (ℤ‘(𝑁 + 1))) = ((1...𝑁) ∪ (ℤ‘(𝑁 + 1))))
4942, 48eqtrd 2774 . . . . . . . . . . . 12 (𝜑 → ℕ = ((1...𝑁) ∪ (ℤ‘(𝑁 + 1))))
5049iuneq1d 5023 . . . . . . . . . . 11 (𝜑 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)) = 𝑖 ∈ ((1...𝑁) ∪ (ℤ‘(𝑁 + 1)))((,)‘(𝐹𝑖)))
51 iunxun 5098 . . . . . . . . . . 11 𝑖 ∈ ((1...𝑁) ∪ (ℤ‘(𝑁 + 1)))((,)‘(𝐹𝑖)) = ( 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)) ∪ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))
5250, 51eqtrdi 2790 . . . . . . . . . 10 (𝜑 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)) = ( 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)) ∪ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
53 ioof 13483 . . . . . . . . . . . . . 14 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
54 inss2 4245 . . . . . . . . . . . . . . . 16 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
55 rexpssxrxp 11303 . . . . . . . . . . . . . . . 16 (ℝ × ℝ) ⊆ (ℝ* × ℝ*)
5654, 55sstri 4004 . . . . . . . . . . . . . . 15 ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)
57 fss 6752 . . . . . . . . . . . . . . 15 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)) → 𝐹:ℕ⟶(ℝ* × ℝ*))
5813, 56, 57sylancl 586 . . . . . . . . . . . . . 14 (𝜑𝐹:ℕ⟶(ℝ* × ℝ*))
59 fco 6760 . . . . . . . . . . . . . 14 (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐹:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
6053, 58, 59sylancr 587 . . . . . . . . . . . . 13 (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
61 ffn 6736 . . . . . . . . . . . . 13 (((,) ∘ 𝐹):ℕ⟶𝒫 ℝ → ((,) ∘ 𝐹) Fn ℕ)
62 fniunfv 7266 . . . . . . . . . . . . 13 (((,) ∘ 𝐹) Fn ℕ → 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ran ((,) ∘ 𝐹))
6360, 61, 623syl 18 . . . . . . . . . . . 12 (𝜑 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ran ((,) ∘ 𝐹))
64 fvco3 7007 . . . . . . . . . . . . . 14 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑖 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹𝑖)))
6513, 64sylan 580 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹𝑖)))
6665iuneq2dv 5020 . . . . . . . . . . . 12 (𝜑 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)))
6763, 66eqtr3d 2776 . . . . . . . . . . 11 (𝜑 ran ((,) ∘ 𝐹) = 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)))
6816, 67eqtrid 2786 . . . . . . . . . 10 (𝜑𝐴 = 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)))
69 uniioombl.l . . . . . . . . . . . 12 𝐿 = (((,) ∘ 𝐹) “ (1...𝑁))
70 ffun 6739 . . . . . . . . . . . . . 14 (((,) ∘ 𝐹):ℕ⟶𝒫 ℝ → Fun ((,) ∘ 𝐹))
71 funiunfv 7267 . . . . . . . . . . . . . 14 (Fun ((,) ∘ 𝐹) → 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = (((,) ∘ 𝐹) “ (1...𝑁)))
7260, 70, 713syl 18 . . . . . . . . . . . . 13 (𝜑 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = (((,) ∘ 𝐹) “ (1...𝑁)))
73 elfznn 13589 . . . . . . . . . . . . . . 15 (𝑖 ∈ (1...𝑁) → 𝑖 ∈ ℕ)
7413, 73, 64syl2an 596 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (1...𝑁)) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹𝑖)))
7574iuneq2dv 5020 . . . . . . . . . . . . 13 (𝜑 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)))
7672, 75eqtr3d 2776 . . . . . . . . . . . 12 (𝜑 (((,) ∘ 𝐹) “ (1...𝑁)) = 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)))
7769, 76eqtrid 2786 . . . . . . . . . . 11 (𝜑𝐿 = 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)))
7877uneq1d 4176 . . . . . . . . . 10 (𝜑 → (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ( 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)) ∪ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
7952, 68, 783eqtr4d 2784 . . . . . . . . 9 (𝜑𝐴 = (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
8079ineq2d 4227 . . . . . . . 8 (𝜑 → (𝐾𝐴) = (𝐾 ∩ (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))))
81 indi 4289 . . . . . . . 8 (𝐾 ∩ (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))) = ((𝐾𝐿) ∪ (𝐾 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
8280, 81eqtrdi 2790 . . . . . . 7 (𝜑 → (𝐾𝐴) = ((𝐾𝐿) ∪ (𝐾 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))))
83 fss 6752 . . . . . . . . . . . . . . 15 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ* × ℝ*)) → 𝐺:ℕ⟶(ℝ* × ℝ*))
846, 56, 83sylancl 586 . . . . . . . . . . . . . 14 (𝜑𝐺:ℕ⟶(ℝ* × ℝ*))
85 fco 6760 . . . . . . . . . . . . . 14 (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐺:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
8653, 84, 85sylancr 587 . . . . . . . . . . . . 13 (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
87 ffun 6739 . . . . . . . . . . . . 13 (((,) ∘ 𝐺):ℕ⟶𝒫 ℝ → Fun ((,) ∘ 𝐺))
88 funiunfv 7267 . . . . . . . . . . . . 13 (Fun ((,) ∘ 𝐺) → 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = (((,) ∘ 𝐺) “ (1...𝑀)))
8986, 87, 883syl 18 . . . . . . . . . . . 12 (𝜑 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = (((,) ∘ 𝐺) “ (1...𝑀)))
90 elfznn 13589 . . . . . . . . . . . . . 14 (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
91 fvco3 7007 . . . . . . . . . . . . . 14 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑗) = ((,)‘(𝐺𝑗)))
926, 90, 91syl2an 596 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (((,) ∘ 𝐺)‘𝑗) = ((,)‘(𝐺𝑗)))
9392iuneq2dv 5020 . . . . . . . . . . . 12 (𝜑 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)))
9489, 93eqtr3d 2776 . . . . . . . . . . 11 (𝜑 (((,) ∘ 𝐺) “ (1...𝑀)) = 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)))
952, 94eqtrid 2786 . . . . . . . . . 10 (𝜑𝐾 = 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)))
9695ineq2d 4227 . . . . . . . . 9 (𝜑 → ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ 𝐾) = ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗))))
97 incom 4216 . . . . . . . . 9 (𝐾 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ 𝐾)
98 iunin2 5075 . . . . . . . . . . . . 13 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖))) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))
99 incom 4216 . . . . . . . . . . . . . . 15 (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖)))
10099a1i 11 . . . . . . . . . . . . . 14 (𝑖 ∈ (ℤ‘(𝑁 + 1)) → (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖))))
101100iuneq2i 5017 . . . . . . . . . . . . 13 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖)))
102 incom 4216 . . . . . . . . . . . . 13 ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))
10398, 101, 1023eqtr4ri 2773 . . . . . . . . . . . 12 ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))
104103a1i 11 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑀) → ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
105104iuneq2i 5017 . . . . . . . . . 10 𝑗 ∈ (1...𝑀)( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))
106 iunin2 5075 . . . . . . . . . 10 𝑗 ∈ (1...𝑀)( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)))
107105, 106eqtr3i 2764 . . . . . . . . 9 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = ( 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)) ∩ 𝑗 ∈ (1...𝑀)((,)‘(𝐺𝑗)))
10896, 97, 1073eqtr4g 2799 . . . . . . . 8 (𝜑 → (𝐾 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
109108uneq2d 4177 . . . . . . 7 (𝜑 → ((𝐾𝐿) ∪ (𝐾 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))) = ((𝐾𝐿) ∪ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
11082, 109eqtrd 2774 . . . . . 6 (𝜑 → (𝐾𝐴) = ((𝐾𝐿) ∪ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
11135, 110sseqtrrid 4048 . . . . 5 (𝜑 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ (𝐾𝐴))
112111, 1sstrdi 4007 . . . 4 (𝜑 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾)
113 ovolsscl 25534 . . . 4 (( 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) → (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
114112, 12, 29, 113syl3anc 1370 . . 3 (𝜑 → (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
11534, 114readdcld 11287 . 2 (𝜑 → ((vol*‘(𝐾𝐿)) + (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))) ∈ ℝ)
11618rpred 13074 . . 3 (𝜑𝐶 ∈ ℝ)
11734, 116readdcld 11287 . 2 (𝜑 → ((vol*‘(𝐾𝐿)) + 𝐶) ∈ ℝ)
118110fveq2d 6910 . . 3 (𝜑 → (vol*‘(𝐾𝐴)) = (vol*‘((𝐾𝐿) ∪ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))))
11932, 12sstrid 4006 . . . 4 (𝜑 → (𝐾𝐿) ⊆ ℝ)
120112, 12sstrd 4005 . . . 4 (𝜑 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ℝ)
121 ovolun 25547 . . . 4 ((((𝐾𝐿) ⊆ ℝ ∧ (vol*‘(𝐾𝐿)) ∈ ℝ) ∧ ( 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ℝ ∧ (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)) → (vol*‘((𝐾𝐿) ∪ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))) ≤ ((vol*‘(𝐾𝐿)) + (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))))
122119, 34, 120, 114, 121syl22anc 839 . . 3 (𝜑 → (vol*‘((𝐾𝐿) ∪ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))) ≤ ((vol*‘(𝐾𝐿)) + (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))))
123118, 122eqbrtrd 5169 . 2 (𝜑 → (vol*‘(𝐾𝐴)) ≤ ((vol*‘(𝐾𝐿)) + (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))))
124 fzfid 14010 . . . . 5 (𝜑 → (1...𝑀) ∈ Fin)
125 iunss 5049 . . . . . . . 8 ( 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾 ↔ ∀𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾)
126112, 125sylib 218 . . . . . . 7 (𝜑 → ∀𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾)
127126r19.21bi 3248 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑀)) → 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾)
12812adantr 480 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑀)) → 𝐾 ⊆ ℝ)
12929adantr 480 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘𝐾) ∈ ℝ)
130 ovolsscl 25534 . . . . . 6 (( 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ 𝐾𝐾 ⊆ ℝ ∧ (vol*‘𝐾) ∈ ℝ) → (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
131127, 128, 129, 130syl3anc 1370 . . . . 5 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
132124, 131fsumrecl 15766 . . . 4 (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
133127, 128sstrd 4005 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑀)) → 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ℝ)
134133, 131jca 511 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑀)) → ( 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ℝ ∧ (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ))
135134ralrimiva 3143 . . . . 5 (𝜑 → ∀𝑗 ∈ (1...𝑀)( 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ℝ ∧ (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ))
136 ovolfiniun 25549 . . . . 5 (((1...𝑀) ∈ Fin ∧ ∀𝑗 ∈ (1...𝑀)( 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ℝ ∧ (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)) → (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
137124, 135, 136syl2anc 584 . . . 4 (𝜑 → (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
138 uniioombl.m . . . . . . . 8 (𝜑𝑀 ∈ ℕ)
139116, 138nndivred 12317 . . . . . . 7 (𝜑 → (𝐶 / 𝑀) ∈ ℝ)
140139adantr 480 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐶 / 𝑀) ∈ ℝ)
14177ineq2d 4227 . . . . . . . . . . . . 13 (𝜑 → (((,)‘(𝐺𝑗)) ∩ 𝐿) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖))))
142141adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺𝑗)) ∩ 𝐿) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖))))
14399a1i 11 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...𝑁) → (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖))))
144143iuneq2i 5017 . . . . . . . . . . . . 13 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = 𝑖 ∈ (1...𝑁)(((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖)))
145 iunin2 5075 . . . . . . . . . . . . 13 𝑖 ∈ (1...𝑁)(((,)‘(𝐺𝑗)) ∩ ((,)‘(𝐹𝑖))) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)))
146144, 145eqtri 2762 . . . . . . . . . . . 12 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)))
147142, 146eqtr4di 2792 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺𝑗)) ∩ 𝐿) = 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
148 fzfid 14010 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (1...𝑁) ∈ Fin)
149 ffvelcdm 7100 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑖 ∈ ℕ) → (𝐹𝑖) ∈ ( ≤ ∩ (ℝ × ℝ)))
15013, 73, 149syl2an 596 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (1...𝑁)) → (𝐹𝑖) ∈ ( ≤ ∩ (ℝ × ℝ)))
151150elin2d 4214 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (1...𝑁)) → (𝐹𝑖) ∈ (ℝ × ℝ))
152 1st2nd2 8051 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑖) ∈ (ℝ × ℝ) → (𝐹𝑖) = ⟨(1st ‘(𝐹𝑖)), (2nd ‘(𝐹𝑖))⟩)
153151, 152syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (1...𝑁)) → (𝐹𝑖) = ⟨(1st ‘(𝐹𝑖)), (2nd ‘(𝐹𝑖))⟩)
154153fveq2d 6910 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹𝑖)) = ((,)‘⟨(1st ‘(𝐹𝑖)), (2nd ‘(𝐹𝑖))⟩))
155 df-ov 7433 . . . . . . . . . . . . . . . . 17 ((1st ‘(𝐹𝑖))(,)(2nd ‘(𝐹𝑖))) = ((,)‘⟨(1st ‘(𝐹𝑖)), (2nd ‘(𝐹𝑖))⟩)
156154, 155eqtr4di 2792 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹𝑖)) = ((1st ‘(𝐹𝑖))(,)(2nd ‘(𝐹𝑖))))
157 ioombl 25613 . . . . . . . . . . . . . . . 16 ((1st ‘(𝐹𝑖))(,)(2nd ‘(𝐹𝑖))) ∈ dom vol
158156, 157eqeltrdi 2846 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹𝑖)) ∈ dom vol)
159158adantlr 715 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹𝑖)) ∈ dom vol)
160 ffvelcdm 7100 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
1616, 90, 160syl2an 596 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐺𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
162161elin2d 4214 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐺𝑗) ∈ (ℝ × ℝ))
163 1st2nd2 8051 . . . . . . . . . . . . . . . . . . 19 ((𝐺𝑗) ∈ (ℝ × ℝ) → (𝐺𝑗) = ⟨(1st ‘(𝐺𝑗)), (2nd ‘(𝐺𝑗))⟩)
164162, 163syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐺𝑗) = ⟨(1st ‘(𝐺𝑗)), (2nd ‘(𝐺𝑗))⟩)
165164fveq2d 6910 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺𝑗)) = ((,)‘⟨(1st ‘(𝐺𝑗)), (2nd ‘(𝐺𝑗))⟩))
166 df-ov 7433 . . . . . . . . . . . . . . . . 17 ((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗))) = ((,)‘⟨(1st ‘(𝐺𝑗)), (2nd ‘(𝐺𝑗))⟩)
167165, 166eqtr4di 2792 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺𝑗)) = ((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗))))
168 ioombl 25613 . . . . . . . . . . . . . . . 16 ((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗))) ∈ dom vol
169167, 168eqeltrdi 2846 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺𝑗)) ∈ dom vol)
170169adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐺𝑗)) ∈ dom vol)
171 inmbl 25590 . . . . . . . . . . . . . 14 ((((,)‘(𝐹𝑖)) ∈ dom vol ∧ ((,)‘(𝐺𝑗)) ∈ dom vol) → (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol)
172159, 170, 171syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol)
173172ralrimiva 3143 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → ∀𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol)
174 finiunmbl 25592 . . . . . . . . . . . 12 (((1...𝑁) ∈ Fin ∧ ∀𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol) → 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol)
175148, 173, 174syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol)
176147, 175eqeltrd 2838 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺𝑗)) ∩ 𝐿) ∈ dom vol)
177 inss2 4245 . . . . . . . . . . 11 (((,)‘(𝐺𝑗)) ∩ 𝐴) ⊆ 𝐴
17813uniiccdif 25626 . . . . . . . . . . . . . . 15 (𝜑 → ( ran ((,) ∘ 𝐹) ⊆ ran ([,] ∘ 𝐹) ∧ (vol*‘( ran ([,] ∘ 𝐹) ∖ ran ((,) ∘ 𝐹))) = 0))
179178simpld 494 . . . . . . . . . . . . . 14 (𝜑 ran ((,) ∘ 𝐹) ⊆ ran ([,] ∘ 𝐹))
180 ovolficcss 25517 . . . . . . . . . . . . . . 15 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ran ([,] ∘ 𝐹) ⊆ ℝ)
18113, 180syl 17 . . . . . . . . . . . . . 14 (𝜑 ran ([,] ∘ 𝐹) ⊆ ℝ)
182179, 181sstrd 4005 . . . . . . . . . . . . 13 (𝜑 ran ((,) ∘ 𝐹) ⊆ ℝ)
18316, 182eqsstrid 4043 . . . . . . . . . . . 12 (𝜑𝐴 ⊆ ℝ)
184183adantr 480 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → 𝐴 ⊆ ℝ)
185177, 184sstrid 4006 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺𝑗)) ∩ 𝐴) ⊆ ℝ)
186 inss1 4244 . . . . . . . . . . 11 (((,)‘(𝐺𝑗)) ∩ 𝐴) ⊆ ((,)‘(𝐺𝑗))
187 ioossre 13444 . . . . . . . . . . . 12 ((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗))) ⊆ ℝ
188167, 187eqsstrdi 4049 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺𝑗)) ⊆ ℝ)
189167fveq2d 6910 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺𝑗))) = (vol*‘((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗)))))
190 ovolfcl 25514 . . . . . . . . . . . . . . 15 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1st ‘(𝐺𝑗)) ∈ ℝ ∧ (2nd ‘(𝐺𝑗)) ∈ ℝ ∧ (1st ‘(𝐺𝑗)) ≤ (2nd ‘(𝐺𝑗))))
1916, 90, 190syl2an 596 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑀)) → ((1st ‘(𝐺𝑗)) ∈ ℝ ∧ (2nd ‘(𝐺𝑗)) ∈ ℝ ∧ (1st ‘(𝐺𝑗)) ≤ (2nd ‘(𝐺𝑗))))
192 ovolioo 25616 . . . . . . . . . . . . . 14 (((1st ‘(𝐺𝑗)) ∈ ℝ ∧ (2nd ‘(𝐺𝑗)) ∈ ℝ ∧ (1st ‘(𝐺𝑗)) ≤ (2nd ‘(𝐺𝑗))) → (vol*‘((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗)))) = ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))))
193191, 192syl 17 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘((1st ‘(𝐺𝑗))(,)(2nd ‘(𝐺𝑗)))) = ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))))
194189, 193eqtrd 2774 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺𝑗))) = ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))))
195191simp2d 1142 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (2nd ‘(𝐺𝑗)) ∈ ℝ)
196191simp1d 1141 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (1st ‘(𝐺𝑗)) ∈ ℝ)
197195, 196resubcld 11688 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → ((2nd ‘(𝐺𝑗)) − (1st ‘(𝐺𝑗))) ∈ ℝ)
198194, 197eqeltrd 2838 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺𝑗))) ∈ ℝ)
199 ovolsscl 25534 . . . . . . . . . . 11 (((((,)‘(𝐺𝑗)) ∩ 𝐴) ⊆ ((,)‘(𝐺𝑗)) ∧ ((,)‘(𝐺𝑗)) ⊆ ℝ ∧ (vol*‘((,)‘(𝐺𝑗))) ∈ ℝ) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) ∈ ℝ)
200186, 188, 198, 199mp3an2i 1465 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) ∈ ℝ)
201 mblsplit 25580 . . . . . . . . . 10 (((((,)‘(𝐺𝑗)) ∩ 𝐿) ∈ dom vol ∧ (((,)‘(𝐺𝑗)) ∩ 𝐴) ⊆ ℝ ∧ (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) ∈ ℝ) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) = ((vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺𝑗)) ∩ 𝐿))) + (vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿)))))
202176, 185, 200, 201syl3anc 1370 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) = ((vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺𝑗)) ∩ 𝐿))) + (vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿)))))
203 imassrn 6090 . . . . . . . . . . . . . . 15 (((,) ∘ 𝐹) “ (1...𝑁)) ⊆ ran ((,) ∘ 𝐹)
204203unissi 4920 . . . . . . . . . . . . . 14 (((,) ∘ 𝐹) “ (1...𝑁)) ⊆ ran ((,) ∘ 𝐹)
205204, 69, 163sstr4i 4038 . . . . . . . . . . . . 13 𝐿𝐴
206 sslin 4250 . . . . . . . . . . . . 13 (𝐿𝐴 → (((,)‘(𝐺𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺𝑗)) ∩ 𝐴))
207205, 206mp1i 13 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺𝑗)) ∩ 𝐴))
208 sseqin2 4230 . . . . . . . . . . . 12 ((((,)‘(𝐺𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺𝑗)) ∩ 𝐴) ↔ ((((,)‘(𝐺𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺𝑗)) ∩ 𝐿)) = (((,)‘(𝐺𝑗)) ∩ 𝐿))
209207, 208sylib 218 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → ((((,)‘(𝐺𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺𝑗)) ∩ 𝐿)) = (((,)‘(𝐺𝑗)) ∩ 𝐿))
210209fveq2d 6910 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺𝑗)) ∩ 𝐿))) = (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)))
211 indifdir 4300 . . . . . . . . . . . . 13 ((𝐴𝐿) ∩ ((,)‘(𝐺𝑗))) = ((𝐴 ∩ ((,)‘(𝐺𝑗))) ∖ (𝐿 ∩ ((,)‘(𝐺𝑗))))
212 incom 4216 . . . . . . . . . . . . . 14 (𝐴 ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ 𝐴)
213 incom 4216 . . . . . . . . . . . . . 14 (𝐿 ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ 𝐿)
214212, 213difeq12i 4133 . . . . . . . . . . . . 13 ((𝐴 ∩ ((,)‘(𝐺𝑗))) ∖ (𝐿 ∩ ((,)‘(𝐺𝑗)))) = ((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿))
215211, 214eqtri 2762 . . . . . . . . . . . 12 ((𝐴𝐿) ∩ ((,)‘(𝐺𝑗))) = ((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿))
21679eqcomd 2740 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = 𝐴)
21777ineq1d 4226 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ( 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
218 2fveq3 6911 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑖 → ((,)‘(𝐹𝑥)) = ((,)‘(𝐹𝑖)))
219218cbvdisjv 5125 . . . . . . . . . . . . . . . . . . . 20 (Disj 𝑥 ∈ ℕ ((,)‘(𝐹𝑥)) ↔ Disj 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)))
22014, 219sylib 218 . . . . . . . . . . . . . . . . . . 19 (𝜑Disj 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)))
221 fz1ssnn 13591 . . . . . . . . . . . . . . . . . . . 20 (1...𝑁) ⊆ ℕ
222221a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1...𝑁) ⊆ ℕ)
223 uzss 12898 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 + 1) ∈ (ℤ‘1) → (ℤ‘(𝑁 + 1)) ⊆ (ℤ‘1))
22439, 223syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (ℤ‘(𝑁 + 1)) ⊆ (ℤ‘1))
225224, 36sseqtrrdi 4046 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℤ‘(𝑁 + 1)) ⊆ ℕ)
22647ineq1d 4226 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((1...((𝑁 + 1) − 1)) ∩ (ℤ‘(𝑁 + 1))) = ((1...𝑁) ∩ (ℤ‘(𝑁 + 1))))
227 uzdisj 13633 . . . . . . . . . . . . . . . . . . . 20 ((1...((𝑁 + 1) − 1)) ∩ (ℤ‘(𝑁 + 1))) = ∅
228226, 227eqtr3di 2789 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅)
229 disjiun 5135 . . . . . . . . . . . . . . . . . . 19 ((Disj 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)) ∧ ((1...𝑁) ⊆ ℕ ∧ (ℤ‘(𝑁 + 1)) ⊆ ℕ ∧ ((1...𝑁) ∩ (ℤ‘(𝑁 + 1))) = ∅)) → ( 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ∅)
230220, 222, 225, 228, 229syl13anc 1371 . . . . . . . . . . . . . . . . . 18 (𝜑 → ( 𝑖 ∈ (1...𝑁)((,)‘(𝐹𝑖)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ∅)
231217, 230eqtrd 2774 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ∅)
232 uneqdifeq 4498 . . . . . . . . . . . . . . . . 17 ((𝐿𝐴 ∧ (𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = ∅) → ((𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = 𝐴 ↔ (𝐴𝐿) = 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
233205, 231, 232sylancr 587 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐿 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))) = 𝐴 ↔ (𝐴𝐿) = 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
234216, 233mpbid 232 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴𝐿) = 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))
235234adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑀)) → (𝐴𝐿) = 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))
236235ineq2d 4227 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺𝑗)) ∩ (𝐴𝐿)) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖))))
237 incom 4216 . . . . . . . . . . . . 13 ((𝐴𝐿) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ (𝐴𝐿))
238101, 98eqtri 2762 . . . . . . . . . . . . 13 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) = (((,)‘(𝐺𝑗)) ∩ 𝑖 ∈ (ℤ‘(𝑁 + 1))((,)‘(𝐹𝑖)))
239236, 237, 2383eqtr4g 2799 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → ((𝐴𝐿) ∩ ((,)‘(𝐺𝑗))) = 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
240215, 239eqtr3id 2788 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → ((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿)) = 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
241240fveq2d 6910 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿))) = (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
242210, 241oveq12d 7448 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺𝑗)) ∩ 𝐿))) + (vol*‘((((,)‘(𝐺𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺𝑗)) ∩ 𝐿)))) = ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))))
243202, 242eqtrd 2774 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) = ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))))
244200, 140resubcld 11688 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ∈ ℝ)
245 inss2 4245 . . . . . . . . . . . . 13 (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((,)‘(𝐺𝑗))
246188adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐺𝑗)) ⊆ ℝ)
247198adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol*‘((,)‘(𝐺𝑗))) ∈ ℝ)
248 ovolsscl 25534 . . . . . . . . . . . . 13 (((((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((,)‘(𝐺𝑗)) ∧ ((,)‘(𝐺𝑗)) ⊆ ℝ ∧ (vol*‘((,)‘(𝐺𝑗))) ∈ ℝ) → (vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
249245, 246, 247, 248mp3an2i 1465 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
250148, 249fsumrecl 15766 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
251 uniioombl.n2 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑗 ∈ (1...𝑀)(abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))
252251r19.21bi 3248 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → (abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))
253250, 200, 140absdifltd 15468 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → ((abs‘(Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) − (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀) ↔ (((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∧ Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) < ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) + (𝐶 / 𝑀)))))
254252, 253mpbid 232 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∧ Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) < ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) + (𝐶 / 𝑀))))
255254simpld 494 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
256244, 250, 255ltled 11406 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
257147fveq2d 6910 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) = (vol*‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
258 mblvol 25578 . . . . . . . . . . . . . . . . 17 ((((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol → (vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = (vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
259172, 258syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = (vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
260259, 249eqeltrd 2838 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ)
261172, 260jca 511 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ))
262261ralrimiva 3143 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → ∀𝑖 ∈ (1...𝑁)((((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ))
263 inss1 4244 . . . . . . . . . . . . . . . 16 (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((,)‘(𝐹𝑖))
264263rgenw 3062 . . . . . . . . . . . . . . 15 𝑖 ∈ ℕ (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((,)‘(𝐹𝑖))
265220adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)))
266 disjss2 5117 . . . . . . . . . . . . . . 15 (∀𝑖 ∈ ℕ (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ⊆ ((,)‘(𝐹𝑖)) → (Disj 𝑖 ∈ ℕ ((,)‘(𝐹𝑖)) → Disj 𝑖 ∈ ℕ (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
267264, 265, 266mpsyl 68 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ ℕ (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
268 disjss1 5120 . . . . . . . . . . . . . 14 ((1...𝑁) ⊆ ℕ → (Disj 𝑖 ∈ ℕ (((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) → Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
269221, 267, 268mpsyl 68 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))
270 volfiniun 25595 . . . . . . . . . . . . 13 (((1...𝑁) ∈ Fin ∧ ∀𝑖 ∈ (1...𝑁)((((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ∈ ℝ) ∧ Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) → (vol‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
271148, 262, 269, 270syl3anc 1370 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (vol‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
272 mblvol 25578 . . . . . . . . . . . . 13 ( 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))) ∈ dom vol → (vol‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = (vol*‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
273175, 272syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → (vol‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = (vol*‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
274259sumeq2dv 15734 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀)) → Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
275271, 273, 2743eqtr3d 2782 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
276257, 275eqtrd 2774 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) = Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))))
277256, 276breqtrrd 5175 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)))
278276, 250eqeltrd 2838 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) ∈ ℝ)
279200, 140, 278lesubaddd 11857 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑀)) → (((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) ↔ (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) ≤ ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀))))
280277, 279mpbid 232 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐴)) ≤ ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀)))
281243, 280eqbrtrrd 5171 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))) ≤ ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀)))
282131, 140, 278leadd2d 11855 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑀)) → ((vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ (𝐶 / 𝑀) ↔ ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))) ≤ ((vol*‘(((,)‘(𝐺𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀))))
283281, 282mpbird 257 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑀)) → (vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ (𝐶 / 𝑀))
284124, 131, 140, 283fsumle 15831 . . . . 5 (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀))
285139recnd 11286 . . . . . . 7 (𝜑 → (𝐶 / 𝑀) ∈ ℂ)
286 fsumconst 15822 . . . . . . 7 (((1...𝑀) ∈ Fin ∧ (𝐶 / 𝑀) ∈ ℂ) → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = ((♯‘(1...𝑀)) · (𝐶 / 𝑀)))
287124, 285, 286syl2anc 584 . . . . . 6 (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = ((♯‘(1...𝑀)) · (𝐶 / 𝑀)))
288 nnnn0 12530 . . . . . . . 8 (𝑀 ∈ ℕ → 𝑀 ∈ ℕ0)
289 hashfz1 14381 . . . . . . . 8 (𝑀 ∈ ℕ0 → (♯‘(1...𝑀)) = 𝑀)
290138, 288, 2893syl 18 . . . . . . 7 (𝜑 → (♯‘(1...𝑀)) = 𝑀)
291290oveq1d 7445 . . . . . 6 (𝜑 → ((♯‘(1...𝑀)) · (𝐶 / 𝑀)) = (𝑀 · (𝐶 / 𝑀)))
292116recnd 11286 . . . . . . 7 (𝜑𝐶 ∈ ℂ)
293138nncnd 12279 . . . . . . 7 (𝜑𝑀 ∈ ℂ)
294138nnne0d 12313 . . . . . . 7 (𝜑𝑀 ≠ 0)
295292, 293, 294divcan2d 12042 . . . . . 6 (𝜑 → (𝑀 · (𝐶 / 𝑀)) = 𝐶)
296287, 291, 2953eqtrd 2778 . . . . 5 (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = 𝐶)
297284, 296breqtrd 5173 . . . 4 (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘ 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ 𝐶)
298114, 132, 116, 137, 297letrd 11415 . . 3 (𝜑 → (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗)))) ≤ 𝐶)
299114, 116, 34, 298leadd2dd 11875 . 2 (𝜑 → ((vol*‘(𝐾𝐿)) + (vol*‘ 𝑗 ∈ (1...𝑀) 𝑖 ∈ (ℤ‘(𝑁 + 1))(((,)‘(𝐹𝑖)) ∩ ((,)‘(𝐺𝑗))))) ≤ ((vol*‘(𝐾𝐿)) + 𝐶))
30031, 115, 117, 123, 299letrd 11415 1 (𝜑 → (vol*‘(𝐾𝐴)) ≤ ((vol*‘(𝐾𝐿)) + 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wcel 2105  wral 3058  cdif 3959  cun 3960  cin 3961  wss 3962  c0 4338  𝒫 cpw 4604  cop 4636   cuni 4911   ciun 4995  Disj wdisj 5114   class class class wbr 5147   × cxp 5686  dom cdm 5688  ran crn 5689  cima 5691  ccom 5692  Fun wfun 6556   Fn wfn 6557  wf 6558  cfv 6562  (class class class)co 7430  1st c1st 8010  2nd c2nd 8011  Fincfn 8983  supcsup 9477  cc 11150  cr 11151  0cc0 11152  1c1 11153   + caddc 11155   · cmul 11157  *cxr 11291   < clt 11292  cle 11293  cmin 11489   / cdiv 11917  cn 12263  0cn0 12523  cuz 12875  +crp 13031  (,)cioo 13383  [,]cicc 13386  ...cfz 13543  seqcseq 14038  chash 14365  abscabs 15269  Σcsu 15718  vol*covol 25510  volcvol 25511
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-disj 5115  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-er 8743  df-map 8866  df-pm 8867  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fi 9448  df-sup 9479  df-inf 9480  df-oi 9547  df-dju 9938  df-card 9976  df-acn 9979  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-z 12611  df-uz 12876  df-q 12988  df-rp 13032  df-xneg 13151  df-xadd 13152  df-xmul 13153  df-ioo 13387  df-ico 13389  df-icc 13390  df-fz 13544  df-fzo 13691  df-fl 13828  df-seq 14039  df-exp 14099  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-rlim 15521  df-sum 15719  df-rest 17468  df-topgen 17489  df-psmet 21373  df-xmet 21374  df-met 21375  df-bl 21376  df-mopn 21377  df-top 22915  df-topon 22932  df-bases 22968  df-cmp 23410  df-ovol 25512  df-vol 25513
This theorem is referenced by:  uniioombllem5  25635
  Copyright terms: Public domain W3C validator