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 25335

Description: Lemma for uniioombl 25338. (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 4227	. . 3 ⊢ (𝐾 ∩ 𝐴) ⊆ 𝐾
2		uniioombl.k	. . . . 5 ⊢ 𝐾 = ∪ (((,) ∘ 𝐺) “ (1...𝑀))
3		imassrn 6069	. . . . . 6 ⊢ (((,) ∘ 𝐺) “ (1...𝑀)) ⊆ ran ((,) ∘ 𝐺)
4	3	unissi 4916	. . . . 5 ⊢ ∪ (((,) ∘ 𝐺) “ (1...𝑀)) ⊆ ∪ ran ((,) ∘ 𝐺)
5	2, 4	eqsstri 4015	. . . 4 ⊢ 𝐾 ⊆ ∪ ran ((,) ∘ 𝐺)
6		uniioombl.g	. . . . . . 7 ⊢ (𝜑 → 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
7	6	uniiccdif 25327	. . . . . 6 ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ([,] ∘ 𝐺) ∧ (vol*‘(∪ ran ([,] ∘ 𝐺) ∖ ∪ ran ((,) ∘ 𝐺))) = 0))
8	7	simpld 493	. . . . 5 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ([,] ∘ 𝐺))
9		ovolficcss 25218	. . . . . 6 ⊢ (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ)
10	6, 9	syl 17	. . . . 5 ⊢ (𝜑 → ∪ ran ([,] ∘ 𝐺) ⊆ ℝ)
11	8, 10	sstrd 3991	. . . 4 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) ⊆ ℝ)
12	5, 11	sstrid 3992	. . 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 25330	. . . . 5 ⊢ (𝜑 → sup(ran 𝑇, ℝ^*, < ) ∈ ℝ)
23		ssid 4003	. . . . . 6 ⊢ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)
24	20	ovollb 25228	. . . . . 6 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ∪ ran ((,) ∘ 𝐺)) → (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < ))
25	6, 23, 24	sylancl 584	. . . . 5 ⊢ (𝜑 → (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < ))
26		ovollecl 25232	. . . . 5 ⊢ ((∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ sup(ran 𝑇, ℝ^, < ) ∈ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ≤ sup(ran 𝑇, ℝ^, < )) → (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ)
27	11, 22, 25, 26	syl3anc 1369	. . . 4 ⊢ (𝜑 → (vol*‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ)
28		ovolsscl 25235	. . . 4 ⊢ ((𝐾 ⊆ ∪ ran ((,) ∘ 𝐺) ∧ ∪ ran ((,) ∘ 𝐺) ⊆ ℝ ∧ (vol‘∪ ran ((,) ∘ 𝐺)) ∈ ℝ) → (vol‘𝐾) ∈ ℝ)
29	5, 11, 27, 28	mp3an2i 1464	. . 3 ⊢ (𝜑 → (vol*‘𝐾) ∈ ℝ)
30		ovolsscl 25235	. . 3 ⊢ (((𝐾 ∩ 𝐴) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘(𝐾 ∩ 𝐴)) ∈ ℝ)
31	1, 12, 29, 30	mp3an2i 1464	. 2 ⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐴)) ∈ ℝ)
32		inss1 4227	. . . 4 ⊢ (𝐾 ∩ 𝐿) ⊆ 𝐾
33		ovolsscl 25235	. . . 4 ⊢ (((𝐾 ∩ 𝐿) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘(𝐾 ∩ 𝐿)) ∈ ℝ)
34	32, 12, 29, 33	mp3an2i 1464	. . 3 ⊢ (𝜑 → (vol*‘(𝐾 ∩ 𝐿)) ∈ ℝ)
35		ssun2 4172	. . . . . 6 ⊢ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
36		nnuz 12869	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
37		uniioombl.n	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℕ)
38	37	peano2nnd 12233	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ)
39	38, 36	eleqtrdi 2841	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘1))
40		uzsplit 13577	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘1) → (ℤ_≥‘1) = ((1...((𝑁 + 1) − 1)) ∪ (ℤ_≥‘(𝑁 + 1))))
41	39, 40	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℤ_≥‘1) = ((1...((𝑁 + 1) − 1)) ∪ (ℤ_≥‘(𝑁 + 1))))
42	36, 41	eqtrid 2782	. . . . . . . . . . . . 13 ⊢ (𝜑 → ℕ = ((1...((𝑁 + 1) − 1)) ∪ (ℤ_≥‘(𝑁 + 1))))
43	37	nncnd 12232	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℂ)
44		ax-1cn 11170	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℂ
45		pncan 11470	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
46	43, 44, 45	sylancl 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
47	46	oveq2d 7427	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1...((𝑁 + 1) − 1)) = (1...𝑁))
48	47	uneq1d 4161	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1...((𝑁 + 1) − 1)) ∪ (ℤ_≥‘(𝑁 + 1))) = ((1...𝑁) ∪ (ℤ_≥‘(𝑁 + 1))))
49	42, 48	eqtrd 2770	. . . . . . . . . . . 12 ⊢ (𝜑 → ℕ = ((1...𝑁) ∪ (ℤ_≥‘(𝑁 + 1))))
50	49	iuneq1d 5023	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) = ∪ 𝑖 ∈ ((1...𝑁) ∪ (ℤ_≥‘(𝑁 + 1)))((,)‘(𝐹‘𝑖)))
51		iunxun 5096	. . . . . . . . . . 11 ⊢ ∪ 𝑖 ∈ ((1...𝑁) ∪ (ℤ_≥‘(𝑁 + 1)))((,)‘(𝐹‘𝑖)) = (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
52	50, 51	eqtrdi 2786	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) = (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
53		ioof 13428	. . . . . . . . . . . . . 14 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
54		inss2 4228	. . . . . . . . . . . . . . . 16 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ × ℝ)
55		rexpssxrxp 11263	. . . . . . . . . . . . . . . 16 ⊢ (ℝ × ℝ) ⊆ (ℝ^* × ℝ^*)
56	54, 55	sstri 3990	. . . . . . . . . . . . . . 15 ⊢ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^*)
57		fss 6733	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^)) → 𝐹:ℕ⟶(ℝ^ × ℝ^*))
58	13, 56, 57	sylancl 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ^* × ℝ^*))
59		fco 6740	. . . . . . . . . . . . . 14 ⊢ (((,):(ℝ^* × ℝ^)⟶𝒫 ℝ ∧ 𝐹:ℕ⟶(ℝ^ × ℝ^*)) → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
60	53, 58, 59	sylancr 585	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
61		ffn 6716	. . . . . . . . . . . . 13 ⊢ (((,) ∘ 𝐹):ℕ⟶𝒫 ℝ → ((,) ∘ 𝐹) Fn ℕ)
62		fniunfv 7248	. . . . . . . . . . . . 13 ⊢ (((,) ∘ 𝐹) Fn ℕ → ∪ 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ∪ ran ((,) ∘ 𝐹))
63	60, 61, 62	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ∪ ran ((,) ∘ 𝐹))
64		fvco3 6989	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑖 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹‘𝑖)))
65	13, 64	sylan 578	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹‘𝑖)))
66	65	iuneq2dv 5020	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑖 ∈ ℕ (((,) ∘ 𝐹)‘𝑖) = ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
67	63, 66	eqtr3d 2772	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
68	16, 67	eqtrid 2782	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 = ∪ 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
69		uniioombl.l	. . . . . . . . . . . 12 ⊢ 𝐿 = ∪ (((,) ∘ 𝐹) “ (1...𝑁))
70		ffun 6719	. . . . . . . . . . . . . 14 ⊢ (((,) ∘ 𝐹):ℕ⟶𝒫 ℝ → Fun ((,) ∘ 𝐹))
71		funiunfv 7249	. . . . . . . . . . . . . 14 ⊢ (Fun ((,) ∘ 𝐹) → ∪ 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = ∪ (((,) ∘ 𝐹) “ (1...𝑁)))
72	60, 70, 71	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = ∪ (((,) ∘ 𝐹) “ (1...𝑁)))
73		elfznn 13534	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (1...𝑁) → 𝑖 ∈ ℕ)
74	13, 73, 64	syl2an 594	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (((,) ∘ 𝐹)‘𝑖) = ((,)‘(𝐹‘𝑖)))
75	74	iuneq2dv 5020	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ 𝑖 ∈ (1...𝑁)(((,) ∘ 𝐹)‘𝑖) = ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))
76	72, 75	eqtr3d 2772	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ (((,) ∘ 𝐹) “ (1...𝑁)) = ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))
77	69, 76	eqtrid 2782	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐿 = ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))
78	77	uneq1d 4161	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
79	52, 68, 78	3eqtr4d 2780	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 = (𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
80	79	ineq2d 4211	. . . . . . . 8 ⊢ (𝜑 → (𝐾 ∩ 𝐴) = (𝐾 ∩ (𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))))
81		indi 4272	. . . . . . . 8 ⊢ (𝐾 ∩ (𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) = ((𝐾 ∩ 𝐿) ∪ (𝐾 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
82	80, 81	eqtrdi 2786	. . . . . . 7 ⊢ (𝜑 → (𝐾 ∩ 𝐴) = ((𝐾 ∩ 𝐿) ∪ (𝐾 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))))
83		fss 6733	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ ( ≤ ∩ (ℝ × ℝ)) ⊆ (ℝ^* × ℝ^)) → 𝐺:ℕ⟶(ℝ^ × ℝ^*))
84	6, 56, 83	sylancl 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺:ℕ⟶(ℝ^* × ℝ^*))
85		fco 6740	. . . . . . . . . . . . . 14 ⊢ (((,):(ℝ^* × ℝ^)⟶𝒫 ℝ ∧ 𝐺:ℕ⟶(ℝ^ × ℝ^*)) → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
86	53, 84, 85	sylancr 585	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
87		ffun 6719	. . . . . . . . . . . . 13 ⊢ (((,) ∘ 𝐺):ℕ⟶𝒫 ℝ → Fun ((,) ∘ 𝐺))
88		funiunfv 7249	. . . . . . . . . . . . 13 ⊢ (Fun ((,) ∘ 𝐺) → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ (((,) ∘ 𝐺) “ (1...𝑀)))
89	86, 87, 88	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ (((,) ∘ 𝐺) “ (1...𝑀)))
90		elfznn 13534	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (1...𝑀) → 𝑗 ∈ ℕ)
91		fvco3 6989	. . . . . . . . . . . . . 14 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑗) = ((,)‘(𝐺‘𝑗)))
92	6, 90, 91	syl2an 594	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,) ∘ 𝐺)‘𝑗) = ((,)‘(𝐺‘𝑗)))
93	92	iuneq2dv 5020	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)(((,) ∘ 𝐺)‘𝑗) = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
94	89, 93	eqtr3d 2772	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ (((,) ∘ 𝐺) “ (1...𝑀)) = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
95	2, 94	eqtrid 2782	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 = ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
96	95	ineq2d 4211	. . . . . . . . 9 ⊢ (𝜑 → (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ 𝐾) = (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗))))
97		incom 4200	. . . . . . . . 9 ⊢ (𝐾 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ 𝐾)
98		iunin2 5073	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
99		incom 4200	. . . . . . . . . . . . . . 15 ⊢ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖)))
100	99	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (ℤ_≥‘(𝑁 + 1)) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))))
101	100	iuneq2i 5017	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖)))
102		incom 4200	. . . . . . . . . . . . 13 ⊢ (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
103	98, 101, 102	3eqtr4ri 2769	. . . . . . . . . . . 12 ⊢ (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))
104	103	a1i 11	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...𝑀) → (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
105	104	iuneq2i 5017	. . . . . . . . . 10 ⊢ ∪ 𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))
106		iunin2 5073	. . . . . . . . . 10 ⊢ ∪ 𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
107	105, 106	eqtr3i 2760	. . . . . . . . 9 ⊢ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑗 ∈ (1...𝑀)((,)‘(𝐺‘𝑗)))
108	96, 97, 107	3eqtr4g 2795	. . . . . . . 8 ⊢ (𝜑 → (𝐾 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
109	108	uneq2d 4162	. . . . . . 7 ⊢ (𝜑 → ((𝐾 ∩ 𝐿) ∪ (𝐾 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))) = ((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
110	82, 109	eqtrd 2770	. . . . . 6 ⊢ (𝜑 → (𝐾 ∩ 𝐴) = ((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
111	35, 110	sseqtrrid 4034	. . . . 5 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ (𝐾 ∩ 𝐴))
112	111, 1	sstrdi 3993	. . . 4 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾)
113		ovolsscl 25235	. . . 4 ⊢ ((∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
114	112, 12, 29, 113	syl3anc 1369	. . 3 ⊢ (𝜑 → (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
115	34, 114	readdcld 11247	. 2 ⊢ (𝜑 → ((vol‘(𝐾 ∩ 𝐿)) + (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ∈ ℝ)
116	18	rpred 13020	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
117	34, 116	readdcld 11247	. 2 ⊢ (𝜑 → ((vol*‘(𝐾 ∩ 𝐿)) + 𝐶) ∈ ℝ)
118	110	fveq2d 6894	. . 3 ⊢ (𝜑 → (vol‘(𝐾 ∩ 𝐴)) = (vol‘((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
119	32, 12	sstrid 3992	. . . 4 ⊢ (𝜑 → (𝐾 ∩ 𝐿) ⊆ ℝ)
120	112, 12	sstrd 3991	. . . 4 ⊢ (𝜑 → ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ)
121		ovolun 25248	. . . 4 ⊢ ((((𝐾 ∩ 𝐿) ⊆ ℝ ∧ (vol‘(𝐾 ∩ 𝐿)) ∈ ℝ) ∧ (∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧ (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)) → (vol‘((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
122	119, 34, 120, 114, 121	syl22anc 835	. . 3 ⊢ (𝜑 → (vol‘((𝐾 ∩ 𝐿) ∪ ∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
123	118, 122	eqbrtrd 5169	. 2 ⊢ (𝜑 → (vol‘(𝐾 ∩ 𝐴)) ≤ ((vol‘(𝐾 ∩ 𝐿)) + (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
124		fzfid 13942	. . . . 5 ⊢ (𝜑 → (1...𝑀) ∈ Fin)
125		iunss 5047	. . . . . . . 8 ⊢ (∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾 ↔ ∀𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾)
126	112, 125	sylib 217	. . . . . . 7 ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾)
127	126	r19.21bi 3246	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾)
128	12	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐾 ⊆ ℝ)
129	29	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘𝐾) ∈ ℝ)
130		ovolsscl 25235	. . . . . 6 ⊢ ((∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ 𝐾 ∧ 𝐾 ⊆ ℝ ∧ (vol‘𝐾) ∈ ℝ) → (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
131	127, 128, 129, 130	syl3anc 1369	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
132	124, 131	fsumrecl 15684	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
133	127, 128	sstrd 3991	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ)
134	133, 131	jca 510	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧ (vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ))
135	134	ralrimiva 3144	. . . . 5 ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧ (vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ))
136		ovolfiniun 25250	. . . . 5 ⊢ (((1...𝑀) ∈ Fin ∧ ∀𝑗 ∈ (1...𝑀)(∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ℝ ∧ (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)) → (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
137	124, 135, 136	syl2anc 582	. . . 4 ⊢ (𝜑 → (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
138		uniioombl.m	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℕ)
139	116, 138	nndivred 12270	. . . . . . 7 ⊢ (𝜑 → (𝐶 / 𝑀) ∈ ℝ)
140	139	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐶 / 𝑀) ∈ ℝ)
141	77	ineq2d 4211	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖))))
142	141	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖))))
143	99	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑁) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))))
144	143	iuneq2i 5017	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖)))
145		iunin2 5073	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐺‘𝑗)) ∩ ((,)‘(𝐹‘𝑖))) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))
146	144, 145	eqtri 2758	. . . . . . . . . . . 12 ⊢ ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)))
147	142, 146	eqtr4di 2788	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) = ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
148		fzfid 13942	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1...𝑁) ∈ Fin)
149		ffvelcdm 7082	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑖 ∈ ℕ) → (𝐹‘𝑖) ∈ ( ≤ ∩ (ℝ × ℝ)))
150	13, 73, 149	syl2an 594	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑖) ∈ ( ≤ ∩ (ℝ × ℝ)))
151	150	elin2d 4198	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑖) ∈ (ℝ × ℝ))
152		1st2nd2 8016	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑖) ∈ (ℝ × ℝ) → (𝐹‘𝑖) = ⟨(1^st ‘(𝐹‘𝑖)), (2^nd ‘(𝐹‘𝑖))⟩)
153	151, 152	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑖) = ⟨(1^st ‘(𝐹‘𝑖)), (2^nd ‘(𝐹‘𝑖))⟩)
154	153	fveq2d 6894	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) = ((,)‘⟨(1^st ‘(𝐹‘𝑖)), (2^nd ‘(𝐹‘𝑖))⟩))
155		df-ov 7414	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘(𝐹‘𝑖))(,)(2^nd ‘(𝐹‘𝑖))) = ((,)‘⟨(1^st ‘(𝐹‘𝑖)), (2^nd ‘(𝐹‘𝑖))⟩)
156	154, 155	eqtr4di 2788	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) = ((1^st ‘(𝐹‘𝑖))(,)(2^nd ‘(𝐹‘𝑖))))
157		ioombl 25314	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘(𝐹‘𝑖))(,)(2^nd ‘(𝐹‘𝑖))) ∈ dom vol
158	156, 157	eqeltrdi 2839	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) ∈ dom vol)
159	158	adantlr 711	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐹‘𝑖)) ∈ dom vol)
160		ffvelcdm 7082	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
161	6, 90, 160	syl2an 594	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ ( ≤ ∩ (ℝ × ℝ)))
162	161	elin2d 4198	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) ∈ (ℝ × ℝ))
163		1st2nd2 8016	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺‘𝑗) ∈ (ℝ × ℝ) → (𝐺‘𝑗) = ⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
164	162, 163	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐺‘𝑗) = ⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
165	164	fveq2d 6894	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((,)‘⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩))
166		df-ov 7414	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))) = ((,)‘⟨(1^st ‘(𝐺‘𝑗)), (2^nd ‘(𝐺‘𝑗))⟩)
167	165, 166	eqtr4di 2788	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) = ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))))
168		ioombl 25314	. . . . . . . . . . . . . . . 16 ⊢ ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))) ∈ dom vol
169	167, 168	eqeltrdi 2839	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ∈ dom vol)
170	169	adantr 479	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐺‘𝑗)) ∈ dom vol)
171		inmbl 25291	. . . . . . . . . . . . . 14 ⊢ ((((,)‘(𝐹‘𝑖)) ∈ dom vol ∧ ((,)‘(𝐺‘𝑗)) ∈ dom vol) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol)
172	159, 170, 171	syl2anc 582	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol)
173	172	ralrimiva 3144	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∀𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol)
174		finiunmbl 25293	. . . . . . . . . . . 12 ⊢ (((1...𝑁) ∈ Fin ∧ ∀𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol) → ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol)
175	148, 173, 174	syl2anc 582	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol)
176	147, 175	eqeltrd 2831	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) ∈ dom vol)
177		inss2 4228	. . . . . . . . . . 11 ⊢ (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ 𝐴
178	13	uniiccdif 25327	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran ([,] ∘ 𝐹) ∧ (vol*‘(∪ ran ([,] ∘ 𝐹) ∖ ∪ ran ((,) ∘ 𝐹))) = 0))
179	178	simpld 493	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ∪ ran ([,] ∘ 𝐹))
180		ovolficcss 25218	. . . . . . . . . . . . . . 15 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ)
181	13, 180	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ)
182	179, 181	sstrd 3991	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) ⊆ ℝ)
183	16, 182	eqsstrid 4029	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
184	183	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → 𝐴 ⊆ ℝ)
185	177, 184	sstrid 3992	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ℝ)
186		inss1 4227	. . . . . . . . . . 11 ⊢ (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ((,)‘(𝐺‘𝑗))
187		ioossre 13389	. . . . . . . . . . . 12 ⊢ ((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗))) ⊆ ℝ
188	167, 187	eqsstrdi 4035	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ)
189	167	fveq2d 6894	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘((,)‘(𝐺‘𝑗))) = (vol‘((1^st ‘(𝐺‘𝑗))(,)(2^nd ‘(𝐺‘𝑗)))))
190		ovolfcl 25215	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑗 ∈ ℕ) → ((1^st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1^st ‘(𝐺‘𝑗)) ≤ (2^nd ‘(𝐺‘𝑗))))
191	6, 90, 190	syl2an 594	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((1^st ‘(𝐺‘𝑗)) ∈ ℝ ∧ (2^nd ‘(𝐺‘𝑗)) ∈ ℝ ∧ (1^st ‘(𝐺‘𝑗)) ≤ (2^nd ‘(𝐺‘𝑗))))
192		ovolioo 25317	. . . . . . . . . . . . . 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 2770	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺‘𝑗))) = ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))))
195	191	simp2d 1141	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (2^nd ‘(𝐺‘𝑗)) ∈ ℝ)
196	191	simp1d 1140	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (1^st ‘(𝐺‘𝑗)) ∈ ℝ)
197	195, 196	resubcld 11646	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((2^nd ‘(𝐺‘𝑗)) − (1^st ‘(𝐺‘𝑗))) ∈ ℝ)
198	194, 197	eqeltrd 2831	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ)
199		ovolsscl 25235	. . . . . . . . . . 11 ⊢ (((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ((,)‘(𝐺‘𝑗)) ∧ ((,)‘(𝐺‘𝑗)) ⊆ ℝ ∧ (vol‘((,)‘(𝐺‘𝑗))) ∈ ℝ) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ∈ ℝ)
200	186, 188, 198, 199	mp3an2i 1464	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ∈ ℝ)
201		mblsplit 25281	. . . . . . . . . 10 ⊢ (((((,)‘(𝐺‘𝑗)) ∩ 𝐿) ∈ dom vol ∧ (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ⊆ ℝ ∧ (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ∈ ℝ) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) = ((vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) + (vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)))))
202	176, 185, 200, 201	syl3anc 1369	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) = ((vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) + (vol*‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)))))
203		imassrn 6069	. . . . . . . . . . . . . . 15 ⊢ (((,) ∘ 𝐹) “ (1...𝑁)) ⊆ ran ((,) ∘ 𝐹)
204	203	unissi 4916	. . . . . . . . . . . . . 14 ⊢ ∪ (((,) ∘ 𝐹) “ (1...𝑁)) ⊆ ∪ ran ((,) ∘ 𝐹)
205	204, 69, 16	3sstr4i 4024	. . . . . . . . . . . . 13 ⊢ 𝐿 ⊆ 𝐴
206		sslin 4233	. . . . . . . . . . . . 13 ⊢ (𝐿 ⊆ 𝐴 → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺‘𝑗)) ∩ 𝐴))
207	205, 206	mp1i 13	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺‘𝑗)) ∩ 𝐴))
208		sseqin2 4214	. . . . . . . . . . . 12 ⊢ ((((,)‘(𝐺‘𝑗)) ∩ 𝐿) ⊆ (((,)‘(𝐺‘𝑗)) ∩ 𝐴) ↔ ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = (((,)‘(𝐺‘𝑗)) ∩ 𝐿))
209	207, 208	sylib 217	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = (((,)‘(𝐺‘𝑗)) ∩ 𝐿))
210	209	fveq2d 6894	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) = (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)))
211		indifdir 4283	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = ((𝐴 ∩ ((,)‘(𝐺‘𝑗))) ∖ (𝐿 ∩ ((,)‘(𝐺‘𝑗))))
212		incom 4200	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ 𝐴)
213		incom 4200	. . . . . . . . . . . . . 14 ⊢ (𝐿 ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ 𝐿)
214	212, 213	difeq12i 4119	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∩ ((,)‘(𝐺‘𝑗))) ∖ (𝐿 ∩ ((,)‘(𝐺‘𝑗)))) = ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))
215	211, 214	eqtri 2758	. . . . . . . . . . . 12 ⊢ ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))
216	79	eqcomd 2736	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = 𝐴)
217	77	ineq1d 4210	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐿 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
218		2fveq3 6895	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝑖 → ((,)‘(𝐹‘𝑥)) = ((,)‘(𝐹‘𝑖)))
219	218	cbvdisjv 5123	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Disj 𝑥 ∈ ℕ ((,)‘(𝐹‘𝑥)) ↔ Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
220	14, 219	sylib 217	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
221		fz1ssnn 13536	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...𝑁) ⊆ ℕ
222	221	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ)
223		uzss 12849	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘1) → (ℤ_≥‘(𝑁 + 1)) ⊆ (ℤ_≥‘1))
224	39, 223	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℤ_≥‘(𝑁 + 1)) ⊆ (ℤ_≥‘1))
225	224, 36	sseqtrrdi 4032	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℤ_≥‘(𝑁 + 1)) ⊆ ℕ)
226	47	ineq1d 4210	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((1...((𝑁 + 1) − 1)) ∩ (ℤ_≥‘(𝑁 + 1))) = ((1...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))))
227		uzdisj 13578	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1...((𝑁 + 1) − 1)) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅
228	226, 227	eqtr3di 2785	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅)
229		disjiun 5134	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) ∧ ((1...𝑁) ⊆ ℕ ∧ (ℤ_≥‘(𝑁 + 1)) ⊆ ℕ ∧ ((1...𝑁) ∩ (ℤ_≥‘(𝑁 + 1))) = ∅)) → (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅)
230	220, 222, 225, 228, 229	syl13anc 1370	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (∪ 𝑖 ∈ (1...𝑁)((,)‘(𝐹‘𝑖)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅)
231	217, 230	eqtrd 2770	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐿 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅)
232		uneqdifeq 4491	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐿 ⊆ 𝐴 ∧ (𝐿 ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = ∅) → ((𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = 𝐴 ↔ (𝐴 ∖ 𝐿) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
233	205, 231, 232	sylancr 585	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 ∪ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))) = 𝐴 ↔ (𝐴 ∖ 𝐿) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
234	216, 233	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 ∖ 𝐿) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
235	234	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (𝐴 ∖ 𝐿) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
236	235	ineq2d 4211	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((,)‘(𝐺‘𝑗)) ∩ (𝐴 ∖ 𝐿)) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖))))
237		incom 4200	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ (𝐴 ∖ 𝐿))
238	101, 98	eqtri 2758	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) = (((,)‘(𝐺‘𝑗)) ∩ ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))((,)‘(𝐹‘𝑖)))
239	236, 237, 238	3eqtr4g 2795	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((𝐴 ∖ 𝐿) ∩ ((,)‘(𝐺‘𝑗))) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
240	215, 239	eqtr3id 2784	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = ∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
241	240	fveq2d 6894	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) = (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
242	210, 241	oveq12d 7429	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∩ (((,)‘(𝐺‘𝑗)) ∩ 𝐿))) + (vol‘((((,)‘(𝐺‘𝑗)) ∩ 𝐴) ∖ (((,)‘(𝐺‘𝑗)) ∩ 𝐿)))) = ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
243	202, 242	eqtrd 2770	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) = ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))))
244	200, 140	resubcld 11646	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ∈ ℝ)
245		inss2 4228	. . . . . . . . . . . . 13 ⊢ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐺‘𝑗))
246	188	adantr 479	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((,)‘(𝐺‘𝑗)) ⊆ ℝ)
247	198	adantr 479	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol*‘((,)‘(𝐺‘𝑗))) ∈ ℝ)
248		ovolsscl 25235	. . . . . . . . . . . . 13 ⊢ (((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐺‘𝑗)) ∧ ((,)‘(𝐺‘𝑗)) ⊆ ℝ ∧ (vol‘((,)‘(𝐺‘𝑗))) ∈ ℝ) → (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
249	245, 246, 247, 248	mp3an2i 1464	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
250	148, 249	fsumrecl 15684	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
251		uniioombl.n2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑗 ∈ (1...𝑀)(abs‘(Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))
252	251	r19.21bi 3246	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (abs‘(Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) − (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)))) < (𝐶 / 𝑀))
253	250, 200, 140	absdifltd 15384	. . . . . . . . . . . . 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 493	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) < Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
256	244, 250, 255	ltled 11366	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
257	147	fveq2d 6894	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
258		mblvol 25279	. . . . . . . . . . . . . . . . 17 ⊢ ((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol → (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
259	172, 258	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
260	259, 249	eqeltrd 2831	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ)
261	172, 260	jca 510	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑖 ∈ (1...𝑁)) → ((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ))
262	261	ralrimiva 3144	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ∀𝑖 ∈ (1...𝑁)((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ))
263		inss1 4227	. . . . . . . . . . . . . . . 16 ⊢ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐹‘𝑖))
264	263	rgenw 3063	. . . . . . . . . . . . . . 15 ⊢ ∀𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐹‘𝑖))
265	220	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)))
266		disjss2 5115	. . . . . . . . . . . . . . 15 ⊢ (∀𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ⊆ ((,)‘(𝐹‘𝑖)) → (Disj 𝑖 ∈ ℕ ((,)‘(𝐹‘𝑖)) → Disj 𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
267	264, 265, 266	mpsyl 68	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
268		disjss1 5118	. . . . . . . . . . . . . 14 ⊢ ((1...𝑁) ⊆ ℕ → (Disj 𝑖 ∈ ℕ (((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) → Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
269	221, 267, 268	mpsyl 68	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))
270		volfiniun 25296	. . . . . . . . . . . . 13 ⊢ (((1...𝑁) ∈ Fin ∧ ∀𝑖 ∈ (1...𝑁)((((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol ∧ (vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ∈ ℝ) ∧ Disj 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
271	148, 262, 269, 270	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
272		mblvol 25279	. . . . . . . . . . . . 13 ⊢ (∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))) ∈ dom vol → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
273	175, 272	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = (vol*‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
274	259	sumeq2dv 15653	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol*‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
275	271, 273, 274	3eqtr3d 2778	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘∪ 𝑖 ∈ (1...𝑁)(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
276	257, 275	eqtrd 2770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) = Σ𝑖 ∈ (1...𝑁)(vol‘(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))))
277	256, 276	breqtrrd 5175	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)))
278	276, 250	eqeltrd 2831	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) ∈ ℝ)
279	200, 140, 278	lesubaddd 11815	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) − (𝐶 / 𝑀)) ≤ (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) ↔ (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ≤ ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀))))
280	277, 279	mpbid 231	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐴)) ≤ ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀)))
281	243, 280	eqbrtrrd 5171	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol*‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀)))
282	131, 140, 278	leadd2d 11813	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → ((vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ (𝐶 / 𝑀) ↔ ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (vol‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol‘(((,)‘(𝐺‘𝑗)) ∩ 𝐿)) + (𝐶 / 𝑀))))
283	281, 282	mpbird 256	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀)) → (vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ (𝐶 / 𝑀))
284	124, 131, 140, 283	fsumle 15749	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀))
285	139	recnd 11246	. . . . . . 7 ⊢ (𝜑 → (𝐶 / 𝑀) ∈ ℂ)
286		fsumconst 15740	. . . . . . 7 ⊢ (((1...𝑀) ∈ Fin ∧ (𝐶 / 𝑀) ∈ ℂ) → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = ((♯‘(1...𝑀)) · (𝐶 / 𝑀)))
287	124, 285, 286	syl2anc 582	. . . . . 6 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = ((♯‘(1...𝑀)) · (𝐶 / 𝑀)))
288		nnnn0 12483	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ₀)
289		hashfz1 14310	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ₀ → (♯‘(1...𝑀)) = 𝑀)
290	138, 288, 289	3syl 18	. . . . . . 7 ⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀)
291	290	oveq1d 7426	. . . . . 6 ⊢ (𝜑 → ((♯‘(1...𝑀)) · (𝐶 / 𝑀)) = (𝑀 · (𝐶 / 𝑀)))
292	116	recnd 11246	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℂ)
293	138	nncnd 12232	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℂ)
294	138	nnne0d 12266	. . . . . . 7 ⊢ (𝜑 → 𝑀 ≠ 0)
295	292, 293, 294	divcan2d 11996	. . . . . 6 ⊢ (𝜑 → (𝑀 · (𝐶 / 𝑀)) = 𝐶)
296	287, 291, 295	3eqtrd 2774	. . . . 5 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(𝐶 / 𝑀) = 𝐶)
297	284, 296	breqtrd 5173	. . . 4 ⊢ (𝜑 → Σ𝑗 ∈ (1...𝑀)(vol*‘∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ 𝐶)
298	114, 132, 116, 137, 297	letrd 11375	. . 3 ⊢ (𝜑 → (vol*‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗)))) ≤ 𝐶)
299	114, 116, 34, 298	leadd2dd 11833	. 2 ⊢ (𝜑 → ((vol‘(𝐾 ∩ 𝐿)) + (vol‘∪ 𝑗 ∈ (1...𝑀)∪ 𝑖 ∈ (ℤ_≥‘(𝑁 + 1))(((,)‘(𝐹‘𝑖)) ∩ ((,)‘(𝐺‘𝑗))))) ≤ ((vol*‘(𝐾 ∩ 𝐿)) + 𝐶))
300	31, 115, 117, 123, 299	letrd 11375	1 ⊢ (𝜑 → (vol‘(𝐾 ∩ 𝐴)) ≤ ((vol‘(𝐾 ∩ 𝐿)) + 𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1085 = wceq 1539 ∈ wcel 2104 ∀wral 3059 ∖ cdif 3944 ∪ cun 3945 ∩ cin 3946 ⊆ wss 3947 ∅c0 4321 𝒫 cpw 4601 ⟨cop 4633 ∪ cuni 4907 ∪ ciun 4996 Disj wdisj 5112 class class class wbr 5147 × cxp 5673 dom cdm 5675 ran crn 5676 “ cima 5678 ∘ ccom 5679 Fun wfun 6536 Fn wfn 6537 ⟶wf 6538 ‘cfv 6542 (class class class)co 7411 1^st c1st 7975 2^nd c2nd 7976 Fincfn 8941 supcsup 9437 ℂcc 11110 ℝcr 11111 0cc0 11112 1c1 11113 + caddc 11115 · cmul 11117 ℝ^*cxr 11251 < clt 11252 ≤ cle 11253 − cmin 11448 / cdiv 11875 ℕcn 12216 ℕ₀cn0 12476 ℤ_≥cuz 12826 ℝ⁺crp 12978 (,)cioo 13328 [,]cicc 13331 ...cfz 13488 seqcseq 13970 ♯chash 14294 abscabs 15185 Σcsu 15636 vol*covol 25211 volcvol 25212

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-inf2 9638 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-disj 5113 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-isom 6551 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-of 7672 df-om 7858 df-1st 7977 df-2nd 7978 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-2o 8469 df-er 8705 df-map 8824 df-pm 8825 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fi 9408 df-sup 9439 df-inf 9440 df-oi 9507 df-dju 9898 df-card 9936 df-acn 9939 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-div 11876 df-nn 12217 df-2 12279 df-3 12280 df-n0 12477 df-z 12563 df-uz 12827 df-q 12937 df-rp 12979 df-xneg 13096 df-xadd 13097 df-xmul 13098 df-ioo 13332 df-ico 13334 df-icc 13335 df-fz 13489 df-fzo 13632 df-fl 13761 df-seq 13971 df-exp 14032 df-hash 14295 df-cj 15050 df-re 15051 df-im 15052 df-sqrt 15186 df-abs 15187 df-clim 15436 df-rlim 15437 df-sum 15637 df-rest 17372 df-topgen 17393 df-psmet 21136 df-xmet 21137 df-met 21138 df-bl 21139 df-mopn 21140 df-top 22616 df-topon 22633 df-bases 22669 df-cmp 23111 df-ovol 25213 df-vol 25214

This theorem is referenced by: uniioombllem5 25336

W3C validator