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 25336

Description: Lemma for uniioombl 25339. (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 4229	. . 3 ⊢ (𝐾 ∩ 𝐴) ⊆ 𝐾
2		uniioombl.k	. . . . 5 ⊢ 𝐾 = ∪ (((,) ∘ 𝐺) “ (1...𝑀))
3		imassrn 6071	. . . . . 6 ⊢ (((,) ∘ 𝐺) “ (1...𝑀)) ⊆ ran ((,) ∘ 𝐺)
4	3	unissi 4918	. . . . 5 ⊢ ∪ (((,) ∘ 𝐺) “ (1...𝑀)) ⊆ ∪ ran ((,) ∘ 𝐺)
5	2, 4	eqsstri 4017	. . . 4 ⊢ 𝐾 ⊆ ∪ ran ((,) ∘ 𝐺)
6		uniioombl.g	. . . . . . 7 ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
7	6	uniiccdif 25328	. . . . . 6 ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ([,] ∘ 𝐺) ∧ (vol*‘(∪ ran ([,] ∘ 𝐺) ∖ ∪ ran ((,) ∘ 𝐺))) = 0))
8	7	simpld 494	. . . . 5 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ([,] ∘ 𝐺))
9		ovolficcss 25219	. . . . . 6 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ)
10	6, 9	syl 17	. . . . 5 ⊢ (𝜑 → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ)
11	8, 10	sstrd 3993	. . . 4 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ℝ)
12	5, 11	sstrid 3994	. . 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 25331	. . . . 5 ⊢ (𝜑 → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
23		ssid 4005	. . . . . 6 ⊢ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)
24	20	ovollb 25229	. . . . . 6 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)) → (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < ))
25	6, 23, 24	sylancl 585	. . . . 5 ⊢ (𝜑 → (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < ))
26		ovollecl 25233	. . . . 5 ⊢ ((∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ sup(ran 𝑇, ℝ^, < ) ∈ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < )) → (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ)
27	11, 22, 25, 26	syl3anc 1370	. . . 4 ⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ)
28		ovolsscl 25236	. . . 4 ⊢ ((𝐾 ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol‘𝐾) ∈ ℝ)
29	5, 11, 27, 28	mp3an2i 1465	. . 3 ⊢ (𝜑 → (vol*‘𝐾) ∈ ℝ)
30		ovolsscl 25236	. . 3 ⊢ (((𝐾 ∩ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘(𝐾 ∩ 𝐴)) ∈ ℝ)
31	1, 12, 29, 30	mp3an2i 1465	. 2 ⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ)
32		inss1 4229	. . . 4 ⊢ (𝐾 ∩ 𝐿) ⊆ 𝐾
33		ovolsscl 25236	. . . 4 ⊢ (((𝐾 ∩ 𝐿) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘(𝐾 ∩ 𝐿)) ∈ ℝ)
34	32, 12, 29, 33	mp3an2i 1465	. . 3 ⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐿)) ∈ ℝ)
35		ssun2 4174	. . . . . 6 ⊢ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
36		nnuz 12870	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
37		uniioombl.n	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℕ)
38	37	peano2nnd 12234	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ)
39	38, 36	eleqtrdi 2842	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘1))
40		uzsplit 13578	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘1) → (ℤ_≥‘1) = ((1...((𝑁 + 1) − 1)) ∪ (ℤ_≥‘(𝑁 + 1))))
41	39, 40	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℤ_≥‘1) = ((1...((𝑁 + 1) − 1)) ∪ (ℤ_≥‘(𝑁 + 1))))
42	36, 41	eqtrid 2783	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℕ = ((1...((𝑁 + 1) − 1)) ∪ (ℤ_≥‘(𝑁 + 1))))
43	37	nncnd 12233	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℂ)
44		ax-1cn 11171	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℂ
45		pncan 11471	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
46	43, 44, 45	sylancl 585	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
47	46	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...((𝑁 + 1) − 1)) = (1...𝑁))
48	47	uneq1d 4163	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1...((𝑁 + 1) − 1)) ∪ (ℤ_≥‘(𝑁 + 1))) = ((1...𝑁) ∪ (ℤ_≥‘(𝑁 + 1))))
49	42, 48	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (𝜑 → ℕ = ((1...𝑁) ∪ (ℤ_≥‘(𝑁 + 1))))
50	49	iuneq1d 5025	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) = ∪ 𝑖 ∈ ((1...𝑁) ∪ (ℤ_≥‘(𝑁 + 1)))((,)‘(𝐹‘𝑖)))
51		iunxun 5098	. . . . . . . . . . 11 ⊢ ∪ 𝑖 ∈ ((1...𝑁) ∪ (ℤ_≥‘(𝑁 + 1)))((,)‘(𝐹‘𝑖)) = (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
52	50, 51	eqtrdi 2787	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) = (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
53		ioof 13429	. . . . . . . . . . . . . 14 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
54		inss2 4230	. . . . . . . . . . . . . . . 16 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
55		rexpssxrxp 11264	. . . . . . . . . . . . . . . 16 ⊢ (ℝ × ℝ) ⊆ (ℝ^* × ℝ^*)
56	54, 55	sstri 3992	. . . . . . . . . . . . . . 15 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^*)
57		fss 6735	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^)) → 𝐹:ℕ⟶(ℝ^ × ℝ^*))
58	13, 56, 57	sylancl 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ^* × ℝ^*))
59		fco 6742	. . . . . . . . . . . . . 14 ⊢ (((,):(ℝ^* × ℝ^)⟶𝒫 ℝ ∧ 𝐹:ℕ⟶(ℝ^ × ℝ^*)) → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
60	53, 58, 59	sylancr 586	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
61		ffn 6718	. . . . . . . . . . . . 13 ⊢ (((,) ∘ 𝐹):ℕ⟶𝒫 ℝ → ((,) ∘ 𝐹) Fn ℕ)
62		fniunfv 7249	. . . . . . . . . . . . 13 ⊢ (((,) ∘ 𝐹) Fn ℕ → ∪ 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ∪ ran ((,) ∘ 𝐹))
63	60, 61, 62	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ∪ ran ((,) ∘ 𝐹))
64		fvco3 6991	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑖 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹‘𝑖)))
65	13, 64	sylan 579	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹‘𝑖)))
66	65	iuneq2dv 5022	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
67	63, 66	eqtr3d 2773	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
68	16, 67	eqtrid 2783	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 = ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
69		uniioombl.l	. . . . . . . . . . . 12 ⊢ 𝐿 = ∪ (((,) ∘ 𝐹) “ (1...𝑁))
70		ffun 6721	. . . . . . . . . . . . . 14 ⊢ (((,) ∘ 𝐹):ℕ⟶𝒫 ℝ → Fun ((,) ∘ 𝐹))
71		funiunfv 7250	. . . . . . . . . . . . . 14 ⊢ (Fun ((,) ∘ 𝐹) → ∪ 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = ∪ (((,) ∘ 𝐹) “ (1...𝑁)))
72	60, 70, 71	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = ∪ (((,) ∘ 𝐹) “ (1...𝑁)))
73		elfznn 13535	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑁) → 𝑖 ∈ ℕ)
74	13, 73, 64	syl2an 595	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹‘𝑖)))
75	74	iuneq2dv 5022	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))
76	72, 75	eqtr3d 2773	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ (((,) ∘ 𝐹) “ (1...𝑁)) = ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))
77	69, 76	eqtrid 2783	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 = ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))
78	77	uneq1d 4163	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
79	52, 68, 78	3eqtr4d 2781	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 = (𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
80	79	ineq2d 4213	. . . . . . . 8 ⊢ (𝜑 → (𝐾 ∩ 𝐴) = (𝐾 ∩ (𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))))
81		indi 4274	. . . . . . . 8 ⊢ (𝐾 ∩ (𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) = ((𝐾 ∩ 𝐿) ∪ (𝐾 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
82	80, 81	eqtrdi 2787	. . . . . . 7 ⊢ (𝜑 → (𝐾 ∩ 𝐴) = ((𝐾 ∩ 𝐿) ∪ (𝐾 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))))
83		fss 6735	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^)) → 𝐺:ℕ⟶(ℝ^ × ℝ^*))
84	6, 56, 83	sylancl 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺:ℕ⟶(ℝ^* × ℝ^*))
85		fco 6742	. . . . . . . . . . . . . 14 ⊢ (((,):(ℝ^* × ℝ^)⟶𝒫 ℝ ∧ 𝐺:ℕ⟶(ℝ^ × ℝ^*)) → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
86	53, 84, 85	sylancr 586	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
87		ffun 6721	. . . . . . . . . . . . 13 ⊢ (((,) ∘ 𝐺):ℕ⟶𝒫 ℝ → Fun ((,) ∘ 𝐺))
88		funiunfv 7250	. . . . . . . . . . . . 13 ⊢ (Fun ((,) ∘ 𝐺) → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ (((,) ∘ 𝐺) “ (1...𝑀)))
89	86, 87, 88	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ (((,) ∘ 𝐺) “ (1...𝑀)))
90		elfznn 13535	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
91		fvco3 6991	. . . . . . . . . . . . . 14 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑗) = ((,)‘(𝐺‘𝑗)))
92	6, 90, 91	syl2an 595	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,) ∘ 𝐺)‘𝑗) = ((,)‘(𝐺‘𝑗)))
93	92	iuneq2dv 5022	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
94	89, 93	eqtr3d 2773	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (1...𝑀)) = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
95	2, 94	eqtrid 2783	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
96	95	ineq2d 4213	. . . . . . . . 9 ⊢ (𝜑 → (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ 𝐾) = (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))))
97		incom 4202	. . . . . . . . 9 ⊢ (𝐾 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ 𝐾)
98		iunin2 5075	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
99		incom 4202	. . . . . . . . . . . . . . 15 ⊢ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖)))
100	99	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ_≥‘(𝑁 + 1)) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))))
101	100	iuneq2i 5019	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖)))
102		incom 4202	. . . . . . . . . . . . 13 ⊢ (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
103	98, 101, 102	3eqtr4ri 2770	. . . . . . . . . . . 12 ⊢ (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))
104	103	a1i 11	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑀) → (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
105	104	iuneq2i 5019	. . . . . . . . . 10 ⊢ ∪ 𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))
106		iunin2 5075	. . . . . . . . . 10 ⊢ ∪ 𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
107	105, 106	eqtr3i 2761	. . . . . . . . 9 ⊢ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
108	96, 97, 107	3eqtr4g 2796	. . . . . . . 8 ⊢ (𝜑 → (𝐾 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
109	108	uneq2d 4164	. . . . . . 7 ⊢ (𝜑 → ((𝐾 ∩ 𝐿) ∪ (𝐾 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) = ((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
110	82, 109	eqtrd 2771	. . . . . 6 ⊢ (𝜑 → (𝐾 ∩ 𝐴) = ((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
111	35, 110	sseqtrrid 4036	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ (𝐾 ∩ 𝐴))
112	111, 1	sstrdi 3995	. . . 4 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾)
113		ovolsscl 25236	. . . 4 ⊢ ((∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
114	112, 12, 29, 113	syl3anc 1370	. . 3 ⊢ (𝜑 → (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
115	34, 114	readdcld 11248	. 2 ⊢ (𝜑 → ((vol‘(𝐾 ∩ 𝐿)) + (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ∈ ℝ)
116	18	rpred 13021	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
117	34, 116	readdcld 11248	. 2 ⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐿)) + 𝐶) ∈ ℝ)
118	110	fveq2d 6896	. . 3 ⊢ (𝜑 → (vol‘(𝐾 ∩ 𝐴)) = (vol‘((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
119	32, 12	sstrid 3994	. . . 4 ⊢ (𝜑 → (𝐾 ∩ 𝐿) ⊆ ℝ)
120	112, 12	sstrd 3993	. . . 4 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ)
121		ovolun 25249	. . . 4 ⊢ ((((𝐾 ∩ 𝐿) ⊆ ℝ ∧ (vol‘(𝐾 ∩ 𝐿)) ∈ ℝ) ∧ (∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧ (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)) → (vol‘((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
122	119, 34, 120, 114, 121	syl22anc 836	. . 3 ⊢ (𝜑 → (vol‘((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
123	118, 122	eqbrtrd 5171	. 2 ⊢ (𝜑 → (vol‘(𝐾 ∩ 𝐴)) ≤ ((vol‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
124		fzfid 13943	. . . . 5 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
125		iunss 5049	. . . . . . . 8 ⊢ (∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾 ↔ ∀𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾)
126	112, 125	sylib 217	. . . . . . 7 ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾)
127	126	r19.21bi 3247	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾)
128	12	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐾 ⊆ ℝ)
129	29	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘𝐾) ∈ ℝ)
130		ovolsscl 25236	. . . . . 6 ⊢ ((∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
131	127, 128, 129, 130	syl3anc 1370	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
132	124, 131	fsumrecl 15685	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
133	127, 128	sstrd 3993	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ)
134	133, 131	jca 511	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧ (vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ))
135	134	ralrimiva 3145	. . . . 5 ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧ (vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ))
136		ovolfiniun 25251	. . . . 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 12271	. . . . . . 7 ⊢ (𝜑 → (𝐶 / 𝑀) ∈ ℝ)
140	139	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐶 / 𝑀) ∈ ℝ)
141	77	ineq2d 4213	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖))))
142	141	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖))))
143	99	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑁) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))))
144	143	iuneq2i 5019	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖)))
145		iunin2 5075	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))
146	144, 145	eqtri 2759	. . . . . . . . . . . 12 ⊢ ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))
147	142, 146	eqtr4di 2789	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) = ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
148		fzfid 13943	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1...𝑁) ∈ Fin)
149		ffvelcdm 7084	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ ( ≤ ∩ (ℝ × ℝ)))
150	13, 73, 149	syl2an 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑖) ∈ ( ≤ ∩ (ℝ × ℝ)))
151	150	elin2d 4200	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑖) ∈ (ℝ × ℝ))
152		1st2nd2 8017	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑖) ∈ (ℝ × ℝ) → (𝐹‘𝑖) = ⟨(1^st ‘(𝐹‘𝑖)), (2^nd ‘(𝐹‘𝑖))⟩)
153	151, 152	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑖) = ⟨(1^st ‘(𝐹‘𝑖)), (2^nd ‘(𝐹‘𝑖))⟩)
154	153	fveq2d 6896	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) = ((,)‘⟨(1^st ‘(𝐹‘𝑖)), (2^nd ‘(𝐹‘𝑖))⟩))
155		df-ov 7415	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘(𝐹‘𝑖))(,)(2^nd ‘(𝐹‘𝑖))) = ((,)‘⟨(1^st ‘(𝐹‘𝑖)), (2^nd ‘(𝐹‘𝑖))⟩)
156	154, 155	eqtr4di 2789	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) = ((1^st ‘(𝐹‘𝑖))(,)(2^nd ‘(𝐹‘𝑖))))
157		ioombl 25315	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘(𝐹‘𝑖))(,)(2^nd ‘(𝐹‘𝑖))) ∈ dom vol
158	156, 157	eqeltrdi 2840	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) ∈ dom vol)
159	158	adantlr 712	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) ∈ dom vol)
160		ffvelcdm 7084	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
161	6, 90, 160	syl2an 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
162	161	elin2d 4200	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ (ℝ × ℝ))
163		1st2nd2 8017	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺‘𝑗) ∈ (ℝ × ℝ) → (𝐺‘𝑗) = ⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
164	162, 163	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) = ⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
165	164	fveq2d 6896	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((,)‘⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩))
166		df-ov 7415	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))) = ((,)‘⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
167	165, 166	eqtr4di 2789	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))))
168		ioombl 25315	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))) ∈ dom vol
169	167, 168	eqeltrdi 2840	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ∈ dom vol)
170	169	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐺‘𝑗)) ∈ dom vol)
171		inmbl 25292	. . . . . . . . . . . . . 14 ⊢ ((((,)‘(𝐹‘𝑖)) ∈ dom vol ∧ ((,)‘(𝐺‘𝑗)) ∈ dom vol) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol)
172	159, 170, 171	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol)
173	172	ralrimiva 3145	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∀𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol)
174		finiunmbl 25294	. . . . . . . . . . . 12 ⊢ (((1...𝑁) ∈ Fin ∧ ∀𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol) → ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol)
175	148, 173, 174	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol)
176	147, 175	eqeltrd 2832	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) ∈ dom vol)
177		inss2 4230	. . . . . . . . . . 11 ⊢ (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ 𝐴
178	13	uniiccdif 25328	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran ([,] ∘ 𝐹) ∧ (vol*‘(∪ ran ([,] ∘ 𝐹) ∖ ∪ ran ((,) ∘ 𝐹))) = 0))
179	178	simpld 494	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran ([,] ∘ 𝐹))
180		ovolficcss 25219	. . . . . . . . . . . . . . 15 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ)
181	13, 180	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ)
182	179, 181	sstrd 3993	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ℝ)
183	16, 182	eqsstrid 4031	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
184	183	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐴 ⊆ ℝ)
185	177, 184	sstrid 3994	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ℝ)
186		inss1 4229	. . . . . . . . . . 11 ⊢ (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ((,)‘(𝐺‘𝑗))
187		ioossre 13390	. . . . . . . . . . . 12 ⊢ ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))) ⊆ ℝ
188	167, 187	eqsstrdi 4037	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ)
189	167	fveq2d 6896	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘((,)‘(𝐺‘𝑗))) = (vol‘((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗)))))
190		ovolfcl 25216	. . . . . . . . . . . . . . 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 25318	. . . . . . . . . . . . . 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 2771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺‘𝑗))) = ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))))
195	191	simp2d 1142	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (2^nd ‘(𝐺‘𝑗)) ∈ ℝ)
196	191	simp1d 1141	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1^st ‘(𝐺‘𝑗)) ∈ ℝ)
197	195, 196	resubcld 11647	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℝ)
198	194, 197	eqeltrd 2832	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ)
199		ovolsscl 25236	. . . . . . . . . . 11 ⊢ (((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ((,)‘(𝐺‘𝑗)) ∧ ((,)‘(𝐺‘𝑗)) ⊆ ℝ ∧ (vol‘((,)‘(𝐺‘𝑗))) ∈ ℝ) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ∈ ℝ)
200	186, 188, 198, 199	mp3an2i 1465	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ∈ ℝ)
201		mblsplit 25282	. . . . . . . . . 10 ⊢ (((((,)‘(𝐺‘𝑗)) ∩ 𝐿) ∈ dom vol ∧ (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ℝ ∧ (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ∈ ℝ) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) = ((vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) + (vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)))))
202	176, 185, 200, 201	syl3anc 1370	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) = ((vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) + (vol*‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)))))
203		imassrn 6071	. . . . . . . . . . . . . . 15 ⊢ (((,) ∘ 𝐹) “ (1...𝑁)) ⊆ ran ((,) ∘ 𝐹)
204	203	unissi 4918	. . . . . . . . . . . . . 14 ⊢ ∪ (((,) ∘ 𝐹) “ (1...𝑁)) ⊆ ∪ ran ((,) ∘ 𝐹)
205	204, 69, 16	3sstr4i 4026	. . . . . . . . . . . . 13 ⊢ 𝐿 ⊆ 𝐴
206		sslin 4235	. . . . . . . . . . . . 13 ⊢ (𝐿 ⊆ 𝐴 → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺‘𝑗)) ∩ 𝐴))
207	205, 206	mp1i 13	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺‘𝑗)) ∩ 𝐴))
208		sseqin2 4216	. . . . . . . . . . . 12 ⊢ ((((,)‘(𝐺‘𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ↔ ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = (((,)‘(𝐺‘𝑗)) ∩ 𝐿))
209	207, 208	sylib 217	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = (((,)‘(𝐺‘𝑗)) ∩ 𝐿))
210	209	fveq2d 6896	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) = (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)))
211		indifdir 4285	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = ((𝐴 ∩ ((,)‘(𝐺‘𝑗))) ∖ (𝐿 ∩ ((,)‘(𝐺‘𝑗))))
212		incom 4202	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ 𝐴)
213		incom 4202	. . . . . . . . . . . . . 14 ⊢ (𝐿 ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ 𝐿)
214	212, 213	difeq12i 4121	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∩ ((,)‘(𝐺‘𝑗))) ∖ (𝐿 ∩ ((,)‘(𝐺‘𝑗)))) = ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))
215	211, 214	eqtri 2759	. . . . . . . . . . . 12 ⊢ ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))
216	79	eqcomd 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = 𝐴)
217	77	ineq1d 4212	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐿 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
218		2fveq3 6897	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑖 → ((,)‘(𝐹‘𝑥)) = ((,)‘(𝐹‘𝑖)))
219	218	cbvdisjv 5125	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)) ↔ Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
220	14, 219	sylib 217	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
221		fz1ssnn 13537	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...𝑁) ⊆ ℕ
222	221	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ)
223		uzss 12850	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘1) → (ℤ_≥‘(𝑁 + 1)) ⊆ (ℤ_≥‘1))
224	39, 223	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℤ_≥‘(𝑁 + 1)) ⊆ (ℤ_≥‘1))
225	224, 36	sseqtrrdi 4034	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℤ_≥‘(𝑁 + 1)) ⊆ ℕ)
226	47	ineq1d 4212	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((1...((𝑁 + 1) − 1)) ∩ (ℤ_≥‘(𝑁 + 1))) = ((1...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))))
227		uzdisj 13579	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1...((𝑁 + 1) − 1)) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅
228	226, 227	eqtr3di 2786	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅)
229		disjiun 5136	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) ∧ ((1...𝑁) ⊆ ℕ ∧ (ℤ_≥‘(𝑁 + 1)) ⊆ ℕ ∧ ((1...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅)) → (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅)
230	220, 222, 225, 228, 229	syl13anc 1371	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅)
231	217, 230	eqtrd 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐿 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅)
232		uneqdifeq 4493	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐿 ⊆ 𝐴 ∧ (𝐿 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅) → ((𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = 𝐴 ↔ (𝐴 ∖ 𝐿) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
233	205, 231, 232	sylancr 586	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = 𝐴 ↔ (𝐴 ∖ 𝐿) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
234	216, 233	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 ∖ 𝐿) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
235	234	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐴 ∖ 𝐿) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
236	235	ineq2d 4213	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ (𝐴 ∖ 𝐿)) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
237		incom 4202	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ (𝐴 ∖ 𝐿))
238	101, 98	eqtri 2759	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
239	236, 237, 238	3eqtr4g 2796	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
240	215, 239	eqtr3id 2785	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
241	240	fveq2d 6896	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) = (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
242	210, 241	oveq12d 7430	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) + (vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)))) = ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
243	202, 242	eqtrd 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) = ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
244	200, 140	resubcld 11647	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ∈ ℝ)
245		inss2 4230	. . . . . . . . . . . . 13 ⊢ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐺‘𝑗))
246	188	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ)
247	198	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ)
248		ovolsscl 25236	. . . . . . . . . . . . 13 ⊢ (((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐺‘𝑗)) ∧ ((,)‘(𝐺‘𝑗)) ⊆ ℝ ∧ (vol‘((,)‘(𝐺‘𝑗))) ∈ ℝ) → (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
249	245, 246, 247, 248	mp3an2i 1465	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
250	148, 249	fsumrecl 15685	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
251		uniioombl.n2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)(abs‘(Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))
252	251	r19.21bi 3247	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (abs‘(Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))
253	250, 200, 140	absdifltd 15385	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((abs‘(Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀) ↔ (((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∧ Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) < ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) + (𝐶 / 𝑀)))))
254	252, 253	mpbid 231	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∧ Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) < ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) + (𝐶 / 𝑀))))
255	254	simpld 494	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
256	244, 250, 255	ltled 11367	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
257	147	fveq2d 6896	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
258		mblvol 25280	. . . . . . . . . . . . . . . . 17 ⊢ ((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol → (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
259	172, 258	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
260	259, 249	eqeltrd 2832	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
261	172, 260	jca 511	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ))
262	261	ralrimiva 3145	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∀𝑖 ∈ (1...𝑁)((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ))
263		inss1 4229	. . . . . . . . . . . . . . . 16 ⊢ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐹‘𝑖))
264	263	rgenw 3064	. . . . . . . . . . . . . . 15 ⊢ ∀𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐹‘𝑖))
265	220	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
266		disjss2 5117	. . . . . . . . . . . . . . 15 ⊢ (∀𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐹‘𝑖)) → (Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) → Disj 𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
267	264, 265, 266	mpsyl 68	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
268		disjss1 5120	. . . . . . . . . . . . . 14 ⊢ ((1...𝑁) ⊆ ℕ → (Disj 𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) → Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
269	221, 267, 268	mpsyl 68	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
270		volfiniun 25297	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∈ Fin ∧ ∀𝑖 ∈ (1...𝑁)((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) ∧ Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
271	148, 262, 269, 270	syl3anc 1370	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
272		mblvol 25280	. . . . . . . . . . . . 13 ⊢ (∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
273	175, 272	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
274	259	sumeq2dv 15654	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
275	271, 273, 274	3eqtr3d 2779	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
276	257, 275	eqtrd 2771	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
277	256, 276	breqtrrd 5177	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)))
278	276, 250	eqeltrd 2832	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) ∈ ℝ)
279	200, 140, 278	lesubaddd 11816	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) ↔ (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ≤ ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀))))
280	277, 279	mpbid 231	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ≤ ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀)))
281	243, 280	eqbrtrrd 5173	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀)))
282	131, 140, 278	leadd2d 11814	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ (𝐶 / 𝑀) ↔ ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀))))
283	281, 282	mpbird 256	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ (𝐶 / 𝑀))
284	124, 131, 140, 283	fsumle 15750	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀))
285	139	recnd 11247	. . . . . . 7 ⊢ (𝜑 → (𝐶 / 𝑀) ∈ ℂ)
286		fsumconst 15741	. . . . . . 7 ⊢ (((1...𝑀) ∈ Fin ∧ (𝐶 / 𝑀) ∈ ℂ) → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = ((♯‘(1...𝑀)) · (𝐶 / 𝑀)))
287	124, 285, 286	syl2anc 583	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = ((♯‘(1...𝑀)) · (𝐶 / 𝑀)))
288		nnnn0 12484	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ₀)
289		hashfz1 14311	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ₀ → (♯‘(1...𝑀)) = 𝑀)
290	138, 288, 289	3syl 18	. . . . . . 7 ⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀)
291	290	oveq1d 7427	. . . . . 6 ⊢ (𝜑 → ((♯‘(1...𝑀)) · (𝐶 / 𝑀)) = (𝑀 · (𝐶 / 𝑀)))
292	116	recnd 11247	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℂ)
293	138	nncnd 12233	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℂ)
294	138	nnne0d 12267	. . . . . . 7 ⊢ (𝜑 → 𝑀 ≠ 0)
295	292, 293, 294	divcan2d 11997	. . . . . 6 ⊢ (𝜑 → (𝑀 · (𝐶 / 𝑀)) = 𝐶)
296	287, 291, 295	3eqtrd 2775	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = 𝐶)
297	284, 296	breqtrd 5175	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ 𝐶)
298	114, 132, 116, 137, 297	letrd 11376	. . 3 ⊢ (𝜑 → (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ 𝐶)
299	114, 116, 34, 298	leadd2dd 11834	. 2 ⊢ (𝜑 → ((vol‘(𝐾 ∩ 𝐿)) + (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol*‘(𝐾 ∩ 𝐿)) + 𝐶))
300	31, 115, 117, 123, 299	letrd 11376	1 ⊢ (𝜑 → (vol‘(𝐾 ∩ 𝐴)) ≤ ((vol‘(𝐾 ∩ 𝐿)) + 𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2105 ∀wral 3060 ∖ cdif 3946 ∪ cun 3947 ∩ cin 3948 ⊆ wss 3949 ∅c0 4323 𝒫 cpw 4603 ⟨cop 4635 ∪ cuni 4909 ∪ ciun 4998 Disj wdisj 5114 class class class wbr 5149 × cxp 5675 dom cdm 5677 ran crn 5678 “ cima 5680 ∘ ccom 5681 Fun wfun 6538 Fn wfn 6539 ⟶wf 6540 ‘cfv 6544 (class class class)co 7412 1^st c1st 7976 2^nd c2nd 7977 Fincfn 8942 supcsup 9438 ℂcc 11111 ℝcr 11112 0cc0 11113 1c1 11114 + caddc 11116 · cmul 11118 ℝ^*cxr 11252 < clt 11253 ≤ cle 11254 − cmin 11449 / cdiv 11876 ℕcn 12217 ℕ₀cn0 12477 ℤ_≥cuz 12827 ℝ⁺crp 12979 (,)cioo 13329 [,]cicc 13332 ...cfz 13489 seqcseq 13971 ♯chash 14295 abscabs 15186 Σcsu 15637 vol*covol 25212 volcvol 25213

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7728 ax-inf2 9639 ax-cnex 11169 ax-resscn 11170 ax-1cn 11171 ax-icn 11172 ax-addcl 11173 ax-addrcl 11174 ax-mulcl 11175 ax-mulrcl 11176 ax-mulcom 11177 ax-addass 11178 ax-mulass 11179 ax-distr 11180 ax-i2m1 11181 ax-1ne0 11182 ax-1rid 11183 ax-rnegex 11184 ax-rrecex 11185 ax-cnre 11186 ax-pre-lttri 11187 ax-pre-lttrn 11188 ax-pre-ltadd 11189 ax-pre-mulgt0 11190 ax-pre-sup 11191

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-int 4952 df-iun 5000 df-disj 5115 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-se 5633 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-isom 6553 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7673 df-om 7859 df-1st 7978 df-2nd 7979 df-frecs 8269 df-wrecs 8300 df-recs 8374 df-rdg 8413 df-1o 8469 df-2o 8470 df-er 8706 df-map 8825 df-pm 8826 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-fi 9409 df-sup 9440 df-inf 9441 df-oi 9508 df-dju 9899 df-card 9937 df-acn 9940 df-pnf 11255 df-mnf 11256 df-xr 11257 df-ltxr 11258 df-le 11259 df-sub 11451 df-neg 11452 df-div 11877 df-nn 12218 df-2 12280 df-3 12281 df-n0 12478 df-z 12564 df-uz 12828 df-q 12938 df-rp 12980 df-xneg 13097 df-xadd 13098 df-xmul 13099 df-ioo 13333 df-ico 13335 df-icc 13336 df-fz 13490 df-fzo 13633 df-fl 13762 df-seq 13972 df-exp 14033 df-hash 14296 df-cj 15051 df-re 15052 df-im 15053 df-sqrt 15187 df-abs 15188 df-clim 15437 df-rlim 15438 df-sum 15638 df-rest 17373 df-topgen 17394 df-psmet 21137 df-xmet 21138 df-met 21139 df-bl 21140 df-mopn 21141 df-top 22617 df-topon 22634 df-bases 22670 df-cmp 23112 df-ovol 25214 df-vol 25215

This theorem is referenced by: uniioombllem5 25337

W3C validator