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		ffvelcdm	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
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 · 𝐶 ) ) )