uniioombllem4 - Metamath Proof Explorer

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

Theorem uniioombllem4 25640

Description: Lemma for uniioombl 25643. (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**
Step	Hyp	Ref	Expression
1		inss1 4258	. . 3 ⊢ (𝐾 ∩ 𝐴) ⊆ 𝐾
2		uniioombl.k	. . . . 5 ⊢ 𝐾 = ∪ (((,) ∘ 𝐺) “ (1...𝑀))
3		imassrn 6100	. . . . . 6 ⊢ (((,) ∘ 𝐺) “ (1...𝑀)) ⊆ ran ((,) ∘ 𝐺)
4	3	unissi 4940	. . . . 5 ⊢ ∪ (((,) ∘ 𝐺) “ (1...𝑀)) ⊆ ∪ ran ((,) ∘ 𝐺)
5	2, 4	eqsstri 4043	. . . 4 ⊢ 𝐾 ⊆ ∪ ran ((,) ∘ 𝐺)
6		uniioombl.g	. . . . . . 7 ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
7	6	uniiccdif 25632	. . . . . 6 ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ([,] ∘ 𝐺) ∧ (vol*‘(∪ ran ([,] ∘ 𝐺) ∖ ∪ ran ((,) ∘ 𝐺))) = 0))
8	7	simpld 494	. . . . 5 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ([,] ∘ 𝐺))
9		ovolficcss 25523	. . . . . 6 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ)
10	6, 9	syl 17	. . . . 5 ⊢ (𝜑 → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ)
11	8, 10	sstrd 4019	. . . 4 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ℝ)
12	5, 11	sstrid 4020	. . 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‘𝐸) + 𝐶))
22	13, 14, 15, 16, 17, 18, 6, 19, 20, 21	uniioombllem1 25635	. . . . 5 ⊢ (𝜑 → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
23		ssid 4031	. . . . . 6 ⊢ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)
24	20	ovollb 25533	. . . . . 6 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)) → (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < ))
25	6, 23, 24	sylancl 585	. . . . 5 ⊢ (𝜑 → (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < ))
26		ovollecl 25537	. . . . 5 ⊢ ((∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ sup(ran 𝑇, ℝ^, < ) ∈ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < )) → (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ)
27	11, 22, 25, 26	syl3anc 1371	. . . 4 ⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ)
28		ovolsscl 25540	. . . 4 ⊢ ((𝐾 ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol‘𝐾) ∈ ℝ)
29	5, 11, 27, 28	mp3an2i 1466	. . 3 ⊢ (𝜑 → (vol*‘𝐾) ∈ ℝ)
30		ovolsscl 25540	. . 3 ⊢ (((𝐾 ∩ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘(𝐾 ∩ 𝐴)) ∈ ℝ)
31	1, 12, 29, 30	mp3an2i 1466	. 2 ⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ)
32		inss1 4258	. . . 4 ⊢ (𝐾 ∩ 𝐿) ⊆ 𝐾
33		ovolsscl 25540	. . . 4 ⊢ (((𝐾 ∩ 𝐿) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘(𝐾 ∩ 𝐿)) ∈ ℝ)
34	32, 12, 29, 33	mp3an2i 1466	. . 3 ⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐿)) ∈ ℝ)
35		ssun2 4202	. . . . . 6 ⊢ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
36		nnuz 12946	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
37		uniioombl.n	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℕ)
38	37	peano2nnd 12310	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ)
39	38, 36	eleqtrdi 2854	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘1))
40		uzsplit 13656	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘1) → (ℤ_≥‘1) = ((1...((𝑁 + 1) − 1)) ∪ (ℤ_≥‘(𝑁 + 1))))
41	39, 40	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℤ_≥‘1) = ((1...((𝑁 + 1) − 1)) ∪ (ℤ_≥‘(𝑁 + 1))))
42	36, 41	eqtrid 2792	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℕ = ((1...((𝑁 + 1) − 1)) ∪ (ℤ_≥‘(𝑁 + 1))))
43	37	nncnd 12309	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℂ)
44		ax-1cn 11242	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℂ
45		pncan 11542	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
46	43, 44, 45	sylancl 585	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
47	46	oveq2d 7464	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...((𝑁 + 1) − 1)) = (1...𝑁))
48	47	uneq1d 4190	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1...((𝑁 + 1) − 1)) ∪ (ℤ_≥‘(𝑁 + 1))) = ((1...𝑁) ∪ (ℤ_≥‘(𝑁 + 1))))
49	42, 48	eqtrd 2780	. . . . . . . . . . . 12 ⊢ (𝜑 → ℕ = ((1...𝑁) ∪ (ℤ_≥‘(𝑁 + 1))))
50	49	iuneq1d 5042	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) = ∪ 𝑖 ∈ ((1...𝑁) ∪ (ℤ_≥‘(𝑁 + 1)))((,)‘(𝐹‘𝑖)))
51		iunxun 5117	. . . . . . . . . . 11 ⊢ ∪ 𝑖 ∈ ((1...𝑁) ∪ (ℤ_≥‘(𝑁 + 1)))((,)‘(𝐹‘𝑖)) = (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
52	50, 51	eqtrdi 2796	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) = (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
53		ioof 13507	. . . . . . . . . . . . . 14 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
54		inss2 4259	. . . . . . . . . . . . . . . 16 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
55		rexpssxrxp 11335	. . . . . . . . . . . . . . . 16 ⊢ (ℝ × ℝ) ⊆ (ℝ^* × ℝ^*)
56	54, 55	sstri 4018	. . . . . . . . . . . . . . 15 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^*)
57		fss 6763	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^)) → 𝐹:ℕ⟶(ℝ^ × ℝ^*))
58	13, 56, 57	sylancl 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ^* × ℝ^*))
59		fco 6771	. . . . . . . . . . . . . 14 ⊢ (((,):(ℝ^* × ℝ^)⟶𝒫 ℝ ∧ 𝐹:ℕ⟶(ℝ^ × ℝ^*)) → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
60	53, 58, 59	sylancr 586	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
61		ffn 6747	. . . . . . . . . . . . 13 ⊢ (((,) ∘ 𝐹):ℕ⟶𝒫 ℝ → ((,) ∘ 𝐹) Fn ℕ)
62		fniunfv 7284	. . . . . . . . . . . . 13 ⊢ (((,) ∘ 𝐹) Fn ℕ → ∪ 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ∪ ran ((,) ∘ 𝐹))
63	60, 61, 62	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ∪ ran ((,) ∘ 𝐹))
64		fvco3 7021	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑖 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹‘𝑖)))
65	13, 64	sylan 579	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹‘𝑖)))
66	65	iuneq2dv 5039	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
67	63, 66	eqtr3d 2782	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
68	16, 67	eqtrid 2792	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 = ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
69		uniioombl.l	. . . . . . . . . . . 12 ⊢ 𝐿 = ∪ (((,) ∘ 𝐹) “ (1...𝑁))
70		ffun 6750	. . . . . . . . . . . . . 14 ⊢ (((,) ∘ 𝐹):ℕ⟶𝒫 ℝ → Fun ((,) ∘ 𝐹))
71		funiunfv 7285	. . . . . . . . . . . . . 14 ⊢ (Fun ((,) ∘ 𝐹) → ∪ 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = ∪ (((,) ∘ 𝐹) “ (1...𝑁)))
72	60, 70, 71	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = ∪ (((,) ∘ 𝐹) “ (1...𝑁)))
73		elfznn 13613	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑁) → 𝑖 ∈ ℕ)
74	13, 73, 64	syl2an 595	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹‘𝑖)))
75	74	iuneq2dv 5039	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))
76	72, 75	eqtr3d 2782	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ (((,) ∘ 𝐹) “ (1...𝑁)) = ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))
77	69, 76	eqtrid 2792	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 = ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))
78	77	uneq1d 4190	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
79	52, 68, 78	3eqtr4d 2790	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 = (𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
80	79	ineq2d 4241	. . . . . . . 8 ⊢ (𝜑 → (𝐾 ∩ 𝐴) = (𝐾 ∩ (𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))))
81		indi 4303	. . . . . . . 8 ⊢ (𝐾 ∩ (𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) = ((𝐾 ∩ 𝐿) ∪ (𝐾 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
82	80, 81	eqtrdi 2796	. . . . . . 7 ⊢ (𝜑 → (𝐾 ∩ 𝐴) = ((𝐾 ∩ 𝐿) ∪ (𝐾 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))))
83		fss 6763	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^)) → 𝐺:ℕ⟶(ℝ^ × ℝ^*))
84	6, 56, 83	sylancl 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺:ℕ⟶(ℝ^* × ℝ^*))
85		fco 6771	. . . . . . . . . . . . . 14 ⊢ (((,):(ℝ^* × ℝ^)⟶𝒫 ℝ ∧ 𝐺:ℕ⟶(ℝ^ × ℝ^*)) → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
86	53, 84, 85	sylancr 586	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
87		ffun 6750	. . . . . . . . . . . . 13 ⊢ (((,) ∘ 𝐺):ℕ⟶𝒫 ℝ → Fun ((,) ∘ 𝐺))
88		funiunfv 7285	. . . . . . . . . . . . 13 ⊢ (Fun ((,) ∘ 𝐺) → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ (((,) ∘ 𝐺) “ (1...𝑀)))
89	86, 87, 88	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ (((,) ∘ 𝐺) “ (1...𝑀)))
90		elfznn 13613	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
91		fvco3 7021	. . . . . . . . . . . . . 14 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑗) = ((,)‘(𝐺‘𝑗)))
92	6, 90, 91	syl2an 595	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,) ∘ 𝐺)‘𝑗) = ((,)‘(𝐺‘𝑗)))
93	92	iuneq2dv 5039	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
94	89, 93	eqtr3d 2782	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (1...𝑀)) = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
95	2, 94	eqtrid 2792	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
96	95	ineq2d 4241	. . . . . . . . 9 ⊢ (𝜑 → (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ 𝐾) = (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))))
97		incom 4230	. . . . . . . . 9 ⊢ (𝐾 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ 𝐾)
98		iunin2 5094	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
99		incom 4230	. . . . . . . . . . . . . . 15 ⊢ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖)))
100	99	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ_≥‘(𝑁 + 1)) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))))
101	100	iuneq2i 5036	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖)))
102		incom 4230	. . . . . . . . . . . . 13 ⊢ (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
103	98, 101, 102	3eqtr4ri 2779	. . . . . . . . . . . 12 ⊢ (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))
104	103	a1i 11	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑀) → (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
105	104	iuneq2i 5036	. . . . . . . . . 10 ⊢ ∪ 𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))
106		iunin2 5094	. . . . . . . . . 10 ⊢ ∪ 𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
107	105, 106	eqtr3i 2770	. . . . . . . . 9 ⊢ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
108	96, 97, 107	3eqtr4g 2805	. . . . . . . 8 ⊢ (𝜑 → (𝐾 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
109	108	uneq2d 4191	. . . . . . 7 ⊢ (𝜑 → ((𝐾 ∩ 𝐿) ∪ (𝐾 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) = ((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
110	82, 109	eqtrd 2780	. . . . . 6 ⊢ (𝜑 → (𝐾 ∩ 𝐴) = ((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
111	35, 110	sseqtrrid 4062	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ (𝐾 ∩ 𝐴))
112	111, 1	sstrdi 4021	. . . 4 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾)
113		ovolsscl 25540	. . . 4 ⊢ ((∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
114	112, 12, 29, 113	syl3anc 1371	. . 3 ⊢ (𝜑 → (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
115	34, 114	readdcld 11319	. 2 ⊢ (𝜑 → ((vol‘(𝐾 ∩ 𝐿)) + (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ∈ ℝ)
116	18	rpred 13099	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
117	34, 116	readdcld 11319	. 2 ⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐿)) + 𝐶) ∈ ℝ)
118	110	fveq2d 6924	. . 3 ⊢ (𝜑 → (vol‘(𝐾 ∩ 𝐴)) = (vol‘((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
119	32, 12	sstrid 4020	. . . 4 ⊢ (𝜑 → (𝐾 ∩ 𝐿) ⊆ ℝ)
120	112, 12	sstrd 4019	. . . 4 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ)
121		ovolun 25553	. . . 4 ⊢ ((((𝐾 ∩ 𝐿) ⊆ ℝ ∧ (vol‘(𝐾 ∩ 𝐿)) ∈ ℝ) ∧ (∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧ (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)) → (vol‘((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
122	119, 34, 120, 114, 121	syl22anc 838	. . 3 ⊢ (𝜑 → (vol‘((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
123	118, 122	eqbrtrd 5188	. 2 ⊢ (𝜑 → (vol‘(𝐾 ∩ 𝐴)) ≤ ((vol‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
124		fzfid 14024	. . . . 5 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
125		iunss 5068	. . . . . . . 8 ⊢ (∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾 ↔ ∀𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾)
126	112, 125	sylib 218	. . . . . . 7 ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾)
127	126	r19.21bi 3257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾)
128	12	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐾 ⊆ ℝ)
129	29	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘𝐾) ∈ ℝ)
130		ovolsscl 25540	. . . . . 6 ⊢ ((∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
131	127, 128, 129, 130	syl3anc 1371	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
132	124, 131	fsumrecl 15782	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
133	127, 128	sstrd 4019	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ)
134	133, 131	jca 511	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧ (vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ))
135	134	ralrimiva 3152	. . . . 5 ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧ (vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ))
136		ovolfiniun 25555	. . . . 5 ⊢ (((1...𝑀) ∈ Fin ∧ ∀𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧ (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)) → (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
137	124, 135, 136	syl2anc 583	. . . 4 ⊢ (𝜑 → (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
138		uniioombl.m	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ)
139	116, 138	nndivred 12347	. . . . . . 7 ⊢ (𝜑 → (𝐶 / 𝑀) ∈ ℝ)
140	139	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐶 / 𝑀) ∈ ℝ)
141	77	ineq2d 4241	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖))))
142	141	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖))))
143	99	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑁) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))))
144	143	iuneq2i 5036	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖)))
145		iunin2 5094	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))
146	144, 145	eqtri 2768	. . . . . . . . . . . 12 ⊢ ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))
147	142, 146	eqtr4di 2798	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) = ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
148		fzfid 14024	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1...𝑁) ∈ Fin)
149		ffvelcdm 7115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ ( ≤ ∩ (ℝ × ℝ)))
150	13, 73, 149	syl2an 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑖) ∈ ( ≤ ∩ (ℝ × ℝ)))
151	150	elin2d 4228	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑖) ∈ (ℝ × ℝ))
152		1st2nd2 8069	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑖) ∈ (ℝ × ℝ) → (𝐹‘𝑖) = ⟨(1^st ‘(𝐹‘𝑖)), (2^nd ‘(𝐹‘𝑖))⟩)
153	151, 152	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑖) = ⟨(1^st ‘(𝐹‘𝑖)), (2^nd ‘(𝐹‘𝑖))⟩)
154	153	fveq2d 6924	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) = ((,)‘⟨(1^st ‘(𝐹‘𝑖)), (2^nd ‘(𝐹‘𝑖))⟩))
155		df-ov 7451	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘(𝐹‘𝑖))(,)(2^nd ‘(𝐹‘𝑖))) = ((,)‘⟨(1^st ‘(𝐹‘𝑖)), (2^nd ‘(𝐹‘𝑖))⟩)
156	154, 155	eqtr4di 2798	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) = ((1^st ‘(𝐹‘𝑖))(,)(2^nd ‘(𝐹‘𝑖))))
157		ioombl 25619	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘(𝐹‘𝑖))(,)(2^nd ‘(𝐹‘𝑖))) ∈ dom vol
158	156, 157	eqeltrdi 2852	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) ∈ dom vol)
159	158	adantlr 714	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) ∈ dom vol)
160		ffvelcdm 7115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
161	6, 90, 160	syl2an 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
162	161	elin2d 4228	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ (ℝ × ℝ))
163		1st2nd2 8069	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺‘𝑗) ∈ (ℝ × ℝ) → (𝐺‘𝑗) = ⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
164	162, 163	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) = ⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
165	164	fveq2d 6924	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((,)‘⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩))
166		df-ov 7451	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))) = ((,)‘⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
167	165, 166	eqtr4di 2798	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))))
168		ioombl 25619	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))) ∈ dom vol
169	167, 168	eqeltrdi 2852	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ∈ dom vol)
170	169	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐺‘𝑗)) ∈ dom vol)
171		inmbl 25596	. . . . . . . . . . . . . 14 ⊢ ((((,)‘(𝐹‘𝑖)) ∈ dom vol ∧ ((,)‘(𝐺‘𝑗)) ∈ dom vol) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol)
172	159, 170, 171	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol)
173	172	ralrimiva 3152	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∀𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol)
174		finiunmbl 25598	. . . . . . . . . . . 12 ⊢ (((1...𝑁) ∈ Fin ∧ ∀𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol) → ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol)
175	148, 173, 174	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol)
176	147, 175	eqeltrd 2844	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) ∈ dom vol)
177		inss2 4259	. . . . . . . . . . 11 ⊢ (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ 𝐴
178	13	uniiccdif 25632	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran ([,] ∘ 𝐹) ∧ (vol*‘(∪ ran ([,] ∘ 𝐹) ∖ ∪ ran ((,) ∘ 𝐹))) = 0))
179	178	simpld 494	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran ([,] ∘ 𝐹))
180		ovolficcss 25523	. . . . . . . . . . . . . . 15 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ)
181	13, 180	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ)
182	179, 181	sstrd 4019	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ℝ)
183	16, 182	eqsstrid 4057	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
184	183	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐴 ⊆ ℝ)
185	177, 184	sstrid 4020	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ℝ)
186		inss1 4258	. . . . . . . . . . 11 ⊢ (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ((,)‘(𝐺‘𝑗))
187		ioossre 13468	. . . . . . . . . . . 12 ⊢ ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))) ⊆ ℝ
188	167, 187	eqsstrdi 4063	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ)
189	167	fveq2d 6924	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘((,)‘(𝐺‘𝑗))) = (vol‘((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗)))))
190		ovolfcl 25520	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1^st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1^st ‘(𝐺‘𝑗)) ≤ (2^nd ‘(𝐺‘𝑗))))
191	6, 90, 190	syl2an 595	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((1^st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1^st ‘(𝐺‘𝑗)) ≤ (2^nd ‘(𝐺‘𝑗))))
192		ovolioo 25622	. . . . . . . . . . . . . 14 ⊢ (((1^st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1^st ‘(𝐺‘𝑗)) ≤ (2^nd ‘(𝐺‘𝑗))) → (vol*‘((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗)))) = ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))))
193	191, 192	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗)))) = ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))))
194	189, 193	eqtrd 2780	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺‘𝑗))) = ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))))
195	191	simp2d 1143	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (2^nd ‘(𝐺‘𝑗)) ∈ ℝ)
196	191	simp1d 1142	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1^st ‘(𝐺‘𝑗)) ∈ ℝ)
197	195, 196	resubcld 11718	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℝ)
198	194, 197	eqeltrd 2844	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ)
199		ovolsscl 25540	. . . . . . . . . . 11 ⊢ (((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ((,)‘(𝐺‘𝑗)) ∧ ((,)‘(𝐺‘𝑗)) ⊆ ℝ ∧ (vol‘((,)‘(𝐺‘𝑗))) ∈ ℝ) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ∈ ℝ)
200	186, 188, 198, 199	mp3an2i 1466	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ∈ ℝ)
201		mblsplit 25586	. . . . . . . . . 10 ⊢ (((((,)‘(𝐺‘𝑗)) ∩ 𝐿) ∈ dom vol ∧ (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ℝ ∧ (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ∈ ℝ) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) = ((vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) + (vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)))))
202	176, 185, 200, 201	syl3anc 1371	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) = ((vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) + (vol*‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)))))
203		imassrn 6100	. . . . . . . . . . . . . . 15 ⊢ (((,) ∘ 𝐹) “ (1...𝑁)) ⊆ ran ((,) ∘ 𝐹)
204	203	unissi 4940	. . . . . . . . . . . . . 14 ⊢ ∪ (((,) ∘ 𝐹) “ (1...𝑁)) ⊆ ∪ ran ((,) ∘ 𝐹)
205	204, 69, 16	3sstr4i 4052	. . . . . . . . . . . . 13 ⊢ 𝐿 ⊆ 𝐴
206		sslin 4264	. . . . . . . . . . . . 13 ⊢ (𝐿 ⊆ 𝐴 → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺‘𝑗)) ∩ 𝐴))
207	205, 206	mp1i 13	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺‘𝑗)) ∩ 𝐴))
208		sseqin2 4244	. . . . . . . . . . . 12 ⊢ ((((,)‘(𝐺‘𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ↔ ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = (((,)‘(𝐺‘𝑗)) ∩ 𝐿))
209	207, 208	sylib 218	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = (((,)‘(𝐺‘𝑗)) ∩ 𝐿))
210	209	fveq2d 6924	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) = (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)))
211		indifdir 4314	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = ((𝐴 ∩ ((,)‘(𝐺‘𝑗))) ∖ (𝐿 ∩ ((,)‘(𝐺‘𝑗))))
212		incom 4230	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ 𝐴)
213		incom 4230	. . . . . . . . . . . . . 14 ⊢ (𝐿 ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ 𝐿)
214	212, 213	difeq12i 4147	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∩ ((,)‘(𝐺‘𝑗))) ∖ (𝐿 ∩ ((,)‘(𝐺‘𝑗)))) = ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))
215	211, 214	eqtri 2768	. . . . . . . . . . . 12 ⊢ ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))
216	79	eqcomd 2746	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = 𝐴)
217	77	ineq1d 4240	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐿 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
218		2fveq3 6925	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑖 → ((,)‘(𝐹‘𝑥)) = ((,)‘(𝐹‘𝑖)))
219	218	cbvdisjv 5144	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)) ↔ Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
220	14, 219	sylib 218	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
221		fz1ssnn 13615	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...𝑁) ⊆ ℕ
222	221	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ)
223		uzss 12926	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘1) → (ℤ_≥‘(𝑁 + 1)) ⊆ (ℤ_≥‘1))
224	39, 223	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℤ_≥‘(𝑁 + 1)) ⊆ (ℤ_≥‘1))
225	224, 36	sseqtrrdi 4060	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℤ_≥‘(𝑁 + 1)) ⊆ ℕ)
226	47	ineq1d 4240	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((1...((𝑁 + 1) − 1)) ∩ (ℤ_≥‘(𝑁 + 1))) = ((1...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))))
227		uzdisj 13657	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1...((𝑁 + 1) − 1)) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅
228	226, 227	eqtr3di 2795	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅)
229		disjiun 5154	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) ∧ ((1...𝑁) ⊆ ℕ ∧ (ℤ_≥‘(𝑁 + 1)) ⊆ ℕ ∧ ((1...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅)) → (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅)
230	220, 222, 225, 228, 229	syl13anc 1372	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅)
231	217, 230	eqtrd 2780	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐿 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅)
232		uneqdifeq 4516	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐿 ⊆ 𝐴 ∧ (𝐿 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅) → ((𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = 𝐴 ↔ (𝐴 ∖ 𝐿) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
233	205, 231, 232	sylancr 586	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = 𝐴 ↔ (𝐴 ∖ 𝐿) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
234	216, 233	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 ∖ 𝐿) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
235	234	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐴 ∖ 𝐿) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
236	235	ineq2d 4241	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ (𝐴 ∖ 𝐿)) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
237		incom 4230	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ (𝐴 ∖ 𝐿))
238	101, 98	eqtri 2768	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
239	236, 237, 238	3eqtr4g 2805	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
240	215, 239	eqtr3id 2794	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
241	240	fveq2d 6924	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) = (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
242	210, 241	oveq12d 7466	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) + (vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)))) = ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
243	202, 242	eqtrd 2780	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) = ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
244	200, 140	resubcld 11718	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ∈ ℝ)
245		inss2 4259	. . . . . . . . . . . . 13 ⊢ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐺‘𝑗))
246	188	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ)
247	198	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ)
248		ovolsscl 25540	. . . . . . . . . . . . 13 ⊢ (((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐺‘𝑗)) ∧ ((,)‘(𝐺‘𝑗)) ⊆ ℝ ∧ (vol‘((,)‘(𝐺‘𝑗))) ∈ ℝ) → (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
249	245, 246, 247, 248	mp3an2i 1466	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
250	148, 249	fsumrecl 15782	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
251		uniioombl.n2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)(abs‘(Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))
252	251	r19.21bi 3257	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (abs‘(Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))
253	250, 200, 140	absdifltd 15482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((abs‘(Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀) ↔ (((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∧ Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) < ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) + (𝐶 / 𝑀)))))
254	252, 253	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∧ Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) < ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) + (𝐶 / 𝑀))))
255	254	simpld 494	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
256	244, 250, 255	ltled 11438	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
257	147	fveq2d 6924	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
258		mblvol 25584	. . . . . . . . . . . . . . . . 17 ⊢ ((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol → (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
259	172, 258	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
260	259, 249	eqeltrd 2844	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
261	172, 260	jca 511	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ))
262	261	ralrimiva 3152	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∀𝑖 ∈ (1...𝑁)((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ))
263		inss1 4258	. . . . . . . . . . . . . . . 16 ⊢ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐹‘𝑖))
264	263	rgenw 3071	. . . . . . . . . . . . . . 15 ⊢ ∀𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐹‘𝑖))
265	220	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
266		disjss2 5136	. . . . . . . . . . . . . . 15 ⊢ (∀𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐹‘𝑖)) → (Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) → Disj 𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
267	264, 265, 266	mpsyl 68	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
268		disjss1 5139	. . . . . . . . . . . . . 14 ⊢ ((1...𝑁) ⊆ ℕ → (Disj 𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) → Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
269	221, 267, 268	mpsyl 68	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
270		volfiniun 25601	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∈ Fin ∧ ∀𝑖 ∈ (1...𝑁)((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) ∧ Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
271	148, 262, 269, 270	syl3anc 1371	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
272		mblvol 25584	. . . . . . . . . . . . 13 ⊢ (∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
273	175, 272	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
274	259	sumeq2dv 15750	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
275	271, 273, 274	3eqtr3d 2788	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
276	257, 275	eqtrd 2780	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
277	256, 276	breqtrrd 5194	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)))
278	276, 250	eqeltrd 2844	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) ∈ ℝ)
279	200, 140, 278	lesubaddd 11887	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) ↔ (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ≤ ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀))))
280	277, 279	mpbid 232	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ≤ ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀)))
281	243, 280	eqbrtrrd 5190	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀)))
282	131, 140, 278	leadd2d 11885	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ (𝐶 / 𝑀) ↔ ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀))))
283	281, 282	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ (𝐶 / 𝑀))
284	124, 131, 140, 283	fsumle 15847	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀))
285	139	recnd 11318	. . . . . . 7 ⊢ (𝜑 → (𝐶 / 𝑀) ∈ ℂ)
286		fsumconst 15838	. . . . . . 7 ⊢ (((1...𝑀) ∈ Fin ∧ (𝐶 / 𝑀) ∈ ℂ) → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = ((♯‘(1...𝑀)) · (𝐶 / 𝑀)))
287	124, 285, 286	syl2anc 583	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = ((♯‘(1...𝑀)) · (𝐶 / 𝑀)))
288		nnnn0 12560	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ₀)
289		hashfz1 14395	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ₀ → (♯‘(1...𝑀)) = 𝑀)
290	138, 288, 289	3syl 18	. . . . . . 7 ⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀)
291	290	oveq1d 7463	. . . . . 6 ⊢ (𝜑 → ((♯‘(1...𝑀)) · (𝐶 / 𝑀)) = (𝑀 · (𝐶 / 𝑀)))
292	116	recnd 11318	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℂ)
293	138	nncnd 12309	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℂ)
294	138	nnne0d 12343	. . . . . . 7 ⊢ (𝜑 → 𝑀 ≠ 0)
295	292, 293, 294	divcan2d 12072	. . . . . 6 ⊢ (𝜑 → (𝑀 · (𝐶 / 𝑀)) = 𝐶)
296	287, 291, 295	3eqtrd 2784	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = 𝐶)
297	284, 296	breqtrd 5192	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ 𝐶)
298	114, 132, 116, 137, 297	letrd 11447	. . 3 ⊢ (𝜑 → (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ 𝐶)
299	114, 116, 34, 298	leadd2dd 11905	. 2 ⊢ (𝜑 → ((vol‘(𝐾 ∩ 𝐿)) + (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol*‘(𝐾 ∩ 𝐿)) + 𝐶))
300	31, 115, 117, 123, 299	letrd 11447	1 ⊢ (𝜑 → (vol‘(𝐾 ∩ 𝐴)) ≤ ((vol‘(𝐾 ∩ 𝐿)) + 𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1537 ∈ wcel 2108 ∀wral 3067 ∖ cdif 3973 ∪ cun 3974 ∩ cin 3975 ⊆ wss 3976 ∅c0 4352 𝒫 cpw 4622 ⟨cop 4654 ∪ cuni 4931 ∪ ciun 5015 Disj wdisj 5133 class class class wbr 5166 × cxp 5698 dom cdm 5700 ran crn 5701 “ cima 5703 ∘ ccom 5704 Fun wfun 6567 Fn wfn 6568 ⟶wf 6569 ‘cfv 6573 (class class class)co 7448 1^st c1st 8028 2^nd c2nd 8029 Fincfn 9003 supcsup 9509 ℂcc 11182 ℝcr 11183 0cc0 11184 1c1 11185 + caddc 11187 · cmul 11189 ℝ^*cxr 11323 < clt 11324 ≤ cle 11325 − cmin 11520 / cdiv 11947 ℕcn 12293 ℕ₀cn0 12553 ℤ_≥cuz 12903 ℝ⁺crp 13057 (,)cioo 13407 [,]cicc 13410 ...cfz 13567 seqcseq 14052 ♯chash 14379 abscabs 15283 Σcsu 15734 vol*covol 25516 volcvol 25517

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-inf2 9710 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-pre-sup 11262

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-disj 5134 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-se 5653 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-isom 6582 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-of 7714 df-om 7904 df-1st 8030 df-2nd 8031 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-1o 8522 df-2o 8523 df-er 8763 df-map 8886 df-pm 8887 df-en 9004 df-dom 9005 df-sdom 9006 df-fin 9007 df-fi 9480 df-sup 9511 df-inf 9512 df-oi 9579 df-dju 9970 df-card 10008 df-acn 10011 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-div 11948 df-nn 12294 df-2 12356 df-3 12357 df-n0 12554 df-z 12640 df-uz 12904 df-q 13014 df-rp 13058 df-xneg 13175 df-xadd 13176 df-xmul 13177 df-ioo 13411 df-ico 13413 df-icc 13414 df-fz 13568 df-fzo 13712 df-fl 13843 df-seq 14053 df-exp 14113 df-hash 14380 df-cj 15148 df-re 15149 df-im 15150 df-sqrt 15284 df-abs 15285 df-clim 15534 df-rlim 15535 df-sum 15735 df-rest 17482 df-topgen 17503 df-psmet 21379 df-xmet 21380 df-met 21381 df-bl 21382 df-mopn 21383 df-top 22921 df-topon 22938 df-bases 22974 df-cmp 23416 df-ovol 25518 df-vol 25519

This theorem is referenced by: uniioombllem5 25641

W3C validator