Metamath Proof Explorer

Theorem uniioombllem5

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses uniioombl.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
uniioombl.2 ⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
uniioombl.3 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
uniioombl.a ⊢ 𝐴 = ∪ ran ( (,) ∘ 𝐹 )
uniioombl.e ⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
uniioombl.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
uniioombl.g ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
uniioombl.s ⊢ ( 𝜑 → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
uniioombl.t ⊢ 𝑇 = seq 1 ( + , ( ( 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 uniioombllem5 ( 𝜑 → ( ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) ) ≤ ( ( vol* ‘ 𝐸 ) + ( 4 · 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 uniioombl.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
2 uniioombl.2 ⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
3 uniioombl.3 ⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
4 uniioombl.a ⊢ 𝐴 = ∪ ran ( (,) ∘ 𝐹 )
5 uniioombl.e ⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
6 uniioombl.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
7 uniioombl.g ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
8 uniioombl.s ⊢ ( 𝜑 → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
9 uniioombl.t ⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
10 uniioombl.v ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
11 uniioombl.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
12 uniioombl.m2 ⊢ ( 𝜑 → ( abs ‘ ( ( 𝑇 ‘ 𝑀 ) − sup ( ran 𝑇 , ℝ* , < ) ) ) < 𝐶 )
13 uniioombl.k ⊢ 𝐾 = ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) )
14 uniioombl.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
15 uniioombl.n2 ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 1 ... 𝑀 ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( vol* ‘ ( ( (,) ‘ ( 𝐹 ‘ 𝑖 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ) ) − ( vol* ‘ ( ( (,) ‘ ( 𝐺 ‘ 𝑗 ) ) ∩ 𝐴 ) ) ) ) < ( 𝐶 / 𝑀 ) )
16 uniioombl.l ⊢ 𝐿 = ∪ ( ( (,) ∘ 𝐹 ) “ ( 1 ... 𝑁 ) )
17 inss1 ⊢ ( 𝐸 ∩ 𝐴 ) ⊆ 𝐸
18 7 uniiccdif ⊢ ( 𝜑 → ( ∪ ran ( (,) ∘ 𝐺 ) ⊆ ∪ ran ( [,] ∘ 𝐺 ) ∧ ( vol* ‘ ( ∪ ran ( [,] ∘ 𝐺 ) ∖ ∪ ran ( (,) ∘ 𝐺 ) ) ) = 0 ) )
19 18 simpld ⊢ ( 𝜑 → ∪ ran ( (,) ∘ 𝐺 ) ⊆ ∪ ran ( [,] ∘ 𝐺 ) )
20 ovolficcss ⊢ ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ∪ ran ( [,] ∘ 𝐺 ) ⊆ ℝ )
21 7 20 syl ⊢ ( 𝜑 → ∪ ran ( [,] ∘ 𝐺 ) ⊆ ℝ )
22 19 21 sstrd ⊢ ( 𝜑 → ∪ ran ( (,) ∘ 𝐺 ) ⊆ ℝ )
23 8 22 sstrd ⊢ ( 𝜑 → 𝐸 ⊆ ℝ )
24 ovolsscl ⊢ ( ( ( 𝐸 ∩ 𝐴 ) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ ( vol* ‘ 𝐸 ) ∈ ℝ ) → ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) ∈ ℝ )
25 17 23 5 24 mp3an2i ⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) ∈ ℝ )
26 difssd ⊢ ( 𝜑 → ( 𝐸 ∖ 𝐴 ) ⊆ 𝐸 )
27 ovolsscl ⊢ ( ( ( 𝐸 ∖ 𝐴 ) ⊆ 𝐸 ∧ 𝐸 ⊆ ℝ ∧ ( vol* ‘ 𝐸 ) ∈ ℝ ) → ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) ∈ ℝ )
28 26 23 5 27 syl3anc ⊢ ( 𝜑 → ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) ∈ ℝ )
29 25 28 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) ) ∈ ℝ )
30 inss1 ⊢ ( 𝐾 ∩ 𝐴 ) ⊆ 𝐾
31 imassrn ⊢ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) ⊆ ran ( (,) ∘ 𝐺 )
32 31 unissi ⊢ ∪ ( ( (,) ∘ 𝐺 ) “ ( 1 ... 𝑀 ) ) ⊆ ∪ ran ( (,) ∘ 𝐺 )
33 13 32 eqsstri ⊢ 𝐾 ⊆ ∪ ran ( (,) ∘ 𝐺 )
34 33 22 sstrid ⊢ ( 𝜑 → 𝐾 ⊆ ℝ )
35 1 2 3 4 5 6 7 8 9 10 uniioombllem1 ⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ )
36 ssid ⊢ ∪ ran ( (,) ∘ 𝐺 ) ⊆ ∪ ran ( (,) ∘ 𝐺 )
37 9 ovollb ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ∪ ran ( (,) ∘ 𝐺 ) ⊆ ∪ ran ( (,) ∘ 𝐺 ) ) → ( vol* ‘ ∪ ran ( (,) ∘ 𝐺 ) ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
38 7 36 37 sylancl ⊢ ( 𝜑 → ( vol* ‘ ∪ ran ( (,) ∘ 𝐺 ) ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
39 ovollecl ⊢ ( ( ∪ ran ( (,) ∘ 𝐺 ) ⊆ ℝ ∧ sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ ∧ ( vol* ‘ ∪ ran ( (,) ∘ 𝐺 ) ) ≤ sup ( ran 𝑇 , ℝ* , < ) ) → ( vol* ‘ ∪ ran ( (,) ∘ 𝐺 ) ) ∈ ℝ )
40 22 35 38 39 syl3anc ⊢ ( 𝜑 → ( vol* ‘ ∪ ran ( (,) ∘ 𝐺 ) ) ∈ ℝ )
41 ovolsscl ⊢ ( ( 𝐾 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ∧ ∪ ran ( (,) ∘ 𝐺 ) ⊆ ℝ ∧ ( vol* ‘ ∪ ran ( (,) ∘ 𝐺 ) ) ∈ ℝ ) → ( vol* ‘ 𝐾 ) ∈ ℝ )
42 33 22 40 41 mp3an2i ⊢ ( 𝜑 → ( vol* ‘ 𝐾 ) ∈ ℝ )
43 ovolsscl ⊢ ( ( ( 𝐾 ∩ 𝐴 ) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ ( vol* ‘ 𝐾 ) ∈ ℝ ) → ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) ∈ ℝ )
44 30 34 42 43 mp3an2i ⊢ ( 𝜑 → ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) ∈ ℝ )
45 difssd ⊢ ( 𝜑 → ( 𝐾 ∖ 𝐴 ) ⊆ 𝐾 )
46 ovolsscl ⊢ ( ( ( 𝐾 ∖ 𝐴 ) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ ( vol* ‘ 𝐾 ) ∈ ℝ ) → ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) ∈ ℝ )
47 45 34 42 46 syl3anc ⊢ ( 𝜑 → ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) ∈ ℝ )
48 44 47 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) ) ∈ ℝ )
49 6 rpred ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
50 49 49 readdcld ⊢ ( 𝜑 → ( 𝐶 + 𝐶 ) ∈ ℝ )
51 48 50 readdcld ⊢ ( 𝜑 → ( ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) ) + ( 𝐶 + 𝐶 ) ) ∈ ℝ )
52 4re ⊢ 4 ∈ ℝ
53 remulcl ⊢ ( ( 4 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 4 · 𝐶 ) ∈ ℝ )
54 52 49 53 sylancr ⊢ ( 𝜑 → ( 4 · 𝐶 ) ∈ ℝ )
55 5 54 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ 𝐸 ) + ( 4 · 𝐶 ) ) ∈ ℝ )
56 1 2 3 4 5 6 7 8 9 10 11 12 13 uniioombllem3 ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) ) < ( ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) ) + ( 𝐶 + 𝐶 ) ) )
57 29 51 56 ltled ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) ) ≤ ( ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) ) + ( 𝐶 + 𝐶 ) ) )
58 5 50 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ 𝐸 ) + ( 𝐶 + 𝐶 ) ) ∈ ℝ )
59 42 49 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ 𝐾 ) + 𝐶 ) ∈ ℝ )
60 inss1 ⊢ ( 𝐾 ∩ 𝐿 ) ⊆ 𝐾
61 ovolsscl ⊢ ( ( ( 𝐾 ∩ 𝐿 ) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ ( vol* ‘ 𝐾 ) ∈ ℝ ) → ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) ∈ ℝ )
62 60 34 42 61 mp3an2i ⊢ ( 𝜑 → ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) ∈ ℝ )
63 62 49 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) + 𝐶 ) ∈ ℝ )
64 difssd ⊢ ( 𝜑 → ( 𝐾 ∖ 𝐿 ) ⊆ 𝐾 )
65 ovolsscl ⊢ ( ( ( 𝐾 ∖ 𝐿 ) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ ( vol* ‘ 𝐾 ) ∈ ℝ ) → ( vol* ‘ ( 𝐾 ∖ 𝐿 ) ) ∈ ℝ )
66 64 34 42 65 syl3anc ⊢ ( 𝜑 → ( vol* ‘ ( 𝐾 ∖ 𝐿 ) ) ∈ ℝ )
67 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 uniioombllem4 ⊢ ( 𝜑 → ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) ≤ ( ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) + 𝐶 ) )
68 imassrn ⊢ ( ( (,) ∘ 𝐹 ) “ ( 1 ... 𝑁 ) ) ⊆ ran ( (,) ∘ 𝐹 )
69 68 unissi ⊢ ∪ ( ( (,) ∘ 𝐹 ) “ ( 1 ... 𝑁 ) ) ⊆ ∪ ran ( (,) ∘ 𝐹 )
70 69 16 4 3sstr4i ⊢ 𝐿 ⊆ 𝐴
71 sscon ⊢ ( 𝐿 ⊆ 𝐴 → ( 𝐾 ∖ 𝐴 ) ⊆ ( 𝐾 ∖ 𝐿 ) )
72 70 71 mp1i ⊢ ( 𝜑 → ( 𝐾 ∖ 𝐴 ) ⊆ ( 𝐾 ∖ 𝐿 ) )
73 64 34 sstrd ⊢ ( 𝜑 → ( 𝐾 ∖ 𝐿 ) ⊆ ℝ )
74 ovolss ⊢ ( ( ( 𝐾 ∖ 𝐴 ) ⊆ ( 𝐾 ∖ 𝐿 ) ∧ ( 𝐾 ∖ 𝐿 ) ⊆ ℝ ) → ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) ≤ ( vol* ‘ ( 𝐾 ∖ 𝐿 ) ) )
75 72 73 74 syl2anc ⊢ ( 𝜑 → ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) ≤ ( vol* ‘ ( 𝐾 ∖ 𝐿 ) ) )
76 44 47 63 66 67 75 le2addd ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) ) ≤ ( ( ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) + 𝐶 ) + ( vol* ‘ ( 𝐾 ∖ 𝐿 ) ) ) )
77 62 recnd ⊢ ( 𝜑 → ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) ∈ ℂ )
78 49 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
79 66 recnd ⊢ ( 𝜑 → ( vol* ‘ ( 𝐾 ∖ 𝐿 ) ) ∈ ℂ )
80 77 78 79 add32d ⊢ ( 𝜑 → ( ( ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) + 𝐶 ) + ( vol* ‘ ( 𝐾 ∖ 𝐿 ) ) ) = ( ( ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) + ( vol* ‘ ( 𝐾 ∖ 𝐿 ) ) ) + 𝐶 ) )
81 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
82 inss2 ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
83 rexpssxrxp ⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
84 82 83 sstri ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* )
85 fss ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* ) ) → 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) )
86 1 84 85 sylancl ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) )
87 fco ⊢ ( ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ ∧ 𝐹 : ℕ ⟶ ( ℝ* × ℝ* ) ) → ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ )
88 81 86 87 sylancr ⊢ ( 𝜑 → ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ )
89 ffun ⊢ ( ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ → Fun ( (,) ∘ 𝐹 ) )
90 funiunfv ⊢ ( Fun ( (,) ∘ 𝐹 ) → ∪ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ∪ ( ( (,) ∘ 𝐹 ) “ ( 1 ... 𝑁 ) ) )
91 88 89 90 3syl ⊢ ( 𝜑 → ∪ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ∪ ( ( (,) ∘ 𝐹 ) “ ( 1 ... 𝑁 ) ) )
92 91 16 eqtr4di ⊢ ( 𝜑 → ∪ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = 𝐿 )
93 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
94 elfznn ⊢ ( 𝑛 ∈ ( 1 ... 𝑁 ) → 𝑛 ∈ ℕ )
95 fvco3 ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) )
96 1 94 95 syl2an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) )
97 ffvelrn ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
98 1 94 97 syl2an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
99 98 elin2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) )
100 1st2nd2 ⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑛 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
101 99 100 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑛 ) = ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
102 101 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ ) )
103 df-ov ⊢ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) = ( (,) ‘ ⟨ ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ⟩ )
104 102 103 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( (,) ‘ ( 𝐹 ‘ 𝑛 ) ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
105 96 104 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) = ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
106 ioombl ⊢ ( ( 1st ‘ ( 𝐹 ‘ 𝑛 ) ) (,) ( 2nd ‘ ( 𝐹 ‘ 𝑛 ) ) ) ∈ dom vol
107 105 106 eqeltrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ∈ dom vol )
108 107 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ∈ dom vol )
109 finiunmbl ⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ ∀ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ∈ dom vol ) → ∪ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ∈ dom vol )
110 93 108 109 syl2anc ⊢ ( 𝜑 → ∪ 𝑛 ∈ ( 1 ... 𝑁 ) ( ( (,) ∘ 𝐹 ) ‘ 𝑛 ) ∈ dom vol )
111 92 110 eqeltrrd ⊢ ( 𝜑 → 𝐿 ∈ dom vol )
112 mblsplit ⊢ ( ( 𝐿 ∈ dom vol ∧ 𝐾 ⊆ ℝ ∧ ( vol* ‘ 𝐾 ) ∈ ℝ ) → ( vol* ‘ 𝐾 ) = ( ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) + ( vol* ‘ ( 𝐾 ∖ 𝐿 ) ) ) )
113 111 34 42 112 syl3anc ⊢ ( 𝜑 → ( vol* ‘ 𝐾 ) = ( ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) + ( vol* ‘ ( 𝐾 ∖ 𝐿 ) ) ) )
114 113 oveq1d ⊢ ( 𝜑 → ( ( vol* ‘ 𝐾 ) + 𝐶 ) = ( ( ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) + ( vol* ‘ ( 𝐾 ∖ 𝐿 ) ) ) + 𝐶 ) )
115 80 114 eqtr4d ⊢ ( 𝜑 → ( ( ( vol* ‘ ( 𝐾 ∩ 𝐿 ) ) + 𝐶 ) + ( vol* ‘ ( 𝐾 ∖ 𝐿 ) ) ) = ( ( vol* ‘ 𝐾 ) + 𝐶 ) )
116 76 115 breqtrd ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) ) ≤ ( ( vol* ‘ 𝐾 ) + 𝐶 ) )
117 5 49 readdcld ⊢ ( 𝜑 → ( ( vol* ‘ 𝐸 ) + 𝐶 ) ∈ ℝ )
118 9 ovollb ⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐾 ⊆ ∪ ran ( (,) ∘ 𝐺 ) ) → ( vol* ‘ 𝐾 ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
119 7 33 118 sylancl ⊢ ( 𝜑 → ( vol* ‘ 𝐾 ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
120 42 35 117 119 10 letrd ⊢ ( 𝜑 → ( vol* ‘ 𝐾 ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
121 42 117 49 120 leadd1dd ⊢ ( 𝜑 → ( ( vol* ‘ 𝐾 ) + 𝐶 ) ≤ ( ( ( vol* ‘ 𝐸 ) + 𝐶 ) + 𝐶 ) )
122 5 recnd ⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℂ )
123 122 78 78 addassd ⊢ ( 𝜑 → ( ( ( vol* ‘ 𝐸 ) + 𝐶 ) + 𝐶 ) = ( ( vol* ‘ 𝐸 ) + ( 𝐶 + 𝐶 ) ) )
124 121 123 breqtrd ⊢ ( 𝜑 → ( ( vol* ‘ 𝐾 ) + 𝐶 ) ≤ ( ( vol* ‘ 𝐸 ) + ( 𝐶 + 𝐶 ) ) )
125 48 59 58 116 124 letrd ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) ) ≤ ( ( vol* ‘ 𝐸 ) + ( 𝐶 + 𝐶 ) ) )
126 48 58 50 125 leadd1dd ⊢ ( 𝜑 → ( ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) ) + ( 𝐶 + 𝐶 ) ) ≤ ( ( ( vol* ‘ 𝐸 ) + ( 𝐶 + 𝐶 ) ) + ( 𝐶 + 𝐶 ) ) )
127 50 recnd ⊢ ( 𝜑 → ( 𝐶 + 𝐶 ) ∈ ℂ )
128 122 127 127 addassd ⊢ ( 𝜑 → ( ( ( vol* ‘ 𝐸 ) + ( 𝐶 + 𝐶 ) ) + ( 𝐶 + 𝐶 ) ) = ( ( vol* ‘ 𝐸 ) + ( ( 𝐶 + 𝐶 ) + ( 𝐶 + 𝐶 ) ) ) )
129 2t2e4 ⊢ ( 2 · 2 ) = 4
130 129 oveq1i ⊢ ( ( 2 · 2 ) · 𝐶 ) = ( 4 · 𝐶 )
131 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
132 131 131 78 mulassd ⊢ ( 𝜑 → ( ( 2 · 2 ) · 𝐶 ) = ( 2 · ( 2 · 𝐶 ) ) )
133 78 2timesd ⊢ ( 𝜑 → ( 2 · 𝐶 ) = ( 𝐶 + 𝐶 ) )
134 133 oveq2d ⊢ ( 𝜑 → ( 2 · ( 2 · 𝐶 ) ) = ( 2 · ( 𝐶 + 𝐶 ) ) )
135 127 2timesd ⊢ ( 𝜑 → ( 2 · ( 𝐶 + 𝐶 ) ) = ( ( 𝐶 + 𝐶 ) + ( 𝐶 + 𝐶 ) ) )
136 132 134 135 3eqtrd ⊢ ( 𝜑 → ( ( 2 · 2 ) · 𝐶 ) = ( ( 𝐶 + 𝐶 ) + ( 𝐶 + 𝐶 ) ) )
137 130 136 eqtr3id ⊢ ( 𝜑 → ( 4 · 𝐶 ) = ( ( 𝐶 + 𝐶 ) + ( 𝐶 + 𝐶 ) ) )
138 137 oveq2d ⊢ ( 𝜑 → ( ( vol* ‘ 𝐸 ) + ( 4 · 𝐶 ) ) = ( ( vol* ‘ 𝐸 ) + ( ( 𝐶 + 𝐶 ) + ( 𝐶 + 𝐶 ) ) ) )
139 128 138 eqtr4d ⊢ ( 𝜑 → ( ( ( vol* ‘ 𝐸 ) + ( 𝐶 + 𝐶 ) ) + ( 𝐶 + 𝐶 ) ) = ( ( vol* ‘ 𝐸 ) + ( 4 · 𝐶 ) ) )
140 126 139 breqtrd ⊢ ( 𝜑 → ( ( ( vol* ‘ ( 𝐾 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐾 ∖ 𝐴 ) ) ) + ( 𝐶 + 𝐶 ) ) ≤ ( ( vol* ‘ 𝐸 ) + ( 4 · 𝐶 ) ) )
141 29 51 55 57 140 letrd ⊢ ( 𝜑 → ( ( vol* ‘ ( 𝐸 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐸 ∖ 𝐴 ) ) ) ≤ ( ( vol* ‘ 𝐸 ) + ( 4 · 𝐶 ) ) )